Physical inverse pair: exact rounding cancellation and an explicit precision guard

[aliromman]

FINDING — exact local rounding transfer for the physical inverse-coded pair. This closes one part of the precision question in PR #5069. It supplies a precision guard for the two inverse recodings. It does not admit a complete caller or increase kappa.

Use the exact operators and order in the source pair proof. Let e0 be the residual just after the entrance C^-1, e1 the residual just after the thin C^-1 on its actual, possibly perturbed input, and e2 the residual just after the exit C, before the final Q^-1. Other operations are exact in this local statement. Then the output errors are exactly

Delta X = -D Q C e0
Delta Y = Q^-1 (C e1 + e2).

In particular, the entrance inverse error cancels from Y. The second inverse need not be linear or have an error independent of its input: define e1 as its actual output minus C^-1 of that input. Thus this formula also applies to the noninjective rounded kernel in PR #5035. It has no product of e0 and e1.

Proof: after entrance and FULL,

y1 = C^-1 y + e0
x2 = D x - D Q y - D Q C e0
y2 = D C^-1 y + D e0.

The thin adds Q^-1(C^-1 x2+e1) to y2. Use [C,DQ]=0, which the source proves for the actual signed normalizers. Both the original-y term and the e0 term cancel. The remaining value is Q^-1 C^-1 D x+Q^-1 e1. Applying the exit Q^-1 C Q, with e2 injected at the stated site, gives D Q^-1 x+Q^-1(C e1+e2). This proof never commutes C through Q alone.

Component precision, for every positive tensor width f. Measure the maximum absolute real or imaginary component. The exact 112-owner code has absolute row sum 26. A row of a k-axis canonical complex Gaussian has real-component absolute row sum 2^ceil(k/2): its 2^k coefficients have modulus 2^(-k/2); for even k each is real or imaginary, while for odd k both components have equal magnitude. Right multiplication by a real signed monomial preserves this sum. Each owner block of C_f is A_ij K_i,f^-1 K_j,f, with A applied once across owners. Therefore

||D_f Q_f C_f||_(infinity,real) = 26 * 2^ceil(9f/2)
||Q_f^-1 C_f||_(infinity,real) = 26 * 2^ceil(f/2)
||Delta X|| <= 26 * 2^ceil(9f/2) ||e0||
||Delta Y|| <= 2^ceil(f/2) (26 ||e1|| + ||e2||).

These are induced norms for arbitrary residual vectors. They do not assert that a rounded kernel attains each worst case. With exact exit recoding and each inverse error at most 22^-P, the two inverse errors contribute at most 522^(ceil(9f/2)-P) to any output component. Hence

P = p + ceil(9f/2) + 6

makes their combined contribution strictly less than 2^-p. The width-dependent guard cannot be replaced by the width-independent Euclidean norm 13 when the contract is componentwise absolute precision.

Sharper guard for the actual mode kernel. The source kernel rounds each of the eight modes before owner updates. In common coordinates its residual is -M delta, where delta contains the eight mode rounding errors. Since A M=-13 M, each physical residual obeys C_f e=-13 e. For these two kernel calls, with exact wrappers and exact other operations, the formula improves to

Delta X = 13 D Q e0
Delta Y = -13 Q^-1 e1          (e2=0).

The component bound is then 26*2^(ceil(9f/2)-P), and P=p+ceil(9f/2)+5 suffices. This reduces the generic residual guard by one bit. It uses the source kernel's error shape, not a better rounding rule or a new machine tariff. A different inverse implementation must establish that error-shape premise before it uses the sharper guard.

Evidence. The checker below authenticates three input files, verifies A^2+12A=13I and all 112 row sums and A M=-13 M, and checks the chronological residual formula with exact rational complex arithmetic in seven actual signed-normalizer Walsh fibers at widths 1,2,3,5. It rejects omitted X error, reversed thin order and the wrong exit injection site. Literal Gaussian tensor rows through 12 axes check the real-component norm; integer guards are checked for f=1,...,100. The written operator and row arguments establish the all-width statement; these finite fixtures do not enumerate every address. Twelve actual finite-kernel invocations also satisfy C e=-13 e and return owned scratch clean. Normal and optimized CPython 3.12.13 give the same receipt.

