[RossRichardson]

Summary

Prove a sharp repair count for the inherited BIT bank recipe: with 2B arbitrary public banks, the fixed word needs exactly 2B+1 allowed repair calls for odd B and 2B−1 for even B. Explicit rank-one idempotent decompositions attain the bound, including any finite number of restored dirty spectators.

For a separate mixed coded/clean local alphabet on the same recipe, move the correction to the terminal cut and reduce six source-code applications to two. A written all-B identity and a restricted determinant lower bound match that count. At the assigned 1,499-ADD code size this saves 5,996 scalar ADDs. See research/bit-fixed-controller-repairs/README.md and its two proof notes.

Scope and limits

The sharp repair theorem fixes every original local call, bridge and exchange; its added calls are scalar-conjugated single-bank applications of one common nonidentity involution. It is not an unrestricted caller lower bound. The two-code optimum separately fixes the coded first pair and the single-bank generator alphabet.

The hybrid's two 111-port normalization sweeps remain, and its conditional comparison with the all-clean word still loses 102 rank units. The actual early-promotion route witness rejects one free native-code admission. Logical algebra does not supply mixed helper ownership, physical frames, source access or rounding. No 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 package inputs.
• Separate mathematical and verification reviews, with findings resolved.
• Automatic hosted package CI passed on b512fd71e9eb5711d24abaa35978660eeb87f363.

The package replays three complete historical receipts and two independent implementations. Checks include the all-B formula and attaining-repair fixtures, arbitrary dirty spectator instantiations, ordered free-group-ring inverse/dual identities, an explicit binary VALUE fiber witness and normal/optimized acceptance controls. The universal results are written proofs; finite fixtures and AI review are not formal-kernel proofs.

Sources and credit

Retains the DreamingOfClouds/eumemic/Zhihao Chen/chafreaky bank-recipe lineage and source notices, Ali Romman's R438/source-code ancestry, and Sagar Thakrar's transport/rehosting. #3645 supplies the coded local interface; #4039 supplies distinct FULL-target/seeded-caller context and is not republished. #4185 supplies the separate returned-owner comparison. Exact source pins and differing related alphabets are recorded in the package manifests.

Original findings, new all-parameter proofs and two-code construction, independent checking contexts and publication were prepared by Ross Richardson with substantial OpenAI Codex assistance. Apache-2.0.

[rcfc-jreed]

Independent scoped audit of fixed BIT repairs / two-code hybrid at b512fd71: no defect found in the finite tariff / invoice layer

Code-disjoint reimplementation over pinned receipts; does not import package verify.py / controls.py / frozen review checkers. CLAIM.

What passes (29 of 29):

1. Pins. SOURCES.base is 12fa8c5c. Recipe SHA 6368196a… agrees across recipe / hybrid / CHECKS. FROZEN-SHA256 matches review CHECKS. CONTROLS no_new_kappa; small hybrid word replayed. VALIDATION receipts byte-identical.
2. Sharp repair tariff. Written k(B)=2B+1 (odd) / 2B−1 (even). All twelve certificates B=1..12 match k(B), rank_M(B), rank_A=2B, trace_M=1, odd parity. B=4 → 7 repairs. Historical nilpotent cases agree. formal_kernel_proof=false.
3. Two-code hybrid. Historical 6 code apps / 9216 ADDs → new 2 / 3220; save 5996. Net vs all-clean −102 (=2·60−222). Lower bound minimum 2 attained. 14+14 fixtures keep those code counts and −102. Coded stages [0,1], clean 2..8. Early-promotion counterexample PASS.

Not covered: all-B theorem as formal-kernel proof; native B=1 instance; supplier / κ (package correctly claims none).

This is a finite replay of committed receipts, not a formal proof.

check_4194.py

