[RossRichardson]

Summary

Audit the saved R429 sign variant: 23 quotient ADD signs change while the complete binary map, 429 arbitrary integer helper returns and paid rank mass 4989 remain unchanged. A fixed prefix–quotient–suffix proof bounds forward source and target changes by ranks 9 and 3 for all 2^47 sign choices; this witness attains both.

The source-selected scalar controller has a smaller range upper bound, but the new exact adjoint calculation shows mixed error sensitivity. Forward sensitivity worsens, while inverse ADD sensitivity improves and the inverse MOVE/COPY aggregate stays unchanged. See research/r429-signed-range/README.md and its two proof notes.

Scope and limits

The controller is explicitly instantiated with the actual 1,499-ADD source code. Its archived 6,372-gate listing has a different binary endpoint; an independent free noncommuting schedule proof justifies the abstract substitution. The old six-copy suffix receipt is not reused for these three-copy words.

Range bounds and exact atomic error constants belong to the specified normalized scalar model, including conditional COPY/ERASE assignments. They do not admit native child interiors, physical cleanup, a precision law or a supplier. No sign optimality, paid-profile improvement, selected-record change or new kappa is claimed.

Test plan

• CPython 3.12 committed-byte/source-history preflight and all four registered commands.
• Read-only Git-free export replay with unchanged inputs.
• Separate AI integer, range/defect and verification reviews, with findings resolved.
• Automatic registered-package CI passed on 4323518ffa8a8a9885bd1d81df6f3dae2dd3f6a9 (plan and package replay).

Checks cover all 651 public columns in both orientations and roundtrips, every COPY/ERASE cut and frame event, the fixed nine-dimensional transfer certificate, all 16,102 atomic suffixes in each word/direction, and attaining input/error witnesses. Full compressed receipts retain complete coverage; normal/optimized controls test intended failures and deliberate check deletion. No sign search is rerun.

Sources and credit

The immediate word is #3645, with Ali Romman/#1043 and Sagar Thakrar/#2423 transport/rehosting ancestry and prior #1307 geometry. #4185 supplies the separate controller accounting boundary; its paid deficit is unchanged. Exact source bytes, retained notices, heads and storage encodings are recorded in the package manifests. Original sign witness, independent mathematical checks, new proofs and publication were prepared by Ross Richardson with substantial OpenAI Codex assistance. AI review is separate from human acceptance or formal-kernel proof. Apache-2.0.

[rcfc-jreed]

Independent structural audit of the signed R429 witness at 4323518f: no defect found in the scope below

This was a code-disjoint check, standard library only, posted under this CLAIM. It imports none of this package's code (verify.py, check_integer.py, check_range.py, controls.py).

What passes (17 of 17 checks):

1. SHA pins. Parent gzip 1a6841fc… and candidate e8026111… match FROZEN-SHA256.json and RESULT.json.
2. Sign-variant contract. Both words have 16,102 records and identical opcode inventory (MOVE:2873, ADD:13223, COPY:3, ERASE:3). There are exactly 47 quotient ADD gates (op=1, phase/rank=23) with unit parent coefficients. The candidate flips exactly 23 of those coefficients to −1 (matching RESULT.quotient_signs); every other record is byte-identical. Rebuilding parent+signs recovers the candidate under the signed-variant format tag. The quotient touches exactly 9 registers.
3. RESULT / GROWTH consistency. Declared paid rank mass 4989 with identical forward/inverse profiles; prefix L1 norms [80639, 239014] match GROWTH.local_prefix; controller bit-length 401 / 64-rounded 448 / after-decode 519 match the README table.
4. Binary interface. Independent F₂ execution of both words on all 111 source unit vectors (and the zero input) yields identical public views. Odd coefficients act as XOR; MOVE copies; COPY/ERASE touch only the private register. This confirms F₂ invariance of the 23-sign witness under that model; it is not a full integer-column audit.
5. Negative controls:
   • a 24th quotient minus-sign breaks the 23-sign contract;
   • mutating a non-quotient ADD leaves the declared change set;
   • appending a spurious source→target ADD breaks F₂ agreement with the parent.