Save the code as pair_error.py and run against canonical main ff3cc58:

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

Expected marker: PASS_PHYSICAL_PAIR_ERROR_TRANSFER.

Remaining limits and next step. This is a local residual theorem. It does not fund native or Gaussian rounding, movement, field storage, common-coordinate access, or the whole caller's error budget. The second inverse input bound H must include the perturbed x2. The source kernel uses paid classical destructive writes; no reversible cleanup follows. No full native, compiler, outer-ledger or selected replay ran. First use this guard in a changed or shared-boundary caller with an affordable complete invoice; the unshared p19 boundary budget already rejects repeated use of the original recipe.

Overlap: the current #4930 thread, the complete cached note/PR/Discussion inventory from 15:42–15:43 UTC, and a fresh all-state GitHub search for #5069 rounding were checked. The active native-history construction and other callers are outside this scope. No reservation is retained.

Source-number note: some retained package prose calls the finite-grid kernel PR5037. The actual kernel contribution is PR5035, as its PR body and package paths confirm. Links here use that verified identity.

Credit: JoyboyBrian supplied the physical pair and finite-grid kernel; Dillon supplied the actual normalizers and code factorization; Dugongue supplied the center-free producer; Cayden Burkart supplied the coded controller. Cinna Davis, Cao Yifan, zxv, Jacob Alan Sussman and retained native/precision/compiler contributors keep their source credit. New residual derivation and checker: Ali Romman with OpenAI Codex assistance, Apache-2.0. This is author-checked evidence, not independent human or proof-kernel review.

"""Check the local pair error formula. Ali Romman with OpenAI Codex assistance.
Apache-2.0. The written proof gives the all-width statement.
"""
from fractions import Fraction as F
from hashlib import sha256
from pathlib import Path
import json
import importlib.util
import sys

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

root = Path(sys.argv[1])
paths = ['research/native-center-free-code/CODE.json',
         'research/coded-native-caller/NORMALIZERS.json',
         'research/coded-inverse-fixed-grid/kernel.py']
raw = [(root / p).read_bytes() for p in paths]
need([sha256(b).hexdigest() for b in raw] == [
    '8be7f3f073b7981ec91c6af43edff0ac8a89f4824ef6026ae758c287dd6c03d0',
    'ae8aad06aa5d1811d725895b3ab5a4f4daa9dcdd88294aa0d5f723e78bb1e0da',
    'bc0e9f705665d6981c0f9176dad0f2d71471735e866c44643cb6835423435303'], 'Source pins')
a = [[F(v) for v in row] for row in json.loads(raw[0])['A']]
records = json.loads(raw[1])['ports']
n = len(a)
need(n == 112 and len(records) == n, 'Owner count')
need(all(sum(map(abs, row)) == 26 for row in a), 'Absolute code row sums')
modes = json.loads(raw[1])['mode_columns']
need(all(sum(a[i][j]*m[j] for j in range(n)) == -13*m[i]
         for m in modes for i in range(n)), 'Error modes have eigenvalue -13')
# A^2 + 12A = 13I gives the inverse used below.
need(all(sum(a[i][k]*a[k][j] for k in range(n)) + 12*a[i][j]
         == 13*(i == j) for i in range(n) for j in range(n)), 'Inverse identity')

def add(x, y, s=1):
    return [(p[0]+s*q[0], p[1]+s*q[1]) for p,q in zip(x,y)]

def phase(x, exponents):
    out = []
    for (r,i), e in zip(x, exponents):
        out.append(((r,i),(-i,r),(-r,-i),(i,-r))[e % 4])
    return out

def code(x, inverse=False):
    y = [(sum(aij*v[0] for aij,v in zip(row,x)),
          sum(aij*v[1] for aij,v in zip(row,x))) for row in a]
    if inverse:
        return [((u[0]+12*v[0])/13,(u[1]+12*v[1])/13) for u,v in zip(y,x)]
    return y

def mv(rows, u):
    return sum(((r & u).bit_count() % 2) << i for i,r in enumerate(rows))

