quantum.py — frc/ledgers/master

1"""master/quantum — a ledger file of the master's block F, quantum: the rows the quantum theme proves (ledger migration,2task LM28, 6 October 2026).34The master's block F is bound by this file (the quantum theme). It binds F2, multi-body registration, and F5, the graded registration law (task LM42, 7 October 2026; its source 39-s173 is5unpublished, named and not linked, Q04): the table of keys6(generated from docs/00-ledger.json by ci/make_ledgers.py), the Lean proofs its key conjoins (PROOFS), the cycles, and7the checks, which call the quantum theme (frc/quantum.py). The Lean side is lean/FrcCore/Theme/Quantum.lean, the key8file lean/FrcCore/Keys/Quantum.lean and the certificate lean/FrcCore/Ledgers/Master/Quantum.lean.910    python3 -m frc.ledgers.master.quantum        every block, the census; exit 1 if a check fails1112Blocks:  J  the unequal-cycle composite: joint recurrence, gcd offset, dephasing     EXACT  (00:F2)13         R  the graded registration law: depth, home, sign, visibility              EXACT  (00:F5)1415The notebook frc/ledgers/master/quantum.ipynb runs one row per cell, the cell's id its key (gate G13).16"""17import random18import sys19from math import gcd, lcm2021from frc import arith22from frc.registry import Registry23from frc.quantum import joint_period, orbits, offset, reach, root_of_unity, character_sums, components, depth, home2425# ---- generated by ci/make_ledgers.py from docs/00-ledger.json; edit the ledger, not this table ----26BLOCK = "F"27KEYS = {"F1": "p00059", "F2": "p00191", "F4": "p00062", "F5": "p00194", "F6": "p00064"}       # every row of the block: its label and its accession key28LEAN = {"F2": "core", "F5": "core"}       # the rows with a Lean declaration: the libraries whose key files prove them29# ---- end of the generated table ----3031# The Lean proofs of the rows' keys: the theorems of the themes that each key conjoins (lean/make_keys.py writes the keys32# 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.33PROOFS = {34    "F2": ["FRC.Quantum.joint_recurrence", "FRC.Quantum.joint_least", "FRC.Quantum.pair_offset",35           "FRC.Quantum.dephasing"],36    "F5": ["FRC.Quantum.absorbed", "FRC.Quantum.unique_home", "FRC.Quantum.two_part_homes", "FRC.Quantum.sign_both",37           "FRC.Quantum.visibility_cap", "FRC.Quantum.registration_instances"],38}3940LEAN_ONLY = ()                  # the rows with a Lean declaration and no python check (gate G12): none4142PAIRS = 30                      # every pair of periods a, b ≤ PAIRS43TRIPLES = 10                    # every triple of periods ≤ TRIPLES4445SUBJECTS = 6000                 # the Subjects p ≡ 1 (mod 4) with κ odd below it, every Object q ≡ 1 (mod 4) with q² < p4647LEDGER = {"J1": "00:F2", "J2": "00:F2", "J3": "00:F2", "R1": "00:F5", "R2": "00:F5", "R3": "00:F5"}48BLOCKS = {"J": "the unequal-cycle composite: joint recurrence, gcd offset, dephasing",49          "R": "the graded registration law: depth, home, sign, visibility"}50PREDICATES = {"00:F2": "J1", "00:F5": "R1"}5152R = Registry("00", "quantum", LEDGER, PREDICATES, sources=[__file__])535455def _prime_1_mod(N):56    q = N + 157    while not arith.is_prime(q): q += N58    return q596061# ------------------------------------------------------------------------------------------------------------62# block J: the unequal-cycle composite (00:F2)63# the joint recurrence is the lcm of the periods; two joint states share an orbit exactly when their offsets agree64# modulo g, g T = a b; every character the drive moves sums to zero over every joint recurrence (Quantum.lean:65# joint_recurrence, joint_least, pair_offset, dephasing).66@R.block("J", BLOCKS["J"])67def block_J():68    """Block J — the unequal-cycle composite (EXACT): J1–J3."""69    # 00:F2 (p00060)70    bad = []71    for a in range(1, PAIRS + 1):72        for b in range(1, PAIRS + 1):73            T = joint_period([a, b])74            g = a * b // T75            orbs = orbits(a, b)76            ok = T == lcm(a, b) and g == gcd(a, b) and g * T == a * b77            ok &= all((t % a == 0 and t % b == 0) == (t % T == 0) for t in range(3 * a * b))78            ok &= len(orbs) == g and all(len(o) == T for o in orbs)79            ok &= all(len({offset(x, y, g) for x, y in o}) == 1 for o in orbs)80            ok &= len({offset(o[0][0], o[0][1], g) for o in orbs}) == g81            if not ok: bad.append((a, b))82    bad3 = [(a, b, c) for a in range(1, TRIPLES + 1) for b in range(1, TRIPLES + 1) for c in range(1, TRIPLES + 1)83            if joint_period([a, b, c]) != lcm(a, b, c)]84    R.check("J1", f"every pair of periods a, b ≤ {PAIRS}: the joint recurrences are exactly the multiples of T = lcm(a, b); "85            "the joint drive has g = gcd(a, b) orbits of T states, g T = a b, each orbit one offset class (x − y) mod g, "86            f"the g classes all occupied; every triple ≤ {TRIPLES}: the joint period is lcm(a, b, c)", not bad and not bad3,87            f"{PAIRS * PAIRS} pairs, {TRIPLES ** 3} triples; exceptions {bad[:3]} {bad3[:3]}")88    # J2 a second method: reachability by search against the offset criterion, random pairs up to 20089    rng = random.Random(28)90    bad = []91    for _ in range(300):92        a, b = rng.randrange(1, 200), rng.randrange(1, 200)93        g = gcd(a, b)94        x, y, x2, y2 = rng.randrange(a), rng.randrange(b), rng.randrange(a), rng.randrange(b)95        if (reach(x, y, x2, y2, a, b) is not None) != ((x + y2) % g == (x2 + y) % g): bad.append((a, b))96    R.check("J2", "300 random pairs of periods below 200 and random states: a chronon carries (x, y) to (x', y') exactly when "97            "(x + y') ≡ (x' + y) mod g, by search", not bad, f"exceptions {bad[:3]}")98    # J3 dephasing: every character of ℤ/a × ℤ/b in 𝔽_q, q ≡ 1 (mod lcm(a, b))99    tot, moved, bad = 0, 0, []100    for a, b in [(4, 6), (12, 232), (5, 7), (8, 12), (10, 14)]:101        T = lcm(a, b); q = _prime_1_mod(T)102        for M in (T, a * b):103            sums = character_sums(q, a, b, M)104            tot += len(sums)105            moved += sum(1 for m, _ in sums if m)106            if not all((s == 0) if m else (s == M % q) for m, s in sums): bad.append((a, b, M))107    R.check("J3", "the cycles (4, 6), (12, 232), (5, 7), (8, 12), (10, 14) in 𝔽_q with q ≡ 1 mod lcm: every character the drive "108            "moves sums to zero along it over one joint period T and over the product period a b; the others give T or a b",109            not bad, f"{moved} of {tot} character sums cancel; exceptions {bad}")110111112113114# ------------------------------------------------------------------------------------------------------------115# block R: the graded registration law (00:F5; 39-s173, rows B1–B5)116# an Object component ℓᵃ registers at depth d = ord_{ℓᵃ}(p): d = 1 absorbed in C_{p−1}, its image unique; d = 2 for odd117# ℓ on the boost torus C_{p+1}, the home unique (gcd(p − 1, p + 1) = 2); a 2-component past the quarter off both tori;118# the sign on both faces; the cap 2 where p² < Ω < p³ (Quantum.lean: absorbed, unique_home, two_part_homes, sign_both,119# visibility_cap, registration_instances).120@R.block("R", BLOCKS["R"])121def block_R():122    """Block R — the graded registration law (EXACT): R1–R3."""123    # 00:F5 (p00194)124    bad, n_towers, n_comp, seen = [], 0, 0, {"absorbed": 0, "torus": 0, "quadratic": 0, "beyond": 0}125    for p in range(13, SUBJECTS, 4):126        if not arith.is_prime(p) or ((p - 1) // 4) % 2 == 0: continue127        for q in range(5, p, 4):128            if q * q >= p: break129            if not arith.is_prime(q): continue130            n_towers += 1131            for face in (q - 1, q + 1):132                for l, a, n in components(face):133                    n_comp += 1134                    d, h = depth(n, p), home(n, p)135                    seen[h] += 1136                    ok = (d == 1) == (h == "absorbed")                                   # d = 1 iff absorbed137                    if l > 2: ok &= (d == 2) == (h == "torus")                          # odd ℓ: d = 2 iff on the boost torus138                    else: ok &= (n <= 4) == (h == "absorbed") and h != "torus" if n > 2 else h == "absorbed"139                    ok &= (h != "quadratic" or d == 2) and (h != "beyond" or d > 2)140                    if not ok: bad.append((q, p, n, d, h))141            ok = pow(p - 1, p - 1, p) == 1 and pow(p - 1, p + 1, p) == 1 and gcd(p - 1, p + 1) == 2142            if not ok: bad.append((q, p, "sign"))143    R.check("R1", f"every Subject p ≡ 1 (mod 4) with κ odd below {SUBJECTS}, every Object q ≡ 1 (mod 4) prime with q² < p, every "144            "primary component ℓᵃ of q − 1 and q + 1: depth 1 iff absorbed in C_{p−1}; for odd ℓ depth 2 iff on the boost torus "145            "C_{p+1}, gcd(p − 1, p + 1) = 2; the 2-components 2 and 4 absorbed, 8 and beyond on neither torus; the sign on both "146            "faces", not bad, f"{n_towers} towers, {n_comp} components {seen}; exceptions {bad[:3]}")147    # R2 the instances (39:B2, B3, B5): decided directly148    roots4 = sorted(x for x in range(1, 173) if pow(x, 4, 173) == 1)149    ok = (depth(7, 173), depth(7, 181), depth(7, 197)) == (6, 2, 1) and roots4 == [1, 80, 93, 172]150    ok &= home(4, 173) == "absorbed" and home(3, 173) == "torus" and home(7, 173) == "beyond"           # hydrogen, q = 13151    ok &= all(depth(n, 173) <= 2 for f in (4, 6) for _, _, n in components(f))                           # the proton, q = 5152    ok &= 5 * 5 > 13                                                                                      # (5, 13) refused153    R.check("R2", "the instances: the depth of hydrogen's interior 7 is 6 at 173, 2 at 181, 1 at 197; the quarter absorbed at 173 "154            "with the images {1, 80, 93, 172}, the triality on the torus, the 7 beyond; the proton whole (depth ≤ 2); (5, 13) "155            "refused, 25 > 13", ok, f"4th roots of unity in 𝔽_173: {roots4}")156    # R3 the cap: p² < Ω < p³ on the minimal tower and the laboratory tower; every saturating tower p² < Ω ≤ (p + 1)²157    ok = 173 ** 2 < 30089 <= 174 ** 2 and 30089 < 173 ** 3 and 1373 ** 2 < 2408561 < 1373 ** 3158    ok &= all((p + 1) ** 2 < p ** 3 for p in range(3, 2000))159    R.check("R3", "the visibility cap 2: (173, 30 089) saturating, 173² < Ω ≤ 174² < 173³; the laboratory (1 373, 2 408 561) "160            "with p² < Ω < p³; (p + 1)² < p³ for every 3 ≤ p < 2000", ok, "")161162if __name__ == "__main__":163    blocks = [a for a in sys.argv[1:] if a in R.blocks]164    if blocks:165        for b in blocks: R.run_block(b)166        sys.exit(0 if R.summary(write=False) else 1)167    sys.exit(0 if R.verify_all() else 1)168