Not covered: the 2^47 universal sign proof, the dense 651-column integer/frame/COPY audit, the adjoint defect constants J, and precision / all-size admission.

This is a finite structural replay and not a formal proof.

check_4190.py (run: python3 -B check_4190.py --repo <clone with 4323518f>, ≈4 s)

#!/usr/bin/env python3
"""Independent structural check of PR4190's signed R429 witness.

Code-disjoint from package verify.py / check_integer.py / check_range.py.
Confirms the fixed 23-sign quotient variant, opcode inventory, SHA pins,
RESULT/GROWTH consistency, and binary (F₂) interface invariance by executing
both words on the public source basis. Does not re-prove the 2^47 universal
sign theorem or recompute the full adjoint defect constants.

James Reed (@rcfc-jreed), with substantial AI assistance (Claude, in Cursor).
Apache-2.0.
"""
import argparse, collections, copy, gzip, hashlib, json, subprocess, sys

HEAD = '4323518ffa8a8a9885bd1d81df6f3dae2dd3f6a9'
BASE = '12fa8c5c844be21bfefb38a19503fbd867a11244'
PKG = 'research/r429-signed-range/'
results = []


def check(name, ok, detail=''):
    results.append((name, bool(ok), detail))
    print(('PASS ' if ok else 'FAIL ') + name + ((': ' + str(detail)) if detail else ''), flush=True)
    return bool(ok)


def show(repo, path, rev=HEAD):
    return subprocess.run(['git', '-C', repo, 'show', f'{rev}:{path}'],
                          capture_output=True, check=True).stdout


def js(b):
    if b[:2] == b'\x1f\x8b':
        b = gzip.decompress(b)
    return json.loads(b)


def load(repo):
    g = lambda p: show(repo, p)
    d = dict(
        parent=js(g(PKG + 'frozen/parent/WORD.json.gz')),
        candidate=js(g(PKG + 'frozen/candidate/WORD.json.gz')),
        parent_raw=g(PKG + 'frozen/parent/WORD.json.gz'),
        cand_raw=g(PKG + 'frozen/candidate/WORD.json.gz'),
        result=js(g(PKG + 'frozen/candidate/RESULT.json')),
        growth=js(g(PKG + 'frozen/candidate/GROWTH.json')),
        frozen=js(g(PKG + 'FROZEN-SHA256.json')),
        snapshot=js(g(PKG + 'CORE-SNAPSHOT.json')),
    )
    return d


def opcode_counts(records):
    return dict(sorted(collections.Counter(r[0] for r in records).items()))


def f2_execute(word, x_bits):
    """Execute the coded word over GF(2). Odd coefficients act as XOR; MOVE copies;
    COPY/ERASE follow the private C lifecycle at the bit level (presence only).
    Returns the public register bit-vector as a dict reg->0/1.
    """
    regs = {int(r): 0 for r in word['public_registers']} if isinstance(word['public_registers'], list) else {}
    # public_registers may be an int count
    if isinstance(word['public_registers'], int):
        n = word['public_registers']
        regs = {i: 0 for i in range(n)}
    priv = word['private_register']
    regs[priv] = 0
    # start: apply source bits into the source block if named; else first V regs
    # The interface is (x,y,h)->...; sources are the first 111 public fields.
    V = 111
    for i, b in enumerate(x_bits):
        regs[i] = b & 1
    for op, dst, src, c, *_ in word['records']:
        if op == 0:  # MOVE
            regs[dst] = regs.get(src, 0)
        elif op == 1:  # ADD
            if c % 2:  # odd coefficient
                regs[dst] = regs.get(dst, 0) ^ regs.get(src, 0)
        elif op == 2:  # COPY into private
            regs[priv] = regs.get(src, 0)
        elif op == 3:  # ERASE private
            regs[priv] = 0
        else:
            raise ValueError('unknown op')
    return {i: regs.get(i, 0) for i in range(V * 2)}  # sources+targets public view


