FINDING / TOOLING: independent replay of 18 P104 words across 14 open PRs - all pass (no new kappa)

[rcfc-jreed]

Type: independent verification and a tooling handoff. No new kappa, no construction, and no claim about hosting, native phases, physical charts, precision or recursive cost.

Summary

p104_word_replay.py (below) is one standard-library script that replays any P104 framed scalar word in the shared JSON format.

• Input forms: either a complete {initial_frames, final_frames, program} word, or an insertion circuit applied to LOWRANK-WITNESS.json. Inputs can be files or git specs REV:PATH, so PR heads need no checkout.
• Contract: it enforces the rules all these packages state:
  • an ADD or COPY happens only when both registers sit in the stated frame, with dyadic coefficients;
  • SIGN is ±1 in frame;
  • transports are strictly nested and priced at the dimension change;
  • the private ZERO/COPY/ERASE lifetime is legal;
  • final frames match.
• Comparison: frames are compared as canonical F2 echelon bases, and register values are exact rational linear forms.
• Report: what the word actually computes, by class. This covers which registers restore, which targets are unchanged or end at y+x, the rank profile and mass, and the row l1 and denominator.

I ran it on every word-format artifact in the open P104 PRs: 18 words from 14 PRs, all passing, about 10 s in total. It builds on my code-disjoint check of #2521 (comment) and shares no code with any package's verifier.

Forward correction circuits (base: main 0fdd7d82 LOWRANK-WITNESS.json)

PR @ head	Artifact	New helpers	Added rank mass	Targets at y+x	Other targets
#2393 @ 8b3e3a22	p104-y0-source-acquisition/CIRCUIT	48	432	Y0	103 unchanged
#2496 @ f13badee	p104-y2-late-acquisition/CIRCUIT	39	351	Y2	103 unchanged
#2445 @ 6def43ad	p104-two-target-sharing/CIRCUIT	78	702	Y0, Y1	102 unchanged
#2445 @ 6def43ad	p104-two-target-sharing/SEPARATE	96	864	Y0, Y1	102 unchanged
#2460 @ a0030819	p104-third-target-collector-rank/CIRCUIT	94	846	Y0–Y2	101 unchanged
#2504 @ 9db4192b	p104-late-y2-acquisition-s34/CIRCUIT	92	828	Y0–Y2	101 unchanged
#2521 @ 78e7e4c1	p104-cross-group-collectors/CIRCUIT	90	810	Y0–Y2	101 unchanged
#2521 @ 78e7e4c1	p104-cross-group-collectors/CROSS-CONTROL	92	828	Y0–Y2	101 unchanged
#2548 @ c7a32868	p104-pooled-collectors/CIRCUIT	91	819	Y0–Y2	101 unchanged

In every row the following also hold:

• All X values, the 72 original dirty helpers and all new helpers restore exactly.
• New helpers are born in ZERO, only climb, and end at FULL.
• The maximum row l1 is 106 and the maximum denominator is 4, the same as the uncorrected channel.

Because helpers only climb from ZERO to FULL, added rank mass is always 9 × new helpers in this family. Rank-mass savings between these circuits are therefore helper savings; only the transport count and the profile shape carry extra information.

Complete words, including the inverse-transpose ("dual") words

PR @ head	Artifact	Rank mass	Endpoint
#1972 @ fd82d172	LOWRANK-WITNESS	2368	Y gets (G/2)x; all else restores
#1972 @ fd82d172	DIRTY-WITNESS	1184	Y reads Q only; Q and H restore
#2479 @ 65e58f85	p104-private-macro-dual/WORD	2368	X += −(G/2)ᵀ y
#2503 @ 6ea94fa4	p104-dual-precision/source/pr2479/WORD (vendored #2479)	2368	same
#2522 @ bd1f069a	p104-persistent-dual/WORD	2424	X += −(G/2)ᵀ y
#2497 @ 7f2cf129	p104-owned-collector-dual/DUAL	3070	X += −Aᵀ y for the two-target corrected A
#2497 @ 7f2cf129	p104-owned-collector-dual/CLEAN-DUAL	3126	same
#2549 @ bd3bea4b	p104-clean-dual-precision/WORD	3126	same
#2586 @ 7953c9a8	p104-physical-corrected-dual/WORD	3542	same

