Mode-fiber rounding radius: 1 ≤ R ≤ 2; R = 1 reduces to zonotope filling (no κ)

research/mode-fiber-radius-bounds/CERTIFICATE.json

@@ -0,0 +1,15 @@
+{
+ "schema": "mode-fiber-radius-basis-v1",
+ "basis_rows": [
+  7,
+  35,
+  57,
+  73,
+  87,
+  90,
+  92,
+  99
+ ],
+ "tau": 6,
+ "scope": "Rows of M forming a basis of L = M^T Z^112; every other row has integer coordinates in this basis with l1 norm at most tau. Found by search/basis_search.py; verify.py recomputes everything exactly."
+}

research/mode-fiber-radius-bounds/PROOF.md

@@ -0,0 +1,183 @@
+# Mode-fiber rounding radius: a finite reduction and 1 ≤ R ≤ 2
+
+Prepared for apoursh with substantial Anthropic Claude assistance. Apache-2.0.
+
+## Setting
+
+M is the 112×8 mode matrix of Dillon Amburgey's
+[PR4933](https://github.com/CrocSwap/integer-mult-bounds/pull/4933), read from
+`research/coded-native-caller/NORMALIZERS.json` (`mode_columns`), with rows
+m_0, …, m_111. Nick Petalas's #6312 (`research/mode-preserving-rounding`, open
+at head `46593234bfe658b63fb829f0d22b7eb216e392a2`) studies rounding x ∈ ℝ^112 to
+z ∈ ℤ^112 with Mᵀz = Mᵀx, and asks in its first open question for the least
+uniform radius
+
+    R = sup { ρ(x) : the fiber F(x) = {z ∈ ℤ^112 : Mᵀz = Mᵀx} is nonempty },
+    ρ(x) = min { ‖z − x‖∞ : z ∈ F(x) }.
+
+The minimum exists because F(x) is discrete. #6312 proves R ≥ 1, using
+x = (e_0+e_7+e_20+e_111)/2. This note gives a finite characterisation of R = 1
+and explicit upper bounds: a basis certificate gives R ≤ 6, and the block structure of M gives R ≤ 2.
+
+Write L = Mᵀℤ^112 ⊂ ℤ^8, V = ker Mᵀ ⊂ ℝ^112, Z = Mᵀ[0,1]^112 (a zonotope) and
+S = {Mᵀz : z ∈ {0,1}^112} (subset sums of rows).
+
+## 1. Structure of M (exact, verify.py)
+
+* Every row has four nonzero entries, all ±1. The rows are distinct, and MᵀM = 56·I.
+* The 14 row supports are exactly the 14 weight-four words of the extended
+  Hamming code H8 = [8,4,4]. Each support carries 8 rows, so 8 of its 16 sign
+  patterns occur. The row set is **not** closed under negation.
+* L = {x ∈ ℤ^8 : x mod 2 ∈ H8}, the Hamming construction of √2·E8, with
+  [ℤ^8 : L] = 16. verify.py proves this by comparing Hermite normal forms
+  of the rows and of H8 ∪ 2ℤ^8.
+* For every i, the other 111 rows have rank 8.
+
+## 2. Theorem A (finite reduction)
+
+**R ≤ 1 if and only if L ∩ int Z ⊆ S.** If some t ∈ L ∩ int Z is not a 0/1
+subset sum of the rows, then every y ∈ (0,1)^112 with Mᵀy = t has ρ(y) > 1,
+so R > 1. With #6312's lower bound:
+
+    R = 1   ⇔   every lattice point of L in the open zonotope int Z is a subset sum of rows.
+
+*Proof.*
+
+(a) *Invariance and continuity.* F(x+n) = F(x)+n for n ∈ ℤ^112, so ρ is
+ℤ^112-periodic. For v ∈ V, F(x+v) = F(x), so |ρ(x+v) − ρ(x)| ≤ ‖v‖∞.
+
+(b) *Generic points suffice.* Fix x with F(x) ≠ ∅. The coordinate functional
+v ↦ v_i is not identically zero on V. Otherwise e_i ∈ V^⊥ = col span(M), say
+e_i = Ma. Then m_k·a = 0 for all k ≠ i, and since those rows have rank 8
+(§1), a = 0, a contradiction. So {v ∈ V : x_i + v_i ∈ ℤ} is a countable union
+of proper affine hyperplanes of V for each i. The union over i is a null set,
+so there are v ∈ V with arbitrarily small ‖v‖∞ such that x+v has no integral
+coordinate. By (a), R is the supremum of ρ over points with no integral coordinate.
+
+(c) *Reduction to the open cube.* For such x, put y = x − ⌊x⌋ ∈ (0,1)^112.
+Then ρ(y) = ρ(x), and t := Mᵀy ∈ L, because Mᵀx ∈ L (the fiber is nonempty)
+and Mᵀ⌊x⌋ ∈ L. For y_i ∈ (0,1), an integer z_i satisfies |z_i − y_i| ≤ 1 if
+and only if z_i ∈ {0,1}. Hence ρ(y) ≤ 1 ⇔ t ∈ S, and otherwise ρ(y) > 1.
+
+(d) *Which t occur.* Mᵀ is a surjective linear map ℝ^112 → ℝ^8. The image of the
+open cube is the interior of the image of the closed cube, so
+{Mᵀy : y ∈ (0,1)^112} = int Z.
+
+Combining (b)–(d): R ≤ 1 ⇔ L ∩ int Z ⊆ S. If t ∈ (L ∩ int Z) \ S, every y in
+the open cube over t has ρ(y) > 1. ∎
+
+Consequences. Deciding R = 1 is a **finite** problem, since Z is bounded. A
+counterexample has a finite exact certificate: a lattice point t, a rational
+y ∈ (0,1)^112 with Mᵀy = t, and infeasibility of the 0/1 system Mᵀz = t.
+Conversely, R = 1 needs every one of the finitely many interior lattice points
+to be a subset sum. Boundary lattice points of Z impose no condition.
+
+## 3. Theorem B (explicit upper bound): R ≤ 6
+
+Let B be the eight rows `[7, 35, 57, 73, 87, 90, 92, 99]` from CERTIFICATE.json.
+verify.py checks |det M_B| = 16 = covol(L). Since the rows lie in L, B is a basis
+of L. Each other row m_i (i ∈ N, |N| = 104) has integer coordinates w_i ∈ ℤ^8
+in this basis, and max_i ‖w_i‖₁ = τ = 6. Let W be the 8×104 matrix with columns w_i.
+
+Take y ∈ (0,1)^112 with Mᵀy = t ∈ L, as in Theorem A(b,c).
+
+*Step 1 (Beck–Fiala rounding of y_N against W).* Keep x ∈ [0,1]^N, starting
+from x = y_N, and let F be its fractional coordinates. Call row b of W
+*active* if Σ_{i∈F}|W_{bi}| > τ. Since Σ_b Σ_{i∈F}|W_{bi}| ≤ τ|F|, there are
+fewer than |F| active rows. So some nonzero d supported on F satisfies
+W_active d = 0. Move x along d until one more coordinate is integral, and
+repeat until F = ∅. Each active row value is preserved. Once a row becomes
+inactive, only coordinates of F change afterwards, each by less than 1. Its
+total later change is therefore less than Σ_{i∈F}|W_{bi}| ≤ τ, or zero. The
+result z_N ∈ {0,1}^N has ‖W(y_N − z_N)‖∞ < τ.
+
+*Step 2 (absorb into the basis).* Set z_B = y_B + W(y_N − z_N). Then
+
+    Σ_{b∈B} z_b m_b = Σ_B y_b m_b + Σ_N (y_i − z_i) m_i = t − Σ_N z_i m_i ∈ L,
+
+and B is a basis of L, so z_B ∈ ℤ^8. Hence z ∈ F(y), with |z_i − y_i| < 1 on N
+and |z_b − y_b| < τ on B.
+
+So ρ(y) < 6 for every generic y, and R ≤ 6 by Theorem A(a,b). ∎
+
+Local search over row bases (`search/basis_search.py`, three seeds × 200 restarts)
+found no basis with τ < 6. This method therefore stops at 6. Theorem C below
+uses the block structure instead.
+
+## 3′. Theorem C: R ≤ 2
+
+*Block structure (exact, verify.py).* For each of the 14 supports s, its 8 rows
+are exactly {σ_s e_{p(s)} + Σ_{k∈s∖p(s)} ε_k e_k : ε ∈ {±1}³}. So one *pinned*
+coordinate p(s) has a fixed sign σ_s, and the three free coordinates take every
+sign pattern. In particular, for every j ∈ s the block contains **four disjoint
+row pairs** (a,b) with ±2e_j ∈ {m_a − m_b, m_a + m_b}:
+
+- if j is free, pair rows that differ only at j, so m_a − m_b = 2(m_a)_j e_j;
+- if j = p(s), pair opposite free patterns, so m_a + m_b = 2σ_s e_j.
+
+Either sign of 2e_j is available with coefficients in {±1} on the pair.
+
+*Hall lemma (exact, verify.py).* For every set X of at most three supports and
+every nonempty J ⊆ {0,…,7}, at least |J| supports outside X meet J. The
+minimum slack over all cases is 3.
+
+*Proof of R ≤ 2.* Let y ∈ [0,1)^112 with t = Mᵀy ∈ L.
+
+1. *Vertex.* P_t = {y′ ∈ [0,1]^112 : Mᵀy′ = t} is a nonempty polytope. Take a
+   vertex y*. Its fractional coordinates F index linearly independent rows, so
+   |F| ≤ 8, and |y*_i − y_i| < 1 for all i. Each block's rows lie in a
+   four-dimensional coordinate subspace, so F contains at most 4 rows of any block.
+2. *Round F.* Let z_F be y*_F rounded to the nearest of {0,1}. Then
+   r′ = Σ_F (y*_i − z_i) m_i lies in L, because t, Σ_{i∉F} y*_i m_i and Σ_F z_i m_i
+   do, and |r′_j| ≤ ½·#{i ∈ F : m_ij ≠ 0} ≤ 4.
+3. *Parity.* h = r′ mod 2 ∈ H8 (§1). If h is a weight-four word, let U be one
+   row outside F with support h. If h = 1⁸, let U be two rows outside F with
+   complementary supports (the complement of a word is a word). If h = 0, let
+   U = ∅. Step 1 guarantees each block has at least 4 rows outside F. Put
+   u = Σ_U m_i, so |u_j| ≤ 1 and r′ − u = 2w with w ∈ ℤ^8 and |w_j| ≤ 2.
+4. *Distinct blocks.* Call rows in F ∪ U damaged, at most 10 of them. A block with
+   at most 2 damaged rows keeps at least 2 intact pairs for each of its
+   coordinates. At most three blocks have three or more damaged rows. By the
+   Hall lemma, the coordinates with w_j ≠ 0 have distinct undamaged-enough
+   blocks s_j ∋ j.
+5. *Assemble.* Set z_i = y*_i for i ∉ F ∪ U, then add 1 on U and, for each j,
+   ±1 on the rows of |w_j| intact pairs of s_j representing 2·sign(w_j)·e_j.
+   All touched rows are distinct. Then Mᵀz = Σ_{i∉F} y*_i m_i + Σ_F z_i m_i + u + 2w = t,
+   and z ∈ ℤ^112.
+6. *Error.* On F, |z_i − y_i| < 1. Elsewhere |z_i − y*_i| ≤ 1 and |y*_i − y_i| < 1,
+   so |z_i − y_i| < 2.
+
+Hence ρ(y) < 2 for every y in the open cube. By Theorem A(a,b), R ≤ 2. ∎
+
+`rounder.py` executes these six steps literally in exact rational arithmetic and
+raises if any step's claim fails. verify.py runs it on a fixed set of exact
+inputs. A separate stress run on 12,000 exact random and sparse inputs found
+no failure; its worst error was 839/420 ≈ 1.998, so 2 is the limit of this
+construction, not evidence about R.
+
+## 4. Evidence for R = 1 (not a proof)
+
+`search/evidence.py` (scipy/HiGHS) samples lattice points t ∈ L near the boundary
+of Z, where Theorem A's condition is hardest. It does this in two ways:
+
+- near a vertex (face rank 0): the vertex minus a small inward lattice vector;
+- near faces spanned by 1–7 random rows: rows off the face are pinned by the side
+  of the supporting functional, rows on the face get fractional weights with
+  denominator 2, 3, 4 or 6, and a small inward lattice vector is subtracted.
+
+It keeps t with a positive LP interior margin and solves the 0/1 system. All
+1,864 interior points found (by face rank 0–7: 401, 350, 402, 372, 175, 60, 72, 32)
+are subset sums. verify.py re-checks each witness exactly, t ∈ L and Σ_{i∈z} m_i = t.
+Interiority comes only from a floating-point LP and is **not** certified.
+This sample supports, but does not prove, the conjecture R = 1.
+
+## Scope
+
+R is a property of the stated exact-mode contract for this M, inherited from
+#6312. Nothing here shows that an actual caller must preserve these modes, or
+supplies a physical rounder, error ledger, tape/precision bill, supplier
+admission, new κ or frontier change. The five framework assumptions keep
+their status. Theorems A, B and C are written proofs whose finite inputs are
+checked exactly; no proof-assistant or independent human review is claimed.
+Beck–Fiala's iterative rounding (1981), Hall's marriage theorem and the Hamming
+construction of E8 are classical and credited as such.

