Mode-fiber rounding radius R ≤ 3/2 via a balancing lemma (no κ)

research/mode-fiber-radius-three-halves/PROOF.md

@@ -0,0 +1,117 @@
+# Mode-fiber rounding radius: R ≤ 3/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. As in #6312 (`research/mode-preserving-rounding`) and #6320
+(`research/mode-fiber-radius-bounds`), let
+
+    ρ(x) = min { ‖z − x‖∞ : z ∈ ℤ^112, Mᵀz = Mᵀx },
+    R    = sup { ρ(x) : the fiber is nonempty },
+
+and L = Mᵀℤ^112. #6312 proves R ≥ 1, and #6320 proves R ≤ 2 (its Theorem C).
+This note proves **R ≤ 3/2**, so 1 ≤ R ≤ 3/2, with a shorter argument than
+Theorem C. It needs neither #6320's genericity reduction nor its Hall lemma.
+
+## 1. Finite facts (exact, verify.py)
+
+* **Blocks.** The 112 rows split into 14 blocks of 8 by support. In block s, one
+  *pinned* coordinate p(s) has a fixed sign σ_s, and the three free coordinates
+  take all 8 sign patterns.
+* **Code.** The 14 supports, with 0 and 1⁸, are the 16 words of the extended
+  Hamming code H8 = [8,4,4], and the complement of a support is a support.
+  Since every row reduces mod 2 to its support, L mod 2 ⊆ H8. Each coordinate
+  lies in exactly 7 supports.
+* **Column sums.** Σ_i m_i = (32, 16, 56, 0, 0, −8, 0, 0) ∈ 8ℤ⁸. Hence
+  C := ½ Σ_i m_i ∈ 4ℤ⁸.
+* **Pairs.** Call rows a, b of one block a *j-pair* if they differ only at the
+  free coordinate j, so m_a − m_b = 2(m_a)_j e_j, or if j = p(s) and they are
+  antipodal on the free coordinates, so m_a + m_b = 2σ_s e_j. For every
+  ε ∈ {±1}, a j-pair has signs κ_a, κ_b ∈ {±1} with κ_a m_a + κ_b m_b = 2ε e_j.
+  The signs are κ_a = ε(m_a)_j = −κ_b in the first case and κ_a = κ_b = εσ_s in
+  the second. Every block has two kinds of perfect matching into pairs:
+  - a *straight* matching: 4 j-pairs, for each j ∈ s;
+  - a *rainbow* matching: one j-pair for each of the 4 coordinates j ∈ s.
+
+## 2. Balancing lemma
+
+**Lemma.** Let u ∈ ℤ⁸ with ‖u‖∞ ≤ 4 and u mod 2 ∈ H8. Then some κ ∈ {±1}^112
+satisfies Σ_i κ_i m_i = 2u.
+
+*Proof.* Let h = u mod 2 and g = 1⁸ − h, the set of coordinates where u is even;
+g ∈ H8. Choose matchings as follows:
+
+- if g = 0, every block is rainbow;
+- if g is a support s, block s is straight in direction min s and the rest are rainbow;
+- if g = 1⁸, take a complementary pair of supports s, s̄; both are straight and
+  the rest are rainbow.
+
+Every row lies in exactly one pair. Let n_j be the number of pairs in direction j.
+
+- With all blocks rainbow, n_j = 7, since j lies in 7 supports.
+- Making block s straight in direction a changes n_a to 10 and the other three
+  coordinates of s to 6.
+
+So n_j is odd and equals 7 where u_j is odd, which covers |u_j| ≤ 3. Where u_j is
+even, n_j ∈ {6, 10}, which covers |u_j| ≤ 4. For each j, give
+(n_j + u_j)/2 of its pairs ε = +1 and the rest ε = −1. Summing the pair
+identities gives Σ κ_i m_i = Σ_j 2u_j e_j. ∎
+
+verify.py checks all 16 cases of h. In every case the pair counts are at least
+6 on even coordinates and 7 on odd ones.
+
+## 3. Theorem D: R ≤ 3/2
+
+**Theorem D.** For every x ∈ ℝ^112 with Mᵀx ∈ L, some z ∈ ℤ^112 satisfies
+Mᵀz = Mᵀx and ‖z − x‖∞ ≤ 3/2. Hence R ≤ 3/2.
+
+*Proof.*
+
+1. *Centre.* Let c ∈ ℤ^112 be a nearest integer vector to x and v = x − c ∈ [−½,½]^112.
+   Then r := Mᵀv ∈ L.
+2. *Vertex.* The polytope Q = {v′ ∈ [−½,½]^112 : Mᵀv′ = r} contains v. Take a
+   vertex v*. The set F = {i : |v*_i| < ½} indexes linearly independent rows, so
+   |F| ≤ 8.
+3. *Snap.* Put s_i = +1 if v*_i ≥ 0 and −1 otherwise. Then s_i/2 = v*_i off F.
+   Set u = Mᵀ(v* − s/2) = Σ_{i∈F} (v*_i − s_i/2) m_i. Each coefficient has
+   absolute value at most ½, and column j meets at most 8 rows of F, so
+   ‖u‖∞ ≤ 4. Also
+
+       u = r − ½ Σ_i s_i m_i = r − C + Σ_{s_i = −1} m_i ∈ L,
+
+   because r, C ∈ 4ℤ⁸ ⊂ L (2e_j = m_a − m_b ∈ L) and the rows lie in L. So u ∈ ℤ⁸
+   and u mod 2 ∈ H8.
+4. *Balance.* The lemma gives κ ∈ {±1}^112 with Σ κ_i m_i = 2u.
+5. *Round.* Set e_i = (s_i + κ_i)/2 ∈ {−1, 0, 1} and z = c + e ∈ ℤ^112. Then
+
+       Mᵀz = Mᵀc + ½ Mᵀs + ½ Σ κ_i m_i = Mᵀc + Mᵀ(s/2) + u = Mᵀc + Mᵀv* = Mᵀc + r = Mᵀx,
+
+   and |z_i − x_i| = |e_i − v_i| ≤ 1 + ½. ∎
+
+The point of the vertex is that every row off F is already at ±½, where both
+neighbouring integers are equally close. The rows then enter only through
+signs κ_i, and the pair structure turns signed sums into an 8-coordinate
+balancing problem with a large margin: up to 7 or 10 pairs against a
+demand of at most 4.
+
+`rounder.py` executes steps 1–5 and the lemma in exact rational arithmetic. It
+raises if any claimed bound fails. verify.py runs it on 150 fixed exact
+inputs, including the #6312 witness. A separate stress run on 12,000 exact
+random and sparse inputs found no failure. Its worst error was
+1259/840 ≈ 1.4988, so 3/2 is the limit of this construction, not evidence
+about R. The loss is in step 5: a row with |v_i| near ½ can receive e_i = −2v_i.
+
+## 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. Theorem D is a written proof whose finite inputs are checked exactly;
+no proof-assistant or independent human review is claimed. Theorem D supersedes
+the upper bound of #6320's Theorem C. #6320's Theorem A (R = 1 is a finite
+zonotope-filling question) and its evidence for R = 1 are unchanged.