"Same" here means an exact entrywise match. A dual word's X←Y map equals −Aᵀ, where A is the X→Y map replayed from #2445's two-target forward circuit, or from the original channel for #2479, #2503 and #2522. Y, Q, G and D restore in every row, and so does N where present. This is a logical-chart statement only. #2586's physical-chart claim (conjugated charts, F^-T with Gaussian coefficients) is outside what this replay checks.

Reproduce

git fetch origin 'pull/2521/head:pr2521'   # likewise for each PR listed above
B=0fdd7d82:research/p104-native-channel/inputs/LOWRANK-WITNESS.json
python3 -B p104_word_replay.py "$B" --circuit pr2521:research/p104-cross-group-collectors/CIRCUIT.json --expect-corrected 0,1,2
python3 -B p104_word_replay.py pr2586:research/p104-physical-corrected-dual/WORD.json --json

Exit status 0 means PASS. A contract violation prints FAIL_CONTRACT <rule> <register>, and an endpoint mismatch prints FAIL_ENDPOINT. In the #2521 check, ten single-event mutations (signs, a dropped compensation or inverse, an undercharged transport, a same-dimension wrong frame, an original-helper read, and moved late captures) were all rejected by the same rules. Authors of new P104 words can run it as a quick second opinion before opening a PR.

p104_word_replay.py

#!/usr/bin/env python3
"""Replay a P104 framed scalar word and report its contract, endpoint and transport invoice.

Accepts either a complete word ({initial_frames, final_frames, program}) or an insertion
circuit ({initial_frames, final_frames, insertions}) applied to a base word. Each input is a
file path or a git object spec REV:PATH (read with `git show`, so pinned PR heads need no
checkout).

Semantics (shared by the P104 channel packages):
  * a register holds an exact rational linear form in the initial values of all registers;
  * a frame is the F2 span of 9-bit masks; frames are compared in reduced echelon form;
  * add(dst, src, c, F): dst += c*src, with dst != src, both registers in frame F, c dyadic;
  * sign(r, c, F): r *= c, c in {1, -1}, r in frame F;
  * transport(r, A, B, k): r in A; A and B strictly nested; k = |dim B - dim A|; value unchanged;
  * zero(C, F) / copy(C, src, F) / erase(C, F): private-copy lifetime of register C;
  * an insertion block with completed_cut k runs after the first k base events.
Every violated rule aborts with exit status 1. The report states what the word computes; it
does not decide which endpoint a package intended unless --expect-corrected is given.

Standard library only. James Reed (@rcfc-jreed), with substantial AI assistance (Claude, in
Cursor). Apache-2.0.
"""
import argparse, hashlib, json, subprocess, sys
from collections import Counter
from fractions import Fraction as Q
from pathlib import Path

DIM = 9


class ContractError(Exception):
    pass


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


def read(spec):
    path = Path(spec)
    if path.exists():
        data = path.read_bytes()
    else:
        need(':' in spec, f'not a file or REV:PATH spec: {spec}')
        proc = subprocess.run(['git', 'show', spec], capture_output=True)
        need(proc.returncode == 0, f'git show failed for {spec}: {proc.stderr.decode().strip()}')
        data = proc.stdout
    blob = hashlib.sha1(b'blob %d\0' % len(data) + data).hexdigest()
    return json.loads(data), blob, hashlib.sha256(data).hexdigest()


def rref(masks):
    """Canonical reduced echelon basis of the F2 span of masks (descending pivots)."""
    basis = []
    for v in masks:
        v = int(v)
        need(0 <= v < 1 << DIM, f'frame vector out of range: {v}')
        for b in basis:
            if v >> (b.bit_length() - 1) & 1:
                v ^= b
        if v:
            p = v.bit_length() - 1
            basis = [b ^ v if b >> p & 1 else b for b in basis] + [v]
    return tuple(sorted(basis, reverse=True))


def nested(a, b):
    return rref(a + b) in (a, b)


def dyadic(c):
    return c != 0 and c.denominator & (c.denominator - 1) == 0


def schedule(word, circuit):
    """Yield (event, inserted) in chronological order."""
    base = word['program']
    blocks = {}
    for block in (circuit or {}).get('insertions', []):
        cut = block['completed_cut']
        need(type(cut) is int and 0 <= cut <= len(base), f'insertion cut out of range: {cut}')
        need(cut not in blocks, f'duplicate insertion cut {cut}')
        blocks[cut] = block['events']
    for cut in range(len(base) + 1):
        for e in blocks.get(cut, []):
            yield e, True
        if cut < len(base):
            yield base[cut], False


