Prove rounded inverse injectivity from eight owner residues (no κ)

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.

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.

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

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