hadrons.py — frc/ledgers/master

1"""master/hadrons — a ledger file of the master's block G, the hadron rows: the rows the hadrons theme proves (the master's2witnesses, 19 October 2026).34The master's hadron rows of block G are bound by this file (the hadrons theme above the interactions theme's colour5sector). It binds G8 (the hadron spectrum: the baryon as the centre-neutral triality invariant and the SU(3)_F relations6as scale-cancelling identities), G9 (the residue series: baryon 1, meson 1, with photon 2 and gluon 0) and G10 (the7baryon scale: the exact spin split and Λ–N gap, the finite-stage eigenvalues exact by Sturm's count, the computed8eigenvalue E₀ read against the nucleon): the table of keys (generated from docs/00-ledger.json by ci/make_ledgers.py),9the Lean proofs each key conjoins (PROOFS), and the checks, which call the hadrons theme (frc/hadrons.py) and, for the10readings of G10, the chart theme (frc/chart_hadrons.py). The Lean side is lean/FrcCore/Theme/Hadrons.lean, the key file11lean/FrcCore/Keys/Hadrons.lean and the certificate lean/FrcCore/Ledgers/Master/Hadrons.lean. G10 is a T row of block G,12so its key is the core's (its chart readings stay the row's confrontation, decided here in the python check alone; gate G08).1314    python3 -m frc.ledgers.master.hadrons        every block, the census; exit 1 if a check fails (≈ 4 s)1516Blocks:  S  the hadron spectrum: the colour frame, the identities, the colour–spin–charge arithmetic   EXACT  (00:G8)17         R  the residue series: baryon 1 by the determinant, meson 1 by the contraction            EXACT  (00:G9)18         B  the baryon scale: the exact split and gap, Sturm's count, E₀ against the nucleon        CHART  (00:G10)1920The notebook frc/ledgers/master/hadrons.ipynb runs one row per cell, the cell's id its key (gate G13).21"""22import sys23from fractions import Fraction as Q24from math import comb2526from frc.registry import Registry27from frc import interactions as I28from frc import hadrons as H29from frc import chart_hadrons as CH3031# ---- generated by ci/make_ledgers.py from docs/00-ledger.json; edit the ledger, not this table ----32BLOCK = "G"33KEYS = {"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 key34LEAN = {"G8": "core", "G9": "core", "G10": "core"}       # the rows with a Lean declaration: the libraries whose key files prove them35# ---- end of the generated table ----3637# The Lean proofs of the rows' keys: the theorems of the themes that each key conjoins (lean/make_keys.py writes the keys38# 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.39PROOFS = {40    "G8": ["FRC.Hadrons.colour_group", "FRC.Hadrons.colourless_content", "FRC.Hadrons.gmo", "FRC.Hadrons.spacing",41           "FRC.Hadrons.coleman_glashow", "FRC.Hadrons.charge_structure", "FRC.Hadrons.sigma_lambda",42           "FRC.Hadrons.vector_spacing", "FRC.Hadrons.spin_pattern", "FRC.Hadrons.colour_factor",43           "FRC.Hadrons.adjoint_channel"],            # 35:C1, C15, C2, C3, C7, C8, C9, C18, C5, C4, C6/C14; heavy-quark symmetry (35:C10) is a Mathlib reading, no core clause44    "G9": ["FRC.Hadrons.colourless_content", "FRC.Hadrons.meson_invariant"],                       # 35:C15, 35:C1845    "G10": ["FRC.Hadrons.spin_split", "FRC.Hadrons.lambda_n_gap", "FRC.Hadrons.airy_sturm"],      # 35:C17, C19, C16: the exact clauses of the baryon scale46}4748LEAN_ONLY = ()                  # the rows with a Lean declaration and no python check (gate G12): none4950LEDGER = {"S1": "00:G8", "S2": "00:G8", "S3": "00:G8", "R1": "00:G9", "B1": "00:G10", "B2": "00:G10"}51BLOCKS = {"S": "the hadron spectrum: the colour frame, the identities, the colour–spin–charge arithmetic",52          "R": "the residue series: baryon 1 by the determinant, meson 1 by the contraction",53          "B": "the baryon scale: the exact split and gap, Sturm's count, E₀ against the nucleon"}54PREDICATES = {"00:G8": "S1", "00:G9": "R1", "00:G10": "B1"}5556R = Registry("00", "hadrons", LEDGER, PREDICATES, sources=[__file__])575859def _within(x, centre, tol):60    return abs(Q(x) - Q(centre)) < Q(tol)616263def _between(x, lo, hi):64    return Q(lo) < Q(x) < Q(hi)656667# ------------------------------------------------------------------------------------------------------------68# block S: the hadron spectrum (00:G8)69@R.block("S", BLOCKS["S"])70def block_S():71    """Block S — the hadron spectrum (EXACT): S1 the frame and the identities, S2 the arithmetic, S3 the hyperfine channel."""72    # 00:G8 (p00073)73    F, G = H.colour_group()74    scal = H.colour_scalars(F); cen = H.centre(F, G); content = H.colourless_content(F, G)75    frame = len(G) == 216 and sorted(cen) == sorted(scal) and len(scal) == 3 and content == (1, 0, 0, 1) and H.triality(3, 0) == 076    gmo = H.gmo_vector(); d1, d2 = H.spacing_vectors(); cg = H.coleman_glashow(); v = H.vector_spacing()77    identities = gmo.is_zero() and d1.is_zero() and d2.is_zero() and cg.is_zero() and v.is_zero()78    qp = [H.QUARK_CHARGE[q] for q in "uud"]; qn = [H.QUARK_CHARGE[q] for q in "udd"]79    (op, tp), (on, tn) = H.charge_structure(qp), H.charge_structure(qn)80    pc = H.pair_correlators()81    orderings = (op, tp) == (1, 0) and (on, tn) == (Q(2, 3), Q(-1, 3)) and op > on                   # M_n > M_p: the charge structure, m_d > m_u82    orderings &= pc["ud_spin1"] - pc["ud_spin0"] == 1 and pc["s_pair_sigma"] - pc["s_pair_lambda"] == -1    # M_Σ > M_Λ: a_ll(1 − m_l/m_s) > 083    R.check("S1", "the hadron spectrum's exact content: a baryon is the centre-neutral triality invariant of SU(3, F_2) — the group "84            "built exactly over F_4 (216 elements, the centre the three scalars, Z_3) with the colourless content (1, 0, 0, 1) of "85            "Λ•(3), the determinant the one invariant (triality 0); the SU(3)_F mass relations are zero polynomials in their "86            "parameters, scale-cancelling: Gell-Mann–Okubo 2N + 2Ξ − 3Λ − Σ, the decuplet's two second differences, "87            "Coleman–Glashow (n − p) + (Ξ⁻ − Ξ⁰) − (Σ⁻ − Σ⁺), the vector nonet's 2K* − ρ − φ; the orderings M_n > M_p (the "88            "charge structure Σ Q² = 1 against 2/3, two-body 0 against −1/3) and M_Σ > M_Λ (the light pair's S_u·S_d +1/4 "89            "against −3/4, the strange coupling −1 against 0, M_Σ − M_Λ = a_ll(1 − m_l/m_s) > 0)",90            frame and identities and orderings,91            f"|SU(3, 2)| = {len(G)}, content {content}; GMO {gmo}, spacing {d1}, {d2}, CG {cg}, nonet {v}; p ({op}, {tp}), n ({on}, {tn})")92    c2, sTT, sll, per = H.colour_factor(); e8, e10, sep, de = H.hyperfine_eigenvalues()93    ok = c2 == Q(4, 3) and sTT == -2 and sll == -8 and per == Q(-8, 3)94    ok &= H.g_spin(1) == Q(-3, 4) and H.g_spin(3) == Q(3, 4) and sep == Q(3, 2) and e8 == 2 and e10 == -2 and de == -495    R.check("S2", "the colour–spin arithmetic of the hyperfine: the singlet's colour factor Σ λ_i·λ_j = −8 (−8/3 per pair) from "96            "C₂(3) = 4/3 and C₂(1) = 0; g_spin = ½S(S+1) − 9/8 is −3/4 on the octet and +3/4 on the decuplet, the separation 3/2; "97            "the eigenvalues of Σ(λ·λ)(S·S) on the singlet +2 and −2: M_10 − M_8 = (3/2)A_light, the decuplet heavier", ok,98            f"C₂ = {c2}, Σλ·λ = {sll}; g = {H.g_spin(1)}, {H.g_spin(3)}; eigenvalues {e8}, {e10}")99    E, c = H.weyl_moments(); c1, cadj = H.character_coefficients(3)100    ok = c["adjoint_in_3x3bar"] == 1 and c["adjoint_in_3x3"] == 0 and c["singlet_3x3bar"] == 1 and c["singlet_3x3"] == 0101    ok &= c1 == Q(1, 18) and cadj == Q(1, 36) and E[(1, 1)] == 1 and E[(2, 0)] == 0 and E[(2, 2)] == 2 and E[(3, 1)] == 0102    R.check("S3", "the decuplet–octet hyperfine is the colour-magnetic curvature invariant: by the Weyl constant terms the adjoint 8 "103            "sits once in 3 ⊗ 3̄ (E[χ²χ̄²] − E[χχ̄] = 1) and not in 3 ⊗ 3 (E[χ³χ̄] − E[χ²] = 0), so A_light = √σ c_mag(β) enters at "104            "O(β²) with c_adj = β²/36, the spin-2 partner of the tension's c₁ = β/18 (G5); the dimensionless pattern exact, the "105            "scale √σ the imported Ω-hard one", ok, f"moments {dict((k, v) for k, v in E.items() if k in [(1, 1), (2, 0), (2, 2), (3, 1)])}; c₁ {c1} β, c_adj {cadj} β²")106107108# ------------------------------------------------------------------------------------------------------------109# block R: the residue series (00:G9)110@R.block("R", BLOCKS["R"])111def block_R():112    """Block R — the residue series (EXACT): R1."""113    # 00:G9 (p00074)114    F, G = H.colour_group()115    content = H.colourless_content(F, G); E, c = H.weyl_moments()116    ok = content == (1, 0, 0, 1) and [comb(3, k) for k in range(4)] == [1, 3, 3, 1]           # no invariant vector of 3: the gluon's frame leaves a quark residue 0117    ok &= all(I.det(F, g) == F.one for g in G) and H.hermitian_invariant(F, G)                    # Λ³ = det fixed by every element; g†g = I: the q q̄ contraction invariant118    ok &= c["singlet_3x3bar"] == 1 and c["singlet_3x3"] == 0 and H.triality(3, 0) == 0 and H.triality(1, 1) == 0 and H.triality(1, 0) == 1119    R.check("R1", "the residue series closes: on SU(3, F_2) no nonzero vector of the fundamental is fixed (residue 0 for a single "120            "quark, the gluon frame's), none of Λ²(3), and Λ³(3) = det is fixed by every element — the baryon is the Carrier "121            "residue 1 at k = N = 3, forced; g†g = I on every element makes the q q̄ contraction the one invariant of 3 ⊗ 3̄ "122            "(E[χχ̄] = 1, E[χ²] = 0) — the meson is residue 1 with triality 1 + 2 ≡ 0, B = 0; with the photon's 2 and the "123            "gluon's 0 (G1, G4) the series is photon 2, gluon 0, baryon 1, meson 1; the stability selector is the "124            "realisation 35:B5", ok, f"content {content}, E[χχ̄] = {E[(1, 1)]}, E[χ²] = {E[(2, 0)]}")125126127# ------------------------------------------------------------------------------------------------------------128# block B: the baryon scale (00:G10)129@R.block("B", BLOCKS["B"])130def block_B():131    """Block B — the baryon scale: B1 chart (the exact clauses inside it), B2 the exact brackets."""132    # 00:G10 (p00075)133    gap = H.gap_identity(); s1, s2 = H.spin_split()134    exact = gap.is_zero() and s1.is_zero() and s2.is_zero()                                     # M_Λ − M_N = m_s − m_l; (M_N + M_Δ)/6 = λ_l, M_Δ − M_N = (3/2)λ_hf135    fl = CH.forward_landing(); ss = CH.single_scale(); t = CH.DATA["targets"]136    E0, E1 = fl["E0"], fl["E1"]; s = CH.DATA["scales"]["sqrt_sigma"]; mN = CH.pdg()["N"]137    MN_pred = Q(E0) * s; excess = (MN_pred - mN) / mN138    scale = _within(E0, "2.232", "0.001") and _between(MN_pred, "981", "983") and _between(excess, "0.045", "0.047")139    anchors = _between(ss["lam_l"], "0.822", "0.8224") and _between(ss["ms_over_ml"], "1.488", "1.489") and _between(ss["lam_hf"], "0.444", "0.4441")140    forward = abs(Q(fl["hf"]["lam_hf"]) - t["lam_hf"]) / t["lam_hf"] < Q("0.07") and abs(Q(fl["lam_l_fwd"]) - t["lam_l"]) / t["lam_l"] < Q("0.07")141    forward &= _between(fl["alpha_s"], "1.00", "1.01") and _within(fl["contact_nr"], 1, "0.002")142    R.check("B1", "[chart] the baryon scale: the spectrum is the Ω-hard √σ times sub-horizon numbers — the three anchored masses "143            "read as λ_l = 0.822, m_s/m_l = 1.489, λ_hf = 0.444 at √σ = 440 MeV, with M_Λ − M_N = m_s − m_l and the spin split "144            "inverting as exact identities; the baryon mass over scale is the computed finite eigenvalue E₀ = 2.232 of "145            "H = |p| + r on N = 600 sites, no baryon mass entering, M_N = E₀√σ = 982 MeV, 4.6 % above the nucleon; λ_l and λ_hf "146            "evaluated forward from {N = 3, β} (the contact |u'(0)|² → 1, α_s(√σ) = 2π/(9 ln 2) = 1.007) land within 7 % of the "147            "anchors: the light spectrum is parameter-free over √σ, no new Ω-hard residue",148            exact and scale and anchors and forward,149            f"E₀ = {CH.fmt(E0, 4)}, M_N = {CH.fmt(MN_pred, 0)} MeV ({CH.fmt(Q(excess) * 100, 1)} %); forward λ_hf {CH.fmt(fl['hf']['lam_hf'], 3)}, λ_l {CH.fmt(fl['lam_l_fwd'], 3)}",150            kind="CHART")151    br = [("2.33", "2.34"), ("4.08", "4.09"), ("5.51", "5.52"), ("6.77", "6.79")]152    counts = H.sturm_brackets(400, 20, br)153    R.check("B2", "the finite-stage eigenvalues are exact: Sturm's count of the tridiagonal H^(N) = −u'' + x u on N = 400 sites of "154            "[0, 20], in exact rational arithmetic, places exactly one eigenvalue in each of (2.33, 2.34), (4.08, 4.09), "155            "(5.51, 5.52) and (6.77, 6.79): the decimal Airy values are the [approx] readout of an exact finite spectrum",156            counts == [(k, k + 1) for k in range(4)], f"counts at the bracket ends {counts}")157158159if __name__ == "__main__":160    blocks = [a for a in sys.argv[1:] if a in R.blocks]161    if blocks:162        for b in blocks: R.run_block(b)163        sys.exit(0 if R.summary(write=False) else 1)164    sys.exit(0 if R.verify_all() else 1)165