flavour.py — frc/ledgers/master

1"""master/flavour — a ledger file of the master's rows G15, G17 and P3, the flavour rows the flavour theme proves2(28-flavour's migration, 17 October 2026; the author's decision D7 of its blueprint).34The master's block G is bound by several files, one per theme whose key file proves its rows (task LM25): the5interactions file binds G11, G12 and G16, this file binds G15 (flavour, structure) and G17 (flavour, exact ratios), and6the prediction row P3 (flavour, targets) from docs/predictions.json (BLOCK = "GP"). It holds the table of keys7(generated from docs/00-ledger.json and docs/predictions.json by ci/make_ledgers.py), the Lean proofs each core key8conjoins (PROOFS: G15, G17), the Mathlib theorems P3's key conjoins (CHART), and the checks, which call the flavour9theme (frc/flavour.py), the horizon theme (frc/ladder.py) and the chart theme (frc/chart_flavour.py). The Lean side is10lean/FrcCore/Theme/Flavour.lean and lean/FrcLedger/Theme/Flavour.lean, the key files lean/FrcCore/Keys/Flavour.lean and11lean/FrcLedger/Keys/Chart.lean, the certificates lean/FrcCore/Ledgers/Master/Flavour.lean and12lean/FrcLedger/Ledgers/Master/Flavour.lean. The paper's own checks are frc/ledgers/p28_flavour.py.1314    python3 -m frc.ledgers.master.flavour        every block, the census; exit 1 if a check fails15    python3 -m frc.ledgers.master.flavour F      one block (F, R or T)1617Blocks:  F  flavour, structure: the seesaw's transpose fixed point and the closed role ladder     EXACT  (00:G15)18         R  flavour, exact ratios: the norms, the colour count, the magic matrix, the texture      EXACT  (00:G17)19         T  flavour, targets: the double ratio and the m₁ = 0 floor                                CHART  (00:P3)2021The notebook frc/ledgers/master/flavour.ipynb runs one row per cell, the cell's id its key (gate G13).22"""23import random24import sys25from fractions import Fraction as Q2627from frc.registry import Registry28from frc import arith29from frc import flavour as FL30from frc import ladder as LD31from frc import chart_flavour as CFL3233# ---- generated by ci/make_ledgers.py from docs/00-ledger.json and docs/predictions.json; edit the ledger, not this table ----34BLOCK = "GP"35KEYS = {"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", "P1": "p00133", "P2": "p00061", "P3": "p00180", "P4": "p00091"}       # every row of the blocks: its label and its accession key36LEAN = {"G15": "core", "G17": "core", "P3": "ml"}       # the rows with a Lean declaration: the libraries whose key files prove them37# ---- end of the generated table ----3839# The Lean proofs of the rows' keys: the theorems of the themes that each core key conjoins (lean/make_keys.py writes40# the keys FRC.Ledger.p<key> from them).41PROOFS = {42    "G15": ["FRC.Flavour.transpose_fixed_point", "FRC.Flavour.seesaw_circulant", "FRC.Interactions.koide_two_thirds",43            "FRC.Ladder.tower_reduces"],44    "G17": ["FRC.Interactions.koide_two_thirds", "FRC.Flavour.norm_one_sub_i", "FRC.Flavour.norm_one_sub_omega",45            "FRC.Flavour.colour_count", "FRC.Flavour.trimaximal", "FRC.Flavour.jarlskog_sq", "FRC.Flavour.texture_exponents",46            "FRC.Flavour.trace_double", "FRC.Flavour.trace_triple"],47}4849# The Mathlib theorems of P3's key: the chart clauses it conjoins (the readings of measured data).50CHART = {51    "P3": ["FRC.FlavourML.gj_ratio", "FRC.FlavourML.neutrino_floor"],52}5354LEAN_ONLY = ()                  # the rows with a Lean declaration and no python check (gate G12): none5556LEDGER = {"F1": "00:G15", "F2": "00:G15", "R1": "00:G17", "R2": "00:G17", "T1": "00:P3"}57BLOCKS = {"F": "flavour, structure: the seesaw's transpose fixed point and the closed role ladder",58          "R": "flavour, exact ratios: the norms, the colour count, the magic matrix, the texture",59          "T": "flavour, targets: the double ratio and the m₁ = 0 floor"}60PREDICATES = {"00:G15": "F1", "00:G17": "R1", "00:P3": "T1"}6162R = Registry("00", "flavour", LEDGER, PREDICATES, sources=[__file__])63RNG = random.Random(17)64SHELLS = (17, 53, 89)656667def _within(x, centre, tol): return abs(Q(x) - Q(centre)) < Q(tol)686970# ------------------------------------------------------------------------------------------------------------71# block F: flavour, structure (00:G15)72@R.block("F", BLOCKS["F"])73def block_F():74    """Block F — flavour, structure (EXACT): F1, F2."""75    # F1 the seesaw fixes Q_ν = 2/3: with M_R = c m_D the seesaw collapses to c² det(m_D) m_Dᵀ (20 random rational76    #    circulants), the transpose circulant has the Dirac eigenvalues, and the signed Koide identity holds for them77    ok = True78    for _ in range(20):79        mD = FL.random_circ(RNG); c = Q(RNG.randint(1, 9), RNG.randint(1, 5))80        ok &= FL.transpose_fixed_point(c, mD) and FL.seesaw_closure(mD, FL.random_circ(RNG))[0]81        a, b = FL.QOmega(Q(RNG.randint(1, 9))), FL.QOmega(Q(RNG.randint(-9, 9), RNG.randint(1, 5)), Q(RNG.randint(-9, 9), RNG.randint(1, 5)))82        ok &= FL.transpose_eigen(a, b, b.conj())83        lam = [l.x for l in FL.eigenvalues(a, b, b.conj())]84        ok &= (3 * sum(x * x for x in lam) == 2 * sum(lam) ** 2) == (2 * b.norm() == a.x * a.x)85    for p in SHELLS:                                                          # the Dirac amplitude: Q = 2/3 exactly on the shells86        S = FL.Shell(p); ok &= S.koide_point(1, Q(1, 2))[1] == S.frac(Q(2, 3))87    # 00:G15 (p00080)88    R.check("F1", "the seesaw fixes Q_ν = 2/3: with M_R = c m_D (the 126 alignment) the seesaw m_D·adj(M_R)·m_Dᵀ is c² det(m_D) m_Dᵀ, "89            "whose eigenvalues are the Dirac eigenvalues λ_{−k} (20 random rational circulants), so the colourless Dirac amplitude "90            "2N(b) = a², Q = 2/3 exact on F_17, F_53, F_89, is the neutrinos' (the transpose fixed point)", ok,91            "the seesaw of circulants is circulant; the amplitude is preserved, the phase reset")9293    # F2 the role-ladder ordering and the mixing's reduction: the ladder of roles closes on F_13, F_53, F_157, F_421 (no94    #    fifth role; the three generative roles the generations), the role depths (2, 1, 0) give the texture exponents,95    #    and the trimaximal column is the protected one96    ok = True97    for p in (13, 53, 157, 421):98        g, n = arith.primitive_root(p), p - 199        ok &= all(LD.tower(g, j, p)[0] == LD.tower(g, j, p)[1] for j in range(n)) and any(pow(g, j, p) >= n for j in range(n))100    down, up, Ed, Eu = FL.texture_exponents(); v, u, notprop = FL.protected_column()101    ok &= down == (4, 2, 0) and up == (8, 4, 0) and v and u and notprop102    R.check("F2", "the role-ladder ordering and the mixing's reduction: the tower g^(g^j) is read modulo p − 1 on F_13, F_53, F_157, "103            "F_421 (the ladder closes, three generative roles), the depths (2, 1, 0) give the exponents (4, 2, 0) and (8, 4, 0) of "104            "the role-depth texture, and the shift fixes the trimaximal column (1, 1, 1) alone", ok, "the mixing reduces to the "105            "texture, the lopsided entry and the protected column; the phases stay Ω-hard (Z6)")106107108# ------------------------------------------------------------------------------------------------------------109# block R: flavour, exact ratios (00:G17)110@R.block("R", BLOCKS["R"])111def block_R():112    """Block R — flavour, exact ratios (EXACT): R1, R2."""113    # R1 Koide 2/3 and the norms: Q = 2/3 ⟺ 2N(b) = a² and N(1 − i) = 2, N(1 − ω) = 3 on the shells; the colour count 3;114    #    the magic matrix trimaximal with J² = 1/108 in Q(ω) and 4(−νh²) = 3 in F_p115    ok = all(FL.norms_two_three(p) and FL.jarlskog_framed(p) for p in SHELLS)116    for p in SHELLS:117        S = FL.Shell(p); ok &= S.koide_point(1, Q(1, 2))[1] == S.frac(Q(2, 3)) and S.koide_point(1, Q(3, 4))[1] == S.frac(Q(5, 6))118    dc, ec, nine = FL.colour_count(); tri, q, J2 = FL.magic_matrix()119    ok &= (dc, ec, nine) == (3, 1, 9) and tri and q and J2 == Q(1, 108)120    # 00:G17 (p00179)121    R.check("R1", "the exact ratios: Q = 2/3 exactly at 2N(b) = a² and Q = 5/6 at 4N(b) = 3a² on F_17, F_53, F_89; the squared "122            "amplitudes N(1 − i) = 2 and N(1 − ω) = 3; the Georgi–Jarlskog factor the colour count 3 against 1 on the sixteen; the "123            "magic matrix trimaximal with J² = 1/108 in Q(ω) and 4(−νh²) = 3 in F_p", ok,124            "the split and non-split norms, the colour triplet, the cube-root phase")125126    # R2 the λ-texture from role depths and the locks: the exponents (4, 2, 0), (8, 4, 0); the lock relations as trace127    #    identities on every unit of F_{p²}128    down, up, Ed, Eu = FL.texture_exponents()129    ok = down == (4, 2, 0) and up == (8, 4, 0) and all(FL.trace_relations(p) for p in SHELLS)130    R.check("R2", "the λ-texture from the role depths (2, 1, 0): the exponents (4, 2, 0) and (8, 4, 0); the charged sectors' lock "131            "1 : 1/2 : 1/3 as the trace relations T(z²) = T(z)² − 2, T(z³) = T(z)³ − 3T(z) of a unit, exhaustive on F_{17²}, F_{53²}, "132            "F_{89²}", ok, "c_ℓ = 2c_d² − 1 = 4c_u³ − 3c_u between the cube invariants")133134135# ------------------------------------------------------------------------------------------------------------136# block T: flavour, targets (00:P3)137@R.block("T", BLOCKS["T"])138def block_T():139    """Block T — flavour, targets (CHART): T1."""140    gj, msd, btau = CFL.gj_double_ratio(); tot, m2, m3 = CFL.neutrino_floor(); dl, dd, du, dup = CFL.phase_lock()141    ok = _within(gj, "10.34", "0.02") and Q("0.10") < Q(gj) / 9 - 1 < Q("0.20") and _within(tot, "58.8", "0.05")142    ok &= _within(Q(dd) / Q(dl), "0.496", "0.002") and _within(Q(du) / Q(dl), "0.335", "0.002")143    # 00:P3 (p00180)144    R.check("T1", "[chart] the flavour targets: the Georgi–Jarlskog double ratio 10.34 against 9 (the open 15 % excess, between 10 % "145            "and 20 %); the m₁ = 0 floor Σm_ν = 58.8 meV at NuFIT 6.0; the locks 0.496 and 0.335 in the MS-bar working scheme", ok,146            f"double ratio {gj:.2f}, floor {tot:.1f} meV, locks {dd / dl:.3f}, {du / dl:.3f}", kind="CHART")147148149if __name__ == "__main__":150    want = [a.upper() for a in sys.argv[1:]] or sorted(BLOCKS)151    bad = [b for b in want if b not in BLOCKS]152    if bad: sys.exit(f"no block {', '.join(bad)}: the blocks are {', '.join(sorted(BLOCKS))}")153    for b in want: R.run_block(b)154    sys.exit(0 if R.summary(write=False, expect=list(LEDGER) if want == sorted(BLOCKS) else None) else 1)155