research/mode-fiber-radius-three-halves/README.md

@@ -0,0 +1,78 @@
+# Mode-fiber rounding radius: R ≤ 3/2
+
+This continues the merged #6320 (`research/mode-fiber-radius-bounds`), which
+answered part of Nick Petalas's #6312 question. For the PR4933 mode matrix M
+(112×8), R is the least ℓ∞ radius such that every x with a nonempty integer
+fiber {z : Mᵀz = Mᵀx} has a point of that fiber within R. #6312 proves
+R ≥ 1 and #6320 proves R ≤ 2. This package proves:
+
+- **Theorem D. R ≤ 3/2**, so **1 ≤ R ≤ 3/2**. The bound holds for every x, with
+  no genericity assumption.
+- **The idea.** Centre x at its nearest integer vector. Then move to a vertex of
+  the fiber polytope inside the box [−½,½]^112. All but at most 8 rows land
+  exactly at ±½, where both neighbouring integers are equally close. Snapping
+  the last ≤ 8 leaves an 8-coordinate demand u ∈ L with ‖u‖∞ ≤ 4, which must be
+  met by a sum of signed rows.
+- **The balancing lemma.** Every block of 8 rows is "one pinned coordinate, three
+  free", so it splits into four sign-free pairs worth ±2e_j each. With one pair
+  per coordinate in every block ("rainbow"), each coordinate gets 7 pairs.
+  Switching one or two blocks to four pairs in one direction fixes the parity
+  class of u. That leaves 6 to 10 pairs per coordinate against a demand of at
+  most 4.
+
+[PROOF.md](PROOF.md) has the argument and exact scope, and [rounder.py](rounder.py) runs it
+exactly. The pins are 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. #6320's package is left unchanged; Theorem D supersedes its
+Theorem C upper bound.
+
+## Reproduce
+
+From the repository root; the standard library suffices:
+
+```sh
+python3 -I -W error -B research/mode-fiber-radius-three-halves/verify.py
+python3 -I -O -W error -B research/mode-fiber-radius-three-halves/verify.py
+python3.12 -B scripts/research_package.py --package research/mode-fiber-radius-three-halves
+```
+
+Each prints `PASS_MODE_FIBER_RADIUS_THREE_HALVES` in about five seconds. Checked exactly:
+
+- the 14 pinned blocks and MᵀM = 56·I;
+- that the supports with 0 and 1⁸ form H8, and complements of supports are supports;
+- that the column sums are divisible by 8;
+- for every block, a rainbow matching and the four straight matchings, with every pair identity;
+- the balancing table for all 16 parity classes (minimum 6 pairs on even coordinates, 7 on odd);
+- 150 exact rounder runs, including the #6312 witness and all three parity cases (worst error 503/336).
+
+Seven rejection controls fail closed: a flipped matrix entry, a mislabelled pair
+direction, a skipped parity toggle, a skipped vertex step, a mode vector outside
+L, a claimed radius of 7/5 and a tampered source.
+
+A separate exact stress run of 12,000 random and sparse inputs (seeds 2–5)
+found no failure. Its worst error was 1259/840 ≈ 1.4988, so this construction
+cannot do better than 3/2.
+
+## Open next questions
+
+**Is R = 1?** By #6320's Theorem A this means asking whether every lattice point
+of L in the open zonotope is a 0/1 subset sum of rows. The #6320 sample supports
+yes.
+
+- **Why the bound stops at 3/2.** Theorem D loses ½ only on rows whose vertex
+  value lies on the far side of 0 from v_i.
+- **First step.** Add the sign constraints sgn v′_i = sgn v_i for |v_i| > ¼ to
+  the vertex polytope. Use the slack of the balancing lemma (n_j ≥ 6 against
+  |u_j| ≤ 4) to repair the rows that those constraints leave at 0.
+- **Blocker.** Rows at 0 snap into u with error ½, and nothing yet bounds how
+  many there are.
+
+## 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. #6320 (apoursh) supplies the reduction and the
+earlier bound. The Hamming code and vertex arguments are classical. Prepared by
+apoursh with substantial Anthropic Claude (Claude Code) assistance. New work is
+Apache-2.0.