def replay(word, circuit=None):
    new = dict(circuit['initial_frames']) if circuit else {}
    need(not set(new) & set(word['initial_frames']), 'inserted register name collides with base register')
    init = {**word['initial_frames'], **new}
    final = {**word['final_frames'], **(circuit['final_frames'] if circuit else {})}
    frame = {r: rref(f) for r, f in init.items()}
    rows = {r: {r: Q(1)} for r in init}
    stats = dict(events=Counter(), inserted_events=Counter(), profile=Counter(), inserted_profile=Counter(),
                 l1=Q(1), denominator=1, climbs_only=set(new))
    for e, inserted in schedule(word, circuit):
        op = e[0]
        (stats['inserted_events'] if inserted else stats['events'])[op] += 1
        if op == 'add':
            _, dst, src, c, f = e
            c = Q(c)
            need(dst != src and dst in rows and src in rows, f'add roles {e[:3]}')
            need(frame[dst] == frame[src] == rref(f), f'add frame {e[:3]}')
            need(dyadic(c), f'add coefficient not dyadic {e[:4]}')
            for k, v in rows[src].items():
                w = rows[dst].get(k, 0) + c * v
                if w:
                    rows[dst][k] = w
                else:
                    rows[dst].pop(k, None)
            stats['l1'] = max(stats['l1'], sum(map(abs, rows[dst].values())))
            stats['denominator'] = max([stats['denominator']] + [v.denominator for v in rows[dst].values()])
        elif op == 'sign':
            _, r, c, f = e
            need(r in rows and Q(c) in (1, -1) and frame[r] == rref(f), f'sign {e[:3]}')
            rows[r] = {k: Q(c) * v for k, v in rows[r].items()}
        elif op == 'transport':
            _, r, a, b, k = e
            a, b = rref(a), rref(b)
            need(r in rows and frame[r] == a, f'transport entrance {r}')
            need(a != b and nested(a, b), f'transport frames not strictly nested {r}')
            need(type(k) is int and k == abs(len(b) - len(a)), f'transport price {r}')
            (stats['inserted_profile'] if inserted else stats['profile'])[k] += 1
            if len(b) < len(a):
                stats['climbs_only'].discard(r)
            frame[r] = b
        elif op == 'zero':
            need(e[1] not in rows, f'zero of live register {e[1]}')
            rows[e[1]], frame[e[1]] = {}, rref(e[2])
        elif op == 'copy':
            _, dst, src, f = e
            need(rows.get(dst) == {} and src in rows, f'copy roles {e[:3]}')
            need(frame[dst] == frame[src] == rref(f), f'copy frame {e[:3]}')
            rows[dst] = dict(rows[src])
        elif op == 'erase':
            need(e[1] in rows and e[1] not in init and frame[e[1]] == rref(e[2]), f'erase {e[1]}')
            del rows[e[1]], frame[e[1]]
        else:
            raise ContractError(f'unknown operation {op!r}')
    need(set(rows) == set(final), f'live registers at the end differ from final_frames: '
                                  f'{sorted(set(rows) ^ set(final))[:6]}')
    for r in rows:
        need(frame[r] == rref(final[r]), f'final frame {r}')
    return rows, frame, stats, new


def cls(r):
    return r.rstrip('0123456789')


def summarize(rows, frame, stats, new, init_names):
    changed = sorted((r for r in rows if rows[r] != {r: 1}), key=lambda r: (cls(r), len(r), r))
    restored = Counter(cls(r) for r in rows if rows[r] == {r: 1})
    reads = Counter()
    for r in changed:
        for k in rows[r]:
            if k != r:
                reads[f'{cls(r)}<-{cls(k)}'] += 1
    mass = lambda p: sum(k * n for k, n in p.items())
    return {
        'registers': dict(Counter(cls(r) for r in init_names)),
        'inserted_registers': len(new),
        'events': dict(stats['events']), 'inserted_events': dict(stats['inserted_events']),
        'transport_profile': dict(sorted(stats['profile'].items())),
        'rank_mass': mass(stats['profile']),
        'inserted_transport_profile': dict(sorted(stats['inserted_profile'].items())),
        'inserted_rank_mass': mass(stats['inserted_profile']),
        'inserted_registers_born_zero_end_full_climbing': (
            all(frame[r] and len(frame[r]) == DIM for r in new) and stats['climbs_only'] == set(new)) if new else None,
        'restored_by_class': dict(restored),
        'changed_registers': len(changed),
        'changed_by_class': dict(Counter(cls(r) for r in changed)),
        'endpoint_dependencies': dict(reads),
        'max_row_l1': str(stats['l1']), 'max_denominator': stats['denominator'],
    }