def run(d):
    parent, cand = d['parent'], d['candidate']
    base, rec = parent['records'], cand['records']
    check('I1 parent/candidate gzip SHA256 match FROZEN-SHA256 and RESULT',
          hashlib.sha256(d['parent_raw']).hexdigest() == d['frozen']['frozen/parent/WORD.json.gz']
          == d['result']['parent_sha256'] == '1a6841fccba51fa922993c77b4b296e659c2c538252e5e06113d0438c5edb870'
          and hashlib.sha256(d['cand_raw']).hexdigest() == d['frozen']['frozen/candidate/WORD.json.gz']
          == d['result']['word_sha256'] == 'e802611104c61fc8477837b4ab41abc4f13cf41fbca6ef3de60d0b5e768fb949')

    check('S1 both words have 16102 records', len(base) == len(rec) == 16102)
    check('S2 opcode inventory identical: 2873 MOVE, 13223 ADD, 3 COPY, 3 ERASE',
          opcode_counts(base) == opcode_counts(rec) == {0: 2873, 1: 13223, 2: 3, 3: 3})

    positions = [i for i, r in enumerate(base) if r[0] == 1 and r[5] == 23]
    check('S3 exactly 47 quotient ADD gates (op=1, phase/rank=23) with unit parent coeff',
          len(positions) == 47 and all(base[i][3] == 1 and base[i][4] == 1 for i in positions))
    signs = [rec[i][3] for i in positions]
    check('S4 candidate has exactly 23 minus signs on those gates, rest +1',
          signs.count(-1) == 23 and signs.count(1) == 24 and all(c in (-1, 1) for c in signs)
          and signs == d['result']['quotient_signs'])
    diffs = [i for i, (a, b) in enumerate(zip(base, rec)) if a != b]
    check('S5 the only record differences are those 23 sign flips (coeff field only)',
          set(diffs) <= set(positions) and len(diffs) == 23
          and all(base[i][:3] == rec[i][:3] and base[i][4:] == rec[i][4:] and base[i][3] == 1 and rec[i][3] == -1
                  for i in diffs),
          f'changed_gates={len(diffs)}')
    # reconstruct candidate from parent + signs
    rebuilt = [r[:] for r in base]
    for i, c in zip(positions, signs):
        rebuilt[i][3] = c
    check('S6 candidate == parent with format tag and the rebuilt records',
          cand == dict(parent, format='coded-r429-signed-quotient-variant-v1', records=rebuilt))

    pivots = sorted({base[i][j] for i in positions for j in (1, 2)})
    check('S7 quotient uses exactly 9 registers', len(pivots) == 9, pivots)

    # RESULT / GROWTH consistency
    r, g = d['result'], d['growth']
    check('R1 RESULT declares same F2/rank, mass 4989, copies 3, both directions',
          r['forward']['rank_mass'] == r['inverse']['rank_mass'] == 4989
          and r['forward']['copies'] == r['inverse']['copies'] == 3
          and r['forward']['profile'] == r['inverse']['profile']
          and sum(int(k) * v for k, v in r['forward']['profile'].items()) == 4989)
    check('R2 RESULT prefix L1 matches GROWTH local_prefix [80639, 239014]',
          r['forward']['prefix_row_l1'] == g['local_prefix'][0] == 80639
          and r['inverse']['prefix_row_l1'] == g['local_prefix'][1] == 239014)
    check('R3 GROWTH controller bit-length 401 / 64-rounded 448 matches README table',
          g['whole_controller']['weighted_global_prefix_upper_bits'] == 401
          and g['whole_controller']['charge_rounded_up_to_64_bits'] == 448
          and g['whole_controller']['after_easy_completed_bank_decode_upper_bits'] == 519)
    check('R4 RESULT changed_gates == 23', r['changed_gates'] == 23)

    # Binary interface invariance on the public source basis (111 unit vectors)
    V = 111
    mismatches = 0
    sample = []
    for i in range(V):
        x = [0] * V
        x[i] = 1
        yp = f2_execute(parent, x)
        yc = f2_execute(cand, x)
        if yp != yc:
            mismatches += 1
            if len(sample) < 3:
                sample.append(i)
    check('F1 F₂ execution on all 111 source unit vectors: parent == candidate public view',
          mismatches == 0, f'mismatches={mismatches} sample={sample}')
    # zero input
    check('F2 F₂ zero input stays zero on public view',
          f2_execute(parent, [0] * V) == f2_execute(cand, [0] * V) == {i: 0 for i in range(2 * V)})

    # Negative controls
    bad = copy.deepcopy(cand)
    # flip one more quotient sign that was +1
    j = next(i for i in positions if rec[i][3] == 1)
    bad['records'][j][3] = -1
    # structural: now 24 minus signs
    check('C flipping a 24th quotient sign leaves the 23-sign witness contract',
          [bad['records'][i][3] for i in positions].count(-1) != 23)
    # mutate a non-quotient ADD coefficient
    k = next(i for i, r in enumerate(base) if r[0] == 1 and r[5] != 23)
    bad2 = copy.deepcopy(cand)
    bad2['records'][k][3] = -bad2['records'][k][3] if bad2['records'][k][3] else -1
    diffs2 = [i for i, (a, b) in enumerate(zip(base, bad2['records'])) if a != b]
    check('C mutating a non-quotient ADD is outside the declared change set',
          not set(diffs2) <= set(positions) or len(diffs2) != 23)
    # Append a spurious odd ADD from source 0 into target V; F₂ maps must diverge.
    bad3 = copy.deepcopy(cand)
    bad3['records'] = bad3['records'] + [[1, V, 0, 1, 1, 0]]
    mism = sum(1 for i in range(V) if f2_execute(parent, [1 if j == i else 0 for j in range(V)])
               != f2_execute(bad3, [1 if j == i else 0 for j in range(V)]))
    check('C appending a spurious source-to-target ADD breaks F₂ agreement',
          mism > 0, f'mismatches={mism}')


