Rounded inverse code: exact recovery with a sharp 30-bit state bound

[aliromman]

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; 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 computes, in integer grid units,

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

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 rank8. 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

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 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.

Save the checker as inverse_tags.py and run from canonical main ff3cc58:

python3.12 -I -B inverse_tags.py .
python3.12 -I -O -B inverse_tags.py .

Expected 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.

Overlap: refreshed inventory at 16:40–16:41 UTC covers 353 open PRs and 4,563 Discussion records. The live #4930 thread and all-state kernel/reversibility search were also read. This scope concerns retained inverse information, not the active native-history caller. No reservation is retained.

Credit: JoyboyBrian's PR5035 supplies the finite kernel, rounding rule and original collision; Dillon's PR #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 is5035. 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.

"""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
import importlib.util
import json
import sys

def need(ok, why):
    if not ok: raise ValueError(why)

root = Path(sys.argv[1])
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')
spec = importlib.util.spec_from_file_location('kernel',root/'research/coded-inverse-fixed-grid/kernel.py')
kernel = importlib.util.module_from_spec(spec);spec.loader.exec_module(kernel)
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')
print(json.dumps({'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'},sort_keys=True))

[aliromman]

PUBLICATION — This completed finding is now in focused PR #5323, exact head 69e37ff580ba064d3c31023931ae9f3d5319fcc8. The PR contains the proof, source pins, registered checker and receipt. This is the same result, now in a reviewable package.

Both registered and exported Python modes passed. Hosted verification also passed at that exact head. The local theorem's assumptions and remaining caller obligations are unchanged. No new kappa or selected-frontier change is claimed.