def main(argv=None):
    ap = argparse.ArgumentParser(description=__doc__.split('\n')[0])
    ap.add_argument('word', help='complete word, or the base word when --circuit is given (file or REV:PATH)')
    ap.add_argument('--circuit', help='insertion circuit applied to WORD (file or REV:PATH)')
    ap.add_argument('--reference', help='complete word whose endpoint is compared target by target '
                                        '(default: WORD itself when --circuit is given)')
    ap.add_argument('--expect-corrected', default='', help='comma-separated target indices that must end at y+x')
    ap.add_argument('--json', action='store_true', help='print the full report as JSON')
    args = ap.parse_args(argv)

    word, wblob, wsha = read(args.word)
    circuit = cblob = csha = None
    if args.circuit:
        circuit, cblob, csha = read(args.circuit)
    report = {'word': args.word, 'word_git_blob': wblob, 'word_sha256': wsha}
    if circuit:
        report.update(circuit=args.circuit, circuit_git_blob=cblob, circuit_sha256=csha)
    try:
        rows, frame, stats, new = replay(word, circuit)
    except ContractError as ex:
        report['status'] = 'FAIL_CONTRACT'
        report['violation'] = str(ex)
        print(json.dumps(report, indent=1) if args.json else f"FAIL_CONTRACT {ex}")
        return 1
    init_names = list(word['initial_frames']) + list(new)
    report.update(summarize(rows, frame, stats, new, init_names))

    ref_spec = args.reference or (args.word if circuit else None)
    failures = []
    if ref_spec:
        ref_word = word if ref_spec == args.word else read(ref_spec)[0]
        ref_rows = replay(ref_word)[0]
        targets = sorted((r for r in rows if r.startswith('Y') and r[1:].isdigit()), key=lambda r: int(r[1:]))
        same = [t for t in targets if rows[t] == ref_rows.get(t)]
        plus_x = [t for t in targets if rows[t] == {t: 1, 'X' + t[1:]: 1}]
        report['targets_equal_reference'] = len(same)
        report['targets_y_plus_x'] = [int(t[1:]) for t in plus_x]
        report['targets_other'] = [int(t[1:]) for t in targets if t not in same and t not in plus_x]
        if report['targets_other']:
            failures.append('targets neither unchanged nor y+x')
    if args.expect_corrected:
        want = sorted(int(x) for x in args.expect_corrected.split(','))
        if report.get('targets_y_plus_x') != want:
            failures.append(f'expected y+x exactly on {want}')
    if any(rows[r] != {r: 1} for r in new):
        failures.append('inserted helpers not restored')
    report['status'] = 'PASS' if not failures else 'FAIL_ENDPOINT'
    if failures:
        report['failures'] = failures
    if args.json:
        print(json.dumps(report, indent=1))
    else:
        keys = ('registers', 'inserted_registers', 'events', 'inserted_events', 'rank_mass', 'inserted_rank_mass',
                'inserted_transport_profile', 'inserted_registers_born_zero_end_full_climbing', 'restored_by_class',
                'changed_by_class', 'endpoint_dependencies', 'targets_equal_reference', 'targets_y_plus_x',
                'targets_other', 'max_row_l1', 'max_denominator', 'failures')
        for k in keys:
            if k in report and report[k] not in (None, {}, []):
                print(f'{k}: {report[k]}')
        print(report['status'])
    return 0 if report['status'] == 'PASS' else 1


if __name__ == '__main__':
    sys.exit(main())

Credit: the word format, channel and circuits belong to their authors: Rohan Arun / #1972, ywz65 / #2460, #2479, #2496, #2497, #2503, #2521, #2522 and #2586, Ross Richardson / #2445, CubeJerry / #2504, commdata2338 / #2393, and Nick Petalas / #2548 and #2549, plus the P104 lineage they credit. This replay re-implements the stated semantics independently and imports none of their code.

Prepared by James Reed (@rcfc-jreed) with substantial AI assistance (Claude, in Cursor). It is not a formal proof, and no human independent review is claimed.