[aliromman]

This conditional construction raises the ordinary BIT saving from 0.0034363538396 to 0.0034441226396 at matched compiler and cover parameters, and admits the strict endpoint 0.00344412. It does not raise the complete multiplication κ: the complex supplier still binds. The current selected κ remains 0.003027288235; no selected file changes.

The proof, exact receipt, emitted word, and source pins are fixed at the reviewed head.

Nine initial helper relations make all nine COPY values in the reverse PR589 word zero. Each local call removes nine H1 jobs and nine H7 jobs, with all nine H8 helper targets debited. All 652 retained inputs remain independent. The ten owned fields accept arbitrary entry data and finish at zero. An exact physical involution, including each port's address maps, permits the reverse word at all eighteen full controller calls.

The complete p16/a7 invoice changes by −162 H1 −162 H7 paid jobs and −162 H8 targets. It has 57,231 paid jobs and 11,292 productive fields; the rank surplus remains 753. The raw moment crossing is strictly between 0.003472070044 and 0.003472070045. The same compiler gaps, cover loss and atom fraction give the matched ordinary gain 0.0000077688. All 1,568 added pointwise records per call are charged; the complete raw nonrecursive allowance is 19,170,192, below 10^9.

The branch starts at main d277c97824e50782da6adbc486ca3c76c8fc687e. All thirteen consumed inputs remain byte-identical on submission main 1a3ced60b2f7a46bc70280a04f2eeb8ca027c700. The source record in SOURCES.json is historical provenance. This work follows the scoped claim and does not take the active coupled complex caller.

Verification and limits

CPython 3.12.14, standard library only:

python3.12 -B scripts/research_package.py --package research/bit-nine-owned-relations
python3.12 -O -B research/bit-nine-owned-relations/verify.py

Expected scientific result:

PASS_BIT_NINE_OWNED_RELATIONS_00344412_NO_NEW_MULTIPLICATION_KAPPA

Normal and optimized direct replays pass. The checks rebuild the relations and word; verify all symbolic rows and all 662 separate Boolean input columns; check rational projectors and 111 fresh port charts; replay the literal controller; and verify both complete invoices, two exact moment engines, the compiler tail, cover loss, ordinary conversion and unchanged outer arithmetic. Semantic controls reject missing entry/exit clears, a changed relation, an unearned zero move, missing target debit and the old word at the new saving. A changed external source is also rejected with assertions disabled.

The committed-byte check and official 23-file export pass. Both direct modes pass in the read-only Git-free export, preserving all 24 files including the export receipt. The registered runner passes both declared commands and all metadata/source checks. The hosted planning job failed CurrentCiNavigationTests.test_current_ci_section_matches_selected_record: the current CI guide still names make frontier4610-verify, while the selected record names make frontier5413-verify. The same failure is reproduced from byte-exact main 1a3ced60b2f7a46bc70280a04f2eeb8ca027c700 inputs. Hosted package replay was skipped. The local scientific and export checks above pass; no hosted scientific pass is claimed.

Native all-column, owned-erasure, compiler, precision/tape and analytic-recovery premises remain conditional. The delayed-cover bridge supplies the inherited common-weight interface. The full GL cover, winning uniform word and complete multiplier are not materialized. No Lean, proof-kernel check, optional full-history audit or independent replay of the consumed complex construction was run. This is a BIT component improvement, not a global optimum or a new multiplication bound.

Credit

@DreamingOfClouds supplied the retained two-transport word in PR #589. @eumemic supplied the punctured 111-port/439-helper construction in PR #555, with the earlier word and port lineage credited there. Cinna Davis, @1337isnot1337, supplied the query-thinned controller and native proof and the cover bridge. The compiler source retains @zxv and the mixed-target recursion of Jacob Alan Sussman. Contributor evidence records these identities and source roles.

Ali Romman's PR #5383 supplies the prior owned-helper method. PR #5398 supplies the unchanged complex comparison and its outer receipt; only its outer arithmetic is rerun here. All predecessor notices remain unchanged. Prepared by Ali Romman with substantial OpenAI Codex assistance; no subagents. New work is Apache-2.0.

