"""master/interactions — a ledger file of the master's block G, interactions: the rows the interactions theme proves
(ledger migration, task LM29, 6 October 2026).

The master's block G is bound by this file (the interactions theme). It binds G11 (one generation, its content), G12
(one generation, its origin) and G16 (flavour, the Koide form): the table of keys (generated from docs/00-ledger.json by
ci/make_ledgers.py), the Lean proofs each key conjoins (PROOFS), and the checks, which call the interactions theme
(frc/interactions.py). The Lean side is lean/FrcCore/Theme/Interactions.lean, the key file
lean/FrcCore/Keys/Interactions.lean and the certificate lean/FrcCore/Ledgers/Master/Interactions.lean.

    python3 -m frc.ledgers.master.interactions        every block, the census; exit 1 if a check fails

Blocks:  H  one generation: the reflection algebra, the fifth direction, the 16 read 3 + 2     EXACT  (00:G11, 00:G12)
         K  the Koide form on the cube-root orbit                                             EXACT  (00:G16)

The notebook frc/ledgers/master/interactions.ipynb runs one row per cell, the cell's id its key (gate G13).
"""
import random
import sys
from fractions import Fraction
from math import comb

from frc import arith
from frc.registry import Registry
from frc.interactions import bit, cnt, emul, fifth, gen16, col, wk, y6, q6, koide_q, koide_rho2