research/mode-fiber-radius-bounds/README.md

@@ -0,0 +1,84 @@
+# Mode-fiber rounding radius: 1 ≤ R ≤ 2, and R = 1 is a finite question
+
+A scoped partial answer to the first open question of Nick Petalas's #6312
+(`research/mode-preserving-rounding`, open at head `46593234`). For the PR4933
+mode matrix M (112×8), let R be the least ℓ∞ radius such that every x with a
+nonempty integer fiber {z ∈ ℤ^112 : Mᵀz = Mᵀx} has a point of that fiber within R.
+#6312 proves R ≥ 1. This package proves:
+
+- **Structure.** L = Mᵀℤ^112 = {x ∈ ℤ^8 : x mod 2 ∈ H8}, the Hamming construction
+  of √2·E8, with index 16. The 14 row supports are the weight-four words of
+  [8,4,4], with 8 rows each. MᵀM = 56·I. The row set is not closed under negation.
+- **Theorem A (finite reduction).** R ≤ 1 if and only if every lattice point of L
+  in the *open* zonotope Mᵀ(0,1)^112 is a 0/1 subset sum of rows. One interior
+  lattice point that is not a subset sum forces R > 1. So **R = 1 is a finite
+  decision problem**, and either answer has a finite exact certificate.
+- **Theorem C.** **R ≤ 2.** Each support block is "one pinned coordinate, three
+  free," so every block holds four disjoint row pairs equal to ±2eⱼ for each of
+  its coordinates. Rounding at a vertex of the fiber polytope leaves a small
+  lattice residual. A Hall-theorem block assignment then pays that residual with
+  intact pairs, moving every coordinate by less than 2. `rounder.py` runs the
+  construction exactly. Theorem B, a simpler basis certificate with Beck–Fiala
+  rounding, gives R ≤ 6.
+- **Evidence, not proof.** All 1,864 sampled interior lattice points near vertices
+  and faces (face rank 0–7) are subset sums. This supports the conjecture R = 1.
+
+[PROOF.md](PROOF.md) has the arguments and exact scope. The constructive rounder is
+[rounder.py](rounder.py), the basis is in [CERTIFICATE.json](CERTIFICATE.json), the witnesses in [SEARCH.json](SEARCH.json),
+and the pins in [SOURCES.json](SOURCES.json). Complete κ and the selected frontier
+are unchanged. This is a property of the exact-mode contract. It does not claim
+that any caller needs the contract, and supplies no physical rounder or error/tape bill.
+
+## Reproduce
+
+From the repository root; the standard library suffices:
+
+```sh
+python3 -I -W error -B research/mode-fiber-radius-bounds/verify.py
+python3 -I -O -W error -B research/mode-fiber-radius-bounds/verify.py
+python3.12 -B scripts/research_package.py --package research/mode-fiber-radius-bounds
+```
+
+Each prints `PASS_MODE_FIBER_RADIUS_BOUNDS` in about five seconds. Checked exactly:
+
+- the structure facts, the HNF lattice identity and the rank condition Theorem A needs;
+- the #6312 witness relation;
+- the τ = 6 basis (|det| = 16, integral coordinates, maximum ℓ₁ norm exactly 6);
+- the 14 pinned blocks and their 2eⱼ pairs;
+- the Hall lemma, exhaustively over every set of at most three damaged blocks (minimum slack 3);
+- 120 exact runs of the Theorem C rounder (worst error 279/140);
+- every subset-sum witness.
+
+Nine rejection controls fail closed: a flipped matrix entry (in both the
+structure and block checks), a repeated basis row, a claimed τ = 5, a non-basis,
+a wrong witness mask, an off-lattice target, a broken witness relation and
+non-integral modes passed to the rounder. Interiority of the sampled targets came from a floating-point
+LP and is not certified.
+
+The non-certifying search scripts in `search/` need numpy and scipy:
+`evidence.py SEED TRIALS` regenerates one evidence run (seeds 11–14, 320 trials
+each), and `basis_search.py SEED RESTARTS` repeats the basis search.
+
+## Open next questions
+
+1. **Decide R = 1.** Is every lattice point of L in the open zonotope a subset
+   sum? This would settle #6312's question exactly. First step: reduce the
+   near-boundary cases with the signed-permutation symmetry of the rows, and try
+   a face recursion, where deep points are handled by discrepancy rounding and
+   points near a face reduce to the rows in that flat. Blocker: about 10¹²
+   lattice points rule out brute force, and the recursion is unproved.
+2. **Close the gap between 1 and 2.** Theorem C loses a full unit through the
+   triangle inequality |z − y| ≤ |z − y*| + |y* − y|. An exact stress run of
+   12,000 inputs reaches 1.998 with this construction, so improving the bound needs
+   a different first step. First step: replace the vertex y* by a point of the
+   fiber chosen near y, for example by Beck–Fiala rounding inside each block
+   against the 8 mode constraints. Then reuse the pair-and-Hall repair.
+   Blocker: the repair must stay within the remaining error budget.
+
+## Credit
+
+Dillon Amburgey (PR4933) supplies M. Nick Petalas (#6312) supplies the contract,
+the radius-one witness and the question. Its predecessor credits (JoyboyBrian,
+Dugongue, Ali Romman) carry over. Beck–Fiala rounding and the Hamming
+construction of E8 are classical. Prepared by apoursh with substantial Anthropic
+Claude (Claude Code) assistance. New work is Apache-2.0.

research/mode-fiber-radius-bounds/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc",
+  "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/coded-native-caller/NORMALIZERS.json",
+      "usage": "input",
+      "git_blob": "bca92c222c395d3d75c047fbb678f3cd0947c60f",
+      "sha256": "ae8aad06aa5d1811d725895b3ab5a4f4daa9dcdd88294aa0d5f723e78bb1e0da"
+    }
+  ]
+}