Give the rounded inverse code exact recovery with a sharp state bound

research/inverse-code-recovery-tags/PROOF.md

@@ -0,0 +1,43 @@
+# Exact recovery tags with a sharp state bound for the rounded inverse code
+
+FINDING — the rounded inverse-code kernel has a sharp recovery-state bound: 13^8 states, or 30 packed bits, per real scalar coordinate of its 112 owners. Eight separate four-bit quotient tags give a simple 32-bit implementation of the injective output interface. This answers part of the ownership question left by [PR #5035](https://github.com/CrocSwap/integer-mult-bounds/pull/5035); it is not a reversible circuit, a free cleanup rule, or a new kappa.
+
+Let M be the actual 112-by-8 signed mode matrix, with M^T M=56I. Let round mean nearest integer with exact ties away from zero. The [source kernel](https://github.com/CrocSwap/integer-mult-bounds/blob/ff3cc58e370d0f678e529246f8c73e8094e18fcf/research/coded-inverse-fixed-grid/kernel.py) computes, in integer grid units,
+
+```text
+t=M^T x,  q=round(t/52),  y=x-Mq.
+```
+
+Retain the eight tags a_j=q_j mod 13. Given y and the tags, compute s=M^T y. For each mode, recover the unique integer q in
+
+```text
+ceil((-26-s)/4) <= q <= floor((26-s)/4)
+q mod 13 = a
+round((s+56q)/52) = q.
+```
+
+There are at most fourteen integers in that interval, independently of the input word length. Then return x=y+Mq. This is an exact constructive inverse for the tagged map on every integer input. A caller can pack the tags as sum_j a_j 13^j, or keep eight four-bit fields.
+
+**Why recovery is unique.** Write r=t-52q. The rounding rule gives -26<=r<=26, and s=r-4q. Two distinct candidates with the same residue mod13 must differ by at least13, so their r values differ by at least52. Equality forces the endpoints -26 and +26, with the larger q at +26. For nearest rounding away from zero, r=-26 requires q>=1, while r=+26 requires q<=-1. Those conditions cannot hold for an increasing pair. Thus at most one candidate is valid; the original q supplies existence. Reconstruction also verifies the defining forward relation, since M^T(y+Mq)=s+56q.
+
+**Sharp lower bound.** For every v in {-6,...,6}^8, take x=Mv. Then t=56v and round(56v/52)=v, so y=0. The 13^8 vectors are distinct because M has column rank 8. They all obey ||x||_infinity<=24. Therefore any injective extension of this rounded map needs at least 13^8 distinguishable retained states when the input bound admits H>=24. The tags above attain that state count. Since
+
+```text
+2^29 < 13^8 = 815730721 < 2^30,
+```
+
+30 packed bits are necessary and sufficient for one coordinate. For N independent real scalar coordinates, the exact maximum fiber size is 13^(8N), so the information lower bound is ceil(log2(13^(8N))) bits. A direct separate-tag layout uses 32N bits. Signed monomial physical wrappers are bijections and do not change these fiber counts.
+
+**Why this matters for a caller.** The source kernel's noninjectivity is quantified, rather than treated as an unspecified loss of the entire input word. A caller that must recover the original inputs can retain a fixed amount of information per coordinate. Those tags are output state that must have an owner. This theorem does not permit them to be erased while preserving only y, and does not price a reversible gate implementation, tag movement, whole-field storage or later uncomputation. The original paid classical overwrite contract remains valid on its own terms. The complete physical boundary invoice and global precision remain separate obligations.
+
+**Evidence.** Normal and optimized CPython 3.12.13 checks agree. The checker authenticates the actual [mode source](https://github.com/CrocSwap/integer-mult-bounds/blob/ff3cc58e370d0f678e529246f8c73e8094e18fcf/research/coded-native-caller/NORMALIZERS.json) and kernel, verifies the Gram identity, checks all valid residual cases for q=-200,...,200, and round-trips forty mixed 112-owner vectors through the actual source kernel. The written proof covers all integers. Zero-fiber fixtures and the twelve-residue collision are controls. No whole native, compiler, selected replay or reversible machine run was made.
+
+Run the registered checks with CPython 3.12:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/inverse-code-recovery-tags
+```
+
+Expected verifier marker: PASS_SHARP_INVERSE_KERNEL_TAGS. The checker proves the large zero-fiber count by the exact Gram/scalar identities; it does not enumerate 815 million vectors.
+
+Credit: JoyboyBrian's PR5035 supplies the finite kernel, rounding rule and original collision; Dillon's [PR #4933](https://github.com/CrocSwap/integer-mult-bounds/pull/4933) supplies the mode factorization and physical wrappers; Dugongue and the retained native, ownership, precision and compiler authors keep their source credit. Some retained package prose uses the wrong number PR5037 for this kernel; the verified PR is 5035. New exact recovery formula and sharp fiber count: Ali Romman with OpenAI Codex assistance, Apache-2.0. Author-checked, not independent human or proof-kernel acceptance.

research/inverse-code-recovery-tags/README.md

@@ -0,0 +1,35 @@
+# Exact recovery tags with a sharp state bound for the rounded inverse code
+
+FINDING — the rounded inverse-code kernel has a sharp recovery-state bound: 13^8 states, or 30 packed bits, per real scalar coordinate of its 112 owners. Eight separate four-bit quotient tags give a simple 32-bit implementation of the injective output interface. This answers part of the ownership question left by [PR #5035](https://github.com/CrocSwap/integer-mult-bounds/pull/5035); it is not a reversible circuit, a free cleanup rule, or a new kappa.
+
+[PROOF.md](PROOF.md) states the quantified result, dependencies and limits.
+[RESULT.json](RESULT.json) records the bounded exact replay.
+[SOURCES.json](SOURCES.json) pins the input bytes at canonical main ff3cc58e370d0f678e529246f8c73e8094e18fcf.
+This publishes the result from [its Discussion](https://github.com/CrocSwap/integer-mult-bounds/discussions/5303); it is the same
+contribution, with a committed proof and registered replay.
+
+## Reproduce
+
+Use CPython 3.12 and the standard library:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/inverse-code-recovery-tags
+python3.12 -I -O -W error -B research/inverse-code-recovery-tags/verify.py
+```
+
+Both registered modes authenticate the declared input bytes and compare the
+exact receipt. Source modules load from authenticated source bytes. The written
+proof covers the quantified domain; finite fixtures do not replace it.
+No full physical caller, native/compiler, Lean or selected-frontier replay ran.
+The complete kappa calculation is unchanged.
+
+## Open next questions
+
+Price a reversible implementation and assign an owner to the retained tags in one complete caller.
+The remaining contracts block caller admission. See TASK.json and PROOF.md.
+
+## Credit
+
+The proof retains the named predecessors and links their exact sources.
+New theorem and checks: Ali Romman with substantial OpenAI Codex assistance.
+Apache-2.0. This is author-checked evidence, not independent acceptance.

research/inverse-code-recovery-tags/RESULT.json

@@ -0,0 +1,9 @@
+{
+  "status": "PASS_SHARP_INVERSE_KERNEL_TAGS",
+  "scalar_cases": 20851,
+  "actual_kernel_vectors": 40,
+  "zero_fiber_size": 815730721,
+  "minimum_packed_bits": 30,
+  "simple_separate_tag_bits": 32,
+  "scope": "one scalar coordinate of 112 owners"
+}

research/inverse-code-recovery-tags/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/coded-inverse-fixed-grid/kernel.py",
+      "usage": "input",
+      "git_blob": "70b5d65cae9a8f19cfda4a862c7ecc0bdc42c89b",
+      "sha256": "bc0e9f705665d6981c0f9176dad0f2d71471735e866c44643cb6835423435303"
+    },
+    {
+      "path": "research/coded-native-caller/NORMALIZERS.json",
+      "usage": "input",
+      "git_blob": "bca92c222c395d3d75c047fbb678f3cd0947c60f",
+      "sha256": "ae8aad06aa5d1811d725895b3ab5a4f4daa9dcdd88294aa0d5f723e78bb1e0da"
+    }
+  ]
+}

