From 3cb32200b874692a49e02d874b39ad1b4ac1516c Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Wed, 11 Nov 2026 10:05:31 +0000 Subject: [PATCH] feat(research): prove eight-owner rounded inverse injectivity --- .../eight-owner-rounded-injectivity/PROOF.md | 168 ++++++++++++ .../eight-owner-rounded-injectivity/README.md | 92 +++++++ .../SOURCES.json | 36 +++ .../eight-owner-rounded-injectivity/TASK.json | 92 +++++++ .../VERIFY.json | 36 +++ .../eight-owner-rounded-injectivity/verify.py | 248 ++++++++++++++++++ 6 files changed, 672 insertions(+) create mode 100644 research/eight-owner-rounded-injectivity/PROOF.md create mode 100644 research/eight-owner-rounded-injectivity/README.md create mode 100644 research/eight-owner-rounded-injectivity/SOURCES.json create mode 100644 research/eight-owner-rounded-injectivity/TASK.json create mode 100644 research/eight-owner-rounded-injectivity/VERIFY.json create mode 100644 research/eight-owner-rounded-injectivity/verify.py diff --git a/research/eight-owner-rounded-injectivity/PROOF.md b/research/eight-owner-rounded-injectivity/PROOF.md new file mode 100644 index 0000000000..0814222898 --- /dev/null +++ b/research/eight-owner-rounded-injectivity/PROOF.md @@ -0,0 +1,168 @@ +# Eight owner residues determine the rounded inverse input + +This is a scoped proof for the fixed integer map from zxv's +[PR #5444](https://github.com/CrocSwap/integer-mult-bounds/pull/5444). +The source matrix, its Gram identity and the quotient-fiber method are +predecessor inputs. The new contribution is the selected row certificate, +the sparse injective lattice and its direct residue decoder. The proof and +certificate were produced by Nick Petalas. Apache-2.0. + +## Statement and boundary + +Use the exact 112 by 8 integer matrix M in the pinned +`research/precision-state-frontier/FIXTURE.json`, in its original owner and +mode order. Let R round each component to the nearest integer, with half +ties away from zero. The unchanged map is + +```text +K(z) = z - M R(M^T z / 52), z in Z^112, +M^T M = 56 I_8. +``` + +Owner indices are zero based. Put + +```text +S = (5, 33, 49, 53, 62, 65, 97, 108), +Lambda_g = {z in Z^112 : 2^g divides z_i for every i in S}. +``` + +**Theorem.** K is injective on every fixed residue coset of Lambda_5. +Equivalently, the 112 integer outputs K(z) and the eight residues +`(z_i mod 32)_(i in S)` determine every integer input z uniquely. There +is a direct exact decoder with eight scalar interval selections. Within +this fixed equal-bit observation family, five bits per selected owner +are necessary and sufficient for recovery of every integer input. + +In particular K is injective on Lambda_5, which strictly contains +`32 Z^112`. The coordinate-lattice index is `2^40`, compared with +`2^560` for the uniform sufficient lattice in #5444. These exponents +measure input-lattice restrictions. They are not physical storage or +runtime savings. The forty-bit residue channel is also larger than the +predecessor's thirty-bit optimal packed same-grid recovery tag. + +## The row certificate + +Let A consist of the selected rows of M, in S order: + +```text + 1 0 0 1 1 0 0 -1 + 0 0 1 1 0 0 -1 1 + 0 0 1 1 0 0 1 -1 + 0 1 0 1 0 1 0 1 +-1 0 1 0 0 -1 0 1 + 1 0 0 -1 1 0 0 1 + 1 0 0 -1 -1 0 0 1 + 0 0 1 -1 0 0 1 -1 +``` + +The following integer matrix H satisfies `AH=HA=2I`: + +```text + 1 0 0 0 0 0 1 0 + 3 -1 -3 2 2 -2 1 2 + 0 1 0 0 0 0 0 1 + 0 0 1 0 0 0 0 -1 + 0 0 0 0 0 1 -1 0 +-2 1 1 0 -2 1 -1 0 +-1 -1 2 0 0 1 0 -1 +-1 0 1 0 0 1 0 -1 +``` + +Thus `A^-1=H/2`. In addition `det A=-16` and every entry of +`M A^-1` is integral, so these eight actual rows form an integer basis +of the complete row lattice. The injectivity argument needs only `HA=2I`. +All these fixed matrix identities are checked exactly by the verifier; +separate rational elimination checks the inverse and determinant. + +## Injectivity + +Suppose `K(z)=K(z')=y` and `z_S=z'_S mod 32`. Define + +```text +q = R(M^T z/52), q' = R(M^T z'/52), s = M^T y. +``` + +Then `z=y+Mq`, and the rounding condition implies +`|s_j+4q_j| <= 26` for every mode j. The same holds for q'. Consequently +`|q_j-q'_j| <= 13`. This weak closed bound is enough; the exact half-tie +endpoint rules cannot enlarge it. + +The selected residue equality gives `A(q-q')=32t` for some integer vector +t. Multiplication by H gives `2(q-q')=32Ht`, hence every component of +`q-q'` is a multiple of sixteen. Its absolute value is at most thirteen, +so `q=q'` and therefore `z=z'`. This proves the theorem on every residue +coset, without enumerating the unbounded input domain. + +## Direct decoder + +Given y and a vector r of eight residues in `[0,32)`, compute + +```text +b = r - y_S, +v = H b, +a_j = (v_j/2) mod 16, +s = M^T y. +``` + +For a valid pair every v_j is even, because `Hb=2q mod 32`. If a v_j +is odd, reject. Each q_j must lie in the closed interval + +```text +ceil((-26-s_j)/4) <= q_j <= floor((26-s_j)/4) +``` + +and must satisfy `q_j=a_j mod 16`. The interval has real width thirteen, +so it contains at most one integer in that residue class. Select that +integer if present and check the exact equation +`R((s_j+56q_j)/52)=q_j`, including the half-tie convention. Then set +`z=y+Mq` and check both `z_S=r mod 32` and `K(z)=y`. + +A valid encoded pair passes every check and returns its original z. +The final checks reject an invalid pair whenever it has no preimage. +Each mode requires one interval selection, with no fiber enumeration. +The implementation is an exact integer reference, with a 4096-bit +operational input limit. The mathematical theorem has no magnitude limit. +No bit-operation, tape, reversible scratch or cleanup cost is asserted. + +## Sharp equal-bit threshold + +Let `u=(1,...,1)` in Z^8. Every actual row of M has even row sum, and +M has full column rank. The two distinct inputs + +```text +z_0 = 48 M u, z_1 = 56 M u +``` + +both belong to `16 Z^112`, and therefore to Lambda_g for every `0<=g<=4`. +Using the source Gram identity, + +```text +R(M^T z_0/52) = R((672/13) u) = 52u, +R(M^T z_1/52) = R((784/13) u) = 60u. +``` + +Both outputs equal `-4 M u`. Thus K fails to be injective already on +the zero-residue coset when only four or fewer bits are supplied. The +five-bit construction separates this pair. The coordinate vector e_0 +belongs to Lambda_5 but not to `32 Z^112`, which proves strict enlargement +of the uniform sufficient domain. + +The threshold is for these fixed eight owners with a common bit count. +No optimum over different subsets, unequal bit allocations, nonlinear +observations or global packed tags is claimed. + +## Scope and credit + +This is an input-lattice and observation theorem for the unchanged integer +map K. Writing an input as `D x` with a nonuniform diagonal D does not +establish that `K(Dx)` is the same physical inverse in an anisotropic output +format. D need not commute with the linear inverse. A physical caller must +derive its actual lattice or pay for observations and eventual restoration. +No supplier, signed-invoice gain, new kappa or selected-frontier change follows. + +Credit zxv #5444 for the lattice-fiber formulation, matrix fixture and unequal +precision question; Ali Romman #5323 for the sharp same-grid recovery theorem; +David Ganz #4929 and Dillon Amburgey #4933 for the native matrix/caller lineage; +and Brian / JoyboyBrian #5035 for the rounded kernel. Those results are cited, +not independently audited here. Their original files and notices are unchanged. +Independent human and formal proof-kernel review are unclaimed. diff --git a/research/eight-owner-rounded-injectivity/README.md b/research/eight-owner-rounded-injectivity/README.md new file mode 100644 index 0000000000..1c585102ef --- /dev/null +++ b/research/eight-owner-rounded-injectivity/README.md @@ -0,0 +1,92 @@ +# Recover the rounded inverse input from eight owner residues + +A scoped proof with exact finite corroboration: the fixed 112-owner integer +rounded inverse of zxv's [#5444](https://github.com/CrocSwap/integer-mult-bounds/pull/5444) +is injective when only owners **5, 33, 49, 53, 62, 65, 97 and 108** are +required to be divisible by 32. All other input coordinates remain arbitrary +integers. Indices are zero based. This strictly enlarges the predecessor's +uniform sufficient input lattice `32 Z^112`. + +The new row certificate has `2A^-1` integral. A shared output bounds quotient +differences by thirteen, while equality of the eight residues modulo 32 makes +every quotient difference a multiple of sixteen. This proves injectivity on +every fixed residue coset. A direct decoder recovers any input from its output +and forty residue bits using eight scalar interval selections. A literal pair +in `16 Z^112` has the same output, so the common five-bit threshold on these +eight owners is sharp. [PROOF.md](PROOF.md) gives the matrices and full argument. + +This answers one bounded part of #5444's unequal coordinate-lattice question. +The new certificate, sparse domain and decoder were produced by Nick Petalas. +The predecessor uniform frontier is cited, not audited. The selected frontier +is unchanged. + +## What the improvement measures + +The sufficient input-lattice index drops from `2^560` to `2^40`. This is a +larger injective domain, not a measured saving in fractional storage. The +forty-bit local residue channel uses more bits than the predecessor's optimal +thirty-bit packed same-grid tag, but needs observations on only eight owners +and has an explicit interval decoder. No global optimum for local observations +is claimed. + +The theorem concerns `K(z)=z-M round_away(M^T z/52)` in its fixed integer +coordinates. Nonuniform input scaling need not commute with its linear part. +No implementation of the original physical inverse on unequal output grids, +paid residue acquisition, reversible cleanup, native realization, complete +invoice, new kappa or multiplication theorem is supplied. + +## Reproduce + +From the repository root, using CPython 3.12 and only the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/eight-owner-rounded-injectivity +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/eight-owner-rounded-injectivity/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/eight-owner-rounded-injectivity/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/eight-owner-rounded-injectivity --check-source-history +``` + +The registered commands include normal and optimized execution. Each prints +`PASS_EIGHT_OWNER_INJECTIVITY` in a generated JSON receipt bound to the six +package files' hashes. No handwritten expected receipt is used. In a sparse +checkout first materialize this package and `research/precision-state-frontier`. +The three pinned predecessor documents are live inputs; no predecessor program +is executed. [SOURCES.json](SOURCES.json) records exact Git blobs and SHA256. + +The verifier checks both integer inverse products, a separate rational inverse +and determinant, integer row-lattice spanning, the literal rounded collision, +strict domain inclusion, exact forward/recovery fixtures and rejection controls. +There are 1,128 literal roundtrips, 5,525 scalar candidates across 417 projected +values and eleven rejection controls. Both registered checks finish locally +in under one second each. These are check durations, not speedup claims. +Its finite probes corroborate the written all-input proof. The interpreter's +4096-bit API limit bounds its operational arithmetic, not the theorem. + +The code uses fixed matrix dimensions and bounded test domains, with no +recursion or dynamic code execution. Python integer and collection allocation +is a managed-runtime deviation from fixed-allocation rules; vector lengths, +source sizes and input bit lengths bound the live data. Eleven fixed test +callbacks exercise failures. All proof-relevant checks use explicit errors +and remain enabled with `-O`. Every function has fewer than thirty lines. + +## Open next questions + +1. Can one actual inverse caller supply this sparse input lattice, or acquire + the eight residues at a favorable complete cost? Start by deriving its actual + grid and observations. Physical acquisition, restoration and the invoice are + missing, so no physical saving is inferred. +2. What is the least total local-residue budget over arbitrary owner subsets and + unequal bit allocations? Start with congruence kernels and the bounded quotient + difference box. A global allocation search and attainable-collision lower + bounds are not supplied here. + +Structured questions, scope change and stopping rule are in [TASK.json](TASK.json). + +## Credit and verification limits + +Credit zxv #5444 for the question, matrix and lattice-fiber formulation; +Ali Romman #5323 for same-grid recovery; David Ganz #4929 and Dillon Amburgey +#4933 for the native matrix/caller; and Brian / JoyboyBrian #5035 for the +rounded kernel. All predecessor notices and files remain unchanged. New work +is Apache-2.0. Independent human and formal proof-kernel review are unclaimed. +Hosted CI is separate from local verification. diff --git a/research/eight-owner-rounded-injectivity/SOURCES.json b/research/eight-owner-rounded-injectivity/SOURCES.json new file mode 100644 index 0000000000..bb238adcb4 --- /dev/null +++ b/research/eight-owner-rounded-injectivity/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/precision-state-frontier/FIXTURE.json", + "usage": "input", + "git_blob": "0aa9f7816378c3eb11ec2e3d63ed9e85cfaa893c", + "sha256": "2ca4d7550fcae5b757ec500f87aee1d2ef9f64b59e4abe2bda93319521304af8" + }, + { + "path": "research/precision-state-frontier/PROOF.md", + "usage": "input", + "git_blob": "79090050d47de95750b7321d89848143cc945abe", + "sha256": "f7e4d410cc108bc8b148ed8641c09be20c4c864fbc3908c533fa889b59dae341" + }, + { + "path": "research/precision-state-frontier/README.md", + "usage": "input", + "git_blob": "9c21dc65e529bc234ddafc8683f311185b644c01", + "sha256": "0a62a71cea7e8ec40cf1a175b84b2d42cd81a3d94c7ab106ea7d6c765d75d8d2" + } + ] +} diff --git a/research/eight-owner-rounded-injectivity/TASK.json b/research/eight-owner-rounded-injectivity/TASK.json new file mode 100644 index 0000000000..353ec85555 --- /dev/null +++ b/research/eight-owner-rounded-injectivity/TASK.json @@ -0,0 +1,92 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "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": "Injectivity and constructive recovery of the unchanged 112-owner integer rounded inverse from five residue bits on eight fixed owners; sharp five-versus-four-bit threshold for this fixed observation family.", + "scope_change_reason": "The selected-assumption card is changed to the unequal coordinate-lattice question of zxv PR5444. This is a local input-lattice result, not discharge of a selected assumption or implementation of anisotropic output precision.", + "bottleneck_link": "A sparse, explicit sufficient input-lattice contract can avoid imposing uniform divisibility on every owner. A caller must still supply that lattice or pay for the eight residue observations and their eventual restoration.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved sparse injectivity certificate and its decoder. Leave grid realization and global residue-budget optimization open.", + "outcome": "completed", + "evidence": "PROOF.md proves injectivity for every integer input in each fixed residue coset, gives an exact decoder and a four-bit collision. verify.py checks the exact eight-row certificate, literal roundtrips and rejection controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can an actual caller supply the eight-owner divisibility condition or cheaper residue observations?", + "why_it_matters": "Mathematical injectivity alone does not reduce physical storage, native calls or kappa.", + "first_step": "Identify one inverse invocation and derive its actual coordinate lattice and retained observations before assigning any saving.", + "blocked_by": "No physical grid conversion, residue acquisition, restoration or complete invoice is supplied." + }, + { + "question": "What is the least total residue budget over arbitrary owner subsets and unequal bit allocations?", + "why_it_matters": "The forty-bit construction is a sufficient certificate, not a global optimum; the predecessor packed tag uses thirty bits with a different access/computation contract.", + "first_step": "Use the fixed matrix to test candidate congruence kernels against the bounded quotient-difference box, with explicit endpoint attainability.", + "blocked_by": "No global allocation search or lower bound for this larger class is supplied." + } + ], + "claim_type": "scoped proof with exact finite corroboration", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19539344", + "question_source": "PR #5444" +} diff --git a/research/eight-owner-rounded-injectivity/VERIFY.json b/research/eight-owner-rounded-injectivity/VERIFY.json new file mode 100644 index 0000000000..ea8ed2ea01 --- /dev/null +++ b/research/eight-owner-rounded-injectivity/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/precision-state-frontier/FIXTURE.json", + "research/precision-state-frontier/PROOF.md", + "research/precision-state-frontier/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact eight-row certificate, constructive rounded recovery, sharp four-bit collision and semantic rejection controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same checks with assertions disabled; every proof-relevant check remains active." + } + ] +} diff --git a/research/eight-owner-rounded-injectivity/verify.py b/research/eight-owner-rounded-injectivity/verify.py new file mode 100644 index 0000000000..6aa6918eab --- /dev/null +++ b/research/eight-owner-rounded-injectivity/verify.py @@ -0,0 +1,248 @@ +#!/usr/bin/env python3 +"""Exact finite checks for the eight-owner lattice theorem. Apache-2.0.""" + +from fractions import Fraction +import hashlib +import json +from pathlib import Path +import random + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +OWNERS = (5, 33, 49, 53, 62, 65, 97, 108) +TWICE_INVERSE = ( + (1, 0, 0, 0, 0, 0, 1, 0), + (3, -1, -3, 2, 2, -2, 1, 2), + (0, 1, 0, 0, 0, 0, 0, 1), + (0, 0, 1, 0, 0, 0, 0, -1), + (0, 0, 0, 0, 0, 1, -1, 0), + (-2, 1, 1, 0, -2, 1, -1, 0), + (-1, -1, 2, 0, 0, 1, 0, -1), + (-1, 0, 1, 0, 0, 1, 0, -1), +) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def vector(values, length, label): + require(isinstance(values, (list, tuple)) and len(values) == length, + label + " has the wrong length") + require(all(type(x) is int and x.bit_length() <= 4096 for x in values), + label + " requires integers of at most 4096 bits") + return tuple(values) + + +def matvec(matrix, values): + return tuple(sum(a * b for a, b in zip(row, values, strict=True)) + for row in matrix) + + +def multiply(left, right): + return tuple(matvec(tuple(zip(*right, strict=True)), row) for row in left) + + +def nearest_away(numerator, denominator=52): + value = (2 * abs(numerator) + denominator) // (2 * denominator) + return value if numerator >= 0 else -value + + +def forward(matrix, z): + z = vector(z, 112, "input") + quotients = tuple(nearest_away(x) for x in matvec(tuple(zip(*matrix)), z)) + return tuple(x - t for x, t in zip(z, matvec(matrix, quotients), strict=True)) + + +def recover(matrix, y, residues): + y = vector(y, 112, "output") + residues = vector(residues, 8, "residues") + require(all(0 <= r < 32 for r in residues), "residue outside [0,32)") + rhs = tuple(r - y[i] for i, r in zip(OWNERS, residues, strict=True)) + doubled = matvec(TWICE_INVERSE, rhs) + require(all(x % 2 == 0 for x in doubled), "odd doubled quotient residue") + mode_residues = tuple((x // 2) % 16 for x in doubled) + projected = matvec(tuple(zip(*matrix)), y) + q = [] + for s, r in zip(projected, mode_residues, strict=True): + lower = -((26 + s) // 4) + upper = (26 - s) // 4 + candidate = lower + (r - lower) % 16 + require(candidate <= upper, "no quotient in residual interval") + require(nearest_away(s + 56 * candidate) == candidate, + "quotient violates the half-tie rule") + q.append(candidate) + z = tuple(a + b for a, b in zip(y, matvec(matrix, q), strict=True)) + require(all(z[i] % 32 == r for i, r in zip(OWNERS, residues, strict=True)), + "reconstructed owner residue differs") + require(forward(matrix, z) == y, "reconstructed forward value differs") + return z + + +def rational_inverse(matrix): + work = [[Fraction(x) for x in row] + [Fraction(i == j) for j in range(8)] + for i, row in enumerate(matrix)] + determinant = Fraction(1) + for j in range(8): + pivot = next((i for i in range(j, 8) if work[i][j]), None) + require(pivot is not None, "singular selected rows") + if pivot != j: + work[j], work[pivot] = work[pivot], work[j] + determinant = -determinant + scale = work[j][j] + determinant *= scale + work[j] = [x / scale for x in work[j]] + for i in range(8): + if i != j: + scale = work[i][j] + work[i] = [x - scale * y for x, y in zip(work[i], work[j], strict=True)] + return determinant, tuple(tuple(row[8:]) for row in work) + + +def certificate(matrix, owners=OWNERS, twice_inverse=TWICE_INVERSE): + selected = tuple(matrix[i] for i in owners) + twice_identity = tuple(tuple(2 * (i == j) for j in range(8)) for i in range(8)) + require(multiply(selected, twice_inverse) == twice_identity, "A H differs from 2I") + require(multiply(twice_inverse, selected) == twice_identity, "H A differs from 2I") + return selected + + +def load_matrix(): + sources = json.loads((HERE / "SOURCES.json").read_text()) + live = [row for row in sources["files"] if row["usage"] == "input"] + require(len(live) == 3, "unexpected source inventory") + for row in live: + path = ROOT / row["path"] + require(path.stat().st_size <= 2_000_000, "source exceeds resource bound") + require(hashlib.sha256(path.read_bytes()).hexdigest() == row["sha256"], + "pinned input differs: " + row["path"]) + fixture = ROOT / "research/precision-state-frontier/FIXTURE.json" + columns = json.loads(fixture.read_text())["mode_columns"] + require(len(columns) == 8 and all(len(row) == 112 for row in columns), + "wrong source dimensions") + matrix = tuple(vector(row, 8, "matrix row") for row in zip(*columns, strict=True)) + require(all(sum(x * x for x in row) == 4 for row in matrix), "wrong row norm") + gram = multiply(tuple(zip(*matrix)), matrix) + require(gram == tuple(tuple(56 * (i == j) for j in range(8)) for i in range(8)), + "wrong source Gram matrix") + return matrix + + +def check_scalar_intervals(): + checked = 0 + for s in range(-208, 209): + lower, upper = -((26 + s) // 4), (26 - s) // 4 + candidates = [q for q in range(lower, upper + 1) + if nearest_away(s + 56 * q) == q] + require(len(candidates) <= 13, "scalar fiber exceeds thirteen") + require(len({q % 16 for q in candidates}) == len(candidates), + "sixteen-residue decoding is ambiguous") + checked += upper - lower + 1 + return checked + + +def check_roundtrips(matrix): + count = 0 + for i in range(112): + for value in (-32, -16, -1, 1, 16, 32): + z = tuple(value if j == i else 0 for j in range(112)) + y = forward(matrix, z) + require(recover(matrix, y, tuple(z[k] % 32 for k in OWNERS)) == z, + "basis roundtrip failed") + count += 1 + for i in OWNERS: + for value in range(32): + z = tuple(value if j == i else 0 for j in range(112)) + require(recover(matrix, forward(matrix, z), tuple(z[k] % 32 for k in OWNERS)) == z, + "residue roundtrip failed") + count += 1 + rng = random.Random(5444) + for bits in range(0, 257, 16): + for _ in range(8): + z = tuple(rng.randrange(-(1 << bits), 1 << bits) for _ in range(112)) + require(recover(matrix, forward(matrix, z), tuple(z[k] % 32 for k in OWNERS)) == z, + "large integer roundtrip failed") + count += 1 + for _ in range(64): + z = tuple(rng.randrange(-10**6, 10**6) * (32 if i in OWNERS else 1) + for i in range(112)) + require(recover(matrix, forward(matrix, z), (0,) * 8) == z, + "sparse sublattice roundtrip failed") + count += 1 + return count + + +def expect_rejection(call, fragment): + try: + call() + except ValueError as error: + require(fragment in str(error), "rejected for an unexpected reason") + else: + raise ValueError("invalid fixture was accepted: " + fragment) + + +def check_controls(matrix): + zero = (0,) * 112 + expect_rejection(lambda: recover(matrix, zero, (1,) + (0,) * 7), "odd doubled") + expect_rejection(lambda: recover(matrix, zero, (6,) + (0,) * 7), "no quotient") + expect_rejection(lambda: recover(matrix, zero, (10,) + (0,) * 7), "owner residue differs") + expect_rejection(lambda: recover(matrix, (26,) + zero[1:], (0,) * 8), "half-tie rule") + expect_rejection(lambda: recover(matrix, zero, (0,) * 7), "wrong length") + expect_rejection(lambda: recover(matrix, zero, (32,) + (0,) * 7), "outside") + expect_rejection(lambda: recover(matrix, zero, (False,) + (0,) * 7), "requires integers") + expect_rejection(lambda: recover(matrix, zero[:-1], (0,) * 8), "wrong length") + expect_rejection(lambda: forward(matrix, (1 << 4096,) + zero[1:]), "4096 bits") + expect_rejection(lambda: certificate(matrix, (6,) + OWNERS[1:]), "A H differs") + corrupt = ((2,) + TWICE_INVERSE[0][1:],) + TWICE_INVERSE[1:] + expect_rejection(lambda: certificate(matrix, twice_inverse=corrupt), "A H differs") + require(nearest_away(26) == 1 and nearest_away(-26) == -1, + "half ties must round away from zero") + require(round(Fraction(26, 52)) != nearest_away(26), "tie-even control disappeared") + return 11 + + +def check_threshold(matrix): + sums = matvec(matrix, (1,) * 8) + left, right = tuple(48 * x for x in sums), tuple(56 * x for x in sums) + require(left != right, "collision inputs coincide") + require(all(x % 16 == 0 for x in left + right), "four-bit collision leaves lattice") + expected = tuple(-4 * x for x in sums) + require(forward(matrix, left) == forward(matrix, right) == expected, + "four-bit collision fails") + require(any(left[i] % 32 != right[i] % 32 for i in OWNERS), + "five-bit residues fail to separate the collision") + unit = (1,) + (0,) * 111 + require(0 not in OWNERS and all(unit[i] % 32 == 0 for i in OWNERS), + "strict domain witness leaves sparse lattice") + require(any(x % 32 for x in unit), "strict domain witness is uniform") + require(recover(matrix, forward(matrix, unit), (0,) * 8) == unit, + "strict domain witness fails recovery") + return {"left": left, "right": right, "output": expected} + + +def main(): + matrix = load_matrix() + selected = certificate(matrix) + determinant, inverse = rational_inverse(selected) + require(determinant == -16, "wrong selected determinant") + require(tuple(tuple(2 * x for x in row) for row in inverse) == TWICE_INVERSE, + "rational inversion differs from the integer certificate") + combinations = multiply(matrix, inverse) + require(all(x.denominator == 1 for row in combinations for x in row), + "selected rows do not span the integer row lattice") + threshold = check_threshold(matrix) + report = {"status": "PASS_EIGHT_OWNER_INJECTIVITY", "claim_type": "scoped proof with finite corroboration", + "owners_zero_based": OWNERS, "selected_determinant": int(determinant), + "residue_bits": 40, "sharp_equal_bits_per_selected_owner": 5, + "scalar_candidates_checked": check_scalar_intervals(), + "literal_roundtrips": check_roundtrips(matrix), + "rejection_controls": check_controls(matrix), + "four_bit_collision": threshold, + "package_sha256": {name: hashlib.sha256((HERE / name).read_bytes()).hexdigest() + for name in ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py")}} + print(json.dumps(report, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()