[Matarener]

Independent check of the BIT component claim (no new κ; corroboration, not maintainer acceptance).

At PR head 295b00764305694b3c510d3b0bebc2ab024a7809, on Python 3.12.

1. Author replay. scripts/research_package.py --package research/bit-nine-owned-relations passes in normal and -O mode (PASS_BIT_NINE_OWNED_RELATIONS_00344412_NO_NEW_MULTIPLICATION_KAPPA).
2. Separately written checker (below, standard library, imports nothing from this package, ~4 s):

   • Own GF(2) replay of the emitted WORD.json.gz.

     • All 652 retained columns end at (X,Y)->(X,Y+X) or the identity.
     • All 10 owned fields end at zero from arbitrary entry values.
     • Every XOR is in a common frame, and the 9 ZERO_MOVEs act on zero values.
     • Exit frames equal the source start frames.

   • Structural diff against the reversed PR589 records (249-records.bin). The emitted word is the source with exactly these changes:

     • a relation prologue on pivots 222, 223, 224, 225, 226, 228, 230, 231 and 233 (1,559 events);
     • 9 COPY entries and 9 COPY exits turned into centre CLEARs;
     • 9 rank-1 MOVEs turned into ZERO_MOVEs;
     • 9 exit CLEARs.

     Nothing else differs.

   • Local paid profile. Old {1:1323,2:1342,3:79,4:44,5:102,6:11,7:19}, new {1:1314,…,7:10}.

   • Invoice recomputed from BIT-CONTROLLER.json.

     • 18 FULL calls, 15 thin queries, IDLE events and diagonal targets.
     • 57,231 paid and 11,292 targets; masses 215,457 / 216,210; surplus 753.
     • Δpaid {1:-162, 7:-162}, Δtargets {8:-162}.

   • Raw moment crossing by 60-digit decimal bisection.

     • New root 0.00347207004489…, old root 0.00346424897202….
     • Margin +1.92e-7 at 0.003472070044 and −2.31e-8 at 0.003472070045.

   • Ordinary BIT arithmetic. 0.996·0.0034578 + 0.004·0.0000384599 = 0.0034441226396; old at the same chain 0.0034363538396; gain 0.0000077688.

Not independently checked: the compiler ratios (α, γ, δ, H0/H1), the rational projectors and port routes, the all-f / delayed-cover argument and the 54+4 outer predicates. These were covered only by the author's verifier.

Minor wording point: the old and new tested savings sit 4.249e-6 and 4.270e-6 below their roots. "Matched parameters" therefore means the same rounding rule, uniform gap and cover loss, not an identical root gap. This does not affect the stated gain.

independent.py (run from any folder; set ROOT to a checkout of this PR head)

"""Independent check of PR #5421 (Ali Romman): BIT saving 0.00344412 from nine owned helper relations.

Mark (Matarener), with Claude Code assistance. Standard library only; imports nothing from the PR.
Reads, inside the PR worktree D:/Math/imb-5421:
  research/bit-nine-owned-relations/WORD.json.gz       (emitted local word)
  research/bit-nine-owned-relations/RESULT.json        (claimed numbers, compared at the end)
  research/kappa-rebuild/bit/sources/pr589-regenerated/ (source word, records, frames)
  research/query-thinned-controllers/BIT-CONTROLLER.json
Checks
  L1 own GF(2) replay of the emitted word: every one of the 652 retained columns ends at its
     logical endpoint (X,Y)->(X,Y+X), helpers identity; all 10 owned fields end at zero from
     arbitrary entry values; same-frame XORs; ZERO_MOVE only on zero values; exit frames = start.
  L2 the emitted word is the reversed source word with exactly: a relation prologue, the nine
     COPY entries/exits replaced by centre CLEARs, nine rank-1 MOVEs replaced by ZERO_MOVEs,
     and an exit epilogue; nothing else changed.
  L3 local paid profiles old/new counted from the source records and from the emitted word.
  I  own controller invoice (18 FULL, 15 thin queries, IDLE, diagonal targets) for old and new.
  M  raw moment crossing with 60-digit decimal arithmetic and the ordinary-BIT arithmetic.
"""
import gzip, json, struct, sys, time
from collections import Counter
from decimal import Decimal as D, getcontext
from fractions import Fraction as F
from pathlib import Path