# ---- generated by ci/make_ledgers.py from docs/00-ledger.json; edit the ledger, not this table ----
BLOCK = "G"
KEYS = {"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 key
LEAN = {"G11": "core", "G12": "core", "G16": "core"}       # the rows with a Lean declaration: the libraries whose key files prove them
# ---- end of the generated table ----

# The Lean proofs of the rows' keys: the theorems of the themes that each key conjoins (lean/make_keys.py writes the keys
# 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.
PROOFS = {
    "G11": ["FRC.Interactions.one_generation"],
    "G12": ["FRC.Interactions.reflection_algebra", "FRC.Interactions.fifth_direction"],
    "G16": ["FRC.Interactions.koide_parseval", "FRC.Interactions.koide_two_thirds", "FRC.Interactions.koide_extension",
            "FRC.Interactions.koide_half"],
}

LEAN_ONLY = ()                  # the rows with a Lean declaration and no python check (gate G12): none

LEDGER = {"H1": "00:G12", "H2": "00:G11", "H3": "00:G11", "K1": "00:G16", "K2": "00:G16", "K3": "00:G16"}
BLOCKS = {"H": "one generation: the reflection algebra, the fifth direction, the 16 read 3 + 2",
          "K": "the Koide form on the cube-root orbit"}
PREDICATES = {"00:G12": "H1", "00:G11": "H2", "00:G16": "K1"}

R = Registry("00", "interactions", LEDGER, PREDICATES, sources=[__file__])

# the Standard-Model generation by name: (colour rep, weak rep, Y) and its multiplicity
SM = {"nu^c": ("1", "1", Fraction(0)), "u^c": ("3b", "1", Fraction(-2, 3)), "Q": ("3", "2", Fraction(1, 6)),
      "e^c": ("1", "1", Fraction(1)), "L": ("1", "2", Fraction(-1, 2)), "d^c": ("3b", "1", Fraction(1, 3))}
DIM = {"1": 1, "2": 2, "3": 3, "3b": 3}


# ------------------------------------------------------------------------------------------------------------
# block H: one generation (00:G11, 00:G12)
@R.block("H", BLOCKS["H"])
def block_H():
    """Block H — one generation (EXACT): H1–H3."""
    # 00:G12 (p00155)
    basis = range(16)
    def mulvec(x, y):                     # product of algebra elements as dicts index -> coefficient
        out = {}
        for S, a in x.items():
            for T, b in y.items():
                s, U = emul(S, T)
                if s: out[U] = out.get(U, 0) + s * a * b
        return {k: v for k, v in out.items() if v}
    rng = random.Random(12)
    ok = all(mulvec(mulvec({S: 1}, {T: 1}), {U: 1}) == mulvec({S: 1}, mulvec({T: 1}, {U: 1}))
             for S in basis for T in basis for U in basis)
    for _ in range(200):                  # associativity on random elements
        x, y, z = ({S: rng.randrange(-3, 4) for S in basis} for _ in range(3))
        ok &= mulvec(mulvec(x, y), z) == mulvec(x, mulvec(y, z))
    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]))
              for i in range(4) for j in range(4))
    imgs = [fifth(S) for S in basis]
    ok &= sorted(imgs) == gen16() and len(gen16()) == 16
    ok &= all(emul(S, 16) == (1, S | 16) for S in basis if cnt(S, 0, 4) % 2)
    R.check("H1", "the reflection algebra of four directions: 16 basis elements, the product associative on all 4 096 basis "
            "triples and on 200 random elements, distinct directions anticommuting and squaring to zero; the fifth "
            "direction e_S ↦ e_S, e_S e_4 maps the 16 one-to-one onto the even subsets of five directions", ok,
            f"images {imgs}")
    # 00:G11 (p27020)
    g = gen16()
    content = {}
    # the colour type by triality: the centre ω·1 of SU(3) acts on Λᵏ(ℂ³) as ωᵏ, so k ≡ 0, 1, 2 (mod 3) is the
    # singlet, the 3 and the 3̄ (Λ² ≅ 3̄ by the volume form); the weak type by Λᵏ(ℂ²): k = 1 the doublet, else a singlet
    # (the template Λᵏ(ℂⁿ) for the k-th fundamental is imported)
    TRIALITY = {0: "1", 1: "3", 2: "3b"}
    for S in g:
        c, w = col(S), wk(S)
        rep = (TRIALITY[c % 3], {0: "1", 1: "2", 2: "1"}[w], Fraction(y6(S), 6))
        content[rep] = content.get(rep, 0) + 1
    want = {(c, w, y): DIM[c] * DIM[w] for c, w, y in SM.values()}
    ok = content == want
    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))
    ok &= sum(y6(S) for S in g) == 0 and sum(y6(S) ** 3 for S in g) == 0
    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) == 0
    ok &= sorted(Fraction(q6(S), 6) for S in g) == sorted([Fraction(0), Fraction(0)] + [Fraction(2, 3)] * 3 + [Fraction(-2, 3)] * 3
                                                            + [Fraction(-1, 3)] * 3 + [Fraction(1, 3)] * 3 + [Fraction(1), Fraction(-1)])
    R.check("H2", "the 16 read 3 + 2, the colour type by triality (k mod 3 on Λᵏ(ℂ³)) and the weak type by Λᵏ(ℂ²), dimensions "
            "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 "
            "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,
            f"content {dict((f'{k[0]},{k[1]},{k[2]}', v) for k, v in content.items())}")
    # H3 a second method: the anomaly sums by multiplet, from the table
    s1 = sum(DIM[c] * DIM[w] * y for c, w, y in SM.values())
    s3 = sum(DIM[c] * DIM[w] * y ** 3 for c, w, y in SM.values())
    s33 = sum(DIM[w] * y for c, w, y in SM.values() if c != "1")
    s22 = sum(DIM[c] * y for c, w, y in SM.values() if w == "2")
    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",
            s1 == s3 == s33 == s22 == 0 and sum(DIM[c] for c, w, y in SM.values() if w == "2") == 4,
            f"{s1}, {s3}, {s33}, {s22}")