#!/usr/bin/env python3
"""Independent finite controls for PR4194 (BIT fixed repairs / two-code hybrid).

Recomputes the sharp repair tariff k(B) on the twelve finite B certificates and
the hybrid 6→2 code / 5996-ADD invoice identities from pinned review receipts.
Does not import package verify.py / controls.py / frozen review checkers.

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

HEAD = 'b512fd71e9eb5711d24abaa35978660eeb87f363'
BASE = '12fa8c5c844be21bfefb38a19503fbd867a11244'
PKG = 'research/bit-fixed-controller-repairs/'
RECIPE_SHA = '6368196a393ac25bb2918880e4c4bd31ed733b762c27b6873ab391cbc0c5c3c8'
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 k_of(B):
    return 2 * B + 1 if B % 2 else 2 * B - 1


def rank_M_of(B):
    return 2 * B if B % 2 else 2 * B - 1


def load(repo):
    g = lambda p: show(repo, PKG + p)
    return dict(
        sources=js(g('SOURCES.json')),
        core=js(g('CORE-SNAPSHOT.json')),
        controls=js(g('CONTROLS.json')),
        frozen=js(g('FROZEN-SHA256.json')),
        recipe=js(g('frozen/recipe/BIT-NILPOTENT-RECIPE.json')),
        hybrid=js(g('frozen/hybrid/CLOSED-HYBRID.json')),
        early=js(g('frozen/hybrid/EARLY-PROMOTION.json')),
        recipe_checks=js(g('frozen/reviews/recipe/CHECKS.json.gz')),
        hybrid_checks=js(g('frozen/reviews/hybrid/CHECKS.json.gz')),
        recipe_val=js(g('frozen/reviews/recipe/VALIDATION.json')),
        hybrid_val=js(g('frozen/reviews/hybrid/VALIDATION.json')),
    )


def run(d, repo):
    rc, hc = d['recipe_checks'], d['hybrid_checks']

    check('I1 SOURCES base pin is canonical main', d['sources']['base_commit'] == BASE)
    check('I2 CORE status PASS_B07_REVIEWED_CORE', d['core']['status'] == 'PASS_B07_REVIEWED_CORE')
    check('I3 CONTROLS status PASS_B07_…; no_new_kappa; small hybrid word replayed',
          d['controls']['status'] == 'PASS_B07_COMPACT_SOURCE_AND_MATHEMATICAL_GATES'
          and d['controls']['no_new_kappa'] is True
          and d['controls']['small_fixed_hybrid_word_replayed'] is True)
    check('I4 recipe CHECKS status PASS_FIXED_RECIPE_ALL_B_PROOF_CERTIFICATES',
          rc['status'] == 'PASS_FIXED_RECIPE_ALL_B_PROOF_CERTIFICATES')
    check('I5 hybrid CHECKS status PASS_ALL_B_PROOF_FIXTURES_TWO_CODE_HYBRID…',
          hc['status'] == 'PASS_ALL_B_PROOF_FIXTURES_TWO_CODE_HYBRID_AND_SELECTED_NATIVE_WITNESS')
    check('I6 recipe/hybrid VALIDATION receipts byte-identical in both modes',
          d['recipe_val']['receipts_byte_identical'] is True
          and d['hybrid_val']['full_receipt_byte_identical'] is True)
    check('I7 recipe source SHA matches BIT-NILPOTENT-RECIPE pin',
          d['recipe']['source_recipe_sha256'] == RECIPE_SHA
          and rc['source_hashes']['recipe'] == RECIPE_SHA
          and d['hybrid']['recipe_source_sha256'] == RECIPE_SHA)
    check('I8 FROZEN-SHA256 matches HEAD for recipe + hybrid CHECKS',
          d['frozen']['frozen/reviews/recipe/CHECKS.json.gz']
          == hashlib.sha256(show(repo, PKG + 'frozen/reviews/recipe/CHECKS.json.gz')).hexdigest()
          and d['frozen']['frozen/reviews/hybrid/CHECKS.json.gz']
          == hashlib.sha256(show(repo, PKG + 'frozen/reviews/hybrid/CHECKS.json.gz')).hexdigest())

    # --- Sharp repair tariff ---
    check('R1 written theorem states k(B)=2B+1 odd / 2B−1 even',
          rc['all_parameter_written_theorem']
          == 'k(B)=2B+1 for odd B; k(B)=2B-1 for even B')
    check('R2 twelve finite B cases covering B=1..12',
          len(rc['cases']) == 12
          and [c['B'] for c in rc['cases']] == list(range(1, 13)))
    bad = []
    for c in rc['cases']:
        B = c['B']
        if c['minimum_repair_calls'] != k_of(B):
            bad.append(('k', B, c['minimum_repair_calls'], k_of(B)))
        if c['rank_M'] != rank_M_of(B):
            bad.append(('rank_M', B, c['rank_M'], rank_M_of(B)))
        if c['trace_M'] != 1:
            bad.append(('trace', B, c['trace_M']))
        if c['rank_A'] != 2 * B:
            bad.append(('rank_A', B, c['rank_A']))
        # Odd call count forced by trace
        if c['minimum_repair_calls'] % 2 == 0:
            bad.append(('parity', B))
        # Rank floor: k >= rank_M; for odd B equality; for even B k = rank_M (both 2B-1)
        if c['minimum_repair_calls'] < c['rank_M']:
            bad.append(('floor', B))
    check('R3 every B=1..12: k(B), rank_M(B), rank_A=2B, trace_M=1, odd k',
          not bad, bad[:6])
    check('R4 B=4 certificate is seven repairs (111×7=777 conditional native children)',
          next(c['minimum_repair_calls'] for c in rc['cases'] if c['B'] == 4) == 7)
    # Historical recipe cases in BIT-NILPOTENT-RECIPE.json (6 cases) agree for B=1..4 at least
    hist = d['recipe']['cases']
    hist_bad = []
    for c in hist:
        B = c['B']
        if c['rank_defect_M'] != rank_M_of(B) or c['trace_defect'] != 1:
            hist_bad.append(c)
    check('R5 BIT-NILPOTENT-RECIPE historical cases match rank_M/trace formulas',
          not hist_bad and d['recipe']['status'] == 'PASS_FIXED_RECIPE_NILPOTENT_DEFECT_MATRICES',
          hist_bad)
    check('R6 formal_kernel_proof is False (finite certificates only)',
          rc['formal_kernel_proof'] is False
          and d['recipe_val']['formal_kernel_proof'] is False)
    check('R7 finite coverage: B∈[1,12], spectator_counts include 0/1/3',
          rc['finite_coverage']['B'] == [1, 12]
          and rc['finite_coverage']['spectator_counts'] == [0, 1, 3])

    # --- Hybrid two-code invoice ---
    inv = hc['invoice']
    check('H1 historical 6 code apps / 9216 ADDs → new 2 / 3220; save 5996',
          inv['historical_code_occurrences'] == 6
          and inv['new_code_occurrences'] == 2
          and inv['historical_scalar_ADDs'] == 9216
          and inv['new_scalar_ADDs'] == 3220
          and inv['scalar_ADDs_saved'] == 5996 == 9216 - 3220)
    check('H2 conditional net rank saving vs all-clean is −102 (=2·60−222)',
          inv['conditional_net_rank_saving_vs_allclean'] == -102 == 2 * 60 - 222
          and inv['normalization_rank_one_children'] == 222)
    check('H3 two_code_lower_bound minimum added generator occurrences is 2 (attained)',
          hc['two_code_lower_bound']['minimum_added_single_bank_generator_occurrences'] == 2
          and hc['two_code_lower_bound']['attained_added_exponents'] == [-1, 1])
    # Spot-check finite bank fixtures: every two_code variant has 2 codes; historical has 6
    tc = [c for c in hc['cases'] if c.get('variant') == 'two_code']
    hist_c = [c for c in hc['cases'] if c.get('variant') == 'historical']
    check('H4 all two_code fixtures use 2 code occurrences; historical use 6',
          len(tc) > 0 and all(c['added_code_occurrences'] == 2 for c in tc)
          and len(hist_c) > 0 and all(c['added_code_occurrences'] == 6 for c in hist_c),
          {'two_code': len(tc), 'historical': len(hist_c)})
    check('H5 every fixture keeps net_rank_mass_saved_vs_allclean == −102',
          all(c['net_rank_mass_saved_vs_allclean'] == -102 for c in hc['cases']))
    check('H6 finite_bank_counts include 1..12,16,32',
          hc['finite_bank_counts'] == [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 16, 32])
    check('H7 CLOSED-HYBRID status PASS_CLOSED_NONCOMMUTATIVE_HYBRID_NO_GAIN',
          d['hybrid']['status'] == 'PASS_CLOSED_NONCOMMUTATIVE_HYBRID_NO_GAIN')
    check('H8 CLOSED-HYBRID local_coded=[0,1], local_clean=2..8',
          d['hybrid']['local_coded_stages'] == [0, 1]
          and d['hybrid']['local_clean_stages'] == [2, 3, 4, 5, 6, 7, 8])
    # Historical invoice on CLOSED-HYBRID still records 6 (the old word); new count is in CHECKS
    check('H9 CLOSED-HYBRID invoice records historical 6 source apps (baseline word)',
          d['hybrid']['invoice_per_replica']['source_code_applications'] == 6)
    check('H10 EARLY-PROMOTION status PASS…LOSES_FUTURE_CODE_ADMISSION',
          d['early']['status'] == 'PASS_ACTUAL_EARLY_PROMOTION_LOSES_FUTURE_CODE_ADMISSION')

    # --- Negative controls ---
    check('NEG1 even B=4 with k=8 would violate trace-odd requirement',
          k_of(4) == 7 and 8 % 2 == 0)
    check('NEG2 claiming ADD save without 9216−3220 breaks 5996',
          9216 - 3000 != 5996)
    check('NEG3 odd B=3 with k=2B−1=5 undercounts true 7',
          k_of(3) == 7 != 5)

    failed = [name for name, ok, _ in results if not ok]
    print(f'\n{len(results) - len(failed)}/{len(results)} PASS', flush=True)
    if failed:
        print('FAILED:', ', '.join(failed), flush=True)
        return 1
    return 0


def main():
    ap = argparse.ArgumentParser()
    ap.add_argument('--repo', required=True)
    args = ap.parse_args()
    head = subprocess.run(['git', '-C', args.repo, 'rev-parse', 'HEAD'],
                          capture_output=True, text=True, check=True).stdout.strip()
    check('HEAD is PR4194 tip b512fd71…', head == HEAD, head)
    return run(load(args.repo), args.repo)


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

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

[rcfc-jreed]

Independent scoped audit of #4194 BIT fixed repairs / hybrid controller at b512fd71: 9/9

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

No packaging defect in SOURCES / FROZEN scope. All 9 SOURCES digests match; 22 FROZEN-SHA256.json digests match; SOURCE-CLOSURE PASS.

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