getcontext().prec = 60
ROOT = Path('D:/Math/imb-5421')
PKG = ROOT / 'research/bit-nine-owned-relations'
SRC = ROOT / 'research/kappa-rebuild/bit/sources/pr589-regenerated'
SIZE, PORTS = 661, 111
OUT = Path(__file__).with_name('independent_result.json')


def need(ok, why):
    if not ok:
        raise SystemExit('FAIL: ' + why)
    return True


def log(*a):
    print(time.strftime('%H:%M:%S'), *a, flush=True)


def main():
    res = {}
    word = json.loads(gzip.decompress((SRC / 'WORD.json.gz').read_bytes()))
    recs = list(struct.iter_unpack('<6i', (SRC / 'records/249-records.bin').read_bytes()))
    emitted = json.loads(gzip.decompress((PKG / 'WORD.json.gz').read_bytes()))
    prog, owned = emitted['program'], set(emitted['owned'])
    log('source records', len(recs), 'emitted events', len(prog), 'owned', sorted(owned))

    # ---- L3 old local profile from the source records (reverse order is the BIT word used)
    old = Counter()
    for op, x, y, a, b, _ in recs:
        if op == 0 and b:
            old[b] += 1
        elif op == 3:
            old[7] += 1          # COPY entry into the centre is a paid rank-7 job
    res['old_local_paid'] = dict(sorted(old.items()))
    log('old local paid', res['old_local_paid'])

    # ---- L1 own GF(2) replay of the emitted word, arbitrary owned entries
    rows = [1 << i for i in range(SIZE + 1)]
    frames = list(word['final']) + [None]
    new = Counter(); zero_moves = 0; xors = 0
    for e in prog:
        op = e[0]
        if op == 'CLEAR':
            need(e[1] in owned, 'CLEAR of a non-owned field %r' % e)
            rows[e[1]] = 0; frames[e[1]] = e[2]
        elif op == 'ADD':
            _, d, s, fr = e
            need(d != s and frames[d] == frames[s] == fr, 'ADD frames %r' % e)
            rows[d] ^= rows[s]; xors += 1
        elif op == 'MOVE':
            _, r, a, b, rank = e
            need(frames[r] == a, 'MOVE entrance %r' % e)
            if rank:
                new[rank] += 1
            frames[r] = b
        elif op == 'ZERO_MOVE':
            _, r, a, b = e
            need(frames[r] == a and rows[r] == 0, 'ZERO_MOVE on a nonzero value %r' % e)
            frames[r] = b; zero_moves += 1
        else:
            need(False, 'unknown op %r' % e)
    bad = []
    for i, row in enumerate(rows):
        want = 0 if i in owned else (1 << i) ^ ((1 << (i - PORTS)) if PORTS <= i < 2 * PORTS else 0)
        if row != want:
            bad.append(i)
    need(not bad, 'endpoint columns differ: %r' % bad[:10])
    need(frames[:SIZE] == word['start'] and frames[SIZE] is None, 'exit frames')
    res['new_local_paid'] = dict(sorted(new.items()))
    res['L1'] = {'retained_columns_checked': SIZE - (len(owned) - 1), 'owned_zero_at_exit': len(owned),
                 'xor_records': xors, 'zero_moves': zero_moves}
    log('L1 pass', res['L1'], 'new local paid', res['new_local_paid'])
    delta = Counter(new); delta.subtract(old)
    delta = {k: v for k, v in delta.items() if v}
    need(delta == {1: -9, 7: -9}, 'local paid delta %r' % delta)

    # ---- L2 structural diff against the reversed source records
    srev = list(reversed(recs))
    # strip the prologue (centre CLEAR, then per pivot CLEAR + ADDs) and the epilogue (pivot CLEARs)
    k = 0
    need(prog[0] == ['CLEAR', SIZE, None], 'prologue starts with the centre clear'); k = 1
    pivots = []
    while prog[k][0] == 'CLEAR' and prog[k][1] in owned and prog[k][1] != SIZE:
        piv = prog[k][1]; pivots.append(piv); k += 1
        while prog[k][0] == 'ADD' and prog[k][1] == piv:
            k += 1
    tail = len(prog)
    while prog[tail - 1][0] == 'CLEAR' and prog[tail - 1][1] in owned and prog[tail - 1][1] != SIZE:
        tail -= 1
    body = prog[k:tail]
    need(sorted(pivots) == sorted(owned - {SIZE}) and len(prog) - tail == 9, 'nine relation pivots and nine exit clears')
    j = 0; changed = Counter()
    for op, x, y, a, b, _ in srev:
        if op == 0:
            e = body[j]; j += 1
            if e[0] == 'MOVE':
                need(e[1:] == [x, a, y, b], 'MOVE kept %r vs %r' % (e, (x, a, y, b)))
            else:
                need(e[0] == 'ZERO_MOVE' and e[1:] == [x, a, y], 'ZERO_MOVE %r' % e)
                changed['move_to_zero_move_rank%d' % b] += 1
        elif op == 1:
            if a & 1:
                e = body[j]; j += 1
                need(e == ['ADD', x, y, b], 'ADD kept %r vs %r' % (e, (x, y, b)))
            else:
                changed['even_coefficient_add_dropped'] += 1
        elif op == 3:
            e = body[j]; j += 1
            need(e == ['CLEAR', SIZE, b], 'COPY entry -> centre CLEAR %r' % e); changed['copy_entry_to_clear'] += 1
        elif op == 2:
            e = body[j]; j += 1
            need(e == ['CLEAR', SIZE, None], 'COPY exit -> centre CLEAR %r' % e); changed['copy_exit_to_clear'] += 1
        else:
            need(False, 'unknown source op %r' % op)
    need(j == len(body), 'emitted body has extra events')
    res['L2'] = {'pivots': sorted(pivots), 'changes': dict(changed),
                 'prologue_events': k, 'epilogue_events': len(prog) - tail}
    log('L2 pass', res['L2'])

    # ---- I own invoice from the controller
    ctl = json.loads((ROOT / 'research/query-thinned-controllers/BIT-CONTROLLER.json').read_text())
    helpers = Counter()
    for i in range(2 * PORTS, SIZE):
        if i not in owned:
            helpers[8] += 1          # retained helpers: start frame 0 -> final full (rank 8), checked below
    need(all(word['start'][i] == 0 and word['final'][i] == 1 for i in range(2 * PORTS, SIZE)), 'helper frames')
    old_helpers = Counter({8: SIZE - 2 * PORTS})

    def invoice(local_paid, local_helpers):
        P, T = Counter(), Counter()
        for e in ctl['physical_events']:
            if e[0] == 'LOCAL':
                P.update(local_paid); T.update(local_helpers)
            elif e[0] == 'QUERY_SHEAR':
                P[1] += PORTS
            elif e[0] == 'IDLE':
                P[7 * len(e[2])] += 2 * PORTS
        for term in ctl['diagonal']:
            need(term & 1, 'diagonal term keeps the central direction')
            T[1 + 7 * bin(term >> 1).count('1')] += PORTS
        return P, T
    P0, T0 = invoice(old, old_helpers)
    P1, T1 = invoice(new, helpers)
    nfull = sum(e[0] == 'LOCAL' for e in ctl['physical_events'])
    dP = {k: P1[k] - P0[k] for k in set(P0) | set(P1) if P1[k] != P0[k]}
    dT = {k: T1[k] - T0[k] for k in set(T0) | set(T1) if T1[k] != T0[k]}
    mass = lambda H: sum(r * n for r, n in H.items())
    res['invoice'] = {'full_calls': nfull, 'paid_new_total': sum(P1.values()), 'targets_new_total': sum(T1.values()),
                      'paid_mass_new': mass(P1), 'target_mass_new': mass(T1), 'surplus_new': mass(T1) - mass(P1),
                      'surplus_old': mass(T0) - mass(P0), 'delta_paid': dP, 'delta_targets': dT,
                      'paid_new': dict(sorted(P1.items())), 'targets_new': dict(sorted(T1.items()))}
    log('invoice', {k: v for k, v in res['invoice'].items() if k not in ('paid_new', 'targets_new')})
    need(dP == {1: -162, 7: -162} and dT == {8: -162}, 'invoice delta')

    # ---- M raw moment crossing, 60 digits
    def margin(H_T, H_P, kappa):
        t = 1 - kappa
        return sum(D(n) * (D(r) ** t) for r, n in H_T.items()) - sum(D(n) * (D(r) ** t) for r, n in H_P.items())

    def crossing(H_T, H_P):
        lo, hi = D('0.001'), D('0.01')
        need(margin(H_T, H_P, lo) > 0 > margin(H_T, H_P, hi), 'bracket')
        for _ in range(140):
            mid = (lo + hi) / 2
            if margin(H_T, H_P, mid) > 0:
                lo = mid
            else:
                hi = mid
        return lo, hi
    r_new = crossing(T1, P1); r_old = crossing(T0, P0)
    m_lo = margin(T1, P1, D('0.003472070044')); m_hi = margin(T1, P1, D('0.003472070045'))
    res['moment'] = {'new_root': str(r_new[0])[:24], 'old_root': str(r_old[0])[:24],
                     'margin_at_0.003472070044': '%.6e' % m_lo, 'margin_at_0.003472070045': '%.6e' % m_hi}
    need(m_lo > 0 > m_hi, 'claimed crossing bracket')
    log('moment', res['moment'])

    # ---- ordinary BIT arithmetic
    atom, old_ord = F('0.004'), F('0.0000384599')
    new_ord = (1 - atom) * F('0.0034578') + atom * old_ord
    old_ordv = (1 - atom) * F('0.00345') + atom * old_ord
    res['ordinary'] = {'new': str(D(new_ord.numerator) / D(new_ord.denominator)),
                       'old_matched': str(D(old_ordv.numerator) / D(old_ordv.denominator)),
                       'gain': str(D((new_ord - old_ordv).numerator) / D((new_ord - old_ordv).denominator)),
                       'chain_new': 'root %s > tested .0034678 > uniform .0034668 -> cover -.000009 = .0034578' % res['moment']['new_root'][:14],
                       'chain_old': 'root %s > tested .00346 > uniform .003459 -> cover -.000009 = .00345' % res['moment']['old_root'][:14]}
    need(new_ord == F('0.0034441226396') and new_ord - old_ordv == F('0.0000077688'), 'ordinary BIT arithmetic')
    need(D('0.0034678') < r_new[0] and D('0.00346') < r_old[0], 'tested savings below the roots')
    log('ordinary', res['ordinary'])

    # ---- compare with the PR's RESULT.json
    claimed = json.loads((PKG / 'RESULT.json').read_text())
    cc = claimed['complete_cost']
    lo, hi = (F(x) for x in cc['new_raw_root'])
    need(F(str(r_new[0])) > lo - F(1, 10 ** 12) and F(str(r_new[0])) < hi + F(1, 10 ** 12), 'root matches RESULT.json')
    res['matches_RESULT_json'] = {'new_raw_root': cc['new_raw_root'], 'old_raw_root': cc['old_raw_root'],
                                  'new_ordinary': cc['ordinary_BIT']['new_ordinary'], 'agree': True}
    OUT.write_text(json.dumps(res, indent=1))
    log('PASS_INDEPENDENT_5421')


if __name__ == '__main__':
    main()

Mark (Matarener), with Claude Code assistance.