research/inverse-code-recovery-tags/TASK.json

@@ -0,0 +1,74 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 7,
+  "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Prove one missing implication with explicit quantified hypotheses.",
+      "Find an exact counterexample at the claimed interface boundary."
+    ],
+    "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_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.",
+    "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.",
+    "allowed_variations": [
+      "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller."
+    ],
+    "scope_change_triggers": [
+      "Replacing a quantified obligation with another finite smoke test.",
+      "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses."
+    ],
+    "overlap_terms": [
+      "uniform transfer",
+      "all-size",
+      "precision",
+      "4100",
+      "unconditional-batched-crt"
+    ],
+    "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_status": "refined",
+  "actual_scope": "Exact recovery tags with a sharp state bound for the rounded inverse code",
+  "scope_change_reason": "Publish the completed, scoped Discussion result as a source-bound proof and replay package. The local interface or error obligation is separate from the complete physical caller.",
+  "bottleneck_link": "The physical construction needs funded precision and owned state. This result supplies one exact local obligation; it does not change the paid Gaussian profile.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the stated theorem and its bounded checks. Do not admit a caller or change the selected frontier.",
+  "outcome": "completed",
+  "evidence": "PROOF.md and RESULT.json give the theorem, source-bound exact checks and their limits.",
+  "author": "Ali Romman with OpenAI Codex assistance",
+  "ai_assistance": "Substantial OpenAI Codex assistance; no independent human review.",
+  "open_questions": [
+    {
+      "question": "Price a reversible implementation and assign an owner to the retained tags in one complete caller.",
+      "why_it_matters": "The complete physical cost and accuracy obligations still bind admission.",
+      "first_step": "Price a reversible implementation and assign an owner to the retained tags in one complete caller.",
+      "blocked_by": "The remaining caller contracts listed in PROOF.md."
+    }
+  ]
+}

