interactions.py — frc/ledgers/master

1"""master/interactions — a ledger file of the master's block G, interactions: the rows the interactions theme proves2(ledger migration, task LM29, 6 October 2026).34The master's block G is bound by this file (the interactions theme). It binds G11 (one generation, its content), G125(one generation, its origin) and G16 (flavour, the Koide form): the table of keys (generated from docs/00-ledger.json by6ci/make_ledgers.py), the Lean proofs each key conjoins (PROOFS), and the checks, which call the interactions theme7(frc/interactions.py). The Lean side is lean/FrcCore/Theme/Interactions.lean, the key file8lean/FrcCore/Keys/Interactions.lean and the certificate lean/FrcCore/Ledgers/Master/Interactions.lean.910    python3 -m frc.ledgers.master.interactions        every block, the census; exit 1 if a check fails1112Blocks:  H  one generation: the reflection algebra, the fifth direction, the 16 read 3 + 2     EXACT  (00:G11, 00:G12)13         K  the Koide form on the cube-root orbit                                             EXACT  (00:G16)1415The notebook frc/ledgers/master/interactions.ipynb runs one row per cell, the cell's id its key (gate G13).16"""17import random18import sys19from fractions import Fraction20from math import comb2122from frc import arith23from frc.registry import Registry24from frc.interactions import bit, cnt, emul, fifth, gen16, col, wk, y6, q6, koide_q, koide_rho22526# ---- generated by ci/make_ledgers.py from docs/00-ledger.json; edit the ledger, not this table ----27BLOCK = "G"28KEYS = {"G1": "p00178", "G2": "p00067", "G3": "p00068", "G4": "p00069", "G5": "p00070", "G6": "p00071", "G7": "p27043", "G8": "p00073", "G9": "p00074", "G10": "p00075", "G11": "p27020", "G12": "p00155", "G13": "p00078", "G14": "p00079", "G15": "p00080", "G16": "p00081", "G17": "p00179", "G18": "p00083", "G19": "p00088", "G20": "p00089", "G21": "p00090"}       # every row of the block: its label and its accession key29LEAN = {"G11": "core", "G12": "core", "G16": "core"}       # the rows with a Lean declaration: the libraries whose key files prove them30# ---- end of the generated table ----3132# The Lean proofs of the rows' keys: the theorems of the themes that each key conjoins (lean/make_keys.py writes the keys33# 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.34PROOFS = {35    "G11": ["FRC.Interactions.one_generation"],36    "G12": ["FRC.Interactions.reflection_algebra", "FRC.Interactions.fifth_direction"],37    "G16": ["FRC.Interactions.koide_parseval", "FRC.Interactions.koide_two_thirds", "FRC.Interactions.koide_extension",38            "FRC.Interactions.koide_half"],39}4041LEAN_ONLY = ()                  # the rows with a Lean declaration and no python check (gate G12): none4243LEDGER = {"H1": "00:G12", "H2": "00:G11", "H3": "00:G11", "K1": "00:G16", "K2": "00:G16", "K3": "00:G16"}44BLOCKS = {"H": "one generation: the reflection algebra, the fifth direction, the 16 read 3 + 2",45          "K": "the Koide form on the cube-root orbit"}46PREDICATES = {"00:G12": "H1", "00:G11": "H2", "00:G16": "K1"}4748R = Registry("00", "interactions", LEDGER, PREDICATES, sources=[__file__])4950# the Standard-Model generation by name: (colour rep, weak rep, Y) and its multiplicity51SM = {"nu^c": ("1", "1", Fraction(0)), "u^c": ("3b", "1", Fraction(-2, 3)), "Q": ("3", "2", Fraction(1, 6)),52      "e^c": ("1", "1", Fraction(1)), "L": ("1", "2", Fraction(-1, 2)), "d^c": ("3b", "1", Fraction(1, 3))}53DIM = {"1": 1, "2": 2, "3": 3, "3b": 3}545556# ------------------------------------------------------------------------------------------------------------57# block H: one generation (00:G11, 00:G12)58@R.block("H", BLOCKS["H"])59def block_H():60    """Block H — one generation (EXACT): H1–H3."""61    # 00:G12 (p00155)62    basis = range(16)63    def mulvec(x, y):                     # product of algebra elements as dicts index -> coefficient64        out = {}65        for S, a in x.items():66            for T, b in y.items():67                s, U = emul(S, T)68                if s: out[U] = out.get(U, 0) + s * a * b69        return {k: v for k, v in out.items() if v}70    rng = random.Random(12)71    ok = all(mulvec(mulvec({S: 1}, {T: 1}), {U: 1}) == mulvec({S: 1}, mulvec({T: 1}, {U: 1}))72             for S in basis for T in basis for U in basis)73    for _ in range(200):                  # associativity on random elements74        x, y, z = ({S: rng.randrange(-3, 4) for S in basis} for _ in range(3))75        ok &= mulvec(mulvec(x, y), z) == mulvec(x, mulvec(y, z))76    ok &= all(emul(1 << i, 1 << j) == ((0, 0) if i == j else (-emul(1 << j, 1 << i)[0], emul(1 << j, 1 << i)[1]))77              for i in range(4) for j in range(4))78    imgs = [fifth(S) for S in basis]79    ok &= sorted(imgs) == gen16() and len(gen16()) == 1680    ok &= all(emul(S, 16) == (1, S | 16) for S in basis if cnt(S, 0, 4) % 2)81    R.check("H1", "the reflection algebra of four directions: 16 basis elements, the product associative on all 4 096 basis "82            "triples and on 200 random elements, distinct directions anticommuting and squaring to zero; the fifth "83            "direction e_S ↦ e_S, e_S e_4 maps the 16 one-to-one onto the even subsets of five directions", ok,84            f"images {imgs}")85    # 00:G11 (p27020)86    g = gen16()87    content = {}88    # the colour type by triality: the centre ω·1 of SU(3) acts on Λᵏ(ℂ³) as ωᵏ, so k ≡ 0, 1, 2 (mod 3) is the89    # singlet, the 3 and the 3̄ (Λ² ≅ 3̄ by the volume form); the weak type by Λᵏ(ℂ²): k = 1 the doublet, else a singlet90    # (the template Λᵏ(ℂⁿ) for the k-th fundamental is imported)91    TRIALITY = {0: "1", 1: "3", 2: "3b"}92    for S in g:93        c, w = col(S), wk(S)94        rep = (TRIALITY[c % 3], {0: "1", 1: "2", 2: "1"}[w], Fraction(y6(S), 6))95        content[rep] = content.get(rep, 0) + 196    want = {(c, w, y): DIM[c] * DIM[w] for c, w, y in SM.values()}97    ok = content == want98    ok &= all(comb(3, k) == DIM[TRIALITY[k % 3]] for k in range(4)) and all(comb(2, k) == DIM[{0: "1", 1: "2", 2: "1"}[k]] for k in range(3))99    ok &= sum(y6(S) for S in g) == 0 and sum(y6(S) ** 3 for S in g) == 0100    ok &= sum(y6(S) for S in g if col(S) in (1, 2)) == 0 and sum(y6(S) for S in g if wk(S) == 1) == 0101    ok &= sorted(Fraction(q6(S), 6) for S in g) == sorted([Fraction(0), Fraction(0)] + [Fraction(2, 3)] * 3 + [Fraction(-2, 3)] * 3102                                                            + [Fraction(-1, 3)] * 3 + [Fraction(1, 3)] * 3 + [Fraction(1), Fraction(-1)])103    R.check("H2", "the 16 read 3 + 2, the colour type by triality (k mod 3 on Λᵏ(ℂ³)) and the weak type by Λᵏ(ℂ²), dimensions "104            "binom(3, k) and binom(2, k): the content ν^c + u^c + Q + e^c + L + d^c with their hypercharges, by name against the "105            "Standard-Model table; Σ Y = Σ Y³ = 0, SU(3)²Y = SU(2)²Y = 0; the charges 0, 0, ±2/3 ×3, ±1/3 ×3, ±1", ok,106            f"content {dict((f'{k[0]},{k[1]},{k[2]}', v) for k, v in content.items())}")107    # H3 a second method: the anomaly sums by multiplet, from the table108    s1 = sum(DIM[c] * DIM[w] * y for c, w, y in SM.values())109    s3 = sum(DIM[c] * DIM[w] * y ** 3 for c, w, y in SM.values())110    s33 = sum(DIM[w] * y for c, w, y in SM.values() if c != "1")111    s22 = sum(DIM[c] * y for c, w, y in SM.values() if w == "2")112    R.check("H3", "the anomaly sums from the multiplet table: Σ d Y = 0, Σ d Y³ = 0, SU(3)²Y = 0, SU(2)²Y = 0; four doublets",113            s1 == s3 == s33 == s22 == 0 and sum(DIM[c] for c, w, y in SM.values() if w == "2") == 4,114            f"{s1}, {s3}, {s33}, {s22}")115116117# ------------------------------------------------------------------------------------------------------------118# block K: the Koide form (00:G16)119@R.block("K", BLOCKS["K"])120def block_K():121    """Block K — the Koide form (EXACT): K1–K3."""122    # 00:G16 (p00081)123    bad = []124    for p in [q for q in range(7, 400) if q % 3 == 1 and arith.is_prime(q)]:125        w = next(x for x in range(2, p) if (x * x + x + 1) % p == 0)126        rng = random.Random(p)127        for _ in range(30):128            a = [rng.randrange(p) for _ in range(3)]129            hat, lhs, rhs = koide_rho2(a, p, w)130            if lhs != rhs: bad.append(p)131            if ((lhs - 2 * hat[0] ** 2) % p == 0) != ((2 * hat[1] * hat[2] - hat[0] ** 2) % p == 0): bad.append(p)132    R.check("K1", "every prime p ≡ 1 (mod 3) below 400 with ω² + ω + 1 = 0, 30 random amplitude vectors each: 3 Σ a² = â₀² + "133            "2 â₁â₂ (Q = 1/3 + 2ρ²/3), and 3 Σ a² = 2 â₀² exactly when 2 â₁â₂ = â₀² (Q = 2/3 ⟺ ρ² = 1/2)", not bad,134            f"exceptions {bad[:3]}")135    # K2 a second method: the cube-root orbit a_k = 1 + ρ(z ω^k + z⁻¹ ω^{−k}) in 𝔽_p has Σ a = 3 and Σ a² = 3 + 6ρ²136    bad = []137    for p in [q for q in range(7, 400) if q % 3 == 1 and arith.is_prime(q)]:138        w = next(x for x in range(2, p) if (x * x + x + 1) % p == 0)139        for z in range(1, p, max(1, p // 7)):140            zi = pow(z, -1, p)141            for rho in range(p):142                a = [(1 + rho * (z * pow(w, k, p) + zi * pow(w, -k % 3, p))) % p for k in range(3)]143                if sum(a) % p != 3 % p or sum(x * x for x in a) % p != (3 + 6 * rho * rho) % p: bad.append(p); break144    R.check("K2", "every prime p ≡ 1 (mod 3) below 400: on the cube-root orbit a_k = 1 + ρ(z ω^k + z⁻¹ ω^{−k}), Σ a = 3 and "145            "Σ a² = 3 + 6ρ² for every ρ and seven z, so Q = (3 + 6ρ²)/9 = 1/3 + 2ρ²/3, and Q = 2/3 at ρ² = 1/2",146            not bad, f"exceptions {bad[:3]}")147    # K3 every shell, the Carriers included: in the extension 𝔽_p[w]/(w² + 3), ω = −h + h w (h = 1/2) is a cube root of148    # unity, â₂ = â̄₁, and 3 Σ a² = â₀² + 2 N(â₁) with N(x + y w) = x² + 3 y² (Interactions.lean: koide_extension, koide_half)149    def emul3(z, u, p): return ((z[0] * u[0] - 3 * z[1] * u[1]) % p, (z[0] * u[1] + z[1] * u[0]) % p)150    bad = []151    for p in [q for q in range(5, 400) if q % 3 == 2 and arith.is_prime(q)] + [233, 30089, 2408561]:152        h = (p + 1) // 2153        om = ((-h) % p, h)154        om2 = emul3(om, om, p)155        if ((om2[0] + om[0] + 1) % p, (om2[1] + om[1]) % p) != (0, 0) or emul3(om2, om, p) != (1, 0): bad.append(p); continue156        rng = random.Random(p)157        for _ in range(30):158            a = [rng.randrange(p) for _ in range(3)]159            hat1 = ((a[0] + a[1] * om[0] + a[2] * om2[0]) % p, (a[1] * om[1] + a[2] * om2[1]) % p)160            hat2 = ((a[0] + a[1] * om2[0] + a[2] * om[0]) % p, (a[1] * om2[1] + a[2] * om[1]) % p)161            nrm = (hat1[0] ** 2 + 3 * hat1[1] ** 2) % p162            if hat2 != (hat1[0], (-hat1[1]) % p) or emul3(hat1, hat2, p) != (nrm, 0): bad.append(p); break163            if (3 * sum(x * x for x in a) - sum(a) ** 2 - 2 * nrm) % p: bad.append(p); break164    R.check("K3", "every prime p ≡ 2 (mod 3) below 400 and the Carriers 233, 30 089, 2 408 561 (no cube root of unity in "165            "𝔽_p): in 𝔽_p[w]/(w² + 3), ω = −1/2 + w/2 has ω² + ω + 1 = 0 and ω³ = 1; for 30 random amplitude vectors "166            "â₂ = â̄₁, â₁â₂ = N(â₁), and 3 Σ a² = â₀² + 2 N(â₁)", not bad, f"exceptions {bad[:3]}")167168if __name__ == "__main__":169    blocks = [a for a in sys.argv[1:] if a in R.blocks]170    if blocks:171        for b in blocks: R.run_block(b)172        sys.exit(0 if R.summary(write=False) else 1)173    sys.exit(0 if R.verify_all() else 1)174