Hadrons.lean — FrcCore

1import FrcCore.Theme.Hadrons2import FrcCore.Theme.Fields3import FrcCore.Keys.Hadrons45/-!6# FrcCore.Hadrons — 35-hadrons' paper module (19 October 2026)78The predicate declarations of *Ground-State Light Hadron Spectroscopy over Finite Substrate* (35-hadrons), `FRC.Hadrons.p35NNN`,9one per witnessed row, each the conjunction of the theorems its ledger row cites: the hadrons theme's `Theme/Hadrons.lean`10(the colour group by frames and its centre, the colourless content of the exterior algebra, the meson contraction, the Weyl11constant terms, the Casimir, spin and charge arithmetic, the flavour and isospin relations as ring identities, the admissible12shells, Sturm's count of the finite confinement operator) and the interactions theme's `su3_centre`. The declarations are13generated by `lean/make_predicates.py` from the paper's ledger; the theorems live in the theme files.14-/1516namespace FRC.Hadrons1718-- Ledger predicates of 35-hadrons (generated by make_predicates.py from docs/35-hadrons/35-hadrons-ledger.json; edit the ledger, not this section)19/-- 35:C1 (p35015) — Colour $\SU(3,\F_2)$ built exactly: order $216$, centre $\Z_3$ the triality centre; the colour-singlet baryon is the centre-neutral $\varepsilon_{abc}$ invariant $\Lambda^3\mathbf3=\mathbf1$. -/20theorem p35015 : (FRC.Hadrons.unitv.length = (36 : Nat) ∧ FRC.Hadrons.u3.length = (648 : Nat) ∧ FRC.Hadrons.su3.length = (216 : Nat) ∧ (FRC.Hadrons.su3.all fun g => FRC.Interactions.F4.mm (FRC.Interactions.F4.dg g) g == FRC.Interactions.F4.one && FRC.Interactions.F4.det g == FRC.Interactions.F4.o) = true ∧ (List.filter (fun g => FRC.Interactions.F4.mm g FRC.Hadrons.D1 == FRC.Interactions.F4.mm FRC.Hadrons.D1 g && FRC.Interactions.F4.mm g FRC.Hadrons.U1 == FRC.Interactions.F4.mm FRC.Hadrons.U1 g) FRC.Hadrons.su3).length = (3 : Nat) ∧ ((List.filter (fun g => FRC.Interactions.F4.mm g FRC.Hadrons.D1 == FRC.Interactions.F4.mm FRC.Hadrons.D1 g && FRC.Interactions.F4.mm g FRC.Hadrons.U1 == FRC.Interactions.F4.mm FRC.Hadrons.U1 g) FRC.Hadrons.su3).all fun g => g == FRC.Interactions.F4.one || g == FRC.Interactions.F4.w.scal || g == FRC.Interactions.F4.w2.scal) = true ∧ ([FRC.Interactions.F4.o, FRC.Interactions.F4.w, FRC.Interactions.F4.w2].all fun x => FRC.Hadrons.su3.all fun g => FRC.Interactions.F4.mm x.scal g == FRC.Interactions.F4.mm g x.scal) = true) ∧ ([FRC.Interactions.F4.o, FRC.Interactions.F4.w, FRC.Interactions.F4.w2].all fun x => x * x.conj == FRC.Interactions.F4.o && x * x * x == FRC.Interactions.F4.o) = true ∧ (FRC.Interactions.F4.z * FRC.Interactions.F4.z.conj == FRC.Interactions.F4.o) = false ∧ [FRC.Interactions.F4.o, FRC.Interactions.F4.w, FRC.Interactions.F4.w2].length = (3 : Nat) ∧ (2 : Nat) + (1 : Nat) = (3 : Nat) ∧ ([FRC.Interactions.F4.o, FRC.Interactions.F4.w, FRC.Interactions.F4.w2].all fun x => FRC.Interactions.F4.mm x.scal [FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.z] == FRC.Interactions.F4.mm [FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.z] x.scal && FRC.Interactions.F4.mm x.scal [FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.w, FRC.Interactions.F4.z, FRC.Interactions.F4.w2, FRC.Interactions.F4.z, FRC.Interactions.F4.z] == FRC.Interactions.F4.mm [FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.w, FRC.Interactions.F4.z, FRC.Interactions.F4.w2, FRC.Interactions.F4.z, FRC.Interactions.F4.z] x.scal) = true :=21  @FRC.Ledger.p3501522/-- 35:C2 (p35016) — Gell-Mann--Okubo $\tfrac12(N+\Xi)=\tfrac14(3\Lambda+\Sigma)$: $2N+2\Xi-3\Lambda-\Sigma=0$ identically, scale-cancelling. -/23theorem p35016 : ∀ {p : Nat} [FRC.Pos p] (m a c : FRC.Shell p), FRC.Hadrons.octN m a c + FRC.Hadrons.octN m a c + (FRC.Hadrons.octX m a c + FRC.Hadrons.octX m a c) + -(FRC.Hadrons.octL m a c + FRC.Hadrons.octL m a c + FRC.Hadrons.octL m a c) + -FRC.Hadrons.octS m a c = (0 : FRC.Shell p) :=24  @FRC.Ledger.p3501625/-- 35:C3 (p35017) — Decuplet equal spacing $\Sigma^{*}-\Delta=\Xi^{*}-\Sigma^{*}=\Omega-\Xi^{*}=\beta$: the second differences vanish identically. -/26theorem p35017 : ∀ {p : Nat} [FRC.Pos p] (m b : FRC.Shell p), FRC.Hadrons.decD m b + -(FRC.Hadrons.decSs m b + FRC.Hadrons.decSs m b) + FRC.Hadrons.decXs m b = (0 : FRC.Shell p) ∧ FRC.Hadrons.decSs m b + -(FRC.Hadrons.decXs m b + FRC.Hadrons.decXs m b) + FRC.Hadrons.decO m b = (0 : FRC.Shell p) :=27  @FRC.Ledger.p3501728/-- 35:C4 (p35018) — Colour factor of the singlet $\sum_{i<j}\bvec\lambda_i\!\cdot\!\bvec\lambda_j=-8$ ($-\tfrac83$ per pair) from $C_2(\mathbf3)=\tfrac43$, $C_2(\mathbf1)=0$. -/29theorem p35018 : (3 : Int) * (3 : Int) - (1 : Int) = (8 : Int) ∧ (2 : Nat) * (3 : Nat) * (4 : Nat) = (3 : Nat) * (8 : Nat) ∧ (0 : Int) - (3 : Int) * (8 : Int) = (-24 : Int) ∧ (-24 / 12 : Int) = (-2 : Int) ∧ (4 : Int) * (-2 : Int) = (-8 : Int) :=30  @FRC.Ledger.p3501831/-- 35:C5 (p35019) — Spin structure $g_{\mathrm{spin}}=\half S(S+1)-\tfrac98$, octet $-\tfrac34$, decuplet $+\tfrac34$; eigenvalues $+2,-2$; separation $M_{\mathbf{10}}-M_{\mathbf8}=\tfrac32A_{\mathrm{light}}$. -/32theorem p35019 : (1 : Int) * ((1 : Int) + (2 : Int)) - (9 : Int) = (-6 : Int) ∧ (3 : Int) * ((3 : Int) + (2 : Int)) - (9 : Int) = (6 : Int) ∧ (6 : Int) - (-6 : Int) = (12 : Int) ∧ (-8 : Int) * (-6 : Int) = (2 : Int) * (24 : Int) ∧ (-8 : Int) * (6 : Int) = (-2 : Int) * (24 : Int) :=33  @FRC.Ledger.p3501934/-- 35:C6 (p35020) — $A_{\mathrm{light}}=\sig\,c_{\mathrm{mag}}(\beta)$, with $c_{\mathrm{mag}}$ a colour-curvature character sum of the $c_1$ family ($c_1=\beta/18+\cdots$ reproduced); the dimensionless pattern exact, the absolute scale $\Om$-hard. -/35theorem p35020 : FRC.Hadrons.moment6 (1 : Nat) (1 : Nat) = (6 : Int) * (1 : Int) ∧ FRC.Hadrons.moment6 (2 : Nat) (0 : Nat) = (0 : Int) ∧ FRC.Hadrons.moment6 (2 : Nat) (2 : Nat) - FRC.Hadrons.moment6 (1 : Nat) (1 : Nat) = (6 : Int) * (1 : Int) ∧ FRC.Hadrons.moment6 (3 : Nat) (1 : Nat) - FRC.Hadrons.moment6 (2 : Nat) (0 : Nat) = (0 : Int) ∧ (2 : Nat) * (3 : Nat) ^ (2 : Nat) = (18 : Nat) ∧ ((2 : Nat) * (3 : Nat)) ^ (2 : Nat) = (36 : Nat) :=36  @FRC.Ledger.p3502037/-- 35:C7 (p35021) — Coleman--Glashow $(n-p)+(\Xi^-{-}\Xi^0)=\Sigma^-{-}\Sigma^+$: an exact one-body identity, the two-body electromagnetic term cancelling. -/38theorem p35021 : ∀ {p : Nat} [FRC.Pos p] (δ : FRC.Shell p), δ + δ + -(δ + δ) = (0 : FRC.Shell p) :=39  @FRC.Ledger.p3502140/-- 35:C8 (p35022) — The ordering $M_n>M_p$: the $d-u$ seed exceeds the charge-squared electromagnetic term ($\sum Q^2=1$ for $p$, $\tfrac23$ for $n$), fixing $m_d>m_u$. -/41theorem p35022 : (4 : Int) + (4 : Int) + (1 : Int) = (9 : Int) ∧ (4 : Int) + (1 : Int) + (1 : Int) = (6 : Int) ∧ (2 : Int) * (2 : Int) + (2 : Int) * (-1 : Int) + (2 : Int) * (-1 : Int) = (0 : Int) ∧ (2 : Int) * (-1 : Int) + (2 : Int) * (-1 : Int) + (-1 : Int) * (-1 : Int) = (-3 : Int) ∧ (9 : Int) - (6 : Int) = (3 : Int) ∧ (0 : Int) - (-3 : Int) = (3 : Int) ∧ (0 : Int) < (3 : Int) :=42  @FRC.Ledger.p3502243/-- 35:C9 (p35023) — $M_\Sigma>M_\Lambda$: hyperfine fine structure, the light $(ud)$ pair spin-$1$ vs spin-$0$, $M_\Sigma-M_\Lambda=a_{ll}(1-m_l/m_s)>0$. -/44theorem p35023 : (2 : Int) * (0 : Int) * (1 : Int) - (3 : Int) = (-3 : Int) ∧ (2 : Int) * (1 : Int) * (2 : Int) - (3 : Int) = (1 : Int) ∧ (1 : Int) - (-3 : Int) = (4 : Int) ∧ (3 : Int) - (4 : Int) * ((0 : Int) * (1 : Int)) - (3 : Int) = (0 : Int) ∧ (3 : Int) - (4 : Int) * ((1 : Int) * (2 : Int)) - (3 : Int) = (-8 : Int) :=45  @FRC.Ledger.p3502346/-- 35:C11 (p35025) — Second-order decuplet relation $M_\Delta-3M_{\Sigma^*}+3M_{\Xi^*}-M_\Omega=0$ (vanishing third difference), exact in the linear-seed pairwise-hyperfine model. -/47theorem p35025 : ∀ {p : Nat} [FRC.Pos p] (m d a r : FRC.Shell p), FRC.Hadrons.hfD m d a r + -(FRC.Hadrons.hfSs m d a r + FRC.Hadrons.hfSs m d a r + FRC.Hadrons.hfSs m d a r) + (FRC.Hadrons.hfXs m d a r + FRC.Hadrons.hfXs m d a r + FRC.Hadrons.hfXs m d a r) + -FRC.Hadrons.hfO m d a r = (0 : FRC.Shell p) :=48  @FRC.Ledger.p3502549/-- 35:C12 (p35026) — Octet--decuplet hyperfine links $M_\Sigma-M_\Lambda=\tfrac23[(M_\Delta-M_N)-(M_{\Sigma^*}-M_\Sigma)]$ and $M_{\Sigma^*}-M_\Sigma=M_{\Xi^*}-M_\Xi$, parameter-free. -/50theorem p35026 : ∀ {p : Nat} [FRC.Pos p] (m d a r : FRC.Shell p), FRC.Hadrons.hfS m d a r + -FRC.Hadrons.hfL m d a r + (FRC.Hadrons.hfS m d a r + -FRC.Hadrons.hfL m d a r) + (FRC.Hadrons.hfS m d a r + -FRC.Hadrons.hfL m d a r) = FRC.Hadrons.hfD m d a r + -FRC.Hadrons.hfN m d a r + -(FRC.Hadrons.hfSs m d a r + -FRC.Hadrons.hfS m d a r) + (FRC.Hadrons.hfD m d a r + -FRC.Hadrons.hfN m d a r + -(FRC.Hadrons.hfSs m d a r + -FRC.Hadrons.hfS m d a r)) ∧ FRC.Hadrons.hfSs m d a r + -FRC.Hadrons.hfS m d a r + -(FRC.Hadrons.hfXs m d a r + -FRC.Hadrons.hfX m d a r) = (0 : FRC.Shell p) :=51  @FRC.Ledger.p3502652/-- 35:C13 (p35027) — EM splitting structure: one-body $\sum Q_i^2$ and two-body $\sum_{i<j}Q_iQ_j$ exact ($p$: $1,0$; $n$: $\tfrac23,-\tfrac13$); $\Delta_{\mathrm{EM}}=\alpha\,\sig\times$structure, the absolute reducing to the imported $\alpha$ (A9) and $\sig$ (A3), no new residue. -/53theorem p35027 : (4 : Int) + (4 : Int) + (1 : Int) = (9 : Int) ∧ (4 : Int) + (1 : Int) + (1 : Int) = (6 : Int) ∧ (2 : Int) * (2 : Int) + (2 : Int) * (-1 : Int) + (2 : Int) * (-1 : Int) = (0 : Int) ∧ (2 : Int) * (-1 : Int) + (2 : Int) * (-1 : Int) + (-1 : Int) * (-1 : Int) = (-3 : Int) ∧ (9 : Int) - (6 : Int) = (3 : Int) ∧ (0 : Int) - (-3 : Int) = (3 : Int) ∧ (0 : Int) < (3 : Int) :=54  @FRC.Ledger.p3502755/-- 35:C14 (p35028) — $c_{\mathrm{mag}}$ the adjoint (colour-octet) plaquette character sum, $\mathbf8\subset\mathbf3\otimes\bar{\mathbf3}$ ($\mathbf8\not\subset\mathbf3\otimes\mathbf3$), leading $\beta^2/36$ at $O(\beta^2)$, one order finer than the tension $c_1=\beta/18$. -/56theorem p35028 : FRC.Hadrons.moment6 (1 : Nat) (1 : Nat) = (6 : Int) * (1 : Int) ∧ FRC.Hadrons.moment6 (2 : Nat) (0 : Nat) = (0 : Int) ∧ FRC.Hadrons.moment6 (2 : Nat) (2 : Nat) - FRC.Hadrons.moment6 (1 : Nat) (1 : Nat) = (6 : Int) * (1 : Int) ∧ FRC.Hadrons.moment6 (3 : Nat) (1 : Nat) - FRC.Hadrons.moment6 (2 : Nat) (0 : Nat) = (0 : Int) ∧ (2 : Nat) * (3 : Nat) ^ (2 : Nat) = (18 : Nat) ∧ ((2 : Nat) * (3 : Nat)) ^ (2 : Nat) = (36 : Nat) :=57  @FRC.Ledger.p3502858/-- 35:C15 (p35029) — Baryon $=$ Carrier residue $1$: the colourless content of $\Lambda^\bullet(\mathbf3)$ is $(1,0,0,1)$; the baryon is the determinant $\Lambda^3=\det$ at $k=N=3$ (residue $1$, baryon number), forced by the gluon residue $0$ (the fundamental has no invariant vector on $\SU(3,\F_2)$); parallel to photon $2$, gluon $0$. -/59theorem p35029 : FRC.Hadrons.fixed1.length = (0 : Nat) ∧ FRC.Hadrons.fixed2.length = (0 : Nat) ∧ (FRC.Hadrons.su3.all fun g => FRC.Interactions.F4.det g == FRC.Interactions.F4.o) = true ∧ [(1 : Nat), FRC.Hadrons.fixed1.length, FRC.Hadrons.fixed2.length, (1 : Nat)] = [(1 : Nat), (0 : Nat), (0 : Nat), (1 : Nat)] ∧ (1 : Nat) + (3 : Nat) + (3 : Nat) + (1 : Nat) = (2 : Nat) ^ (3 : Nat) :=60  @FRC.Ledger.p3502961/-- 35:C16 (p35030) — Single-scale reduction: $M_H=\sig\,\lambda_H$, the three anchored masses read as one $\Om$-hard scale $\sig$ and three sub-horizon numbers ($\lambda_l$, $m_s/m_l$, $\lambda_{\mathrm{hf}}$); $M_\Lambda-M_N=m_s-m_l$ exact (hyperfine-cancelling); the finite-stage eigenvalues $\varepsilon_k^{(G)}\in\mathrm{Spec}(H^{(N)})$ exact, the decimal Airy values the [approx] readout, $\Om$-stable. -/62theorem p35030 : (FRC.Hadrons.sturm (200 : Nat) (16 : Nat) ((201 : Int) * (256 : Int) * (233 : Int) / (100 : Int)) = (0 : Nat) ∧ FRC.Hadrons.sturm (200 : Nat) (16 : Nat) ((201 : Int) * (256 : Int) * (234 : Int) / (100 : Int)) = (1 : Nat) ∧ FRC.Hadrons.sturm (200 : Nat) (16 : Nat) ((201 : Int) * (256 : Int) * (408 : Int) / (100 : Int)) = (1 : Nat) ∧ FRC.Hadrons.sturm (200 : Nat) (16 : Nat) ((201 : Int) * (256 : Int) * (409 : Int) / (100 : Int)) = (2 : Nat) ∧ FRC.Hadrons.sturm (200 : Nat) (16 : Nat) ((201 : Int) * (256 : Int) * (551 : Int) / (100 : Int)) = (2 : Nat) ∧ FRC.Hadrons.sturm (200 : Nat) (16 : Nat) ((201 : Int) * (256 : Int) * (552 : Int) / (100 : Int)) = (3 : Nat) ∧ FRC.Hadrons.sturm (200 : Nat) (16 : Nat) ((201 : Int) * (256 : Int) * (677 : Int) / (100 : Int)) = (3 : Nat) ∧ FRC.Hadrons.sturm (200 : Nat) (16 : Nat) ((201 : Int) * (256 : Int) * (679 : Int) / (100 : Int)) = (4 : Nat)) ∧ (∀ {p : Nat} [FRC.Pos p] (l s u : FRC.Shell p), FRC.Hadrons.massL l s u + -FRC.Hadrons.massN l s u = s + -l) ∧ ∀ {p : Nat} [FRC.Pos p] (l f : FRC.Shell p), FRC.Hadrons.splitN l f + FRC.Hadrons.splitD l f = l + l + l + l + l + l ∧ FRC.Hadrons.splitD l f + -FRC.Hadrons.splitN l f = f + f + f + f + f + f :=63  @FRC.Ledger.p3503064/-- 35:C17 (p35031) — The baryon scale: the computed finite eigenvalue $E_0\simeq2.232$ (operator $H_G=T_G^{1/2}+R_G$, no baryon mass entering); $M_N=E_0\sig$ predicts the nucleon to $4.6\%$, the absolute prediction carrying the imported $\Om$-hard $\sig$ (A3). $\lambda_l,\lambda_{\mathrm{hf}}$ evaluated forward from $\{N,\beta\}$ (C19), $\Om$-stable. -/65theorem p35031 : ∀ {p : Nat} [FRC.Pos p] (l f : FRC.Shell p), FRC.Hadrons.splitN l f + FRC.Hadrons.splitD l f = l + l + l + l + l + l ∧ FRC.Hadrons.splitD l f + -FRC.Hadrons.splitN l f = f + f + f + f + f + f :=66  @FRC.Ledger.p3503167/-- 35:C18 (p35032) — Meson Carrier residue: the $q\bar q$ colour singlet is the contraction of $\mathbf3\otimes\bar{\mathbf3}=\mathbf1\oplus\mathbf8$ (the Hermitian invariant), residue $1$, $B=0$ (triality $0$); the residue series closes (photon $2$, gluon $0$, baryon $1$, meson $1$); on the same frame the vector-nonet equal spacing $2M_{K^{*}}=M_\rho+M_\phi$ is an exact identity of linear strangeness. -/68theorem p35032 : ((FRC.Hadrons.su3.all fun g => FRC.Interactions.F4.mm (FRC.Interactions.F4.dg g) g == FRC.Interactions.F4.one && FRC.Interactions.F4.det g == FRC.Interactions.F4.o) = true ∧ ((1 : Nat) + (2 : Nat)) % (3 : Nat) = (0 : Nat) ∧ (3 : Nat) % (3 : Nat) = (0 : Nat) ∧ (1 : Nat) % (3 : Nat) = (1 : Nat) ∧ (2 : Nat) % (3 : Nat) = (2 : Nat)) ∧ ∀ {p : Nat} [FRC.Pos p] (a b : FRC.Shell p), FRC.Hadrons.vecKs a b + FRC.Hadrons.vecKs a b + -FRC.Hadrons.vecRho a b + -FRC.Hadrons.vecPhi a b = (0 : FRC.Shell p) :=69  @FRC.Ledger.p3503270/-- 35:C19 (p35033) — Forward constituent eigenvalues: $\lambda_l,\lambda_{\mathrm{hf}}$ computed from $\{N{=}3,\beta\}$ with no measured baryon mass --- $\lambda_{\mathrm{hf}}$ the colour-magnetic contact ($c_{\mathrm{adj}}{=}\beta^2/36$, the exact overlap $|u'(0)|^2{=}1$, $\alpha_s(\sig)$ transmutation-pinned), $\lambda_l$ from $E_0$ and the exact spin split; matching $0.44,0.85$ to constituent-model accuracy, the margin set by the linear-potential approximation. -/71theorem p35033 : ∀ {p : Nat} [FRC.Pos p] (l f : FRC.Shell p), FRC.Hadrons.splitN l f + FRC.Hadrons.splitD l f = l + l + l + l + l + l ∧ FRC.Hadrons.splitD l f + -FRC.Hadrons.splitN l f = f + f + f + f + f + f :=72  @FRC.Ledger.p3503373/-- 35:C20 (p35034) — Residue resolution, second order: the $\SU(3)_F$ residuals (decuplet third difference $6$ MeV, octet $\mathbf{27}$-plet $0.57\%$) are sub-horizon, $O(\varepsilon_s^2)$ of a convergent strange-breaking expansion, $\Om$-stable (Prop.~\ref{prop:subhorizon}). -/74theorem p35034 : (∀ (k : Nat), ((12 : Nat) * k + (5 : Nat) + (1 : Nat)) % (3 : Nat) = (0 : Nat)) ∧ ([(53 : Nat), (173 : Nat), (389 : Nat), (1373 : Nat)].all fun n => n % (12 : Nat) == (5 : Nat) && (n + (1 : Nat)) % (3 : Nat) == (0 : Nat)) = true :=75  @FRC.Ledger.p3503476/-- 35:C21 (p35035) — Residue resolution, electromagnetic: the splitting magnitude $\Delta_{\mathrm{EM}}=\alpha\,\sig\times$[exact charge structure] reduces to the imported $\alpha$ (A9) and $\sig$ (A3), no new residue (C13); Coleman--Glashow and the orderings derived (C7--C9). -/77theorem p35035 : (4 : Int) + (4 : Int) + (1 : Int) = (9 : Int) ∧ (4 : Int) + (1 : Int) + (1 : Int) = (6 : Int) ∧ (2 : Int) * (2 : Int) + (2 : Int) * (-1 : Int) + (2 : Int) * (-1 : Int) = (0 : Int) ∧ (2 : Int) * (-1 : Int) + (2 : Int) * (-1 : Int) + (-1 : Int) * (-1 : Int) = (-3 : Int) ∧ (9 : Int) - (6 : Int) = (3 : Int) ∧ (0 : Int) - (-3 : Int) = (3 : Int) ∧ (0 : Int) < (3 : Int) :=78  @FRC.Ledger.p3503579/-- 35:C23 (p35037) — Residue resolution, hyperfine: the dimensionless $A_{\mathrm{light}}/\sig$ is a ratio of $\Om$-independent character sums (C14), $\Om$-stable, sub-horizon; the absolute $A_{\mathrm{light}}=\sig\,c_{\mathrm{mag}}$ is $\sig$-scaled (A3, Prop.~\ref{prop:subhorizon}). -/80theorem p35037 : ((∀ (k : Nat), ((12 : Nat) * k + (5 : Nat) + (1 : Nat)) % (3 : Nat) = (0 : Nat)) ∧ ([(53 : Nat), (173 : Nat), (389 : Nat), (1373 : Nat)].all fun n => n % (12 : Nat) == (5 : Nat) && (n + (1 : Nat)) % (3 : Nat) == (0 : Nat)) = true) ∧ FRC.Hadrons.moment6 (1 : Nat) (1 : Nat) = (6 : Int) * (1 : Int) ∧ FRC.Hadrons.moment6 (2 : Nat) (0 : Nat) = (0 : Int) ∧ FRC.Hadrons.moment6 (2 : Nat) (2 : Nat) - FRC.Hadrons.moment6 (1 : Nat) (1 : Nat) = (6 : Int) * (1 : Int) ∧ FRC.Hadrons.moment6 (3 : Nat) (1 : Nat) - FRC.Hadrons.moment6 (2 : Nat) (0 : Nat) = (0 : Int) ∧ (2 : Nat) * (3 : Nat) ^ (2 : Nat) = (18 : Nat) ∧ ((2 : Nat) * (3 : Nat)) ^ (2 : Nat) = (36 : Nat) :=81  @FRC.Ledger.p3503782/-- 35:X1 (p35038) — \textbf{The baryon is three quarks} because the only colourless escape from the gluon residue $0$ is the determinant $\Lambda^N=\det$, which requires exactly $N=3$. -/83theorem p35038 : FRC.Hadrons.fixed1.length = (0 : Nat) ∧ FRC.Hadrons.fixed2.length = (0 : Nat) ∧ (FRC.Hadrons.su3.all fun g => FRC.Interactions.F4.det g == FRC.Interactions.F4.o) = true ∧ [(1 : Nat), FRC.Hadrons.fixed1.length, FRC.Hadrons.fixed2.length, (1 : Nat)] = [(1 : Nat), (0 : Nat), (0 : Nat), (1 : Nat)] ∧ (1 : Nat) + (3 : Nat) + (3 : Nat) + (1 : Nat) = (2 : Nat) ^ (3 : Nat) :=84  @FRC.Ledger.p3503885/-- 35:X2 (p35039) — \textbf{The baryon is colour-neutral} as the centre-neutral, triality-$0$ invariant $\varepsilon_{abc}$ of the triality frame, a derived singlet. -/86theorem p35039 : (FRC.Hadrons.unitv.length = (36 : Nat) ∧ FRC.Hadrons.u3.length = (648 : Nat) ∧ FRC.Hadrons.su3.length = (216 : Nat) ∧ (FRC.Hadrons.su3.all fun g => FRC.Interactions.F4.mm (FRC.Interactions.F4.dg g) g == FRC.Interactions.F4.one && FRC.Interactions.F4.det g == FRC.Interactions.F4.o) = true ∧ (List.filter (fun g => FRC.Interactions.F4.mm g FRC.Hadrons.D1 == FRC.Interactions.F4.mm FRC.Hadrons.D1 g && FRC.Interactions.F4.mm g FRC.Hadrons.U1 == FRC.Interactions.F4.mm FRC.Hadrons.U1 g) FRC.Hadrons.su3).length = (3 : Nat) ∧ ((List.filter (fun g => FRC.Interactions.F4.mm g FRC.Hadrons.D1 == FRC.Interactions.F4.mm FRC.Hadrons.D1 g && FRC.Interactions.F4.mm g FRC.Hadrons.U1 == FRC.Interactions.F4.mm FRC.Hadrons.U1 g) FRC.Hadrons.su3).all fun g => g == FRC.Interactions.F4.one || g == FRC.Interactions.F4.w.scal || g == FRC.Interactions.F4.w2.scal) = true ∧ ([FRC.Interactions.F4.o, FRC.Interactions.F4.w, FRC.Interactions.F4.w2].all fun x => FRC.Hadrons.su3.all fun g => FRC.Interactions.F4.mm x.scal g == FRC.Interactions.F4.mm g x.scal) = true) ∧ ([FRC.Interactions.F4.o, FRC.Interactions.F4.w, FRC.Interactions.F4.w2].all fun x => x * x.conj == FRC.Interactions.F4.o && x * x * x == FRC.Interactions.F4.o) = true ∧ (FRC.Interactions.F4.z * FRC.Interactions.F4.z.conj == FRC.Interactions.F4.o) = false ∧ [FRC.Interactions.F4.o, FRC.Interactions.F4.w, FRC.Interactions.F4.w2].length = (3 : Nat) ∧ (2 : Nat) + (1 : Nat) = (3 : Nat) ∧ ([FRC.Interactions.F4.o, FRC.Interactions.F4.w, FRC.Interactions.F4.w2].all fun x => FRC.Interactions.F4.mm x.scal [FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.z] == FRC.Interactions.F4.mm [FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.z] x.scal && FRC.Interactions.F4.mm x.scal [FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.w, FRC.Interactions.F4.z, FRC.Interactions.F4.w2, FRC.Interactions.F4.z, FRC.Interactions.F4.z] == FRC.Interactions.F4.mm [FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.w, FRC.Interactions.F4.z, FRC.Interactions.F4.w2, FRC.Interactions.F4.z, FRC.Interactions.F4.z] x.scal) = true :=87  @FRC.Ledger.p3503988/-- 35:X3 (p35040) — \textbf{Baryon number is the Carrier residue $1$}, the determinant winding, so its conservation is the invariance of $\Lambda^3$, on the same footing as the photon residue $2$ and the gluon residue $0$. -/89theorem p35040 : FRC.Hadrons.fixed1.length = (0 : Nat) ∧ FRC.Hadrons.fixed2.length = (0 : Nat) ∧ (FRC.Hadrons.su3.all fun g => FRC.Interactions.F4.det g == FRC.Interactions.F4.o) = true ∧ [(1 : Nat), FRC.Hadrons.fixed1.length, FRC.Hadrons.fixed2.length, (1 : Nat)] = [(1 : Nat), (0 : Nat), (0 : Nat), (1 : Nat)] ∧ (1 : Nat) + (3 : Nat) + (3 : Nat) + (1 : Nat) = (2 : Nat) ^ (3 : Nat) :=90  @FRC.Ledger.p3504091/-- 35:X4 (p35041) — \textbf{The Gell-Mann--Okubo relation} is exact, the scale-cancelling identity $2N+2\Xi-3\Lambda-\Sigma=0$ of linear flavour breaking, a derived sum rule. -/92theorem p35041 : ∀ {p : Nat} [FRC.Pos p] (m a c : FRC.Shell p), FRC.Hadrons.octN m a c + FRC.Hadrons.octN m a c + (FRC.Hadrons.octX m a c + FRC.Hadrons.octX m a c) + -(FRC.Hadrons.octL m a c + FRC.Hadrons.octL m a c + FRC.Hadrons.octL m a c) + -FRC.Hadrons.octS m a c = (0 : FRC.Shell p) :=93  @FRC.Ledger.p3504194/-- 35:X5 (p35042) — \textbf{The decuplet is equally spaced} because the strange seed enters the wrap additively. -/95theorem p35042 : ∀ {p : Nat} [FRC.Pos p] (m b : FRC.Shell p), FRC.Hadrons.decD m b + -(FRC.Hadrons.decSs m b + FRC.Hadrons.decSs m b) + FRC.Hadrons.decXs m b = (0 : FRC.Shell p) ∧ FRC.Hadrons.decSs m b + -(FRC.Hadrons.decXs m b + FRC.Hadrons.decXs m b) + FRC.Hadrons.decO m b = (0 : FRC.Shell p) :=96  @FRC.Ledger.p3504297/-- 35:X6 (p35043) — \textbf{The decuplet is heavier than the octet} by the colour-magnetic curvature invariant, the colour factor $-8$ times the spin $\half S(S+1)-\tfrac98$, a derived sign and pattern. -/98theorem p35043 : ((1 : Int) * ((1 : Int) + (2 : Int)) - (9 : Int) = (-6 : Int) ∧ (3 : Int) * ((3 : Int) + (2 : Int)) - (9 : Int) = (6 : Int) ∧ (6 : Int) - (-6 : Int) = (12 : Int) ∧ (-8 : Int) * (-6 : Int) = (2 : Int) * (24 : Int) ∧ (-8 : Int) * (6 : Int) = (-2 : Int) * (24 : Int)) ∧ (3 : Int) * (3 : Int) - (1 : Int) = (8 : Int) ∧ (2 : Nat) * (3 : Nat) * (4 : Nat) = (3 : Nat) * (8 : Nat) ∧ (0 : Int) - (3 : Int) * (8 : Int) = (-24 : Int) ∧ (-24 / 12 : Int) = (-2 : Int) ∧ (4 : Int) * (-2 : Int) = (-8 : Int) :=99  @FRC.Ledger.p35043100/-- 35:X7 (p35044) — \textbf{The proton is stable} as the minimal-wrap residue-$1$ state, with no lighter $B=1$ residue to reach. -/101theorem p35044 : FRC.Hadrons.fixed1.length = (0 : Nat) ∧ FRC.Hadrons.fixed2.length = (0 : Nat) ∧ (FRC.Hadrons.su3.all fun g => FRC.Interactions.F4.det g == FRC.Interactions.F4.o) = true ∧ [(1 : Nat), FRC.Hadrons.fixed1.length, FRC.Hadrons.fixed2.length, (1 : Nat)] = [(1 : Nat), (0 : Nat), (0 : Nat), (1 : Nat)] ∧ (1 : Nat) + (3 : Nat) + (3 : Nat) + (1 : Nat) = (2 : Nat) ^ (3 : Nat) :=102  @FRC.Ledger.p35044103/-- 35:X8 (p35045) — \textbf{The neutron is heavier than the proton} because the $d-u$ seed exceeds the charge-squared electromagnetic term ($\sum Q^2=1$ for $p$, $\tfrac23$ for $n$), a derived ordering. -/104theorem p35045 : (4 : Int) + (4 : Int) + (1 : Int) = (9 : Int) ∧ (4 : Int) + (1 : Int) + (1 : Int) = (6 : Int) ∧ (2 : Int) * (2 : Int) + (2 : Int) * (-1 : Int) + (2 : Int) * (-1 : Int) = (0 : Int) ∧ (2 : Int) * (-1 : Int) + (2 : Int) * (-1 : Int) + (-1 : Int) * (-1 : Int) = (-3 : Int) ∧ (9 : Int) - (6 : Int) = (3 : Int) ∧ (0 : Int) - (-3 : Int) = (3 : Int) ∧ (0 : Int) < (3 : Int) :=105  @FRC.Ledger.p35045106/-- 35:X9 (p35046) — \textbf{$\Sigma$ is heavier than $\Lambda$} by the spin-$1$ versus spin-$0$ light-pair hyperfine, a derived splitting of two states of identical quark content. -/107theorem p35046 : (2 : Int) * (0 : Int) * (1 : Int) - (3 : Int) = (-3 : Int) ∧ (2 : Int) * (1 : Int) * (2 : Int) - (3 : Int) = (1 : Int) ∧ (1 : Int) - (-3 : Int) = (4 : Int) ∧ (3 : Int) - (4 : Int) * ((0 : Int) * (1 : Int)) - (3 : Int) = (0 : Int) ∧ (3 : Int) - (4 : Int) * ((1 : Int) * (2 : Int)) - (3 : Int) = (-8 : Int) :=108  @FRC.Ledger.p35046109/-- 35:X10 (p35047) — \textbf{The isospin splittings obey Coleman--Glashow} exactly at one body, $(n{-}p)+(\Xi^-{-}\Xi^0)=\Sigma^-{-}\Sigma^+$, a derived identity. -/110theorem p35047 : ∀ {p : Nat} [FRC.Pos p] (δ : FRC.Shell p), δ + δ + -(δ + δ) = (0 : FRC.Shell p) :=111  @FRC.Ledger.p35047112/-- 35:X12 (p35049) — \textbf{The vector mesons equally space}, $2M_{K^{*}}=M_\rho+M_\phi$, the meson residue $1$ ($B=0$) on the same frame and scale as the baryons. -/113theorem p35049 : (∀ {p : Nat} [FRC.Pos p] (a b : FRC.Shell p), FRC.Hadrons.vecKs a b + FRC.Hadrons.vecKs a b + -FRC.Hadrons.vecRho a b + -FRC.Hadrons.vecPhi a b = (0 : FRC.Shell p)) ∧ (FRC.Hadrons.su3.all fun g => FRC.Interactions.F4.mm (FRC.Interactions.F4.dg g) g == FRC.Interactions.F4.one && FRC.Interactions.F4.det g == FRC.Interactions.F4.o) = true ∧ ((1 : Nat) + (2 : Nat)) % (3 : Nat) = (0 : Nat) ∧ (3 : Nat) % (3 : Nat) = (0 : Nat) ∧ (1 : Nat) % (3 : Nat) = (1 : Nat) ∧ (2 : Nat) % (3 : Nat) = (2 : Nat) :=114  @FRC.Ledger.p35049115/-- 35:X13 (p35050) — \textbf{The spectrum rests on one scale}, $\sqrt\sigma=\LQCD$, the lone $\Om$-hard residue; every dimensionless mass ratio is a sub-horizon eigenvalue. -/116theorem p35050 : (∀ (k : Nat), ((12 : Nat) * k + (5 : Nat) + (1 : Nat)) % (3 : Nat) = (0 : Nat)) ∧ ([(53 : Nat), (173 : Nat), (389 : Nat), (1373 : Nat)].all fun n => n % (12 : Nat) == (5 : Nat) && (n + (1 : Nat)) % (3 : Nat) == (0 : Nat)) = true :=117  @FRC.Ledger.p35050118/-- 35:P1 (p35051) — Gell-Mann--Okubo exact at leading order; PDG $0.57\%$, the bounded $\chi_3^2$ second order. Falsifier: a violation beyond the second-order insertion. -/119theorem p35051 : ∀ {p : Nat} [FRC.Pos p] (m a c : FRC.Shell p), FRC.Hadrons.octN m a c + FRC.Hadrons.octN m a c + (FRC.Hadrons.octX m a c + FRC.Hadrons.octX m a c) + -(FRC.Hadrons.octL m a c + FRC.Hadrons.octL m a c + FRC.Hadrons.octL m a c) + -FRC.Hadrons.octS m a c = (0 : FRC.Shell p) :=120  @FRC.Ledger.p35051121/-- 35:P2 (p35052) — Decuplet equal spacing exact; PDG $9.2\%$ spread, $\beta\simeq146.8$ MeV, the same second order. Falsifier: a non-equal spacing beyond it. -/122theorem p35052 : ∀ {p : Nat} [FRC.Pos p] (m b : FRC.Shell p), FRC.Hadrons.decD m b + -(FRC.Hadrons.decSs m b + FRC.Hadrons.decSs m b) + FRC.Hadrons.decXs m b = (0 : FRC.Shell p) ∧ FRC.Hadrons.decSs m b + -(FRC.Hadrons.decXs m b + FRC.Hadrons.decXs m b) + FRC.Hadrons.decO m b = (0 : FRC.Shell p) :=123  @FRC.Ledger.p35052124/-- 35:P3 (p35053) — The hyperfine pattern $g_{\mathrm{spin}}=\half S(S+1)-\tfrac98$, octet $-\tfrac34$, decuplet $+\tfrac34$, separation $\tfrac32A_{\mathrm{light}}$ with $A_{\mathrm{light}}\simeq195$ MeV. Falsifier: a spin splitting outside this pattern. -/125theorem p35053 : (1 : Int) * ((1 : Int) + (2 : Int)) - (9 : Int) = (-6 : Int) ∧ (3 : Int) * ((3 : Int) + (2 : Int)) - (9 : Int) = (6 : Int) ∧ (6 : Int) - (-6 : Int) = (12 : Int) ∧ (-8 : Int) * (-6 : Int) = (2 : Int) * (24 : Int) ∧ (-8 : Int) * (6 : Int) = (-2 : Int) * (24 : Int) :=126  @FRC.Ledger.p35053127/-- 35:P4 (p35054) — Proton effective stability: the proton is the minimal colour-neutral wrap, with no allowed strong or electromagnetic channel toward a smaller residue; the single neutron transition is one flavour flip, the $\beta$ channel \cite{akhtman2026fields}. Falsifier: an observed proton decay or a strong/electromagnetic baryon-number-violating process. -/128theorem p35054 : FRC.Hadrons.fixed1.length = (0 : Nat) ∧ FRC.Hadrons.fixed2.length = (0 : Nat) ∧ (FRC.Hadrons.su3.all fun g => FRC.Interactions.F4.det g == FRC.Interactions.F4.o) = true ∧ [(1 : Nat), FRC.Hadrons.fixed1.length, FRC.Hadrons.fixed2.length, (1 : Nat)] = [(1 : Nat), (0 : Nat), (0 : Nat), (1 : Nat)] ∧ (1 : Nat) + (3 : Nat) + (3 : Nat) + (1 : Nat) = (2 : Nat) ^ (3 : Nat) :=129  @FRC.Ledger.p35054130/-- 35:P5 (p35055) — No exotic light multiplets beyond the $\mathbf 8$ and $\mathbf{10}$ at leading wrap order. Falsifier: a confirmed light baryon outside the $\mathbf 8$ and $\mathbf{10}$ at the wrap scale. -/131theorem p35055 : FRC.Hadrons.moment6 (3 : Nat) (0 : Nat) = (6 : Int) * (1 : Int) ∧ FRC.Hadrons.moment6 (4 : Nat) (1 : Nat) - FRC.Hadrons.moment6 (3 : Nat) (0 : Nat) = (6 : Int) * (2 : Int) ∧ FRC.Hadrons.moment6 (3 : Nat) (3 : Nat) = (6 : Int) * ((1 : Int) + (2 : Int) ^ (2 : Nat) + (1 : Int)) ∧ (3 : Nat) ^ (3 : Nat) = (10 : Nat) + (8 : Nat) + (8 : Nat) + (1 : Nat) ∧ (8 : Nat) * (7 : Nat) * (6 : Nat) / ((3 : Nat) * (2 : Nat) * (1 : Nat)) = (56 : Nat) ∧ (10 : Nat) * (4 : Nat) + (8 : Nat) * (2 : Nat) = (56 : Nat) :=132  @FRC.Ledger.p35055133/-- 35:P6 (p35056) — Coleman--Glashow exact at one body; PDG $0.79\%$, the residual the two-body electromagnetic term; the orderings $M_n>M_p$ and $M_\Sigma>M_\Lambda$ fixed. Falsifier: a Coleman--Glashow violation beyond the two-body term. -/134theorem p35056 : ∀ {p : Nat} [FRC.Pos p] (δ : FRC.Shell p), δ + δ + -(δ + δ) = (0 : FRC.Shell p) :=135  @FRC.Ledger.p35056136/-- 35:P8 (p35058) — Second-order decuplet relation \eqref{eq:thirddiff}, the vanishing third difference; PDG $6$ MeV ($0.36\%$). Falsifier: a third difference beyond the few-MeV third-order scale. -/137theorem p35058 : ∀ {p : Nat} [FRC.Pos p] (m d a r : FRC.Shell p), FRC.Hadrons.hfD m d a r + -(FRC.Hadrons.hfSs m d a r + FRC.Hadrons.hfSs m d a r + FRC.Hadrons.hfSs m d a r) + (FRC.Hadrons.hfXs m d a r + FRC.Hadrons.hfXs m d a r + FRC.Hadrons.hfXs m d a r) + -FRC.Hadrons.hfO m d a r = (0 : FRC.Shell p) :=138  @FRC.Ledger.p35058139/-- 35:P9 (p35059) — Vector-meson nonet equal spacing $2M_{K^{*}}=M_\rho+M_\phi$ (PDG $0.42\%$) and ideal mixing $M_\omega\simeq M_\rho$; $\rho,\phi$ anchor, $K^{*},\omega$ predicted $<1\%$; the pseudoscalars are Goldstone bosons (a distinct chiral mechanism). Falsifier: a vector nonet off the linear-strangeness pattern. -/140theorem p35059 : ∀ {p : Nat} [FRC.Pos p] (a b : FRC.Shell p), FRC.Hadrons.vecKs a b + FRC.Hadrons.vecKs a b + -FRC.Hadrons.vecRho a b + -FRC.Hadrons.vecPhi a b = (0 : FRC.Shell p) :=141  @FRC.Ledger.p35059142/-- 35:P10 (p35060) — Absolute octet$+$decuplet spectrum from the $\Om$-hard scale $\sig$ and three sub-horizon eigenvalues ($\lambda_l$, $m_s/m_l$, $\lambda_{\mathrm{hf}}$, the two constituent ratios computed forward, C19): five parameter-free predictions within $1.1\%$ (Table~\ref{tab:absolute}). Falsifier: a predicted mass off beyond the traced second order. -/143theorem p35060 : (∀ {p : Nat} [FRC.Pos p] (l f : FRC.Shell p), FRC.Hadrons.splitN l f + FRC.Hadrons.splitD l f = l + l + l + l + l + l ∧ FRC.Hadrons.splitD l f + -FRC.Hadrons.splitN l f = f + f + f + f + f + f) ∧ ∀ {p : Nat} [FRC.Pos p] (l s u : FRC.Shell p), FRC.Hadrons.massL l s u + -FRC.Hadrons.massN l s u = s + -l :=144  @FRC.Ledger.p35060145/-- 35:P11 (p35061) — The $\Lambda$--$N$ gap is the strange constituent excess, $M_\Lambda-M_N=m_s-m_l=176.8$ MeV, hyperfine- and scale-free \eqref{eq:lamn}. Falsifier: a gap inconsistent with the strange seed and the $\Xi,\Sigma$ splittings. -/146theorem p35061 : ∀ {p : Nat} [FRC.Pos p] (l s u : FRC.Shell p), FRC.Hadrons.massL l s u + -FRC.Hadrons.massN l s u = s + -l :=147  @FRC.Ledger.p35061148-- end ledger predicates149150end FRC.Hadrons151