research/mode-fiber-radius-three-halves/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "a7638a4ce2a29947457ae8d6bf8cd70a234dfeac",
+  "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"
+    },
+    {
+      "path": "research/mode-fiber-radius-bounds/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "ba8a3da373a2bc9cf7c499681e2f3bd0145b45a8",
+      "sha256": "9793a4418f5e24f3577c166640906260913ebf7da3011559abdf175be3e6e341"
+    }
+  ]
+}

research/mode-fiber-radius-three-halves/TASK.json

@@ -0,0 +1,83 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 8,
+  "base_commit": "a7638a4ce2a29947457ae8d6bf8cd70a234dfeac",
+  "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": "Open question 2 of research/mode-fiber-radius-bounds (#6320, merged): lower the upper bound R <= 2 on the least uniform l_inf radius R of exact mode-preserving integer rounding for the PR4933 mode map M, posed after #6312's open question 1.",
+  "scope_change_reason": "Continues the merged #6320 package, which changed this card to #6312's self-contained radius question. That package's second open question had a concrete first step; this package answers it with a different, shorter argument.",
+  "bottleneck_link": "Side result on the precision contract of the coded inverse. It bounds what an exact mode-preserving rounder can achieve on this M; it does not show that any caller needs one, and changes no kappa.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at a written proof of an upper bound below 2 whose finite inputs are checked exactly, or at an exact counterexample to the balancing lemma. Do not claim R = 1.",
+  "outcome": "partial",
+  "evidence": "PROOF.md Theorem D (R <= 3/2) with verify.py exact checks: the 14 pinned blocks, H8 closure and complements, column sums divisible by 8, rainbow and straight matchings with their pair identities, the 16-case balancing table, 150 exact rounder runs and seven rejection controls. A separate 12,000-input exact stress run found no failure (worst error 1259/840).",
+  "author": "apoursh",
+  "ai_assistance": "Anthropic Claude (Claude Code) found the argument, wrote the code and ran the checks under apoursh's direction.",
+  "open_questions": [
+    {
+      "question": "Is R = 1, that is, is every lattice point of L in the open zonotope int Z a 0/1 subset sum of rows (Theorem A of #6320)?",
+      "why_it_matters": "It settles #6312's question exactly; the #6320 search sample supports yes, and 1 <= R <= 3/2 is now known.",
+      "first_step": "Treat rows with |v_i| > 1/4 specially: add the sign constraints sgn v'_i = sgn v_i to the vertex polytope, and use the slack of the balancing lemma (n_j >= 6 against |u_j| <= 4) to fix the rows those constraints leave at 0.",
+      "blocked_by": "Rows that stop at 0 snap with error 1/2 into u, and there is no bound on how many stop there."
+    }
+  ]
+}

research/mode-fiber-radius-three-halves/VERIFY.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/coded-native-caller/NORMALIZERS.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Pinned block structure, H8 closure and complements, column sums divisible by 8, rainbow and straight matchings with pair identities, the 16-case balancing table, 150 exact radius-3/2 rounder runs and seven rejection controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "The same explicit checks under optimized Python."
+    }
+  ]
+}