import FrcCore.Theme.Hadrons
import FrcCore.Theme.Fields
import FrcCore.Keys.Hadrons

/-!
# FrcCore.Hadrons — 35-hadrons' paper module (19 October 2026)

The predicate declarations of *Ground-State Light Hadron Spectroscopy over Finite Substrate* (35-hadrons), `FRC.Hadrons.p35NNN`,
one per witnessed row, each the conjunction of the theorems its ledger row cites: the hadrons theme's `Theme/Hadrons.lean`
(the colour group by frames and its centre, the colourless content of the exterior algebra, the meson contraction, the Weyl
constant terms, the Casimir, spin and charge arithmetic, the flavour and isospin relations as ring identities, the admissible
shells, Sturm's count of the finite confinement operator) and the interactions theme's `su3_centre`. The declarations are
generated by `lean/make_predicates.py` from the paper's ledger; the theorems live in the theme files.
-/

namespace FRC.Hadrons

-- Ledger predicates of 35-hadrons (generated by make_predicates.py from docs/35-hadrons/35-hadrons-ledger.json; edit the ledger, not this section)
/-- 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$. -/
theorem 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 :=
  @FRC.Ledger.p35015
/-- 35:C2 (p35016) — Gell-Mann--Okubo $\tfrac12(N+\Xi)=\tfrac14(3\Lambda+\Sigma)$: $2N+2\Xi-3\Lambda-\Sigma=0$ identically, scale-cancelling. -/
theorem 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) :=
  @FRC.Ledger.p35016
/-- 35:C3 (p35017) — Decuplet equal spacing $\Sigma^{*}-\Delta=\Xi^{*}-\Sigma^{*}=\Omega-\Xi^{*}=\beta$: the second differences vanish identically. -/
theorem 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) :=
  @FRC.Ledger.p35017
/-- 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$. -/
theorem 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) :=
  @FRC.Ledger.p35018
/-- 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}}$. -/
theorem 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) :=
  @FRC.Ledger.p35019
/-- 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. -/
theorem 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) :=
  @FRC.Ledger.p35020
/-- 35:C7 (p35021) — Coleman--Glashow $(n-p)+(\Xi^-{-}\Xi^0)=\Sigma^-{-}\Sigma^+$: an exact one-body identity, the two-body electromagnetic term cancelling. -/
theorem p35021 : ∀ {p : Nat} [FRC.Pos p] (δ : FRC.Shell p), δ + δ + -(δ + δ) = (0 : FRC.Shell p) :=
  @FRC.Ledger.p35021
/-- 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$. -/
theorem 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) :=
  @FRC.Ledger.p35022
/-- 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$. -/
theorem 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) :=
  @FRC.Ledger.p35023
/-- 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. -/
theorem 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) :=
  @FRC.Ledger.p35025
/-- 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. -/
theorem 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) :=
  @FRC.Ledger.p35026
/-- 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. -/
theorem 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) :=
  @FRC.Ledger.p35027
/-- 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$. -/
theorem 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) :=
  @FRC.Ledger.p35028
/-- 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$. -/
theorem 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) :=
  @FRC.Ledger.p35029
/-- 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. -/
theorem 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 :=
  @FRC.Ledger.p35030
/-- 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. -/
theorem 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 :=
  @FRC.Ledger.p35031
/-- 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. -/
theorem 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) :=
  @FRC.Ledger.p35032
/-- 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. -/
theorem 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 :=
  @FRC.Ledger.p35033
/-- 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}). -/
theorem 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 :=
  @FRC.Ledger.p35034
/-- 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). -/
theorem 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) :=
  @FRC.Ledger.p35035
/-- 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}). -/
theorem 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) :=
  @FRC.Ledger.p35037
/-- 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$. -/
theorem 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) :=
  @FRC.Ledger.p35038
/-- 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. -/
theorem 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 :=
  @FRC.Ledger.p35039
/-- 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$. -/
theorem 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) :=
  @FRC.Ledger.p35040
/-- 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. -/
theorem 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) :=
  @FRC.Ledger.p35041
/-- 35:X5 (p35042) — \textbf{The decuplet is equally spaced} because the strange seed enters the wrap additively. -/
theorem 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) :=
  @FRC.Ledger.p35042
/-- 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. -/
theorem 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) :=
  @FRC.Ledger.p35043
/-- 35:X7 (p35044) — \textbf{The proton is stable} as the minimal-wrap residue-$1$ state, with no lighter $B=1$ residue to reach. -/
theorem 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) :=
  @FRC.Ledger.p35044
/-- 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. -/
theorem 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) :=
  @FRC.Ledger.p35045
/-- 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. -/
theorem 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) :=
  @FRC.Ledger.p35046
/-- 35:X10 (p35047) — \textbf{The isospin splittings obey Coleman--Glashow} exactly at one body, $(n{-}p)+(\Xi^-{-}\Xi^0)=\Sigma^-{-}\Sigma^+$, a derived identity. -/
theorem p35047 : ∀ {p : Nat} [FRC.Pos p] (δ : FRC.Shell p), δ + δ + -(δ + δ) = (0 : FRC.Shell p) :=
  @FRC.Ledger.p35047
/-- 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. -/
theorem 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) :=
  @FRC.Ledger.p35049
/-- 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. -/
theorem 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 :=
  @FRC.Ledger.p35050
/-- 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. -/
theorem 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) :=
  @FRC.Ledger.p35051
/-- 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. -/
theorem 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) :=
  @FRC.Ledger.p35052
/-- 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. -/
theorem 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) :=
  @FRC.Ledger.p35053
/-- 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. -/
theorem 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) :=
  @FRC.Ledger.p35054
/-- 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. -/
theorem 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) :=
  @FRC.Ledger.p35055
/-- 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. -/
theorem p35056 : ∀ {p : Nat} [FRC.Pos p] (δ : FRC.Shell p), δ + δ + -(δ + δ) = (0 : FRC.Shell p) :=
  @FRC.Ledger.p35056
/-- 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. -/
theorem 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) :=
  @FRC.Ledger.p35058
/-- 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. -/
theorem 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) :=
  @FRC.Ledger.p35059
/-- 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. -/
theorem 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 :=
  @FRC.Ledger.p35060
/-- 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. -/
theorem 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 :=
  @FRC.Ledger.p35061
-- end ledger predicates

end FRC.Hadrons