carrier.py — frc/ledgers/master

1"""master/carrier — the ledger file of the master's block B, the Carrier (ledger migration, task LM22, 5 October 2026).23The master predicate ledger (00-ledger/predicates/index.md, published as docs/00-ledger.json) states block B. This file4binds its theorem rows to the framework: the table of keys (generated from docs/00-ledger.json by ci/make_ledgers.py),5the Lean proofs each key conjoins (PROOFS, written here: the master has no Lean cells of its own), the shells, and the6checks, which call the foundation and carrier themes (frc/foundation.py, frc/carrier.py). Each check names the rows it7decides or corroborates (LEDGER), under a `# 00:B5 (p00015)` marker on the check that decides the row (PREDICATES).89The rows are B5, B7, B8, B10 and B14, the block's T rows, all on the Carrier's chart Ω = 4S + 1 without a generator.10The checks run on three Carriers: Ω = 233 (S = 58), 30 089 (S = 7 522) and the laboratory 2 408 561 (S = 602 140), each11with a Subject p (13, 173, 1 373) and, on the laboratory Carrier, the nested shell 37; and as sweeps over every prime12below a bound, the theorems' universal clauses checked by search. The Lean side is the key file13lean/FrcCore/Keys/Carrier.lean and the certificate lean/FrcCore/Ledgers/Master/Carrier.lean.1415    python3 -m frc.ledgers.master.carrier        every block, the census; exit 1 if a check fails (≈ 10 s)16    python3 -m frc.ledgers.master.carrier R      one block (S, R, W, V or O)17    from frc.ledgers.master.carrier import R; R.predicate("00:B7")    one row: its blocks run once per session1819Blocks:  S  the substrate residue                   EXACT  (00:B5)20         R  the register in S alone                 EXACT  (00:B7)21         W  the window ladder                       EXACT  (00:B8)22         V  one gauge bit closes the sign sector    EXACT  (00:B10)23         O  the octant sector                       EXACT  (00:B14)2425The notebook frc/ledgers/master/carrier.ipynb runs one row per cell, the cell's id its key (gate G13).26"""27import sys2829from frc import arith30from frc.registry import Registry31from frc.foundation import half_power, quarter_turn, quarter_turns, square_roots, fermat_holds32from frc.carrier import capacity, register, octant, tsirelson, triality_roots, horizon, quarter_root, coherence3334# ---- generated by ci/make_ledgers.py from docs/00-ledger.json; edit the ledger, not this table ----35BLOCK = "B"36KEYS = {"B1": "p00011", "B2": "p00012", "B3": "p00013", "B4": "p00014", "B5": "p00015", "B6": "p00016", "B7": "p00165", "B8": "p00166", "B9": "p00019", "B10": "p00168", "B12": "p00167", "B13": "p00169", "B14": "p00170"}       # every row of the block: its label and its accession key37LEAN = {"B5": "core", "B7": "core", "B8": "core", "B10": "core", "B14": "core"}       # the rows with a Lean declaration: the libraries whose key files prove them38# ---- end of the generated table ----3940# The Lean proofs of the rows' keys: the theorems of the themes that each key conjoins (lean/make_keys.py writes the keys41# FRC.Ledger.p<key> from them). The master's block file is the binding's source, as a paper's \lean{} cells are its own.42PROOFS = {43    "B5": ["FRC.Carrier.substrate_residue"],44    "B7": ["FRC.Carrier.register"],45    "B8": ["FRC.Carrier.window_ladder"],46    "B10": ["FRC.Carrier.sign_sector"],47    "B14": ["FRC.Carrier.octant"],48}4950LEAN_ONLY = ()                  # the rows with a Lean declaration and no python check (gate G12): none5152# The Carriers (Ω, the Subject p): Ω = 4S + 1 prime, p prime with p² < Ω.53SHELLS = [(233, 13), (30089, 173), (2408561, 1373)]54SWEEP = 5000                    # the sweeps run over every prime Ω below it5556# The published residues the register is compared with, as pairs: 10-dimensions' Carrier 233 (10:E4) and the laboratory57# Carrier of 37-sim (validation/constants.py) and 10-dimensions; 14-entropy's octant characters (14:C6), in the chart.58PUBLISHED = {233: {"hbar": 89, "c": 159, "kB": 124, "zeta": 221},59             2408561: {"hbar": 18688, "c": 171106, "kB": 1880160, "zeta": 1639587}}6061# The rows each check decides or corroborates.62LEDGER = {63    "S1": "00:B5", "S2": "00:B5", "S3": "00:B5",64    "R1": "00:B7", "R2": "00:B7", "R3": "00:B7", "R4": "00:B7",65    "W1": "00:B8", "W2": "00:B8", "W3": "00:B8",66    "V1": "00:B10", "V2": "00:B10",67    "O1": "00:B14", "O2": "00:B14", "O3": "00:B14",68}6970BLOCKS = {"S": "the substrate residue", "R": "the register in S alone", "W": "the window ladder",71          "V": "one gauge bit closes the sign sector", "O": "the octant sector"}7273# the deciding check of each row: the three Carriers; for B5 and B14, whose rows are equivalences, the sweeps, which meet74# both sides of the iff (every Carrier has Ω ≡ 5 (mod 12) and S even); the comparisons corroborate75PREDICATES = {"00:B5": "S2", "00:B7": "R1", "00:B8": "W1", "00:B10": "V1", "00:B14": "O2"}7677R = Registry("00", "carrier", LEDGER, PREDICATES, sources=[__file__])7879for _Om, _p in SHELLS:80    assert arith.is_prime(_Om) and _Om % 4 == 1 and arith.is_prime(_p) and _p * _p < _Om, (_Om, _p)818283def _primes(lo, hi):84    return [n for n in range(lo, hi) if arith.is_prime(n)]858687# ------------------------------------------------------------------------------------------------------------88# block S: the substrate residue (00:B5)89# 4 | Ω − 1 and 3 | Ω + 1 jointly hold iff Ω ≡ 5 (mod 12); on a prime Ω > 3, a quarter-turn and no triality root iff90# Ω ≡ 5 (mod 12) (Carrier.lean, substrate_residue).91@R.block("S", BLOCKS["S"])92def block_S():93    """Block S — the substrate residue (EXACT): S1–S3."""94    # 00:B5 (p00015)95    ok, det = True, []96    for Om, _ in SHELLS:97        h = quarter_turn(Om)98        no_tri = arith.legendre(-3 % Om, Om) == -1                 # x² + x + 1 has a root iff −3 is a square99        if Om < 10 ** 5: no_tri = no_tri and not triality_roots(Om)100        ok &= Om % 12 == 5 and (Om - 1) % 4 == 0 and (Om + 1) % 3 == 0 and h * h % Om == Om - 1 and no_tri101        det.append(f"Ω={Om}: Ω≡{Om % 12} (12), ħ={h}, no root of x²+x+1")102    R.check("S1", "on the three Carriers: Ω ≡ 5 (mod 12), 4 | Ω−1, 3 | Ω+1; ħ² = −1 generator-free; x² + x + 1 has no root", ok, "; ".join(det))103    # S2 the structure, by search on every prime 3 < Ω < SWEEP104    bad = [Om for Om in _primes(5, SWEEP)105           if (bool(quarter_turns(Om)) and not triality_roots(Om)) != (Om % 12 == 5)]106    R.check("S2", f"every prime 3 < Ω < {SWEEP}: a root of x² = −1 and none of x² + x + 1 (by search) iff Ω ≡ 5 (mod 12)", not bad,107            f"{len(_primes(5, SWEEP))} primes; exceptions {bad}")108    # S3 the congruences, on every integer below 10⁵109    bad = [n for n in range(10 ** 5) if (((n - 1) % 4 == 0 if n else True) and (n + 1) % 3 == 0) != (n % 12 == 5)]110    R.check("S3", "every Ω < 10⁵: 4 | Ω − 1 and 3 | Ω + 1 iff Ω ≡ 5 (mod 12) (natural subtraction: 0 − 1 = 0)", not bad, f"exceptions {bad[:5]}")111112113# ------------------------------------------------------------------------------------------------------------114# block R: the register in S alone (00:B7)115# c² = 2S + 1 = 2⁻¹; G = 2S = −c², 2G = −1, G unique; ħ² = −1 solvable; c exists iff S even; k_B c = ħ forces k_B² = −2;116# each square fixes its root up to sign; h = −ħ a second root (Carrier.lean, register).117@R.block("R", BLOCKS["R"])118def block_R():119    """Block R — the register in S alone (EXACT): R1–R4."""120    # 00:B7 (p00165)121    ok, det = True, []122    for Om, _ in SHELLS:123        S = capacity(Om); r = register(S); G, c2, hb, c, kB, h = r["G"], r["c2"], r["hbar"], r["c"], r["kB"], r["h"]124        inv2 = arith.inverse(2, Om)125        ok &= (2 * c2 % Om == 1 and c2 == inv2 and G == (-c2) % Om and 2 * G % Om == Om - 1126               and (Om - 1) * inv2 % Om == G                                   # the one solution of 2x = −1127               and hb * hb % Om == Om - 1 and h * h % Om == Om - 1 and h != hb128               and S % 2 == 0 and c is not None and c * c % Om == c2129               and kB * c % Om == hb and kB * kB % Om == Om - 2)130        # the rest up to sign: each defining square's root x has the partner −x ≠ x, and a third root y would give131        # (y − x)(y + x) = 0 with both factors nonzero in the field, so on the Carriers below 10⁵ the roots are found by search132        for x, a in ((c, c2), (hb, Om - 1), (kB, Om - 2)):133            ok &= (Om - x) % Om != x and (Om - x) * (Om - x) % Om == a134            if Om < 10 ** 5: ok &= sorted(square_roots(a, Om)) == sorted([x, (Om - x) % Om])135        det.append(f"Ω={Om}: G={G}, c²={c2}, ħ={hb}, h={h}, c={c}, k_B={kB}")136    R.check("R1", "on the three Carriers, generator-free in S: 2c² = 1, G = 2S = −c², 2G = −1 uniquely, ħ² = h² = −1 with h = −ħ ≠ ħ, "137            "S even and c² = 2S + 1 solved, k_B c = ħ, k_B² = −2; the rest up to sign: c, ħ and k_B each with the distinct "138            "partner −x, the only other root (by search below 10⁵)", ok, "; ".join(det))139    # R2 c exists iff S even, by search on every prime Ω = 4S + 1 < SWEEP140    bad = [Om for Om in _primes(5, SWEEP) if Om % 4 == 1141           and bool(square_roots((Om + 1) // 2, Om)) != (((Om - 1) // 4) % 2 == 0)]142    R.check("R2", f"every prime Ω = 4S + 1 < {SWEEP}: c² = 2S + 1 has a root (by search) iff S is even", not bad, f"exceptions {bad}")143    # R3 up to sign: each defining square has exactly the two roots {x, −x}144    ok, det = True, []145    for Om, _ in SHELLS[:2]:146        r = register(capacity(Om))147        for name, a in (("c²", r["c2"]), ("−1", Om - 1), ("−2", Om - 2)):148            roots = square_roots(a, Om)149            ok &= len(roots) == 2 and (roots[0] + roots[1]) % Om == 0150        det.append(f"Ω={Om}: two roots each, {{x, −x}}")151    R.check("R3", "on Ω = 233 and 30 089, by search: x² = c², x² = −1 and x² = −2 have exactly two roots each, a pair {x, −x}", ok, "; ".join(det))152    # R4 the published residues are the register's pairs153    ok, det = True, []154    for Om, pub in PUBLISHED.items():155        r = register(capacity(Om))156        for k in ("hbar", "c", "kB"):157            ok &= pub[k] in (r[k], (Om - r[k]) % Om)158        det.append(f"Ω={Om}: ħ ∈ {{±{r['hbar']}}} ∋ {pub['hbar']}, c ∈ {{±{r['c']}}} ∋ {pub['c']}, k_B ∈ {{±{r['kB']}}} ∋ {pub['kB']}")159    R.check("R4", "the published residues of 10:E4 (Ω = 233) and 37-sim (the laboratory Carrier) lie in the register's pairs", ok, "; ".join(det))160161162# ------------------------------------------------------------------------------------------------------------163# block W: the window ladder (00:B8)164# a nested Subject p² < Ω: its horizon below the quarter-root, x² ≤ p ⇒ x⁴ < Ω, its shell below the coherence horizon,165# x ≤ p ⇒ x² < Ω; the saturating Subject p² < Ω ≤ (p + 1)² locks both; one square root per embedding (Carrier.lean,166# window_ladder).167@R.block("W", BLOCKS["W"])168def block_W():169    """Block W — the window ladder (EXACT): W1–W3."""170    # 00:B8 (p00166)171    ok, det = True, []172    for Om, p in SHELLS:173        hp, q4, co = horizon(p), quarter_root(Om), coherence(Om)174        sat = Om <= (p + 1) ** 2175        ok &= p * p < Om and hp ** 4 < Om and hp <= q4 and p <= co and (not sat or (hp == q4 and p == co))176        det.append(f"Ω={Om}, p={p}: ⌊√p⌋={hp} ≤ {q4} (x⁴ < Ω), p ≤ {co} (x² < Ω)" + (", saturated: both equal" if sat else ""))177    R.check("W1", "on the three Carriers with their Subjects: p² < Ω, the horizon ⌊√p⌋ inside the quarter-root window, the shell inside "178            "the coherence window; the saturated Subject (30 089, 173) locks both", ok, "; ".join(det))179    # W2 the lock, on every p < 300 and every Ω with p² < Ω ≤ (p + 1)²180    bad = [(p, Om) for p in range(1, 300) for Om in range(p * p + 1, (p + 1) ** 2 + 1)181           if not (horizon(p) == quarter_root(Om) and p == coherence(Om))]182    R.check("W2", "every p < 300 and every Ω with p² < Ω ≤ (p + 1)²: the horizon is the quarter-root window and the shell the coherence window",183            not bad, f"{sum(2 * p + 1 for p in range(1, 300))} pairs; exceptions {bad[:5]}")184    # W3 the laboratory nesting 37 → 1373 → 2 408 561, one square root per embedding185    q, p, Om = 37, 1373, 2408561186    ok = all(arith.is_prime(n) for n in (q, p, Om)) and q * q < p and p * p < Om and q ** 4 < Om and horizon(p) == q187    R.check("W3", "the laboratory ladder: 37, 1 373 and 2 408 561 prime, 37² < 1 373, 1 373² < Ω, 37⁴ < Ω; the Subject's horizon is 37", ok,188            f"37²={q * q}, 1373²={p * p}, 37⁴={q ** 4}, ⌊√1373⌋={horizon(p)}")189190191# ------------------------------------------------------------------------------------------------------------192# block V: one gauge bit closes the sign sector (00:B10)193# −1 a square; the square class blind to x ↔ −x; integer parity flipped by it; (−x)² = x²; {ħ, −ħ} two distinct roots of194# −1 (Carrier.lean, sign_sector).195@R.block("V", BLOCKS["V"])196def block_V():197    """Block V — one gauge bit closes the sign sector (EXACT): V1, V2."""198    # 00:B10 (p00168)199    ok, det = True, []200    for Om, _ in SHELLS:201        hb = quarter_turn(Om); span = range(1, Om) if Om < 10 ** 5 else range(1, 20001)202        blind = all(arith.legendre(x, Om) == arith.legendre(Om - x, Om) for x in span)203        flips = all(x % 2 != (Om - x) % 2 for x in span)204        faces = all(x * x % Om == (Om - x) ** 2 % Om for x in span)205        ok &= hb * hb % Om == Om - 1 and blind and flips and faces and (Om - hb) ** 2 % Om == Om - 1 and Om - hb != hb206        det.append(f"Ω={Om}: x ∈ [1, {span.stop})" + (" (all)" if span.stop == Om else ""))207    R.check("V1", "on the three Carriers: −1 a square; x and −x of one square class and of opposite parity; (−x)² = x²; ħ and −ħ distinct roots of −1",208            ok, "; ".join(det))209    # V2 −1 is a square iff Ω ≡ 1 (mod 4), the quarter-turn criterion, by search below SWEEP210    bad = [Om for Om in _primes(3, SWEEP) if bool(quarter_turns(Om)) != (Om % 4 == 1)]211    R.check("V2", f"every odd prime Ω < {SWEEP}: x² = −1 has a root (by search) iff Ω ≡ 1 (mod 4)", not bad, f"exceptions {bad}")212213214# ------------------------------------------------------------------------------------------------------------215# block O: the octant sector (00:B14)216# an element of order eight exists iff S is even (Carrier.lean, octant).217@R.block("O", BLOCKS["O"])218def block_O():219    """Block O — the octant sector (EXACT): O1–O3."""220    # 00:B14 (p00170)221    ok, det = True, []222    for Om, _ in SHELLS:223        S = capacity(Om); z = octant(Om)224        ok &= S % 2 == 0 and z is not None and pow(z, 8, Om) == 1 and pow(z, 4, Om) == Om - 1 and tsirelson(z, Om) == 2225        if Om < 10 ** 5: ok &= fermat_holds(Om)226        det.append(f"Ω={Om}: S={S} even, ζ={z} = a^(S/2) with a={half_power(Om)}, ζ⁴ = −1, (ζ + ζ⁷)² = 2")227    R.check("O1", "on the three Carriers: S even, ζ = a^(S/2) with a^(2S) = −1 has ζ⁸ = 1 and ζ⁴ = −1 ≠ 1, (ζ + ζ⁷)² = 2; Fermat by computation on 233 and 30 089",228            ok, "; ".join(det))229    # O2 by search on every prime Ω = 4S + 1 < SWEEP: an element of order eight iff S even230    bad = []231    for Om in _primes(5, SWEEP):232        if Om % 4 != 1: continue233        has8 = any(pow(x, 8, Om) == 1 and pow(x, 4, Om) != 1 for x in range(1, Om))234        if has8 != (((Om - 1) // 4) % 2 == 0): bad.append(Om)235    R.check("O2", f"every prime Ω = 4S + 1 < {SWEEP}: an element with ζ⁸ = 1, ζ⁴ ≠ 1 (by search) iff S is even", not bad, f"exceptions {bad}")236    # O3 the octant characters of 14:C6, found in the chart, are the generator-free ζ's odd powers237    ok, det = True, []238    for Om, pub in PUBLISHED.items():239        z = octant(Om); odd = {pow(z, k, Om) for k in (1, 3, 5, 7)}240        ok &= pub["zeta"] in odd241        det.append(f"Ω={Om}: {pub['zeta']} ∈ {{ζ, ζ³, ζ⁵, ζ⁷}} = {sorted(odd)}")242    R.check("O3", "14:C6's octant characters (Ω = 233 and the laboratory Carrier, found in the chart) are primitive eighth roots of the generator-free ζ",243            ok, "; ".join(det))244245246if __name__ == "__main__":247    blocks = [a for a in sys.argv[1:] if a in R.blocks]248    if blocks:249        for b in blocks: R.run_block(b)250        sys.exit(0 if R.summary(write=False) else 1)251    sys.exit(0 if R.verify_all() else 1)252