From e8a55a6edf91c5067b26cdfefbcc76517f86ab02 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 3 Nov 2026 09:13:09 +0000 Subject: [PATCH] feat(research): prove exact signed-frame rounding radii --- .../signed-permutation-frame-radius/PROOF.md | 118 +++++++++ .../signed-permutation-frame-radius/README.md | 139 +++++++++++ .../SOURCES.json | 30 +++ .../signed-permutation-frame-radius/TASK.json | 116 +++++++++ .../VERIFY.json | 34 +++ .../orbit_oracle.py | 66 +++++ .../rounding.py | 90 +++++++ .../signed-permutation-frame-radius/verify.py | 229 ++++++++++++++++++ 8 files changed, 822 insertions(+) create mode 100644 research/signed-permutation-frame-radius/PROOF.md create mode 100644 research/signed-permutation-frame-radius/README.md create mode 100644 research/signed-permutation-frame-radius/SOURCES.json create mode 100644 research/signed-permutation-frame-radius/TASK.json create mode 100644 research/signed-permutation-frame-radius/VERIFY.json create mode 100644 research/signed-permutation-frame-radius/orbit_oracle.py create mode 100644 research/signed-permutation-frame-radius/rounding.py create mode 100644 research/signed-permutation-frame-radius/verify.py diff --git a/research/signed-permutation-frame-radius/PROOF.md b/research/signed-permutation-frame-radius/PROOF.md new file mode 100644 index 0000000000..0f030e2390 --- /dev/null +++ b/research/signed-permutation-frame-radius/PROOF.md @@ -0,0 +1,118 @@ +# Exact radius for conjugated signed-permutation frames + +This contribution was produced by Nick Petalas. Apache-2.0. +Claim type: scoped written mathematical proof with exact finite corroboration. + +## Statement + +Let d>=1, let P belong to GL_d(Z), and let B_d be the group of all signed +permutation matrices. Set G=P B_d P^{-1} and + + L(P) = max_i sum_j |P_ij|. + +For an integer m>=2, consider **every** function +q:(1/m)Z^d -> Z^d satisfying q(gx)=gq(x) for every g in G and every input x. +No linearity, continuity, coordinatewise behavior, translation symmetry or +identity-on-integers condition is imposed in this minimization. Then + + min_q sup_x ||q(x)-x||_infinity = floor(m/2) L(P) / m. (1) + +The minimum is attained by one rule, independent of m, which also fixes every +integer input. On all of R^d, with integer outputs, the exact minimum is + + min_q sup_x ||q(x)-x||_infinity = L(P)/2. (2) + +For grid spacing delta>0, replacing the source and output grids by +(delta/m)Z^d and delta Z^d multiplies (1) by delta. Requiring the identity +on the output grid does not change either optimum. + +## One simultaneous attaining rule + +Let r:R->Z be nearest-integer rounding with half ties away from zero, and +apply it componentwise to vectors. It is odd, fixes integers and commutes +with every signed permutation: r(sy)=s r(y) for s in B_d. Define + + q_P(x) = P r(P^{-1}x). (3) + +Since P and P^{-1} are integer matrices, (3) has integer outputs, preserves +the complete refined grid as its input domain, and fixes Z^d. For +g=P s P^{-1}, direct substitution gives + + q_P(gx)=P r(s P^{-1}x)=P s r(P^{-1}x)=g q_P(x). + +This is one rule for the entire group, including inputs with nontrivial +stabilizers. In particular, if gx=x, the displayed identity forces +g q_P(x)=q_P(x); no independent orbit choices or incompatible ties occur. + +Put c_m=floor(m/2)/m. Every coordinate of y=P^{-1}x is in (1/m)Z, so +|r(y_j)-y_j|<=c_m. Thus + + ||q_P(x)-x||_infinity + = ||P(r(y)-y)||_infinity <= c_m L(P). + +The same argument on real inputs uses |r(y_j)-y_j|<=1/2. This proves both +upper bounds with the same explicit rule. + +## Stabilizers force the matching lower bound + +Choose a row i maximizing its absolute row sum. Choose a sign vector +v in {+1,-1}^d with v_j equal to the sign of P_ij when P_ij is nonzero; +either sign is allowed at a zero entry. Then + + ||Pv||_infinity = L(P). (4) + +Indeed the i-th coordinate equals its absolute row sum, and every other +coordinate is bounded by its own row sum. + +Write D_v=diag(v). The subgroup H=D_v S_d D_v of B_d fixes v, where S_d +denotes all ordinary permutation matrices. Its common fixed vectors are +exactly the line R v: D_v sends that fixed space to the vectors with all +coordinates equal. This includes d=1, where the line is the full space. + +Take x=c_m Pv. It is a valid input because P is integral. Every element +of P H P^{-1} fixes x. Any G-equivariant q must therefore have q(x) in +the fixed space P R v. Moreover P^{-1}q(x) is integral by unimodularity. +An integral vector on R v is n v for an integer n, since every coordinate +of v is +1 or -1. Consequently + + q(x)=n Pv, + ||q(x)-x||_infinity=|n-c_m| L(P) >= c_m L(P), + +because 0=1 and unimodular integer matrix P, let G=P B_d P^-1, where +B_d is the full signed-permutation group, and let L be the largest absolute +row sum of P. Among every G-equivariant function from the complete refined +integer grid to the integer grid, the exact least uniform infinity-norm +rounding error is + + R_m(P) = floor(m/2) L / m, m>=2. + +On all real inputs it is L/2. Output grid spacing delta multiplies these +radii by delta. One rule attains every optimum and fixes integer inputs: + + q_P(x) = P nearest_odd(P^-1 x), + +where scalar nearest rounding sends half ties away from zero. The proof +uses a point stabilizer to force every possible equivariant output onto a +primitive integer line. It covers arbitrary coupled nonlinear rounders. +See [PROOF.md](PROOF.md) for the full statement and argument. + +This answers the signed-permutation conjugacy class of Krzysztof Wojt's +[PR5122 larger-finite-group question](https://github.com/CrocSwap/integer-mult-bounds/pull/5122). +For the sheared dihedral example P=[[1,2],[0,1]], the exact radius is 3/2 +on the half-grid and on real inputs, and 1 on the third-grid. PR5122 already +gives these lower values for a reflection subgroup. The new result attains +them for all eight frames simultaneously and proves the general P,d formula. +Nick Petalas's [PR5079](https://github.com/CrocSwap/integer-mult-bounds/pull/5079) +provides the finite-group existence context and the dihedral example. +Neither predecessor executable is imported, replayed or audited. + +## Evidence + +The all-input and all-dimension conclusions rest on the written proof. +The standard-library verifier supplies exact finite corroboration: + +- All 104 two-by-two unimodular matrices with entries in [-2,2], at every + denominator m=2,...,9 and every transformed residue pair in {0,...,m-1}^2: + 29,536 points and 236,288 literal simultaneous equivariance comparisons. +- A separately implemented integer oracle constructs the eight physical + frames, tests point stabilizers, and optimizes every displayed orbit by + complete integer-box enumeration. Across these points and 832 explicit + attaining orbits it enumerates 99,264 candidate outputs. It imports no + radius formula, quantizer, inverse routine or predecessor executable. +- Eight further frames in dimensions 1,...,8, with 680 rational data points, + 5,440 sign/swap generator checks and 140 witness-stabilizer checks. +- Five semantic controls distinguish an understated radius, the odd-grid + correction, an incompatible stabilizer choice, rounding in physical + coordinates, and an actual nonodd-tie mutation. Fifteen malformed input + cases reject; a 257-bit integer input is fixed exactly. + +The receipt is computed at execution time and binds every package source +by SHA256. It is never handwritten. The verifier writes no files by default; +`--receipt /absolute/new/path.json` exclusively creates an external receipt. + +## Reproduce + +From the repository root, with CPython 3.12 and no additional dependencies: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/signed-permutation-frame-radius/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/signed-permutation-frame-radius/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/signed-permutation-frame-radius +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/signed-permutation-frame-radius --check-source-history +``` + +Another CPython 3.12 executable may replace the local path. Expected markers +are `PASS_SIGNED_PERMUTATION_FRAME_RADIUS`, `PASS_REGISTERED_RESEARCH_PACKAGE` +and `PASS_RESEARCH_COMMIT_BYTES`. Both registered checks run the complete +finite domain, separately with normal and optimized Python, with 180-second +limits. Local CPython is 3.12.15 on macOS arm64. Hosted execution is recorded +separately in the PR body; it is not independent mathematical acceptance. + +## Scope and implementation limits + +The `uniform-transfer-audit` card is explicitly changed to this precision +side theorem. A current supplier is not shown to reach a maximizing orbit. +There is no paid rounding/restoration circuit, native implementation, physical +tape invoice, stock bound, supplier admission, new kappa or selected-frontier +change. The five selected framework assumptions remain. No selected cold +replay, Lean or Docker run is claimed. Other finite integer representations, +restricted reachable domains, frame-dependent rules, changing grids and +magnitude-relative errors require separate arguments. + +The executable frame boundary allows dimensions 1,...,8, integer entries of +at most 16 bits, rational point numerators/denominators of at most 4,096 bits, +and grid denominators at most 65,536. Its trusted frame/inverse pair comes +from `rounding.matrix`. The proof has no such operational size limits. +The independent oracle is a private two-dimensional fixture checker with +denominator at most 11, scaled incumbent radius at most 128 and at most +129 choices per output coordinate. Every loop has a finite input or fixture +bound; all functions are under sixty lines. Python exact integers and +Fractions allocate dynamically; bounded dimensions, coefficient/data bit +lengths and streaming census hashes bound live data. This is the managed +runtime deviation from preallocated steady-state memory. The nonodd-tie +mutation replaces one known local callable inside try/finally; there is no +dynamic evaluation or unbounded dispatch. Explicit exceptions keep the +contracts active under optimization; warning-strict execution and AST +parsing check all new Python sources. These checks do not certify physical +arithmetic complexity. + +## Open next questions + +Structured versions are in [TASK.json](TASK.json). + +- Does an actual carried reader reach the explicit maximizing point or its + orbit? Pin its frame and full dirty-input image, then decide membership. + Actual reachability and the complete paid rounding/restoration bill are + missing; the full-grid radius alone does not price a supplier. +- What is the exact radius outside the signed-permutation conjugacy class? + Start with one explicit finite integral representation and its stabilizer + sublattices. This proof supplies no general finite-group radius algorithm. + +## Provenance and credit + +Canonical base: `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8, +selected conditional kappa `0.003125804`. [SOURCES.json](SOURCES.json) binds +predecessor context as historical provenance; there are no external runtime +inputs. The source question is PR5122, head +`dab8cc5917fbc76564367a973bd6cd1ed5a22ee3`, Open next question 2. PR5079's +exact head is `43f558c1b8fc14fb0ed33a4512fbc976beea6b0f`. + +Credit Krzysztof Wojt for the reflection optima and released question; +Nick Petalas for the earlier existence classification; Sricharan Vagvala +(PR1631), woklerx (PR1892), Sagar Thakrar (PR1537), Ross Richardson (PR1287) +and the retained output-frame/dirty-echo lineage for their context. Scalar +rounding, change of basis, signed permutations and invariant subspaces are +classical. The new contribution is the simultaneous exact radius theorem, +its attaining rule and the finite corroboration; no general literature +priority is claimed. Predecessor credit lines and source bytes are unchanged. + +The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19370162) +records the scope. Live handoffs, local reservations, 505 open PRs, 6,496 +Discussion records, main README searches and merged/all-state object searches +were checked. Sparse local notes, arbitrary historical diffs, unpublished +work and later changes remain coverage limits. diff --git a/research/signed-permutation-frame-radius/SOURCES.json b/research/signed-permutation-frame-radius/SOURCES.json new file mode 100644 index 0000000000..10fe3c5858 --- /dev/null +++ b/research/signed-permutation-frame-radius/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/equivariant-grid-frame-classification/README.md", + "usage": "provenance", + "git_blob": "518d895629bcac67886ec896b192bcc5f085d9ff", + "sha256": "238df9b8569168e8887274dbe8b7e91b5e048b0857293841f0cd0e8a3951b39a" + }, + { + "path": "research/reflection-rounding-radius/README.md", + "usage": "provenance", + "git_blob": "14123795584429567e395216d493041175b94408", + "sha256": "85e837884f9bf164e914c5c0d6d3ae4cfed2e6115a5ea3b3ed7d62e207ee2b62" + } + ] +} diff --git a/research/signed-permutation-frame-radius/TASK.json b/research/signed-permutation-frame-radius/TASK.json new file mode 100644 index 0000000000..dd024d71c6 --- /dev/null +++ b/research/signed-permutation-frame-radius/TASK.json @@ -0,0 +1,116 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact least infinity-norm radius and one simultaneous equivariant rounder for G=P B_d P^-1, every P in GL_d(Z), every d>=1, the complete refined integer grid and all real inputs.", + "scope_change_reason": "Answer the released larger-finite-frame-group question in Krzysztof Wojt PR5122, Open next question 2, as a mathematical precision side result. This does not discharge a selected caller assumption or audit a predecessor.", + "bottleneck_link": "Exact carried-frame rounding needs a compatible error budget for every frame and every point stabilizer. This theorem determines that budget for the signed-permutation conjugacy class; actual-reader reachability and paid realization remain missing.", + "budget_minutes": 60, + "stop_rule": "Stop at this first proved exact radius formula and explicit attaining rule. Leave actual readers and other finite groups open.", + "outcome": "completed", + "evidence": "PROOF.md; exact independent integer orbit optimization and rational equivariance checks in verify.py; generated source-hash-bound stdout receipt.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does one literal carried reader reach x=c_m P v or a whole maximizing orbit in this frame class?", + "why_it_matters": "Only reachable inputs turn a complete-grid minimax radius into a concrete supplier precision requirement.", + "first_step": "Pin one reader, its exact frame matrix P and its dirty-input image, then decide membership of the explicit maximizing point.", + "blocked_by": "No such actual reader or complete paid rounding/restoration implementation is supplied." + }, + { + "question": "What is the exact stabilizer-compatible rounding radius for a finite integer frame group outside the signed-permutation conjugacy class?", + "why_it_matters": "The fixed-line witness and the conjugated scalar rounder need not apply to other integral representations.", + "first_step": "Choose one explicit finite group and solve its point-stabilizer lattice covering problem before constructing a reader.", + "blocked_by": "This proof only handles G=P B_d P^-1 with integral unimodular P." + } + ], + "canonical_discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19370162", + "question_source": { + "pr": 5122, + "author": "krzysztofwojt", + "head": "dab8cc5917fbc76564367a973bd6cd1ed5a22ee3", + "question": "Open next question 2: larger finite integer frame groups and the sheared dihedral example." + }, + "predecessors": [ + { + "pr": 5079, + "author": "Nick Petalas", + "head": "43f558c1b8fc14fb0ed33a4512fbc976beea6b0f", + "scope": "Finite-group existence classification and the sheared dihedral example; not replayed." + }, + { + "pr": 5122, + "author": "Krzysztof Wojt", + "head": "dab8cc5917fbc76564367a973bd6cd1ed5a22ee3", + "scope": "Sharp reflection radii and released larger-group question; not replayed." + } + ], + "overlap": { + "open_pr_snapshot": "505 open PRs, complete pagination, 2026-11-03T09:03:23Z", + "discussion_snapshot": "6496 Discussion records, complete pagination, 2026-11-03T09:04:43Z", + "main_search": "All canonical-main research README paths searched for dihedral rounding, hyperoctahedral, signed-permutation rounding and conjugated rounders; merged and all-state PR object searches and relevant bodies inspected.", + "limits": "Sparse local notes, arbitrary historical diffs, unpublished work and later updates are not covered." + } +} diff --git a/research/signed-permutation-frame-radius/VERIFY.json b/research/signed-permutation-frame-radius/VERIFY.json new file mode 100644 index 0000000000..694ab0ad82 --- /dev/null +++ b/research/signed-permutation-frame-radius/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Exact independent orbit minima, simultaneous equivariance, stabilizer witnesses, odd-grid correction and rejecting controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "The identical mathematical checks with interpreter assertions disabled." + } + ] +} diff --git a/research/signed-permutation-frame-radius/orbit_oracle.py b/research/signed-permutation-frame-radius/orbit_oracle.py new file mode 100644 index 0000000000..afad7ae982 --- /dev/null +++ b/research/signed-permutation-frame-radius/orbit_oracle.py @@ -0,0 +1,66 @@ +"""Independent literal two-dimensional orbit optimization using integers only. + +No radius formula, quantizer, inverse routine or predecessor code is imported. +Produced by Nick Petalas. Apache-2.0. +""" + +from itertools import product + + +def frames(p): + """Build the eight conjugated signed permutations by closed 2x2 algebra.""" + a, b = p[0] + c, d = p[1] + determinant = a * d - b * c + if abs(determinant) != 1: + raise ValueError("oracle requires a unimodular 2x2 frame") + inverse = ((d // determinant, -b // determinant), + (-c // determinant, a // determinant)) + result = [] + for swap, first, second in product((False, True), (-1, 1), (-1, 1)): + s = ((0, first), (second, 0)) if swap else ((first, 0), (0, second)) + left = tuple(tuple(sum(p[i][k] * s[k][j] for k in range(2)) + for j in range(2)) for i in range(2)) + result.append(tuple(tuple(sum(left[i][k] * inverse[k][j] + for k in range(2)) for j in range(2)) + for i in range(2))) + if len(set(result)) != 8: + raise ValueError("oracle group has duplicate frames") + return tuple(result) + + +def image(g, point): + x, y = point + return (g[0][0] * x + g[0][1] * y, g[1][0] * x + g[1][1] * y) + + +def optimize(group, numerator, denominator, incumbent): + """Return minimum scaled whole-orbit radius and enumerated box size. + + Any better output lies in the entrance box given by the incumbent radius. + Stabilizer constraints are tested literally on every candidate output. + """ + if len(group) != 8 or not 2 <= denominator <= 11: + raise ValueError("oracle fixture limits exceeded") + stabilizer = tuple(g for g in group if image(g, numerator) == numerator) + if any(image(g, incumbent) != incumbent for g in stabilizer): + raise ValueError("incumbent violates point stabilizer") + residual = tuple(denominator * z - x for z, x in zip(incumbent, numerator)) + bound = max(abs(entry) for g in group for entry in image(g, residual)) + if bound > 128: + raise ValueError("oracle radius cap exceeded") + axes = tuple(range(-((bound - x) // denominator), + (x + bound) // denominator + 1) for x in numerator) + if any(len(axis) > 129 for axis in axes): + raise ValueError("oracle candidate capacity exceeded") + best = bound + candidates = 0 + for candidate in product(*axes): + candidates += 1 + if any(image(g, candidate) != candidate for g in stabilizer): + continue + error = tuple(denominator * z - x + for z, x in zip(candidate, numerator)) + cost = max(abs(entry) for g in group for entry in image(g, error)) + best = min(best, cost) + return best, candidates diff --git a/research/signed-permutation-frame-radius/rounding.py b/research/signed-permutation-frame-radius/rounding.py new file mode 100644 index 0000000000..8c0d85d3dc --- /dev/null +++ b/research/signed-permutation-frame-radius/rounding.py @@ -0,0 +1,90 @@ +"""Exact bounded implementation of the conjugated nearest-integer rounder. + +Produced by Nick Petalas. Apache-2.0. +The written theorem has no dimension or magnitude limits; this executable does. +""" + +from fractions import Fraction + + +MAX_DIMENSION = 8 +MAX_BITS = 4096 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def matrix(value): + """Validate an integer frame and return its exact integer inverse.""" + require(isinstance(value, tuple), "frame must be a tuple") + dimension = len(value) + require(1 <= dimension <= MAX_DIMENSION, "unsupported dimension") + require(all(isinstance(row, tuple) and len(row) == dimension + for row in value), "frame must be square") + require(all(type(entry) is int and entry.bit_length() <= 16 + for row in value for entry in row), "invalid frame entry") + rows = [[Fraction(entry) for entry in row] + + [Fraction(i == j) for j in range(dimension)] + for i, row in enumerate(value)] + for column in range(dimension): + pivot = next((i for i in range(column, dimension) + if rows[i][column]), None) + require(pivot is not None, "singular frame") + rows[column], rows[pivot] = rows[pivot], rows[column] + divisor = rows[column][column] + rows[column] = [entry / divisor for entry in rows[column]] + for i in range(dimension): + if i != column: + factor = rows[i][column] + rows[i] = [a - factor * b + for a, b in zip(rows[i], rows[column])] + inverse = tuple(tuple(row[dimension:]) for row in rows) + require(all(entry.denominator == 1 for row in inverse for entry in row), + "frame must be unimodular") + return tuple(tuple(int(entry) for entry in row) for row in inverse) + + +def apply(frame, point): + return tuple(sum(a * b for a, b in zip(row, point)) for row in frame) + + +def nearest(value): + """Nearest integer, with half ties away from zero; in particular odd.""" + magnitude = abs(value) + result = (2 * magnitude.numerator + magnitude.denominator) // ( + 2 * magnitude.denominator) + return result if value >= 0 else -result + + +def round_point(frame, inverse, point): + """Trusted frame/inverse from matrix(); validate external rational data.""" + require(isinstance(point, tuple) and len(point) == len(frame), + "point dimension mismatch") + require(all(type(entry) in (int, Fraction) for entry in point), + "point must be exact rational") + exact = tuple(Fraction(entry) for entry in point) + require(all(max(entry.numerator.bit_length(), entry.denominator.bit_length()) + <= MAX_BITS for entry in exact), "point magnitude limit") + coordinates = apply(inverse, exact) + result = apply(frame, tuple(nearest(entry) for entry in coordinates)) + require(all(type(entry) is int for entry in result), "noninteger result") + return result + + +def radius(frame, denominator): + require(type(denominator) is int and 1 <= denominator <= 2**16, + "invalid grid denominator") + return Fraction(denominator // 2, denominator) * max( + sum(abs(entry) for entry in row) for row in frame) + + +def extremizer(frame, denominator): + """One grid point whose stabilizer forces the claimed radius.""" + require(type(denominator) is int and 1 <= denominator <= 2**16, + "invalid grid denominator") + row = max(frame, key=lambda entries: sum(abs(entry) for entry in entries)) + signs = tuple(1 if entry >= 0 else -1 for entry in row) + coordinate = Fraction(denominator // 2, denominator) + return apply(frame, tuple(coordinate * sign for sign in signs)), signs diff --git a/research/signed-permutation-frame-radius/verify.py b/research/signed-permutation-frame-radius/verify.py new file mode 100644 index 0000000000..d906d46ceb --- /dev/null +++ b/research/signed-permutation-frame-radius/verify.py @@ -0,0 +1,229 @@ +#!/usr/bin/env python3 +"""Finite exact corroboration of the signed-permutation frame radius theorem. + +Produced by Nick Petalas. Apache-2.0. No predecessor executable is replayed. +""" + +import argparse +import ast +from fractions import Fraction as F +import hashlib +from itertools import permutations, product +import json +from pathlib import Path +import sys + +# -I removes the script directory; restore only this local package. +PACKAGE = Path(__file__).resolve().parent +SOURCE_FILES = ("PROOF.md", "README.md", "SOURCES.json", "TASK.json", + "VERIFY.json", "orbit_oracle.py", "rounding.py", "verify.py") +sys.path.insert(0, str(PACKAGE)) +import orbit_oracle +import rounding + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def multiply(a, b): + dimension = len(a) + return tuple(tuple(sum(a[i][k] * b[k][j] for k in range(dimension)) + for j in range(dimension)) for i in range(dimension)) + + +def signed_permutations(dimension): + require(1 <= dimension <= 3, "complete group fixture cap exceeded") + return tuple(tuple(tuple(signs[i] if j == perm[i] else 0 + for j in range(dimension)) for i in range(dimension)) + for perm in permutations(range(dimension)) + for signs in product((-1, 1), repeat=dimension)) + + +def error(output, point): + return max(abs(a - b) for a, b in zip(output, point)) + + +def two_dimensional(): + counts = dict(frames=0, grid_points=0, equivariance_checks=0, + integer_candidates=0, attaining_orbits=0) + digest = hashlib.sha256() + for entries in product(range(-2, 3), repeat=4): + a, b, c, d = entries + if abs(a * d - b * c) != 1: + continue + frame = ((a, b), (c, d)) + inverse = rounding.matrix(frame) + group = orbit_oracle.frames(frame) + expected_group = {multiply(multiply(frame, s), inverse) + for s in signed_permutations(2)} + require(set(group) == expected_group, "independent group mismatch") + counts["frames"] += 1 + for m in range(2, 10): + largest = 0 + for residues in product(range(m), repeat=2): + point = rounding.apply(frame, tuple(F(v, m) for v in residues)) + output = rounding.round_point(frame, inverse, point) + require(error(output, point) <= rounding.radius(frame, m), + "quantizer exceeds grid radius") + for g in group: + transported = rounding.apply(g, point) + require(rounding.round_point(frame, inverse, transported) == + rounding.apply(g, output), "equivariance failure") + counts["equivariance_checks"] += 1 + numerator = tuple(int(v * m) for v in point) + best, candidates = orbit_oracle.optimize(group, numerator, m, output) + require(best <= m * rounding.radius(frame, m), "orbit exceeds bound") + largest = max(largest, best) + counts["integer_candidates"] += candidates + counts["grid_points"] += 1 + digest.update((repr((entries, m, residues, best)) + "\n").encode()) + require(largest == m * rounding.radius(frame, m), "grid optimum mismatch") + point, _ = rounding.extremizer(frame, m) + output = rounding.round_point(frame, inverse, point) + best, candidates = orbit_oracle.optimize( + group, tuple(int(v * m) for v in point), m, output) + require(best == m * rounding.radius(frame, m), "extremizer not sharp") + counts["integer_candidates"] += candidates + counts["attaining_orbits"] += 1 + return dict(counts, orbit_optima_sha256=digest.hexdigest()) + + +def check_generators(frame, inverse, data, output): + dimension = len(frame) + count = 0 + integer_coordinates = rounding.apply(inverse, output) + for i in range(dimension): + sign = tuple(-v if k == i else v for k, v in enumerate(data)) + signed_output = tuple(-v if k == i else v + for k, v in enumerate(integer_coordinates)) + require(rounding.round_point(frame, inverse, rounding.apply(frame, sign)) == + rounding.apply(frame, signed_output), "sign generator failure") + count += 1 + for i in range(dimension - 1): + permutation = list(range(dimension)) + permutation[i], permutation[i + 1] = permutation[i + 1], permutation[i] + swapped = tuple(data[j] for j in permutation) + swapped_output = tuple(integer_coordinates[j] for j in permutation) + require(rounding.round_point(frame, inverse, rounding.apply(frame, swapped)) == + rounding.apply(frame, swapped_output), "swap generator failure") + count += 1 + return count + + +def higher_dimensions(): + checks = dict(frames=0, points=0, generator_checks=0, fixed_point_checks=0) + for dimension in range(1, 9): + frame = tuple(tuple(int(i == j) + (i + 1 if j == i + 1 else 0) + for j in range(dimension)) for i in range(dimension)) + inverse = rounding.matrix(frame) + checks["frames"] += 1 + for m in (2, 3, 7, 10, 101): + point, signs = rounding.extremizer(frame, m) + output = rounding.round_point(frame, inverse, point) + require(error(output, point) == rounding.radius(frame, m), + "higher-dimensional sharpness failure") + for i in range(dimension - 1): + permutation = list(range(dimension)) + permutation[i], permutation[i + 1] = permutation[i + 1], permutation[i] + s = tuple(tuple(signs[j] * signs[permutation[j]] + if k == permutation[j] else 0 + for k in range(dimension)) for j in range(dimension)) + g = multiply(multiply(frame, s), inverse) + require(rounding.apply(g, point) == point, "witness stabilizer failure") + require(rounding.apply(g, output) == output, "output stabilizer failure") + checks["fixed_point_checks"] += 1 + for j in range(17): + data = tuple(F(((i + 3) * (j + 5)) % 37 - 18, m) + for i in range(dimension)) + x = rounding.apply(frame, data) + z = rounding.round_point(frame, inverse, x) + require(error(z, x) <= rounding.radius(frame, m), "data radius failure") + checks["generator_checks"] += check_generators(frame, inverse, data, z) + checks["points"] += 1 + return checks + + +def semantic_controls(): + frame = ((1, 2), (0, 1)) + inverse = rounding.matrix(frame) + point = (F(3, 2), F(1, 2)) + output = rounding.round_point(frame, inverse, point) + require(error(output, point) == F(3, 2), "sheared D8 fixture changed") + require(error(output, point) > 1, "understated radius escaped") + require(rounding.radius(frame, 3) == 1, "odd-grid correction missing") + swap = multiply(multiply(frame, ((0, 1), (1, 0))), inverse) + bad = rounding.apply(frame, (0, 1)) + require(rounding.apply(swap, point) == point and + rounding.apply(swap, bad) != bad, "stabilizer omission escaped") + reflection = ((1, -4), (0, -1)) + require(reflection in orbit_oracle.frames(frame), "reflection missing") + witness = (F(0), F(1, 2)) + plain = tuple(rounding.nearest(v) for v in witness) + require(tuple(rounding.nearest(v) for v in rounding.apply(reflection, witness)) != + rounding.apply(reflection, plain), "physical-coordinate rounding control failed") + original = rounding.nearest + try: + rounding.nearest = lambda v: (2 * v.numerator + v.denominator) // (2 * v.denominator) + negative = rounding.round_point(frame, inverse, tuple(-v for v in point)) + require(negative != tuple(-v for v in output), "nonodd tie mutation escaped") + finally: + rounding.nearest = original + require(rounding.round_point(frame, inverse, (2**256, -(2**256))) == + (2**256, -(2**256)), "integer fixing failure") + return {"semantic_controls": 5, "sheared_dihedral_radius": "3/2", + "odd_grid_m3_radius": "1", "large_integer_bits": 257} + + +def invalid_controls(): + frame = ((1, 2), (0, 1)) + inverse = rounding.matrix(frame) + bad_frames = ((), ((1, 2),), ((1, 2), (2, 4)), + ((2, 0), (0, 1)), ((True, 0), (0, 1)), ((2**17,),)) + rejected = 0 + for candidate in bad_frames: + try: + rounding.matrix(candidate) + except ValueError: + rejected += 1 + for candidate in ((), (0.5, 0), (True, 0), (2**4097, 0)): + try: + rounding.round_point(frame, inverse, candidate) + except ValueError: + rejected += 1 + for m in (0, -1, True, F(3, 2), 2**17): + try: + rounding.radius(frame, m) + except ValueError: + rejected += 1 + require(rejected == 15, "input rejection coverage failure") + return rejected + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", type=Path, help="exclusively create an external receipt") + args = parser.parse_args() + sources = {} + for name in SOURCE_FILES: + payload = (PACKAGE / name).read_bytes() + sources[name] = hashlib.sha256(payload).hexdigest() + if name.endswith(".py"): + ast.parse(payload, filename=name) + receipt = {"status": "PASS_SIGNED_PERMUTATION_FRAME_RADIUS", + "claim_type": "scoped written proof with exact finite corroboration", + "two_dimensional": two_dimensional(), + "higher_dimensions": higher_dimensions(), + "controls": semantic_controls(), + "invalid_input_rejections": invalid_controls(), + "source_sha256": sources} + encoded = json.dumps(receipt, indent=2, sort_keys=True) + "\n" + if args.receipt: + with args.receipt.open("x", encoding="utf-8") as stream: + require(stream.write(encoded) == len(encoded), "short receipt write") + print(encoded, end="") + + +if __name__ == "__main__": + main()