# ------------------------------------------------------------------------------------------------------------
# block K: the Koide form (00:G16)
@R.block("K", BLOCKS["K"])
def block_K():
    """Block K — the Koide form (EXACT): K1–K3."""
    # 00:G16 (p00081)
    bad = []
    for p in [q for q in range(7, 400) if q % 3 == 1 and arith.is_prime(q)]:
        w = next(x for x in range(2, p) if (x * x + x + 1) % p == 0)
        rng = random.Random(p)
        for _ in range(30):
            a = [rng.randrange(p) for _ in range(3)]
            hat, lhs, rhs = koide_rho2(a, p, w)
            if lhs != rhs: bad.append(p)
            if ((lhs - 2 * hat[0] ** 2) % p == 0) != ((2 * hat[1] * hat[2] - hat[0] ** 2) % p == 0): bad.append(p)
    R.check("K1", "every prime p ≡ 1 (mod 3) below 400 with ω² + ω + 1 = 0, 30 random amplitude vectors each: 3 Σ a² = â₀² + "
            "2 â₁â₂ (Q = 1/3 + 2ρ²/3), and 3 Σ a² = 2 â₀² exactly when 2 â₁â₂ = â₀² (Q = 2/3 ⟺ ρ² = 1/2)", not bad,
            f"exceptions {bad[:3]}")
    # K2 a second method: the cube-root orbit a_k = 1 + ρ(z ω^k + z⁻¹ ω^{−k}) in 𝔽_p has Σ a = 3 and Σ a² = 3 + 6ρ²
    bad = []
    for p in [q for q in range(7, 400) if q % 3 == 1 and arith.is_prime(q)]:
        w = next(x for x in range(2, p) if (x * x + x + 1) % p == 0)
        for z in range(1, p, max(1, p // 7)):
            zi = pow(z, -1, p)
            for rho in range(p):
                a = [(1 + rho * (z * pow(w, k, p) + zi * pow(w, -k % 3, p))) % p for k in range(3)]
                if sum(a) % p != 3 % p or sum(x * x for x in a) % p != (3 + 6 * rho * rho) % p: bad.append(p); break
    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 "
            "Σ a² = 3 + 6ρ² for every ρ and seven z, so Q = (3 + 6ρ²)/9 = 1/3 + 2ρ²/3, and Q = 2/3 at ρ² = 1/2",
            not bad, f"exceptions {bad[:3]}")
    # K3 every shell, the Carriers included: in the extension 𝔽_p[w]/(w² + 3), ω = −h + h w (h = 1/2) is a cube root of
    # unity, â₂ = â̄₁, and 3 Σ a² = â₀² + 2 N(â₁) with N(x + y w) = x² + 3 y² (Interactions.lean: koide_extension, koide_half)
    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)
    bad = []
    for p in [q for q in range(5, 400) if q % 3 == 2 and arith.is_prime(q)] + [233, 30089, 2408561]:
        h = (p + 1) // 2
        om = ((-h) % p, h)
        om2 = emul3(om, om, p)
        if ((om2[0] + om[0] + 1) % p, (om2[1] + om[1]) % p) != (0, 0) or emul3(om2, om, p) != (1, 0): bad.append(p); continue
        rng = random.Random(p)
        for _ in range(30):
            a = [rng.randrange(p) for _ in range(3)]
            hat1 = ((a[0] + a[1] * om[0] + a[2] * om2[0]) % p, (a[1] * om[1] + a[2] * om2[1]) % p)
            hat2 = ((a[0] + a[1] * om2[0] + a[2] * om[0]) % p, (a[1] * om2[1] + a[2] * om[1]) % p)
            nrm = (hat1[0] ** 2 + 3 * hat1[1] ** 2) % p
            if hat2 != (hat1[0], (-hat1[1]) % p) or emul3(hat1, hat2, p) != (nrm, 0): bad.append(p); break
            if (3 * sum(x * x for x in a) - sum(a) ** 2 - 2 * nrm) % p: bad.append(p); break
    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 "
            "𝔽_p): in 𝔽_p[w]/(w² + 3), ω = −1/2 + w/2 has ω² + ω + 1 = 0 and ω³ = 1; for 30 random amplitude vectors "
            "â₂ = â̄₁, â₁â₂ = N(â₁), and 3 Σ a² = â₀² + 2 N(â₁)", not bad, f"exceptions {bad[:3]}")

if __name__ == "__main__":
    blocks = [a for a in sys.argv[1:] if a in R.blocks]
    if blocks:
        for b in blocks: R.run_block(b)
        sys.exit(0 if R.summary(write=False) else 1)
    sys.exit(0 if R.verify_all() else 1)