From 65f279d1d0c59e46974df9fd1b85d56aafca7a46 Mon Sep 17 00:00:00 2001 From: armin Date: Sat, 31 Oct 2026 09:05:04 -0400 Subject: [PATCH] =?UTF-8?q?Prove=20the=20mode-fiber=20rounding=20radius=20?= =?UTF-8?q?R=20<=3D=203/2=20(no=20=CE=BA)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Theorem D: snapping a vertex of the centred fiber polytope to +-1/2 reduces exact mode-preserving rounding to a signed balancing problem that the block pair structure of the PR4933 mode matrix solves outright. With the #6312 lower bound this gives 1 <= R <= 3/2, superseding the R <= 2 of #6320. Standard-library exact verifier and constructive rounder included. Co-Authored-By: Claude Opus 5.5 --- .../mode-fiber-radius-three-halves/PROOF.md | 117 +++++++++++ .../mode-fiber-radius-three-halves/README.md | 78 ++++++++ .../SOURCES.json | 30 +++ .../mode-fiber-radius-three-halves/TASK.json | 83 ++++++++ .../VERIFY.json | 36 ++++ .../mode-fiber-radius-three-halves/rounder.py | 174 ++++++++++++++++ .../mode-fiber-radius-three-halves/verify.py | 188 ++++++++++++++++++ 7 files changed, 706 insertions(+) create mode 100644 research/mode-fiber-radius-three-halves/PROOF.md create mode 100644 research/mode-fiber-radius-three-halves/README.md create mode 100644 research/mode-fiber-radius-three-halves/SOURCES.json create mode 100644 research/mode-fiber-radius-three-halves/TASK.json create mode 100644 research/mode-fiber-radius-three-halves/VERIFY.json create mode 100644 research/mode-fiber-radius-three-halves/rounder.py create mode 100644 research/mode-fiber-radius-three-halves/verify.py diff --git a/research/mode-fiber-radius-three-halves/PROOF.md b/research/mode-fiber-radius-three-halves/PROOF.md new file mode 100644 index 0000000000..5b0a35868a --- /dev/null +++ b/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. diff --git a/research/mode-fiber-radius-three-halves/README.md b/research/mode-fiber-radius-three-halves/README.md new file mode 100644 index 0000000000..8149e72ed3 --- /dev/null +++ b/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. diff --git a/research/mode-fiber-radius-three-halves/SOURCES.json b/research/mode-fiber-radius-three-halves/SOURCES.json new file mode 100644 index 0000000000..5a344c4acf --- /dev/null +++ b/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" + } + ] +} diff --git a/research/mode-fiber-radius-three-halves/TASK.json b/research/mode-fiber-radius-three-halves/TASK.json new file mode 100644 index 0000000000..01a1056098 --- /dev/null +++ b/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." + } + ] +} diff --git a/research/mode-fiber-radius-three-halves/VERIFY.json b/research/mode-fiber-radius-three-halves/VERIFY.json new file mode 100644 index 0000000000..9375a8e5d7 --- /dev/null +++ b/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." + } + ] +} diff --git a/research/mode-fiber-radius-three-halves/rounder.py b/research/mode-fiber-radius-three-halves/rounder.py new file mode 100644 index 0000000000..1a707a77e4 --- /dev/null +++ b/research/mode-fiber-radius-three-halves/rounder.py @@ -0,0 +1,174 @@ +"""Constructive radius-3/2 rounder for the PR4933 mode map (PROOF.md, Theorem D). + +Exact rational arithmetic, standard library only. Given y in Q^112 whose mode +vector M^T y lies in L = M^T Z^112, returns an integer z with M^T z = M^T y and +max_i |z_i - y_i| <= 3/2. Every step of the proof is executed literally, so a +failure of any lemma raises instead of being silently repaired. +Prepared for apoursh with substantial Anthropic Claude assistance. Apache-2.0. +""" +from fractions import Fraction as Q +import itertools + +HALF = Q(1, 2) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def support(r): + return tuple(j for j in range(8) if r[j]) + + +def blocks_of(rows): + """support -> (row indices, pinned coordinate, pin sign, free coordinates).""" + out = {} + for i, r in enumerate(rows): + out.setdefault(support(r), []).append(i) + info = {} + for s, ix in out.items(): + fixed = [j for j in s if len({rows[i][j] for i in ix}) == 1] + need(len(ix) == 8 and len(fixed) == 1, 'block has eight rows and one pinned coordinate') + p, free = fixed[0], [j for j in s if j != fixed[0]] + need({tuple(rows[i][j] for j in free) for i in ix} == set(itertools.product((-1, 1), repeat=3)), + 'block rows are every sign pattern on the free coordinates') + info[s] = (ix, p, rows[ix[0]][p], free) + need(len(info) == 14, 'fourteen blocks') + return info + + +def direction(rows, block, a, b): + """j with m_a - m_b = +-2 e_j (rows differ at one free coordinate) or m_a + m_b = 2 sigma e_p (antipodal).""" + ix, p, sign, free = block + diff = [k for k in free if rows[a][k] != rows[b][k]] + return diff[0] if len(diff) == 1 else p if len(diff) == 3 else None + + +def straight(rows, block, j): + """The four disjoint pairs of the block in direction j.""" + ix = block[0] + pairs, used = [], set() + for a in ix: + if a not in used: + b = next(b for b in ix if b != a and b not in used and direction(rows, block, a, b) == j) + pairs.append((a, b, j)) + used.update((a, b)) + need(len(pairs) == 4, 'four pairs in one direction') + return pairs + + +def rainbow(rows, block): + """A perfect matching of the block into four pairs with four distinct directions.""" + ix, p, sign, free = block + parity = {i: sum(rows[i][k] < 0 for k in free) % 2 for i in ix} + even = [i for i in ix if parity[i] == 0] + odd = [i for i in ix if parity[i] == 1] + for perm in itertools.permutations(odd): + dirs = [direction(rows, block, a, b) for a, b in zip(even, perm)] + if None not in dirs and len(set(dirs)) == 4: + return [(a, b, d) for a, b, d in zip(even, perm, dirs)] + raise ValueError('no rainbow matching') + + +def kernel_vector(vectors): + """A nonzero rational dependency among vectors in Q^8, or None if they are independent.""" + n = len(vectors) + a = [[Q(vectors[k][j]) for k in range(n)] for j in range(8)] + pivots, r = [], 0 + for c in range(n): + piv = next((i for i in range(r, 8) if a[i][c]), None) + if piv is None: + continue + a[r], a[piv] = a[piv], a[r] + a[r] = [x / a[r][c] for x in a[r]] + for i in range(8): + if i != r and a[i][c]: + f = a[i][c] + a[i] = [x - f * y for x, y in zip(a[i], a[r])] + pivots.append(c) + r += 1 + if r == 8: + break + freec = next((c for c in range(n) if c not in pivots), None) + if freec is None: + return None + d = [Q(0)] * n + d[freec] = Q(1) + for row, c in enumerate(pivots): + d[c] = -a[row][freec] + return d + + +def vertex(rows, w): + """Move w inside {w' in [0,1]^112 : M^T w' = M^T w} until its fractional rows are independent.""" + w = list(w) + while True: + frac = [i for i in range(len(w)) if w[i].denominator != 1] + sample = frac[:9] + d = kernel_vector([rows[i] for i in sample]) + if d is None: + return w, frac + step = min([(1 - w[i]) / di for i, di in zip(sample, d) if di > 0] + + [-w[i] / di for i, di in zip(sample, d) if di < 0]) + for i, di in zip(sample, d): + w[i] += step * di + + +def word(coords): + return tuple(int(j in coords) for j in range(8)) + + +def plan(rows, blocks, h): + """Matchings for every block: rainbow by default (seven pairs, an odd count, per coordinate), and + straight on the toggled blocks, which makes the counts even exactly where the parity word h is 0.""" + even = tuple(1 - x for x in h) + supp = {word(s): s for s in blocks} + if even == (0,) * 8: + toggled = [] + elif even in supp: + toggled = [supp[even]] + else: + need(even == (1,) * 8, 'parity word lies in H8') + s = min(blocks) + toggled = [s, supp[tuple(1 - x for x in word(s))]] + pairs = [] + for s, block in blocks.items(): + pairs += straight(rows, block, s[0]) if s in toggled else rainbow(rows, block) + return pairs, toggled + + +def round_three_halves(rows, y, blocks=None): + blocks = blocks or blocks_of(rows) + n = len(rows) + t = [sum(rows[i][j] * y[i] for i in range(n)) for j in range(8)] + c = [(v + HALF).numerator // (v + HALF).denominator for v in y] # nearest integers + w = [y[i] - c[i] + HALF for i in range(n)] # in [0, 1] + need(all(0 <= x <= 1 for x in w), 'centred box') + wstar, F = vertex(rows, w) + need(len(F) <= 8 and kernel_vector([rows[i] for i in F]) is None, 'independent fractional rows') + snap = [Q(1) if wstar[i] >= HALF else Q(0) for i in range(n)] # every row now at +-1/2 + u = [sum((rows[i][j] * (wstar[i] - snap[i]) for i in F), Q(0)) for j in range(8)] + need(all(v.denominator == 1 and abs(v) <= 4 for v in u), 'balancing target u in Z^8 with |u_j| <= 4') + u = [int(v) for v in u] + pairs, toggled = plan(rows, blocks, tuple(v % 2 for v in u)) + need(sorted(x for a, b, _ in pairs for x in (a, b)) == list(range(n)), 'pairs partition the rows') + kappa = [0] * n + for j in range(8): + mine = [pr for pr in pairs if pr[2] == j] + need(len(mine) % 2 == u[j] % 2 and abs(u[j]) <= len(mine), 'pair count covers u_j') + plus = (len(mine) + u[j]) // 2 + for k, (a, b, _) in enumerate(mine): + eps = 1 if k < plus else -1 + block = blocks[support(rows[a])] + if j == block[1] and rows[a][j] == rows[b][j]: # antipodal: m_a + m_b = 2 sigma e_p + kappa[a] = kappa[b] = eps * block[2] + else: # m_a - m_b = 2 (m_a)_j e_j + kappa[a], kappa[b] = eps * rows[a][j], -eps * rows[a][j] + need([sum(kappa[i] * rows[i][j] for i in range(n)) for j in range(8)] == [2 * v for v in u], + 'signed row sum equals 2u') + z = [c[i] + int(snap[i]) + (kappa[i] - 1) // 2 for i in range(n)] + need([sum(rows[i][j] * z[i] for i in range(n)) for j in range(8)] == t, 'modes preserved') + err = max(abs(z[i] - y[i]) for i in range(n)) + need(err <= Q(3, 2), 'radius at most 3/2') + return z, err, toggled diff --git a/research/mode-fiber-radius-three-halves/verify.py b/research/mode-fiber-radius-three-halves/verify.py new file mode 100644 index 0000000000..ca6c6de640 --- /dev/null +++ b/research/mode-fiber-radius-three-halves/verify.py @@ -0,0 +1,188 @@ +#!/usr/bin/env python3 +"""Exact checks for the radius-3/2 mode-preserving rounder. Standard library only. + +Checks every finite fact Theorem D uses: the block structure of the PR4933 mode +matrix, that the supports with 0 and 1^8 form the [8,4,4] code H8, that the +column sums are divisible by 8, the rainbow and straight matchings with their +pair identities, and the 16-case balancing table. It then runs the rounder on +fixed exact inputs and checks rejection controls. +Prepared for apoursh with substantial Anthropic Claude assistance. Apache-2.0. +""" +from fractions import Fraction as Q +import hashlib +import json +from pathlib import Path +import random +import sys + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import rounder # noqa: E402 + +ROOT = HERE.parents[1] +SOURCE = 'research/coded-native-caller/NORMALIZERS.json' +SOURCE_SHA256 = 'ae8aad06aa5d1811d725895b3ab5a4f4daa9dcdd88294aa0d5f723e78bb1e0da' +WITNESS_SUPPORT = (0, 7, 20, 111) +need = rounder.need + + +def read(path, limit=1 << 20): + need(path.is_file() and not path.is_symlink() and path.stat().st_size <= limit, 'bounded regular file: %s' % path) + return path.read_bytes() + + +def load_rows(raw): + need(hashlib.sha256(raw).hexdigest() == SOURCE_SHA256, 'source hash') + cols = json.loads(raw)['mode_columns'] + need(type(cols) is list and len(cols) == 8 and all(len(c) == 112 for c in cols), 'mode shape') + rows = [tuple(c[i] for c in cols) for i in range(112)] + need(all(type(v) is int and v in (-1, 0, 1) for r in rows for v in r), 'signed entries') + return rows + + +def check_structure(rows): + need(len(set(rows)) == 112 and all(sum(map(abs, r)) == 4 for r in rows), 'distinct rows of weight four') + gram = [[sum(r[a] * r[b] for r in rows) for b in range(8)] for a in range(8)] + need(gram == [[56 * (a == b) for b in range(8)] for a in range(8)], 'M^T M = 56 I') + blocks = rounder.blocks_of(rows) + words = {rounder.word(s) for s in blocks} + code = {(0,) * 8} + for w in words: + code |= {tuple(a ^ b for a, b in zip(w, x)) for x in code} + need(code == words | {(0,) * 8, (1,) * 8} and len(code) == 16, 'supports, 0 and 1^8 form H8') + need(all(tuple(1 - x for x in w) in words for w in words), 'complement of a support is a support') + colsum = [sum(r[j] for r in rows) for j in range(8)] + need(all(v % 8 == 0 for v in colsum), 'column sums divisible by 8') + return blocks, colsum + + +def check_pairs(rows, pairs, block): + ix, p, sign, free = block + need(sorted(x for a, b, _ in pairs for x in (a, b)) == sorted(ix), 'pairs partition the block') + for a, b, j in pairs: + if j == p: + v = [x + y for x, y in zip(rows[a], rows[b])] + need(v == [2 * sign * (k == p) for k in range(8)], 'antipodal pair sums to 2 sigma e_p') + else: + v = [x - y for x, y in zip(rows[a], rows[b])] + need(v == [2 * rows[a][j] * (k == j) for k in range(8)], 'flip pair differs by 2 e_j') + + +def check_matchings(rows, blocks): + for s, block in blocks.items(): + rb = rounder.rainbow(rows, block) + check_pairs(rows, rb, block) + need(sorted(j for _, _, j in rb) == list(s), 'rainbow uses each coordinate once') + for j in s: + st = rounder.straight(rows, block, j) + check_pairs(rows, st, block) + need(all(d == j for _, _, d in st), 'straight matching in one direction') + + +def balancing_table(rows, blocks): + """For every parity word h in H8, the planned pair counts n_j have parity h_j and cover |u_j| <= 4.""" + table = [] + words = {rounder.word(s) for s in blocks} | {(0,) * 8, (1,) * 8} + for h in sorted(words): + pairs, toggled = rounder.plan(rows, blocks, h) + n = [sum(1 for pr in pairs if pr[2] == j) for j in range(8)] + need(all(n[j] % 2 == h[j] and n[j] >= (3 if h[j] else 4) for j in range(8)), 'balancing covers h') + table.append({'h': ''.join(map(str, h)), 'toggled': len(toggled), 'pairs_per_coordinate': n}) + need(len(table) == 16, 'sixteen parity classes') + return table + + +def fixtures(rows, count=150, seed=20261031): + """Exact y with M^T y in L: integer + rational vector projected onto ker M^T (M^T M = 56 I).""" + rng = random.Random(seed) + out = [[Q(1, 2) if i in WITNESS_SUPPORT else Q(0) for i in range(112)]] + for k in range(count - 1): + den = (2, 2, 4, 6, 7, 12, 30)[k % 7] + v = [Q(rng.randint(-6 * den, 6 * den), den) for _ in range(112)] + if k % 3: + keep = set(rng.sample(range(112), rng.randint(2, 24))) + v = [x if i in keep else Q(0) for i, x in enumerate(v)] + mt = [sum(rows[i][j] * v[i] for i in range(112)) for j in range(8)] + out.append([rng.randint(-4, 4) + v[i] - sum(rows[i][j] * mt[j] for j in range(8)) / 56 + for i in range(112)]) + return out + + +def check_rounder(rows, blocks, ys): + worst, toggles = Q(0), {} + for y in ys: + z, err, toggled = rounder.round_three_halves(rows, y, blocks) + need(all(type(v) is int for v in z), 'integer output') + worst = max(worst, err) + toggles[len(toggled)] = toggles.get(len(toggled), 0) + 1 + need(set(toggles) == {0, 1, 2}, 'fixtures exercise all three parity cases') + return worst, toggles + + +def rejects(fn): + try: + fn() + except (ValueError, StopIteration): + return True + return False + + +def controls(rows, blocks, ys): + out = [] + bad = list(rows) + first = next(j for j in range(8) if bad[5][j]) + bad[5] = tuple(-x if k == first else x for k, x in enumerate(bad[5])) + out.append(('flipped matrix entry', rejects(lambda: check_structure(bad)))) + s = min(blocks) + rb = rounder.rainbow(rows, blocks[s]) + (a, b, j), rest = rb[0], rb[1:] + out.append(('mislabelled pair direction', + rejects(lambda: check_pairs(rows, [(a, b, (j + 1) % 8)] + rest, blocks[s])))) + keep = rounder.plan + rounder.plan = lambda r, bl, h: keep(r, bl, (1,) * 8) # never toggle a block + try: + out.append(('parity toggle skipped', any(rejects(lambda y=y: rounder.round_three_halves(rows, y, blocks)) + for y in ys[:40]))) + finally: + rounder.plan = keep + keepv = rounder.vertex + rounder.vertex = lambda r, w: (list(w), [i for i in range(len(w)) if w[i].denominator != 1]) + try: + out.append(('vertex step skipped', any(rejects(lambda y=y: rounder.round_three_halves(rows, y, blocks)) + for y in ys[1:20]))) + finally: + rounder.vertex = keepv + off = [Q(1, 2) if i == 0 else Q(0) for i in range(112)] + out.append(('mode vector outside L', rejects(lambda: rounder.round_three_halves(rows, off, blocks)))) + claimed = Q(7, 5) + out.append(('claimed radius 7/5', any(rounder.round_three_halves(rows, y, blocks)[1] > claimed for y in ys))) + out.append(('source hash', rejects(lambda: load_rows(read(ROOT / SOURCE) + b' ')))) + failed = [name for name, ok in out if not ok] + need(not failed, 'controls failed open: %s' % failed) + return [name for name, _ in out] + + +def main(): + rows = load_rows(read(ROOT / SOURCE)) + blocks, colsum = check_structure(rows) + check_matchings(rows, blocks) + table = balancing_table(rows, blocks) + ys = fixtures(rows) + worst, toggles = check_rounder(rows, blocks, ys) + names = controls(rows, blocks, ys) + print(json.dumps({ + 'column_sums': colsum, + 'blocks': len(blocks), + 'balancing_cases': len(table), + 'min_pairs_even_coordinate': min(n for t in table for n, c in zip(t['pairs_per_coordinate'], t['h']) if c == '0'), + 'min_pairs_odd_coordinate': min(n for t in table for n, c in zip(t['pairs_per_coordinate'], t['h']) if c == '1'), + 'rounder_runs': len(ys), + 'parity_cases_seen': {str(k): v for k, v in sorted(toggles.items())}, + 'worst_error': '%d/%d' % (worst.numerator, worst.denominator), + 'controls_rejected': names, + }, indent=1)) + print('PASS_MODE_FIBER_RADIUS_THREE_HALVES') + + +if __name__ == '__main__': + main()