Prove exact rounding radii for signed-permutation frame groups (no κ)

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<c_m<=1/2. This lower bound applies even to arbitrary coupled,
+nonlinear q, and proves (1). For real inputs take x=Pv/2 and repeat the
+argument with c=1/2 to prove (2). Both lower bounds are attained at an
+actual point, rather than only approached as a supremum. Scaling x and
+q by delta proves the grid-spacing statement.
+
+## The released sheared-dihedral example
+
+For P_k=[[1,k],[0,1]], G has eight elements and
+
+    R_m(P_k)=(|k|+1) floor(m/2)/m,
+    R_real(P_k)=(|k|+1)/2.
+
+In particular the P_2 example in PR5079 has radius 3/2 on the half-grid
+and on R^2, and radius 1 on the third-grid. Krzysztof Wojt's PR5122 already
+gives the same lower value for its reflection subgroup A_(2k); that
+subgroup value is not new here. The new conclusion supplies a compatible
+rounder for all eight frames simultaneously, and the exact formula for
+every unimodular P in every dimension. It answers a class of PR5122's
+larger-finite-group question, not the question for every finite integer group.
+
+## Evidence and boundary
+
+The all-input and all-dimension claims rest on this proof. The executable
+checks a bounded domain using two different arithmetic methods. Its integer
+orbit oracle constructs all eight physical frame matrices, finds every
+point stabilizer, and enumerates every integer output in a box containing
+any improvement on a supplied feasible output. It tests the full orbit
+error and literal stabilizer constraints. It imports no radius formula or
+rounder. Its returned minima corroborate the lower and upper bounds.
+
+No source claims that a current multiplication supplier reaches these
+maximizing inputs. The domain is the complete grid or all real vectors.
+The result supplies no paid rounding circuit, dirty-state restoration,
+native realization, physical movement, stock, precision/tape or complete
+signed supplier invoice. It does not change kappa or settle any of the
+five selected framework assumptions. No formal proof-kernel or independent
+human acceptance is claimed.

research/signed-permutation-frame-radius/README.md

@@ -0,0 +1,139 @@
+# Exact rounding radius for signed-permutation frame groups
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+Independent human and formal proof-kernel review are unclaimed.
+
+**Scoped written proof with exact finite corroboration; no new kappa.**
+For every d>=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.

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"
+    }
+  ]
+}