Independent verification: PR869's U8 word and κ with a code-disjoint checker (no new kappa)

research/u8-independent-xcheck/README.md

@@ -0,0 +1,73 @@
+# Independent verification of PR869's U8 complex word (no new kappa)
+
+**Status: independent verification.** A checker written from the word semantics, sharing no code with
+`audit_local.py`, the PR799 verifiers or PR869's builders, accepts PR869's U8 word and PR799's selected X4 word
+with exactly their claimed local profiles, and re-derives PR869's κ = 0.001661948695165034 from its PLAN profile.
+
+| word | content sha256 | profile (independently recounted) | result |
+|---|---|---|---|
+| X4 (PR799, selected) | `1e1d99ba…` | `{1:2548, 2:338, 3:430, 4:194, 5:56, 8:8}` | PASS |
+| U8 (PR869) | `090fd574…` | `{1:2548, 2:338, 3:446, 4:162, 5:72, 8:8}` | PASS |
+
+Both have width inventory `{4:80, 5:32, 7:54, 8:122, 9:216}` (3778), 216 entering helpers, 126 low ends and 72 cold ends.
+The same checker also accepts the chain's p6n, promo, SW4 and #741-frames words with their README profiles,
+and PR645's word with its recorded `report.local_profile`.
+
+## What is checked, and how it differs
+
+| obligation | `audit_local.py` | here (`xcheck.py`) |
+|---|---|---|
+| exact scalar map | sparse `Fraction` rows, forward and dual | dense residues mod 16 primes plus a rigorous height bound (printed: below 2^91 against a 2^492 limit), so residues fix entries exactly. The dual is the inverse transpose of the forward map, so it is not replayed separately. |
+| dirty compensation | propagated from target dirt | **solved**: `Comp = Rest⁻¹·E·Pre⁻¹` must be the identity plus a target←helper block avoiding every entering and low-end helper |
+| frame chains, centre paths, paid profile, widths | F2 reduced bases | subspaces held as 512-bit membership sets |
+| low-end inverse-row and dirt-column cones | sparse rows | exact nonzero patterns of the prefix and its inverse |
+| κ | Mercator and base-two moment engines | `mpmath` interval moment at both grid endpoints, plus the seven-step bootstrap closed form |
+
+`price.py` also checks PLAN = 72 × local + the idle remainder `{1:1, 3:1, 44:1, 48:2396}` (the same remainder as PR799)
+and the deficit 2560. As a positive control it reproduces PR799's selected κ and recorded moment residuals
+(−6.22e−25 / +2.33e−24). As a negative control it rejects the next grid point `b + 10⁻²⁴` for U8.
+
+## Negative controls
+
+- `controls.py`: six single mutations of U8, each rejected for the intended reason. They negate a scalar, drop a
+  B gate, shrink a B frame, move a low-end tail to full cleanup, add a target read of an entering helper's start
+  value, and claim a wrong profile.
+- All 36 of PR869's mutant words (four mechanisms × global and eight slots) are rejected, and its C0/recipe words
+  pass. `donation_after` fails here with "compensation is not a target←helper block": no compensation of the
+  allowed form can repair it. That is stronger than `audit_local`'s "nonzero entrance response".
+
+## Reproduce
+
+Build PR869's chain (head `73e86f69bf9a391e3c334999f7bbe3825dc42759`) as in its README, with one correction (below).
+Then, from the PR869 checkout:
+
+```sh
+PY=python3 bash research/u8-independent-xcheck/verify.sh OUT   # OUT holds x4/ and b0/
+# expected last line: PASS_U8_INDEPENDENT_XCHECK   (about 50 s; Python 3.12.13, numpy 2.5.4, sympy 1.14.0, mpmath 1.3.0)
+```
+
+`VERIFY.log` is that run's output. Base commit `f567884aeb8851b6e794af1184119a3bfbe1e631`.
+
+**Reproduction note for PR869:** its README runs `reproduce_jx.py --frames-dir /tmp/frames`, but the script only
+accepts `--sw4-dir` (it applies #741's frames itself). The working command is
+`reproduce_jx.py --main . --pr635 <pr635> --sw4-dir <sw4-out> --out <x4-out>`. With that flag, the rebuilt X4
+and U8 words match PR869's pins byte for byte.
+
+## Scope
+
+This checks the finite local obligations of two words and the arithmetic from PLAN profile to κ.
+It does **not** check:
+- owner admission, hosting, the global invoice or the 47 outer constraints (see #813 for an independent outer check);
+- the PR589 bit supplier (c is cited, and it does not bind);
+- PR870;
+- the parent centre-frame interface (unchanged from X4).
+
+All-size compilation, common-label/mutable-source realization, whole-call hosting, precision/tape and analytic
+transfer remain inherited assumptions. This is a finite replay, not a formal proof.
+
+## Credit
+
+Construction: NewBArch/jeremykothe2 (PR869) on PR799 (Jeremy Kothe), PR741 (Chafik Boukhalfa), PR645 (icekylinx)
+and their lineage. The modular-CRT-with-height-bound idea parallels PR835's independent check of the #741 backward
+endpoint. Assignment seed 80 (track 75–84). Prepared with substantial AI assistance (Claude Code, Anthropic).
+Apache-2.0.

research/u8-independent-xcheck/controls.py

@@ -0,0 +1,48 @@
+"""Negative controls for xcheck.py: each single mutation of an honest word must be rejected.
+
+Usage: controls.py FULL-WORD.json.gz CLAIM-JSON
+"""
+import copy, gzip, json, os, subprocess, sys, tempfile
+
+word, claim = json.loads(gzip.open(sys.argv[1]).read()), sys.argv[2]
+here = os.path.dirname(os.path.abspath(__file__))
+b_add = next(i for i, g in enumerate(word['B']) if g[0] == 'add' and len(g[-1]) > 1)
+
+
+def negate(w):
+    w['A'][0][3] *= -1
+
+
+def drop_b(w):
+    del w['B'][b_add]
+
+
+def shrink_frame(w):
+    w['B'][b_add][-1] = w['B'][b_add][-1][1:]
+
+
+def late_tail(w):
+    w['early_cleanup'].pop(0)
+
+
+def entrance(w):  # a target reads an entering helper's start value
+    w['B'].insert(0, ['add', w['report']['v'], int(next(iter(w['start_extra']))), 1, 1, list(range(1, 1 << w['report']['h']))])
+
+
+def wrong_claim(w):
+    return json.dumps(dict(json.loads(claim), profile={**json.loads(claim)['profile'], '1': json.loads(claim)['profile']['1'] + 1}))
+
+
+results = {}
+for mutate in (negate, drop_b, shrink_frame, late_tail, entrance, wrong_claim):
+    w = copy.deepcopy(word)
+    c = mutate(w) or claim
+    with tempfile.NamedTemporaryFile(suffix='.json.gz', delete=False) as f:
+        f.write(gzip.compress(json.dumps(w).encode()))
+    r = subprocess.run([sys.executable, os.path.join(here, 'xcheck.py'), f.name, c], capture_output=True, text=True)
+    os.unlink(f.name)
+    last = (r.stdout + r.stderr).strip().splitlines()[-1]
+    results[mutate.__name__] = last
+    print(f'{mutate.__name__:13} {last}')
+    assert last.startswith('FAIL'), mutate.__name__
+print('PASS all', len(results), 'controls rejected')

research/u8-independent-xcheck/price.py

@@ -0,0 +1,41 @@
+"""Re-price a gauge44 global profile with mpmath interval arithmetic (no shared moment engine).
+
+Usage: price.py PLAN.json LOCAL-PROFILE-JSON BIT-C B-LOWER KAPPA
+Checks: PLAN profile = 72 * local + idle remainder, rank deficit, the moment sign at both
+certificate endpoints, and the closed-form kappa grid step from (b, c).
+"""
+import json, sys
+from fractions import Fraction as Q
+from mpmath import iv, mpf
+
+iv.prec = 400
+plan, local, c, b, kappa = json.load(open(sys.argv[1])), json.loads(sys.argv[2]), Q(sys.argv[3]), Q(sys.argv[4]), Q(sys.argv[5])
+H = {int(r): n for r, n in plan['profile'].items()}
+m, W = plan['M'], plan['live']
+idle = {r: H.get(r, 0) - 72 * local.get(str(r), 0) for r in H}
+assert all(x >= 0 for x in idle.values()), idle
+assert m * W - sum(r * n for r, n in H.items()) == plan['deficit'], 'rank deficit'
+print('idle remainder', {r: x for r, x in idle.items() if x})
+
+
+def moment(z):  # sum_r (r n / (m W)) (m / r)^z, enclosed
+    z = iv.mpf(z.numerator) / z.denominator
+    return sum(iv.mpf(r * n) / (m * W) * iv.exp(z * iv.log(iv.mpf(m) / r)) for r, n in H.items())
+
+
+lo, hi = moment(b), moment(b + Q(1, 10**24))
+assert lo.b < 1 < hi.a, (lo, hi)
+print('moment(b) - 1 <', float(lo.b - 1), '; moment(b + 1e-24) - 1 >', float(hi.a - 1))
+
+# Closed-form kappa from (b, c): common saving s, seven bootstrap steps, eta margin, floor to 1e-18.
+eta = beta = Q(1, 10**24)
+s = min(c, (1 - beta) * b) - Q(1, 10**27)
+a = Q(384599, 10**10)
+for _ in range(7):
+    a = (1 - s) * s + s * a
+q = a * (1 - 2 * eta)
+ticks = (1 - eta) * q / (1 + q) * 10**18
+k = Q((ticks.numerator - 1) // ticks.denominator, 10**18)
+assert k == kappa, (k, kappa)
+print('binding', 'bit' if c < (1 - beta) * b else 'complex', 'kappa', k, float(k))
+print('PASS')

research/u8-independent-xcheck/verify.sh

@@ -0,0 +1,24 @@
+#!/usr/bin/env bash
+# Usage: verify.sh OUT   where OUT holds PR869's chain output (x4/ and b0/ from reproduce_jx.py / reproduce_barch.py)
+# and PR869 is checked out at REPO (default: current directory). Needs Python 3.11+ with numpy, sympy, mpmath.
+set -euo pipefail
+OUT=$1; REPO=${REPO:-.}; PY=${PY:-python3}; HERE=$(cd "$(dirname "$0")" && pwd)
+sha() { gzip -dc "$1" | shasum -a 256 | cut -c1-64; }
+X4=$OUT/x4/jx/FULL-WORD.json.gz; U8=$OUT/b0/barch/FULL-WORD.json.gz
+test "$(sha $X4)" = 1e1d99ba7aab877d6b573c41f7030ee73de9a52fee51d0a822ddaae71251999f
+test "$(sha $U8)" = 090fd574747fbf9628e70cb9beb792732914cfa52e1df147579fe4dbccc68c5a
+W='"widths":{"4":80,"5":32,"7":54,"8":122,"9":216}'
+X4C="{\"profile\":{\"1\":2548,\"2\":338,\"3\":430,\"4\":194,\"5\":56,\"8\":8},$W}"
+U8C="{\"profile\":{\"1\":2548,\"2\":338,\"3\":446,\"4\":162,\"5\":72,\"8\":8},$W}"
+$PY "$HERE/xcheck.py" "$X4" "$X4C"
+$PY "$HERE/xcheck.py" "$U8" "$U8C"
+$PY "$HERE/controls.py" "$U8" "$U8C"
+for f in "$OUT"/b0/barch-controls/*.json.gz; do
+  n=$(basename "$f" .json.gz); r=$($PY "$HERE/xcheck.py" "$f" 2>&1 | tail -1 || true)
+  case $n in C0|recipe) [[ $r == PASS ]];; *) [[ $r == FAIL* ]];; esac
+  echo "PR869 control $n: $r"
+done
+C=1733427039589844234749/1000000000000000000000000
+$PY "$HERE/price.py" "$REPO/research/gauge44-barch/data/PLAN.json" '{"1":2548,"2":338,"3":446,"4":162,"5":72,"8":8}' \
+  $C 1664715366696537282003/1000000000000000000000000 830974347582517/500000000000000000
+echo PASS_U8_INDEPENDENT_XCHECK

research/u8-independent-xcheck/xcheck.py

@@ -0,0 +1,197 @@
+"""Independent re-check of a gauge44 FULL-WORD (written for PR869's U8 word).
+
+Shares no code with audit_local.py and uses different methods:
+- scalar map: dense matrices mod 16 primes (~2^496) plus a rigorous magnitude/2-adic height bound, so residues
+  determine every entry exactly (the run prints the certified height);
+- compensation: solved as Rest^-1 * E * Pre^-1 instead of propagated from dirt;
+- frames: subspaces of F2^h held as 2^h-bit membership sets instead of reduced bases.
+Usage: xcheck.py FULL-WORD.json.gz [expected-profile-json]
+"""
+import gzip, json, sys
+from collections import Counter
+from fractions import Fraction
+import numpy as np
+from math import prod
+from sympy import prevprime
+from sympy.ntheory.modular import crt
+
+P = [2**31 - 1]
+while len(P) < 16:
+    P.append(prevprime(P[-1]))
+PP = np.array(P, dtype=np.int64)[:, None]
+MOD = prod(P)
+
+
+def require(ok, msg):
+    if not ok:
+        raise SystemExit('FAIL ' + msg)
+
+
+def residues(q):
+    return np.array([q.numerator * pow(q.denominator, -1, p) % p for p in P], dtype=np.int64)[:, None]
+
+
+class Mat:
+    """n x n dyadic matrix: residues mod 16 primes, plus an |entry| bound and a 2-adic denominator per row."""
+    def __init__(self, n):
+        self.r = np.broadcast_to(np.eye(n, dtype=np.int64), (len(P), n, n)).copy()
+        self.bound = np.eye(n)
+        self.den = np.zeros(n, dtype=np.int64)
+
+    def addrow(self, t, s, q):  # row t += q * row s
+        e = q.denominator.bit_length() - 1
+        require(q.denominator == 1 << e, 'non-dyadic scalar')
+        self.r[:, t] = (self.r[:, t] + residues(q) * self.r[:, s]) % PP
+        self.bound[t] = (self.bound[t] + abs(float(q)) * self.bound[s]) * (1 + 1e-12)
+        self.den[t] = max(self.den[t], self.den[s] + e)
+
+    def scalerow(self, t, q):
+        require(q != 0 and q.denominator & (q.denominator - 1) == 0 and abs(q.numerator) & (abs(q.numerator) - 1) == 0, 'non-unit dyadic scale')
+        self.r[:, t] = self.r[:, t] * residues(q) % PP
+        self.bound[t] *= abs(float(q))
+        self.den[t] += max(0, q.denominator.bit_length() - 1)
+
+    def apply(self, g, inverse=False):
+        q = Fraction(g[3], g[4]) if g[0] == 'add' else Fraction(g[2], g[3])
+        if g[0] == 'add':
+            require(g[1] != g[2], 'self add')
+            self.addrow(g[1], g[2], -q if inverse else q)
+        else:
+            self.scalerow(g[1], 1 / q if inverse else q)
+
+    def certify(self):
+        """Every numerator N = entry * 2^den[row] satisfies |N| < MOD/2, so residues determine entries exactly."""
+        worst = float((self.bound * 2.0 ** self.den[:, None]).max())
+        require(worst < 2.0 ** (MOD.bit_length() - 3), 'bound too large for exact CRT')
+        return worst
+
+    def entry(self, i, j):
+        """Exact rational entry (i, j) by CRT."""
+        d = 1 << int(self.den[i])
+        x = int(crt(P, [int(a) for a in self.r[:, i, j]])[0]) * d % MOD
+        return Fraction(x - MOD if x > MOD // 2 else x, d)
+
+
+def nonzero(m, minus_identity=False):
+    print(f'certified height < 2^{np.log2(m.certify()):.1f} < MOD/8 = 2^{MOD.bit_length() - 4}')
+    r = m.r - np.eye(N, dtype=np.int64) if minus_identity else m.r
+    return (r != 0).any(axis=0)
+
+
+def product(gates, inverse=False):
+    m = Mat(N)
+    for g in (reversed(gates) if inverse else gates):
+        m.apply(g, inverse)
+    return m
+
+
+def span(gens):
+    s = {0}
+    for g in gens:
+        s |= {x ^ g for x in s}
+    return sum(1 << x for x in s)
+
+
+def rank(mask):
+    return mask.bit_count().bit_length() - 1
+
+
+w = json.loads(gzip.open(sys.argv[1]).read())
+h, v = w['report']['h'], w['report']['v']
+require(len(w['ports']) == v, 'port count')
+R = w['report']['R']
+N = 2 * v + R
+require(all(0 <= q < N for k in ('A', 'cut', 'B', 'precondition', 'cleanup') for g in w[k] for q in (g[1:3] if g[0] == 'add' else g[1:2])), 'register out of range')
+targets, helpers = range(v, 2 * v), range(2 * v, N)
+entering = {int(q) for q in w['start_extra']}
+lowends = {int(q) for q in w['helper_final']}
+regs = lambda g: g[1:3] if g[0] == 'add' else g[1:2]
+
+# 1. Reads: no gate outside the target block reads a target in A/B.
+require(all(not (v <= g[2] < 2 * v) for g in w['A'] + w['B'] if g[0] == 'add' and not v <= g[1] < 2 * v), 'non-target reads target')
+
+# 2. Scalar map, with compensation solved rather than propagated.
+early = dict((i, U) for i, U in w['early_cleanup'])
+require(len(early) == len(w['early_cleanup']), 'duplicate early cleanup')
+tail = [w['cleanup'][i][:-1] + [U] for i, U in w['early_cleanup']]
+clean = [g for i, g in enumerate(w['cleanup']) if i not in early]
+main = w['A'] + w['cut'] + w['B']
+rest = main + tail + clean
+# comp = rest^-1 * E * pre^-1, where E adds source t into target v+t.
+comp = product(w['precondition'], inverse=True)
+for t in range(v):
+    comp.addrow(v + t, t, Fraction(1))
+for g in reversed(rest):
+    comp.apply(g, inverse=True)
+nz = nonzero(comp, minus_identity=True)
+block = np.zeros((N, N), dtype=bool)
+block[np.ix_(targets, helpers)] = True
+require(not nz[~block].any(), 'compensation is not a target<-helper block')
+pairs = list(zip(*np.nonzero(nz)))
+used = {int(k) for _, k in pairs}
+require(not set(used) & entering, 'nonzero entrance response')
+require(not set(used) & lowends, 'compensation touches a low end')
+require(not any(set(regs(g)) & (entering | lowends) for g in w['precondition']), 'precondition touches residual helper')
+require(all(g[-1] == [] for g in w['precondition']), 'framed precondition')
+print('scalar map exact; solved compensation has', len(pairs), 'entries on', len(used), 'helpers')
+
+# 3. Frames and paid profile.
+full = span([1 << i for i in range(h)])
+cur = [span([p]) for p in w['ports']] + [span([])] * (v + R)
+for q, U in w['start_extra'].items():
+    require(int(q) in helpers, 'non-helper entrance')
+    cur[int(q)] = span(U)
+start = cur.copy()
+paid = Counter()
+
+
+def climb(q, U):
+    require(cur[q] & ~U == 0, f'frame not monotone at register {q}')
+    if rank(U) > rank(cur[q]):
+        paid[rank(U) - rank(cur[q])] += 1
+    cur[q] = U
+
+
+for g in w['A']:
+    for q in regs(g):
+        climb(q, span(g[-1]))
+levels = {int(t): span(U) for t, U in w['target_levels'].items()}
+require(all(cur[v + t] == levels.get(t, span([])) for t in range(v)), 'target levels at cut')
+for q, U in zip(w['centers'], w['center_frames']):
+    U = span(U)
+    require(cur[q] == U, 'centre frame')
+    for T in sorted({levels.get(g[1] - v, span([])) for g in w['cut'] if g[2] == q}, key=rank, reverse=True):
+        require(T & ~U == 0, 'centre path not nested')
+        if T != U:
+            paid[rank(U) - rank(T)] += 1
+        U = T
+for g in w['B']:
+    for q in regs(g):
+        climb(q, span(g[-1]))
+endB = cur.copy()
+for g in tail:
+    for q in regs(g):
+        climb(q, span(g[-1]))
+end = [full] * v + [span([x for x in range(1, 1 << h) if (x & p).bit_count() % 2 == 0]) for p in w['ports']] + [full] * R
+for q, U in w['helper_final'].items():
+    end[int(q)] = span(U)
+for q in range(N):
+    climb(q, end[q])
+require(all(end[q] == full for g in clean for q in regs(g)), 'full cleanup reads a low end')
+widths = Counter(rank(end[q]) - rank(start[q]) for q in helpers)
+
+# 4. Low-end cones: rows of prefix^-1 and columns of prefix at each low end stay inside its end frame.
+compgates = [['add', int(y), int(k), c.numerator, c.denominator, []] for y, k in pairs for c in [comp.entry(y, k)]]
+prefix = w['precondition'] + compgates + main
+fwd, inv = nonzero(product(prefix)), nonzero(product(prefix, inverse=True))
+for q in lowends:
+    require(all(endB[k] & ~end[q] == 0 for k in np.nonzero(inv[q])[0]), f'inverse-row cone {q}')
+    require(all(endB[k] & ~end[q] == 0 for k in np.nonzero(fwd[:, q])[0] if k != q), f'dirt-column cone {q}')
+print('cones pass for', len(lowends), 'low ends;', len(entering), 'entering;', len(lowends - entering), 'cold ends')
+profile = {k: paid[k] for k in sorted(paid)}
+print('profile', profile, 'widths', dict(sorted(widths.items())))
+if len(sys.argv) > 2:
+    want = json.loads(sys.argv[2])
+    require(profile == {int(k): x for k, x in want['profile'].items()}, 'profile differs from claim')
+    require(dict(widths) == {int(k): x for k, x in want['widths'].items()}, 'widths differ from claim')
+print('PASS')