def trans(rows):
    return [sum(((r >> i)&1)<<j for j,r in enumerate(rows)) for i in range(9)]

spec = importlib.util.spec_from_file_location('source_kernel', root / paths[2])
kernel = importlib.util.module_from_spec(spec)
spec.loader.exec_module(kernel)
for seed in range(1,13):
    inp = [((i*i+seed*11)%103)-51 for i in range(n)]
    width = kernel.word_width(51)
    words = [kernel.encode(v,width) for v in inp]
    scratch = [[0]*width for _ in range(9)]
    kernel.recode(words,modes,51,scratch)
    actual = [(F(kernel.decode(w)),F(0)) for w in words]
    exact = code([(F(v),F(0)) for v in inp],True)
    err = add(actual,exact,-1)
    need(code(err) == [(-13*r,-13*i) for r,i in err], 'Actual kernel error mode')
    need(max(abs(r) for r,i in err) <= 2, 'Kernel error bound')
    need(all(not any(w) for w in scratch), 'Owned cleanup')
fibers = [(0,), (1,), (19,), (511,), (0,1), (1,19,256), (17,256,3,98,511)]
rejected = {'entry_error_in_X':False, 'thin_order':False, 'exit_error_before_C':False}
for us in fibers:
    v = [[mv(trans(r['G_rows']), u ^ r['Z_mask']) for u in us] for r in records]
    q = [sum(z&1 for z in vs) for vs in v]
    d = [sum((z>>1).bit_count() for z in vs) for vs in v]
    need(all((qi+di-sum(u.bit_count() for u in us))%4 == 0 for qi,di in zip(q,d)),
         'Physical DQ phase')
    qi = [-e for e in q]
    fixtures = [[(F((i*i+3*s)%29,7+s), F((7*i+s)%19,11+s)) for i in range(n)]
                for s in range(1,6)]
    x,y,e0,e1,e2 = fixtures
    y1 = add(code(y, True), e0)
    x2 = phase(add(x, phase(code(y1),q),-1),d)
    y2 = phase(y1,d)
    query = phase(add(code(x2,True),e1),qi)
    y3 = add(y2,query)
    out = phase(add(code(phase(y3,q)),e2),qi)
    idealx = phase(add(x,phase(y,q),-1),d)
    idealy = phase(phase(x,qi),d)
    dx = phase(phase(code(e0),q),d)
    dy = phase(add(code(e1),e2),qi)
    need(x2 == add(idealx,dx,-1), 'Entry error in X')
    need(out == add(idealy,dy), 'Exact local Y residual')
    rejected['entry_error_in_X'] |= x2 != idealx
    wrong = phase(add(code(phase(add(y2,add(code(phase(x2,qi),True),phase(e1,qi))),q)),e2),qi)
    rejected['thin_order'] |= wrong != out
    rejected['exit_error_before_C'] |= out != add(idealy,phase(code(add(e1,e2)),qi))
need(all(rejected.values()), 'Controls must fail')
# Build a literal row of G^tensor k and sum real and imaginary magnitudes.
row = [(F(1),F(0))]
for k in range(1,13):
    row = [((r-s*i)/2,(i+s*r)/2) for r,i in row for s in (1,-1)]
    need(sum(abs(r)+abs(i) for r,i in row) == 2**((k+1)//2), 'Real component norm')
for f in range(1,101):
    guard = (9*f+1)//2 + 5
    need(F(26*2**((9*f+1)//2),2**guard) < 1, 'Precision guard')
print(json.dumps({'status':'PASS_PHYSICAL_PAIR_ERROR_TRANSFER',
 'source_sha256':dict(zip(paths,map(lambda b:sha256(b).hexdigest(),raw))),
 'fibers':[list(u) for u in fibers], 'code_rows':n, 'code_abs_row_sum':26,
 'actual_kernel_fixtures':12, 'gaussian_tensor_rows':12, 'guard_widths_checked':100,
 'controls':rejected},sort_keys=True))

[aliromman]

PUBLICATION — This completed finding is now in focused PR #5322, exact head 57c650a571e23e9f06d7f3aff250d57266054992. 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.