research/inverse-code-recovery-tags/VERIFY.json

@@ -0,0 +1,37 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/coded-inverse-fixed-grid/kernel.py",
+    "research/coded-native-caller/NORMALIZERS.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Authenticate source bytes, check the stated exact identities and controls, and compare the committed receipt."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Authenticate source bytes, check the stated exact identities and controls, and compare the committed receipt."
+    }
+  ]
+}

research/inverse-code-recovery-tags/verify.py

@@ -0,0 +1,88 @@
+"""Exact inverse tags for the source rounded code.
+Ali Romman with OpenAI Codex assistance. Apache-2.0.
+"""
+from pathlib import Path
+from hashlib import sha256
+from types import SimpleNamespace
+import json
+import argparse
+
+def need(ok, why):
+    if not ok: raise ValueError(why)
+
+HERE = Path(__file__).resolve().parent
+root = HERE.parents[1]
+for pin in json.loads((HERE/'SOURCES.json').read_text())['files']:
+    if pin['usage'] == 'input':
+        need(sha256((root/pin['path']).read_bytes()).hexdigest() == pin['sha256'], 'Declared source pin')
+
+p = root/'research/coded-native-caller/NORMALIZERS.json'
+need(sha256(p.read_bytes()).hexdigest() == 'ae8aad06aa5d1811d725895b3ab5a4f4daa9dcdd88294aa0d5f723e78bb1e0da', 'Mode source pin')
+m = json.loads(p.read_text())['mode_columns']
+need(all(sum(a*b for a,b in zip(c,d)) == 56*(i==j)
+         for i,c in enumerate(m) for j,d in enumerate(m)), 'Gram')
+
+def rnd(t):
+    return (1 if t>=0 else -1)*((abs(t)+26)//52)
+
+def expand(v):
+    return [sum(c[i]*z for c,z in zip(m,v)) for i in range(112)]
+
+def forward(x):
+    q = [rnd(sum(a*b for a,b in zip(c,x))) for c in m]
+    z = expand(q)
+    return [a-b for a,b in zip(x,z)], [z%13 for z in q]
+
+def recover_mode(s, tag):
+    lo = -((26+s)//4)
+    hi = (26-s)//4
+    qs = [q for q in range(lo,hi+1) if q%13 == tag and rnd(s+56*q) == q]
+    need(len(qs)==1, 'Unique valid quotient')
+    return qs[0]
+
+def inverse(y,tags):
+    need(len(tags)==8 and all(type(t) is int and 0<=t<13 for t in tags), 'Tags')
+    q = [recover_mode(sum(a*b for a,b in zip(c,y)),tag) for c,tag in zip(m,tags)]
+    z = expand(q)
+    return [a+b for a,b in zip(y,z)]
+
+scalar = 0
+for q in range(-200,201):
+    for r in range(-26,27):
+        t = 52*q+r
+        if rnd(t) != q: continue
+        need(recover_mode(t-56*q,q%13)==q, 'Scalar inverse')
+        scalar += 1
+need(sha256((root/'research/coded-inverse-fixed-grid/kernel.py').read_bytes()).hexdigest() == 'bc0e9f705665d6981c0f9176dad0f2d71471735e866c44643cb6835423435303', 'Kernel source pin')
+namespace = {'__name__': 'source_kernel', '__file__': str(root/'research/coded-inverse-fixed-grid/kernel.py')}
+exec(compile((root/'research/coded-inverse-fixed-grid/kernel.py').read_bytes(), namespace['__file__'], 'exec'), namespace)
+kernel = SimpleNamespace(**namespace)
+for seed in range(1,41):
+    x = [((i*i*seed+7*i+31*seed)%501)-250 for i in range(112)]
+    y,tags = forward(x)
+    need(inverse(y,tags)==x, 'Whole inverse')
+    width=kernel.word_width(250)
+    words=[kernel.encode(v,width) for v in x]; scratch=[[0]*width for _ in range(9)]
+    kernel.recode(words,m,250,scratch)
+    need([kernel.decode(w) for w in words]==y, 'Source kernel agreement')
+for v in [-6,-1,0,1,6]:
+    for mode in range(8):
+        z=[0]*8;z[mode]=v
+        x=expand(z);y,tags=forward(x)
+        need(y==[0]*112 and inverse(y,tags)==x, 'Zero fiber')
+# The scalar condition proves all 13^8 combinations, without a large enumeration.
+need(all(rnd(56*v)==v for v in range(-6,7)), 'All zero-fiber scalar choices')
+need(2**29 < 13**8 <= 2**30, 'Sharp packed bit count')
+# Twelve residue states cannot distinguish the two zero-fiber endpoints.
+need((-6)%12==6%12 and rnd(56*-6)==-6 and rnd(56*6)==6, 'Too few states control')
+result = {'status':'PASS_SHARP_INVERSE_KERNEL_TAGS','scalar_cases':scalar,
+ 'actual_kernel_vectors':40,'zero_fiber_size':13**8,'minimum_packed_bits':30,
+ 'simple_separate_tag_bits':32,'scope':'one scalar coordinate of 112 owners'}
+parser = argparse.ArgumentParser()
+parser.add_argument('--write-result', action='store_true')
+args = parser.parse_args()
+if args.write_result:
+    (HERE/'RESULT.json').write_text(json.dumps(result, indent=2)+'\n')
+else:
+    need(json.loads((HERE/'RESULT.json').read_text()) == result, 'Receipt mismatch')
+print(json.dumps(result, sort_keys=True))