def main():
    ap = argparse.ArgumentParser()
    ap.add_argument('--repo', required=True)
    ap.add_argument('--json')
    a = ap.parse_args()
    d = load(a.repo)
    print('parent', hashlib.sha256(d['parent_raw']).hexdigest())
    print('candidate', hashlib.sha256(d['cand_raw']).hexdigest())
    run(d)
    ok = all(r[1] for r in results)
    print(('PASS' if ok else 'FAIL'), f'{sum(r[1] for r in results)}/{len(results)} checks', flush=True)
    if a.json:
        open(a.json, 'w').write(json.dumps(
            dict(head=HEAD, checks=[dict(name=n, ok=o, detail=str(x)) for n, o, x in results]), indent=1))
    sys.exit(0 if ok else 1)


if __name__ == '__main__':
    main()

James Reed (@rcfc-jreed), with substantial AI assistance (Claude, in Cursor).

[rcfc-jreed]

Independent scoped audit of #4190 signed R429 range at 4323518f: 8/8

Code-disjoint fork of VERIFY entrypoint controls.py --package. Head 4323518ffa8a8a9885bd1d81df6f3dae2dd3f6a9. TASK outcome is partial. CLAIM.

No packaging defect in SOURCES / FROZEN scope. All 7 SOURCES digests match; 25 FROZEN-SHA256.json digests match package files.

What passes: controls.py regenerates PASS.

Not covered here: Lean; new κ; merge/close; treating partial TASK outcome as a completed all-size admission.

Finite pin/seal/control replay ≠ formal proof.

James Reed (@rcfc-jreed), with substantial AI assistance (Claude, in Cursor).