import Mathlib
import FrcLedger.Theme.Hadrons
import FrcLedger.Keys.Hadrons

/-!
# 35-hadrons — the readings on Mathlib (19 October 2026)

The paper module of *Ground-State Light Hadron Spectroscopy over Finite Substrate* (tree `35-hadrons-20260629`) on Mathlib: every
declaration is the hadrons theme's (`FRC.HadronsML`, `FrcLedger/Theme/Hadrons.lean`), under the paper's name — the flavour,
isospin and spin identities over `ℚ`, the Casimir, spin and charge rationals, the PDG confrontations as rational brackets, the
anchored spectrum, the single-scale readings at `√σ = 440 MeV`, the baryon eigenvalue read against the nucleon and the forward
landing. Classical (tier 2). The finite content is the core's (`FrcCore/Theme/Hadrons.lean`, no axioms); the predicates
`p35NNN` at the end are generated by `make_predicates.py`, aliases of the keys of `Keys/Hadrons.lean`.
-/

namespace FRC.Hadrons


/-! ## Old names (19 October 2026): every declaration of this module is an alias of the hadrons theme's (`FRC.HadronsML`),
under the paper's name; the model's and the anchors' definitions are the theme's (`hfN` … `hfO`, `vll`, `ml`, `ms`, `vls`, `vss`, `vm`) -/

open FRC.HadronsML (hfN hfL hfS hfX hfD hfSs hfXs hfO vll ml ms vls vss vm)

/-- 35:C2, 35:X4, 35:P1 — `HadronsML.gmo`. -/
theorem gmo (M₀ a b : ℚ) : 2 * (M₀ + a + b / 2) + 2 * (M₀ - a + b / 2) - 3 * M₀ - (M₀ + 2 * b) = 0 :=
  FRC.HadronsML.gmo M₀ a b

/-- 35:C3, 35:X5, 35:P2 — `HadronsML.spacing`. -/
theorem spacing (α β : ℚ) :
    α - 2 * (α + β) + (α + 2 * β) = 0 ∧ (α + β) - 2 * (α + 2 * β) + (α + 3 * β) = 0 :=
  FRC.HadronsML.spacing α β

/-- 35:C11, 35:P8 — `HadronsML.third_difference`. -/
theorem third_difference (M₀ d A r : ℚ) :
    (M₀ + 3 / 4 * A) - 3 * (M₀ + d + A / 4 * (1 + 2 * r)) + 3 * (M₀ + 2 * d + A / 4 * (2 * r + r ^ 2))
      - (M₀ + 3 * d + 3 / 4 * A * r ^ 2) = 0 :=
  FRC.HadronsML.third_difference M₀ d A r

/-- 35:C12 — `HadronsML.hyperfine_links`. -/
theorem hyperfine_links (M₀ d A r : ℚ) :
    (hfS M₀ d A r - hfL M₀ d A r) - 2 / 3 * ((hfD M₀ d A r - hfN M₀ d A r) - (hfSs M₀ d A r - hfS M₀ d A r)) = 0 ∧
    (hfSs M₀ d A r - hfS M₀ d A r) - (hfXs M₀ d A r - hfX M₀ d A r) = 0 :=
  FRC.HadronsML.hyperfine_links M₀ d A r

/-- 35:C7, 35:X10, 35:P6 — `HadronsML.coleman_glashow`. -/
theorem coleman_glashow (δ : ℚ) : (δ + δ) - 2 * δ = 0 :=
  FRC.HadronsML.coleman_glashow δ

/-- 35:C18, 35:X12, 35:P9 — `HadronsML.vector_spacing`. -/
theorem vector_spacing (a b : ℚ) : 2 * (a + b) - a - (a + 2 * b) = 0 :=
  FRC.HadronsML.vector_spacing a b

/-- 35:C16, 35:P11, 35:P10 — `HadronsML.lambda_n_gap`. -/
theorem lambda_n_gap (ml ms v : ℚ) : (2 * ml + ms - 3 / 4 * v) - (3 * ml - 3 / 4 * v) = ms - ml :=
  FRC.HadronsML.lambda_n_gap ml ms v

/-- 35:C17, 35:C19, 35:P10 — `HadronsML.spin_split`. -/
theorem spin_split (l f : ℚ) :
    ((3 * l - 3 / 4 * f) + (3 * l + 3 / 4 * f)) / 6 = l ∧ (3 * l + 3 / 4 * f) - (3 * l - 3 / 4 * f) = 3 / 2 * f :=
  FRC.HadronsML.spin_split l f

/-- 35:C4, 35:X6 — `HadronsML.colour_factor`. -/
theorem colour_factor :
    ((3 : ℚ) ^ 2 - 1) / (2 * 3) = 4 / 3 ∧ (0 - 3 * (4 / 3 : ℚ)) / 2 = -2 ∧ 4 * (-2 : ℚ) = -8 ∧ (-8 : ℚ) / 3 = -8 / 3 :=
  FRC.HadronsML.colour_factor

/-- 35:C5, 35:X6, 35:P3 — `HadronsML.spin_pattern`. -/
theorem spin_pattern :
    (1 / 2 : ℚ) * (1 / 2) * (1 / 2 + 1) - 9 / 8 = -3 / 4 ∧ (1 / 2 : ℚ) * (3 / 2) * (3 / 2 + 1) - 9 / 8 = 3 / 4 ∧
    (3 / 4 : ℚ) - (-3 / 4) = 3 / 2 ∧ (-8 / 3 : ℚ) * (-3 / 4) = 2 ∧ (-8 / 3 : ℚ) * (3 / 4) = -2 :=
  FRC.HadronsML.spin_pattern

/-- 35:C9, 35:X9 — `HadronsML.sigma_lambda`. -/
theorem sigma_lambda (a r : ℚ) (ha : 0 < a) (hr : r < 1) :
    a * (1 / 4 - (-3 / 4)) + a * r * (-1 - 0) = a - a * r ∧ 0 < a - a * r :=
  FRC.HadronsML.sigma_lambda a r ha hr

/-- 35:C8, 35:C13, 35:X8, 35:C21 — `HadronsML.charge_structure`. -/
theorem charge_structure :
    (2 / 3 : ℚ) ^ 2 + (2 / 3) ^ 2 + (-1 / 3) ^ 2 = 1 ∧ (2 / 3 : ℚ) ^ 2 + (-1 / 3) ^ 2 + (-1 / 3) ^ 2 = 2 / 3 ∧
    (2 / 3 : ℚ) * (2 / 3) + (2 / 3) * (-1 / 3) + (2 / 3) * (-1 / 3) = 0 ∧
    (2 / 3 : ℚ) * (-1 / 3) + (2 / 3) * (-1 / 3) + (-1 / 3) * (-1 / 3) = -1 / 3 ∧
    (1 : ℚ) - 2 / 3 = 1 / 3 ∧ (0 : ℚ) - (-1 / 3) = 1 / 3 :=
  FRC.HadronsML.charge_structure

/-- 35:C14, 35:C6, 35:C23 — `HadronsML.character_coefficients`. -/
theorem character_coefficients : (1 : ℚ) / (2 * 3 ^ 2) = 1 / 18 ∧ (1 : ℚ) / (2 * 3) ^ 2 = 1 / 36 :=
  FRC.HadronsML.character_coefficients

/-- 35:P1 — `HadronsML.gmo_pdg`. -/
theorem gmo_pdg (mN mL mS mX : ℚ) (hN : mN = (938.272 + 939.565) / 2) (hL : mL = 1115.683)
    (hS : mS = (1189.37 + 1192.642 + 1197.449) / 3) (hX : mX = (1314.86 + 1321.71) / 2) :
    (0.0056 : ℚ) < ((3 * mL + mS) / 4 - (mN + mX) / 2) / ((3 * mL + mS) / 4) ∧
    ((3 * mL + mS) / 4 - (mN + mX) / 2) / ((3 * mL + mS) / 4) < 0.0058 :=
  FRC.HadronsML.gmo_pdg mN mL mS mX hN hL hS hX

/-- 35:P2 — `HadronsML.spacing_pdg`. -/
theorem spacing_pdg (mD mSs mXs mO : ℚ) (hD : mD = 1232.0) (hSs : mSs = (1382.8 + 1383.7 + 1387.2) / 3)
    (hXs : mXs = (1531.80 + 1535.0) / 2) (hO : mO = 1672.45) :
    (146.8 : ℚ) < (mO - mD) / 3 ∧ (mO - mD) / 3 < 146.85 ∧
    (0.092 : ℚ) < ((mSs - mD) - (mO - mXs)) / ((mO - mD) / 3) ∧ ((mSs - mD) - (mO - mXs)) / ((mO - mD) / 3) < 0.0921 ∧
    mO - mXs < mXs - mSs ∧ mXs - mSs < mSs - mD :=
  FRC.HadronsML.spacing_pdg mD mSs mXs mO hD hSs hXs hO

/-- 35:P8 — `HadronsML.third_pdg`. -/
theorem third_pdg (mD mSs mXs mO : ℚ) (hD : mD = 1232.0) (hSs : mSs = (1382.8 + 1383.7 + 1387.2) / 3)
    (hXs : mXs = (1531.80 + 1535.0) / 2) (hO : mO = 1672.45) :
    (6.0 : ℚ) < mD - 3 * mSs + 3 * mXs - mO ∧ mD - 3 * mSs + 3 * mXs - mO < 6.1 ∧
    (0.0036 : ℚ) < (mD - 3 * mSs + 3 * mXs - mO) / mO ∧ (mD - 3 * mSs + 3 * mXs - mO) / mO < 0.00363 :=
  FRC.HadronsML.third_pdg mD mSs mXs mO hD hSs hXs hO

/-- 35:C12 — `HadronsML.links_pdg`. -/
theorem links_pdg (mN mL mS mX mD mSs mXs : ℚ) (hN : mN = (938.272 + 939.565) / 2) (hL : mL = 1115.683)
    (hS : mS = (1189.37 + 1192.642 + 1197.449) / 3) (hX : mX = (1314.86 + 1321.71) / 2) (hD : mD = 1232.0)
    (hSs : mSs = (1382.8 + 1383.7 + 1387.2) / 3) (hXs : mXs = (1531.80 + 1535.0) / 2) :
    (0.125 : ℚ) < ((mS - mL) - 2 / 3 * ((mD - mN) - (mSs - mS))) / (mS - mL) ∧
    ((mS - mL) - 2 / 3 * ((mD - mN) - (mSs - mS))) / (mS - mL) < 0.1252 ∧
    (-0.124 : ℚ) < ((mSs - mS) - (mXs - mX)) / (mSs - mS) ∧ ((mSs - mS) - (mXs - mX)) / (mSs - mS) < -0.1238 :=
  FRC.HadronsML.links_pdg mN mL mS mX mD mSs mXs hN hL hS hX hD hSs hXs

/-- 35:P3, 35:C6 — `HadronsML.a_light`. -/
theorem a_light (mN mD mS mSs : ℚ) (hN : mN = (938.272 + 939.565) / 2) (hD : mD = 1232.0)
    (hS : mS = (1189.37 + 1192.642 + 1197.449) / 3) (hSs : mSs = (1382.8 + 1383.7 + 1387.2) / 3) :
    (195.3 : ℚ) < 2 / 3 * (mD - mN) ∧ 2 / 3 * (mD - mN) < 195.4 ∧ (191.4 : ℚ) < mSs - mS ∧ mSs - mS < 191.5 :=
  FRC.HadronsML.a_light mN mD mS mSs hN hD hS hSs

/-- 35:P6, 35:C8, 35:X8, 35:C9, 35:X9 — `HadronsML.cg_pdg`. -/
theorem cg_pdg (p n Sp S0 Sm X0 Xm L : ℚ) (hp : p = 938.272) (hn : n = 939.565) (hSp : Sp = 1189.37)
    (hS0 : S0 = 1192.642) (hSm : Sm = 1197.449) (hX0 : X0 = 1314.86) (hXm : Xm = 1321.71) (hL : L = 1115.683) :
    (0.0079 : ℚ) < ((n - p) + (Xm - X0) - (Sm - Sp)) / (Sm - Sp) ∧ ((n - p) + (Xm - X0) - (Sm - Sp)) / (Sm - Sp) < 0.0080 ∧
    n - p = 1.293 ∧ 0 < n - p ∧ S0 - L = 76.959 ∧ 0 < S0 - L :=
  FRC.HadronsML.cg_pdg p n Sp S0 Sm X0 Xm L hp hn hSp hS0 hSm hX0 hXm hL

/-- 35:C10, 35:X11, 35:P7, 35:C22 — `HadronsML.hqs_pdg`. -/
theorem hqs_pdg (Lc Lb D0 B0 Sc Scs mS mSs : ℚ) (hLc : Lc = 2286.46) (hLb : Lb = 5619.60) (hD : D0 = 1864.84)
    (hB : B0 = 5279.66) (hSc : Sc = 2453.5) (hScs : Scs = 2518.4) (hS : mS = (1189.37 + 1192.642 + 1197.449) / 3)
    (hSs : mSs = (1382.8 + 1383.7 + 1387.2) / 3) :
    (-0.024 : ℚ) < ((Lb - Lc) - (B0 - D0)) / (B0 - D0) ∧ ((Lb - Lc) - (B0 - D0)) / (B0 - D0) < -0.0239 ∧
    (0.339 : ℚ) < (Scs - Sc) / (mSs - mS) ∧ (Scs - Sc) / (mSs - mS) < 0.3391 :=
  FRC.HadronsML.hqs_pdg Lc Lb D0 B0 Sc Scs mS mSs hLc hLb hD hB hSc hScs hS hSs

/-- 35:P9, 35:C18, 35:X12 — `HadronsML.vector_pdg`. -/
theorem vector_pdg (rho ome Ks phi : ℚ) (hr : rho = 775.26) (ho : ome = 782.66) (hK : Ks = (891.67 + 895.55) / 2)
    (hphi : phi = 1019.46) :
    (-0.0042 : ℚ) < (2 * Ks - rho - phi) / (rho + phi) ∧ (2 * Ks - rho - phi) / (rho + phi) < -0.0041 ∧
    (rho + phi) / 2 = 897.36 ∧ |((rho + phi) / 2 - Ks) / Ks| < 0.005 ∧ |(rho - ome) / ome| < 0.01 ∧
    (phi - rho) / 2 = 122.1 :=
  FRC.HadronsML.vector_pdg rho ome Ks phi hr ho hK hphi

/-- 35:P10 — `HadronsML.absolute_spectrum`. -/
theorem absolute_spectrum (mN mL mS mX mD mSs mXs mO : ℚ) (hN : mN = 938.9185) (hL : mL = 1115.683)
    (hS : mS = (1189.37 + 1192.642 + 1197.449) / 3) (hX : mX = (1314.86 + 1321.71) / 2) (hD : mD = 1232.0)
    (hSs : mSs = (1382.8 + 1383.7 + 1387.2) / 3) (hXs : mXs = (1531.80 + 1535.0) / 2) (hO : mO = 1672.45) :
    |((2 * ml mN mD + ms mN mL mD + vll mN mD / 4 - vls mN mL mD) - mS) / mS| < 0.0112 ∧
    0.0111 < |((2 * ml mN mD + ms mN mL mD + vll mN mD / 4 - vls mN mL mD) - mS) / mS| ∧
    |((ml mN mD + 2 * ms mN mL mD - vls mN mL mD + vss mN mL mD / 4) - mX) / mX| < 0.0112 ∧
    |((2 * ml mN mD + ms mN mL mD + vll mN mD / 4 + vls mN mL mD / 2) - mSs) / mSs| < 0.0112 ∧
    |((ml mN mD + 2 * ms mN mL mD + vls mN mL mD / 2 + vss mN mL mD / 4) - mXs) / mXs| < 0.0112 ∧
    |((3 * ms mN mL mD + 3 / 4 * vss mN mL mD) - mO) / mO| < 0.0112 :=
  FRC.HadronsML.absolute_spectrum mN mL mS mX mD mSs mXs mO hN hL hS hX hD hSs hXs hO

/-- 35:P11, 35:C16 — `HadronsML.gap_pdg`. -/
theorem gap_pdg (mN mL : ℚ) (hN : mN = 938.9185) (hL : mL = 1115.683) :
    mL - mN = 176.7645 ∧ (176.75 : ℚ) < mL - mN ∧ mL - mN < 176.85 :=
  FRC.HadronsML.gap_pdg mN mL hN hL

/-- 35:C16, 35:C23, 35:X13 — `HadronsML.single_scale`. -/
theorem single_scale (mN mL mD s : ℚ) (hN : mN = 938.9185) (hL : mL = 1115.683) (hD : mD = 1232.0) (hs : s = 440) :
    (0.822 : ℚ) < ml mN mD / s ∧ ml mN mD / s < 0.8224 ∧ (1.488 : ℚ) < ms mN mL mD / ml mN mD ∧ ms mN mL mD / ml mN mD < 1.489 ∧
    (0.444 : ℚ) < vll mN mD / s ∧ vll mN mD / s < 0.4441 ∧ (2.133 : ℚ) < mN / s ∧ mN / s < 2.134 ∧
    (0.401 : ℚ) < (ms mN mL mD - ml mN mD) / s ∧ (ms mN mL mD - ml mN mD) / s < 0.402 :=
  FRC.HadronsML.single_scale mN mL mD s hN hL hD hs

/-- 35:C17 — `HadronsML.baryon_scale`. -/
theorem baryon_scale (E₀ mN mD s : ℚ) (hE : E₀ = 2.2322) (hN : mN = 938.9185) (hD : mD = 1232.0) (hs : s = 440) :
    (982 : ℚ) < E₀ * s ∧ E₀ * s < 983 ∧ (0.046 : ℚ) < (E₀ * s - mN) / mN ∧ (E₀ * s - mN) / mN < 0.0461 ∧
    (420 : ℚ) < mN / E₀ ∧ mN / E₀ < 421 ∧
    (0.822 : ℚ) < (mN + mD) / (6 * s) ∧ (mN + mD) / (6 * s) < 0.8224 ∧
    (0.444 : ℚ) < 2 * (mD - mN) / (3 * s) ∧ 2 * (mD - mN) / (3 * s) < 0.4441 :=
  FRC.HadronsML.baryon_scale E₀ mN mD s hE hN hD hs

/-- 35:C19 — `HadronsML.alpha_s_bounds`. -/
theorem alpha_s_bounds (π' l : ℚ) (h1 : 3.14 < π') (h2 : π' < 3.15) (h3 : 0.6931471803 < l) (h4 : l < 0.6931471808) :
    (1.00 : ℚ) < 2 * π' / (9 * l) ∧ 2 * π' / (9 * l) < 1.01 :=
  FRC.HadronsML.alpha_s_bounds π' l h1 h2 h3 h4

/-- 35:C19 — `HadronsML.forward_landing`. -/
theorem forward_landing (F E₀ : ℚ) (hF : F = 3.517) (hE : E₀ = 2.2322) :
    |vm F 0.93 - 0.540| / 0.540 < 0.004 ∧ (0.57 : ℚ) < vm F 1 ∧ vm F 1 < 0.58 ∧
    |vm F 0.93 * 0.822 - 0.444| / 0.444 < 0.07 ∧ |vm F 1 * 0.822 - 0.444| / 0.444 < 0.08 ∧
    |(E₀ + 3 / 4 * 0.444) / 3 - 0.822| / 0.822 < 0.07 ∧ |(0.93 : ℚ) - 1.007| / 1.007 < 0.12 :=
  FRC.HadronsML.forward_landing F E₀ hF hE

/-- 35:C13, 35:C21 — `HadronsML.em_magnitude`. -/
theorem em_magnitude (α s : ℚ) (hα : α = 1 / 137.036) (hs : s = 440) :
    (1.07 : ℚ) < α * s * (1 / 3) ∧ α * s * (1 / 3) < 1.08 ∧ |α * s * (1 / 3) - 1.00| < 0.1 :=
  FRC.HadronsML.em_magnitude α s hα hs

/-- 35:C20 — `HadronsML.residual_orders`. -/
theorem residual_orders (mN mL mS mX mD mSs mXs mO : ℚ) (hN : mN = (938.272 + 939.565) / 2) (hL : mL = 1115.683)
    (hS : mS = (1189.37 + 1192.642 + 1197.449) / 3) (hX : mX = (1314.86 + 1321.71) / 2) (hD : mD = 1232.0)
    (hSs : mSs = (1382.8 + 1383.7 + 1387.2) / 3) (hXs : mXs = (1531.80 + 1535.0) / 2) (hO : mO = 1672.45) :
    (0.0169 : ℚ) < ((3 * mL + mS) / 4 - (mN + mX) / 2) / (mX - mN) ∧ ((3 * mL + mS) / 4 - (mN + mX) / 2) / (mX - mN) < 0.0171 ∧
    (0.0412 : ℚ) < (mD - 3 * mSs + 3 * mXs - mO) / ((mO - mD) / 3) ∧ (mD - 3 * mSs + 3 * mXs - mO) / ((mO - mD) / 3) < 0.0413 :=
  FRC.HadronsML.residual_orders mN mL mS mX mD mSs mXs mO hN hL hS hX hD hSs hXs hO

/-- 35:C16 — `HadronsML.airy_ratio`. -/
theorem airy_ratio : (1.748 : ℚ) < 4.08795 / 2.33811 ∧ (4.08795 : ℚ) / 2.33811 < 1.7485 :=
  FRC.HadronsML.airy_ratio

-- 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:C2 (p35016) — Gell-Mann--Okubo $\tfrac12(N+\Xi)=\tfrac14(3\Lambda+\Sigma)$: $2N+2\Xi-3\Lambda-\Sigma=0$ identically, scale-cancelling. -/
theorem p35016 : ∀ (M₀ a b : ℚ), (2 : ℚ) * (M₀ + a + b / (2 : ℚ)) + (2 : ℚ) * (M₀ - a + b / (2 : ℚ)) - (3 : ℚ) * M₀ - (M₀ + (2 : ℚ) * b) = (0 : ℚ) :=
  @FRC.LedgerML.p35016
/-- 35:C3 (p35017) — Decuplet equal spacing $\Sigma^{*}-\Delta=\Xi^{*}-\Sigma^{*}=\Omega-\Xi^{*}=\beta$: the second differences vanish identically. -/
theorem p35017 : ∀ (α β : ℚ), α - (2 : ℚ) * (α + β) + (α + (2 : ℚ) * β) = (0 : ℚ) ∧ α + β - (2 : ℚ) * (α + (2 : ℚ) * β) + (α + (3 : ℚ) * β) = (0 : ℚ) :=
  @FRC.LedgerML.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 : ℚ) ^ (2 : ℕ) - (1 : ℚ)) / ((2 : ℚ) * (3 : ℚ)) = (4 / 3 : ℚ) ∧ ((0 : ℚ) - (3 : ℚ) * (4 / 3 : ℚ)) / (2 : ℚ) = (-2 : ℚ) ∧ (4 : ℚ) * (-2 : ℚ) = (-8 : ℚ) ∧ (-8 / 3 : ℚ) = (-8 / 3 : ℚ) :=
  @FRC.LedgerML.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 / 2 : ℚ) * (1 / 2 : ℚ) * ((1 / 2 : ℚ) + (1 : ℚ)) - (9 / 8 : ℚ) = (-3 / 4 : ℚ) ∧ (1 / 2 : ℚ) * (3 / 2 : ℚ) * ((3 / 2 : ℚ) + (1 : ℚ)) - (9 / 8 : ℚ) = (3 / 4 : ℚ) ∧ (3 / 4 : ℚ) - (-3 / 4 : ℚ) = (3 / 2 : ℚ) ∧ (-8 / 3 : ℚ) * (-3 / 4 : ℚ) = (2 : ℚ) ∧ (-8 / 3 : ℚ) * (3 / 4 : ℚ) = (-2 : ℚ) :=
  @FRC.LedgerML.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 : ((1 : ℚ) / ((2 : ℚ) * (3 : ℚ) ^ (2 : ℕ)) = (1 / 18 : ℚ) ∧ (1 : ℚ) / ((2 : ℚ) * (3 : ℚ)) ^ (2 : ℕ) = (1 / 36 : ℚ)) ∧ ∀ (mN mD mS mSs : ℚ), mN = (938.272 + 939.565) / (2 : ℚ) → mD = 1232.0 → mS = (1189.37 + 1192.642 + 1197.449) / (3 : ℚ) → mSs = (1382.8 + 1383.7 + 1387.2) / (3 : ℚ) → 195.3 < (2 / 3 : ℚ) * (mD - mN) ∧ (2 / 3 : ℚ) * (mD - mN) < 195.4 ∧ 191.4 < mSs - mS ∧ mSs - mS < 191.5 :=
  @FRC.LedgerML.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 : ∀ (δ : ℚ), δ + δ - (2 : ℚ) * δ = (0 : ℚ) :=
  @FRC.LedgerML.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 : (∀ (p n Sp S0 Sm X0 Xm L : ℚ), p = 938.272 → n = 939.565 → Sp = 1189.37 → S0 = 1192.642 → Sm = 1197.449 → X0 = 1314.86 → Xm = 1321.71 → L = 1115.683 → 79e-4 < (n - p + (Xm - X0) - (Sm - Sp)) / (Sm - Sp) ∧ (n - p + (Xm - X0) - (Sm - Sp)) / (Sm - Sp) < 80e-4 ∧ n - p = 1.293 ∧ (0 : ℚ) < n - p ∧ S0 - L = 76.959 ∧ (0 : ℚ) < S0 - L) ∧ (2 / 3 : ℚ) ^ (2 : ℕ) + (2 / 3 : ℚ) ^ (2 : ℕ) + (-1 / 3 : ℚ) ^ (2 : ℕ) = (1 : ℚ) ∧ (2 / 3 : ℚ) ^ (2 : ℕ) + (-1 / 3 : ℚ) ^ (2 : ℕ) + (-1 / 3 : ℚ) ^ (2 : ℕ) = (2 / 3 : ℚ) ∧ (2 / 3 : ℚ) * (2 / 3 : ℚ) + (2 / 3 : ℚ) * (-1 / 3 : ℚ) + (2 / 3 : ℚ) * (-1 / 3 : ℚ) = (0 : ℚ) ∧ (2 / 3 : ℚ) * (-1 / 3 : ℚ) + (2 / 3 : ℚ) * (-1 / 3 : ℚ) + (-1 / 3 : ℚ) * (-1 / 3 : ℚ) = (-1 / 3 : ℚ) ∧ (1 : ℚ) - (2 / 3 : ℚ) = (1 / 3 : ℚ) ∧ (0 : ℚ) - (-1 / 3 : ℚ) = (1 / 3 : ℚ) :=
  @FRC.LedgerML.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 : ∀ (a r : ℚ), (0 : ℚ) < a → r < (1 : ℚ) → a * ((1 / 4 : ℚ) - (-3 / 4 : ℚ)) + a * r * ((-1 : ℚ) - (0 : ℚ)) = a - a * r ∧ (0 : ℚ) < a - a * r :=
  @FRC.LedgerML.p35023
/-- 35:C10 (p35024) — Heavy-quark spin decoupling ($a_{iQ}\sim1/m_Q$): $\Lambda_Q$ a spin-$0$ light diquark; $M_{\Lambda_b}-M_{\Lambda_c}=M_B-M_D$; the $1/m_Q$ hyperfine ratio. -/
theorem p35024 : ∀ (Lc Lb D0 B0 Sc Scs mS mSs : ℚ), Lc = 2286.46 → Lb = 5619.60 → D0 = 1864.84 → B0 = 5279.66 → Sc = 2453.5 → Scs = 2518.4 → mS = (1189.37 + 1192.642 + 1197.449) / (3 : ℚ) → mSs = (1382.8 + 1383.7 + 1387.2) / (3 : ℚ) → -24e-3 < (Lb - Lc - (B0 - D0)) / (B0 - D0) ∧ (Lb - Lc - (B0 - D0)) / (B0 - D0) < -239e-4 ∧ 0.339 < (Scs - Sc) / (mSs - mS) ∧ (Scs - Sc) / (mSs - mS) < 0.3391 :=
  @FRC.LedgerML.p35024
/-- 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 : ∀ (M₀ d A r : ℚ), M₀ + (3 / 4 : ℚ) * A - (3 : ℚ) * (M₀ + d + A / (4 : ℚ) * ((1 : ℚ) + (2 : ℚ) * r)) + (3 : ℚ) * (M₀ + (2 : ℚ) * d + A / (4 : ℚ) * ((2 : ℚ) * r + r ^ (2 : ℕ))) - (M₀ + (3 : ℚ) * d + (3 / 4 : ℚ) * A * r ^ (2 : ℕ)) = (0 : ℚ) :=
  @FRC.LedgerML.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 : (∀ (M₀ d A r : ℚ), FRC.HadronsML.hfS M₀ d A r - FRC.HadronsML.hfL M₀ d A r - (2 / 3 : ℚ) * (FRC.HadronsML.hfD M₀ d A r - FRC.HadronsML.hfN M₀ d A r - (FRC.HadronsML.hfSs M₀ d A r - FRC.HadronsML.hfS M₀ d A r)) = (0 : ℚ) ∧ FRC.HadronsML.hfSs M₀ d A r - FRC.HadronsML.hfS M₀ d A r - (FRC.HadronsML.hfXs M₀ d A r - FRC.HadronsML.hfX M₀ d A r) = (0 : ℚ)) ∧ ∀ (mN mL mS mX mD mSs mXs : ℚ), mN = (938.272 + 939.565) / (2 : ℚ) → mL = 1115.683 → mS = (1189.37 + 1192.642 + 1197.449) / (3 : ℚ) → mX = (1314.86 + 1321.71) / (2 : ℚ) → mD = 1232.0 → mSs = (1382.8 + 1383.7 + 1387.2) / (3 : ℚ) → mXs = (1531.80 + 1535.0) / (2 : ℚ) → 0.125 < (mS - mL - (2 / 3 : ℚ) * (mD - mN - (mSs - mS))) / (mS - mL) ∧ (mS - mL - (2 / 3 : ℚ) * (mD - mN - (mSs - mS))) / (mS - mL) < 0.1252 ∧ -0.124 < (mSs - mS - (mXs - mX)) / (mSs - mS) ∧ (mSs - mS - (mXs - mX)) / (mSs - mS) < -0.1238 :=
  @FRC.LedgerML.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 : ((2 / 3 : ℚ) ^ (2 : ℕ) + (2 / 3 : ℚ) ^ (2 : ℕ) + (-1 / 3 : ℚ) ^ (2 : ℕ) = (1 : ℚ) ∧ (2 / 3 : ℚ) ^ (2 : ℕ) + (-1 / 3 : ℚ) ^ (2 : ℕ) + (-1 / 3 : ℚ) ^ (2 : ℕ) = (2 / 3 : ℚ) ∧ (2 / 3 : ℚ) * (2 / 3 : ℚ) + (2 / 3 : ℚ) * (-1 / 3 : ℚ) + (2 / 3 : ℚ) * (-1 / 3 : ℚ) = (0 : ℚ) ∧ (2 / 3 : ℚ) * (-1 / 3 : ℚ) + (2 / 3 : ℚ) * (-1 / 3 : ℚ) + (-1 / 3 : ℚ) * (-1 / 3 : ℚ) = (-1 / 3 : ℚ) ∧ (1 : ℚ) - (2 / 3 : ℚ) = (1 / 3 : ℚ) ∧ (0 : ℚ) - (-1 / 3 : ℚ) = (1 / 3 : ℚ)) ∧ ∀ (α s : ℚ), α = (1 : ℚ) / 137.036 → s = (440 : ℚ) → 1.07 < α * s * (1 / 3 : ℚ) ∧ α * s * (1 / 3 : ℚ) < 1.08 ∧ |α * s * (1 / 3 : ℚ) - 1.00| < 0.1 :=
  @FRC.LedgerML.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 : (1 : ℚ) / ((2 : ℚ) * (3 : ℚ) ^ (2 : ℕ)) = (1 / 18 : ℚ) ∧ (1 : ℚ) / ((2 : ℚ) * (3 : ℚ)) ^ (2 : ℕ) = (1 / 36 : ℚ) :=
  @FRC.LedgerML.p35028
/-- 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 : And (∀ (ml ms v : Rat), @Eq Rat (@HSub.hSub Rat Rat Rat (@instHSub Rat Rat.instSub) (@HSub.hSub Rat Rat Rat (@instHSub Rat Rat.instSub) (@HAdd.hAdd Rat Rat Rat (@instHAdd Rat Rat.instAdd) (@HMul.hMul Rat Rat Rat (@instHMul Rat Rat.instMul) (@OfNat.ofNat Rat (nat_lit 2) (@Rat.instOfNat (nat_lit 2))) ml) ms) (@HMul.hMul Rat Rat Rat (@instHMul Rat Rat.instMul) (@HDiv.hDiv Rat Rat Rat (@instHDiv Rat Rat.instDiv) (@OfNat.ofNat Rat (nat_lit 3) (@Rat.instOfNat (nat_lit 3))) (@OfNat.ofNat Rat (nat_lit 4) (@Rat.instOfNat (nat_lit 4)))) v)) (@HSub.hSub Rat Rat Rat (@instHSub Rat Rat.instSub) (@HMul.hMul Rat Rat Rat (@instHMul Rat Rat.instMul) (@OfNat.ofNat Rat (nat_lit 3) (@Rat.instOfNat (nat_lit 3))) ml) (@HMul.hMul Rat Rat Rat (@instHMul Rat Rat.instMul) (@HDiv.hDiv Rat Rat Rat (@instHDiv Rat Rat.instDiv) (@OfNat.ofNat Rat (nat_lit 3) (@Rat.instOfNat (nat_lit 3))) (@OfNat.ofNat Rat (nat_lit 4) (@Rat.instOfNat (nat_lit 4)))) v))) (@HSub.hSub Rat Rat Rat (@instHSub Rat Rat.instSub) ms ml)) (And (∀ (mN mL mD s : Rat), @Eq Rat mN (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 9389185) true (nat_lit 4)) → @Eq Rat mL (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 1115683) true (nat_lit 3)) → @Eq Rat mD (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 12320) true (nat_lit 1)) → @Eq Rat s (@OfNat.ofNat Rat (nat_lit 440) (@Rat.instOfNat (nat_lit 440))) → And (@LT.lt Rat Rat.instLT (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 822) true (nat_lit 3)) (@HDiv.hDiv Rat Rat Rat (@instHDiv Rat Rat.instDiv) (FRC.HadronsML.ml mN mD) s)) (And (@LT.lt Rat Rat.instLT (@HDiv.hDiv Rat Rat Rat (@instHDiv Rat Rat.instDiv) (FRC.HadronsML.ml mN mD) s) (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 8224) true (nat_lit 4))) (And (@LT.lt Rat Rat.instLT (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 1488) true (nat_lit 3)) (@HDiv.hDiv Rat Rat Rat (@instHDiv Rat Rat.instDiv) (FRC.HadronsML.ms mN mL mD) (FRC.HadronsML.ml mN mD))) (And (@LT.lt Rat Rat.instLT (@HDiv.hDiv Rat Rat Rat (@instHDiv Rat Rat.instDiv) (FRC.HadronsML.ms mN mL mD) (FRC.HadronsML.ml mN mD)) (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 1489) true (nat_lit 3))) (And (@LT.lt Rat Rat.instLT (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 444) true (nat_lit 3)) (@HDiv.hDiv Rat Rat Rat (@instHDiv Rat Rat.instDiv) (FRC.HadronsML.vll mN mD) s)) (And (@LT.lt Rat Rat.instLT (@HDiv.hDiv Rat Rat Rat (@instHDiv Rat Rat.instDiv) (FRC.HadronsML.vll mN mD) s) (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 4441) true (nat_lit 4))) (And (@LT.lt Rat Rat.instLT (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 2133) true (nat_lit 3)) (@HDiv.hDiv Rat Rat Rat (@instHDiv Rat Rat.instDiv) mN s)) (And (@LT.lt Rat Rat.instLT (@HDiv.hDiv Rat Rat Rat (@instHDiv Rat Rat.instDiv) mN s) (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 2134) true (nat_lit 3))) (And (@LT.lt Rat Rat.instLT (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 401) true (nat_lit 3)) (@HDiv.hDiv Rat Rat Rat (@instHDiv Rat Rat.instDiv) (@HSub.hSub Rat Rat Rat (@instHSub Rat Rat.instSub) (FRC.HadronsML.ms mN mL mD) (FRC.HadronsML.ml mN mD)) s)) (@LT.lt Rat Rat.instLT (@HDiv.hDiv Rat Rat Rat (@instHDiv Rat Rat.instDiv) (@HSub.hSub Rat Rat Rat (@instHSub Rat Rat.instSub) (FRC.HadronsML.ms mN mL mD) (FRC.HadronsML.ml mN mD)) s) (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 402) true (nat_lit 3)))))))))))) (And (@LT.lt Rat Rat.instLT (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 1748) true (nat_lit 3)) (@HDiv.hDiv Rat Rat Rat (@instHDiv Rat Rat.instDiv) (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 408795) true (nat_lit 5)) (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 233811) true (nat_lit 5)))) (@LT.lt Rat Rat.instLT (@HDiv.hDiv Rat Rat Rat (@instHDiv Rat Rat.instDiv) (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 408795) true (nat_lit 5)) (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 233811) true (nat_lit 5))) (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 17485) true (nat_lit 4))))) :=
  @FRC.LedgerML.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 : (∀ (E₀ mN mD s : ℚ), E₀ = 2.2322 → mN = 938.9185 → mD = 1232.0 → s = (440 : ℚ) → (982 : ℚ) < E₀ * s ∧ E₀ * s < (983 : ℚ) ∧ 46e-3 < (E₀ * s - mN) / mN ∧ (E₀ * s - mN) / mN < 461e-4 ∧ (420 : ℚ) < mN / E₀ ∧ mN / E₀ < (421 : ℚ) ∧ 0.822 < (mN + mD) / ((6 : ℚ) * s) ∧ (mN + mD) / ((6 : ℚ) * s) < 0.8224 ∧ 0.444 < (2 : ℚ) * (mD - mN) / ((3 : ℚ) * s) ∧ (2 : ℚ) * (mD - mN) / ((3 : ℚ) * s) < 0.4441) ∧ ∀ (l f : ℚ), ((3 : ℚ) * l - (3 / 4 : ℚ) * f + ((3 : ℚ) * l + (3 / 4 : ℚ) * f)) / (6 : ℚ) = l ∧ (3 : ℚ) * l + (3 / 4 : ℚ) * f - ((3 : ℚ) * l - (3 / 4 : ℚ) * f) = (3 / 2 : ℚ) * f :=
  @FRC.LedgerML.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 : ∀ (a b : ℚ), (2 : ℚ) * (a + b) - a - (a + (2 : ℚ) * b) = (0 : ℚ) :=
  @FRC.LedgerML.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 : And (∀ (F E₀ : Rat), @Eq Rat F (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 3517) true (nat_lit 3)) → @Eq Rat E₀ (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 22322) true (nat_lit 4)) → And (@LT.lt Rat Rat.instLT (@HDiv.hDiv Rat Rat Rat (@instHDiv Rat Rat.instDiv) (@abs Rat Rat.instLattice Rat.addGroup (@HSub.hSub Rat Rat Rat (@instHSub Rat Rat.instSub) (FRC.HadronsML.vm F (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 93) true (nat_lit 2))) (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 540) true (nat_lit 3)))) (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 540) true (nat_lit 3))) (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 4) true (nat_lit 3))) (And (@LT.lt Rat Rat.instLT (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 57) true (nat_lit 2)) (FRC.HadronsML.vm F (@OfNat.ofNat Rat (nat_lit 1) (@Rat.instOfNat (nat_lit 1))))) (And (@LT.lt Rat Rat.instLT (FRC.HadronsML.vm F (@OfNat.ofNat Rat (nat_lit 1) (@Rat.instOfNat (nat_lit 1)))) (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 58) true (nat_lit 2))) (And (@LT.lt Rat Rat.instLT (@HDiv.hDiv Rat Rat Rat (@instHDiv Rat Rat.instDiv) (@abs Rat Rat.instLattice Rat.addGroup (@HSub.hSub Rat Rat Rat (@instHSub Rat Rat.instSub) (@HMul.hMul Rat Rat Rat (@instHMul Rat Rat.instMul) (FRC.HadronsML.vm F (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 93) true (nat_lit 2))) (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 822) true (nat_lit 3))) (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 444) true (nat_lit 3)))) (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 444) true (nat_lit 3))) (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 7) true (nat_lit 2))) (And (@LT.lt Rat Rat.instLT (@HDiv.hDiv Rat Rat Rat (@instHDiv Rat Rat.instDiv) (@abs Rat Rat.instLattice Rat.addGroup (@HSub.hSub Rat Rat Rat (@instHSub Rat Rat.instSub) (@HMul.hMul Rat Rat Rat (@instHMul Rat Rat.instMul) (FRC.HadronsML.vm F (@OfNat.ofNat Rat (nat_lit 1) (@Rat.instOfNat (nat_lit 1)))) (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 822) true (nat_lit 3))) (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 444) true (nat_lit 3)))) (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 444) true (nat_lit 3))) (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 8) true (nat_lit 2))) (And (@LT.lt Rat Rat.instLT (@HDiv.hDiv Rat Rat Rat (@instHDiv Rat Rat.instDiv) (@abs Rat Rat.instLattice Rat.addGroup (@HSub.hSub Rat Rat Rat (@instHSub Rat Rat.instSub) (@HDiv.hDiv Rat Rat Rat (@instHDiv Rat Rat.instDiv) (@HAdd.hAdd Rat Rat Rat (@instHAdd Rat Rat.instAdd) E₀ (@HMul.hMul Rat Rat Rat (@instHMul Rat Rat.instMul) (@HDiv.hDiv Rat Rat Rat (@instHDiv Rat Rat.instDiv) (@OfNat.ofNat Rat (nat_lit 3) (@Rat.instOfNat (nat_lit 3))) (@OfNat.ofNat Rat (nat_lit 4) (@Rat.instOfNat (nat_lit 4)))) (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 444) true (nat_lit 3)))) (@OfNat.ofNat Rat (nat_lit 3) (@Rat.instOfNat (nat_lit 3)))) (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 822) true (nat_lit 3)))) (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 822) true (nat_lit 3))) (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 7) true (nat_lit 2))) (@LT.lt Rat Rat.instLT (@HDiv.hDiv Rat Rat Rat (@instHDiv Rat Rat.instDiv) (@abs Rat Rat.instLattice Rat.addGroup (@HSub.hSub Rat Rat Rat (@instHSub Rat Rat.instSub) (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 93) true (nat_lit 2)) (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 1007) true (nat_lit 3)))) (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 1007) true (nat_lit 3))) (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 12) true (nat_lit 2))))))))) (∀ (π' l : Rat), @LT.lt Rat Rat.instLT (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 314) true (nat_lit 2)) π' → @LT.lt Rat Rat.instLT π' (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 315) true (nat_lit 2)) → @LT.lt Rat Rat.instLT (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 6931471803) true (nat_lit 10)) l → @LT.lt Rat Rat.instLT l (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 6931471808) true (nat_lit 10)) → And (@LT.lt Rat Rat.instLT (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 100) true (nat_lit 2)) (@HDiv.hDiv Rat Rat Rat (@instHDiv Rat Rat.instDiv) (@HMul.hMul Rat Rat Rat (@instHMul Rat Rat.instMul) (@OfNat.ofNat Rat (nat_lit 2) (@Rat.instOfNat (nat_lit 2))) π') (@HMul.hMul Rat Rat Rat (@instHMul Rat Rat.instMul) (@OfNat.ofNat Rat (nat_lit 9) (@Rat.instOfNat (nat_lit 9))) l))) (@LT.lt Rat Rat.instLT (@HDiv.hDiv Rat Rat Rat (@instHDiv Rat Rat.instDiv) (@HMul.hMul Rat Rat Rat (@instHMul Rat Rat.instMul) (@OfNat.ofNat Rat (nat_lit 2) (@Rat.instOfNat (nat_lit 2))) π') (@HMul.hMul Rat Rat Rat (@instHMul Rat Rat.instMul) (@OfNat.ofNat Rat (nat_lit 9) (@Rat.instOfNat (nat_lit 9))) l)) (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 101) true (nat_lit 2)))) :=
  @FRC.LedgerML.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 : ∀ (mN mL mS mX mD mSs mXs mO : ℚ), mN = (938.272 + 939.565) / (2 : ℚ) → mL = 1115.683 → mS = (1189.37 + 1192.642 + 1197.449) / (3 : ℚ) → mX = (1314.86 + 1321.71) / (2 : ℚ) → mD = 1232.0 → mSs = (1382.8 + 1383.7 + 1387.2) / (3 : ℚ) → mXs = (1531.80 + 1535.0) / (2 : ℚ) → mO = 1672.45 → 169e-4 < (((3 : ℚ) * mL + mS) / (4 : ℚ) - (mN + mX) / (2 : ℚ)) / (mX - mN) ∧ (((3 : ℚ) * mL + mS) / (4 : ℚ) - (mN + mX) / (2 : ℚ)) / (mX - mN) < 171e-4 ∧ 412e-4 < (mD - (3 : ℚ) * mSs + (3 : ℚ) * mXs - mO) / ((mO - mD) / (3 : ℚ)) ∧ (mD - (3 : ℚ) * mSs + (3 : ℚ) * mXs - mO) / ((mO - mD) / (3 : ℚ)) < 413e-4 :=
  @FRC.LedgerML.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 : (∀ (α s : ℚ), α = (1 : ℚ) / 137.036 → s = (440 : ℚ) → 1.07 < α * s * (1 / 3 : ℚ) ∧ α * s * (1 / 3 : ℚ) < 1.08 ∧ |α * s * (1 / 3 : ℚ) - 1.00| < 0.1) ∧ (2 / 3 : ℚ) ^ (2 : ℕ) + (2 / 3 : ℚ) ^ (2 : ℕ) + (-1 / 3 : ℚ) ^ (2 : ℕ) = (1 : ℚ) ∧ (2 / 3 : ℚ) ^ (2 : ℕ) + (-1 / 3 : ℚ) ^ (2 : ℕ) + (-1 / 3 : ℚ) ^ (2 : ℕ) = (2 / 3 : ℚ) ∧ (2 / 3 : ℚ) * (2 / 3 : ℚ) + (2 / 3 : ℚ) * (-1 / 3 : ℚ) + (2 / 3 : ℚ) * (-1 / 3 : ℚ) = (0 : ℚ) ∧ (2 / 3 : ℚ) * (-1 / 3 : ℚ) + (2 / 3 : ℚ) * (-1 / 3 : ℚ) + (-1 / 3 : ℚ) * (-1 / 3 : ℚ) = (-1 / 3 : ℚ) ∧ (1 : ℚ) - (2 / 3 : ℚ) = (1 / 3 : ℚ) ∧ (0 : ℚ) - (-1 / 3 : ℚ) = (1 / 3 : ℚ) :=
  @FRC.LedgerML.p35035
/-- 35:C22 (p35036) — Residue resolution, heavy flavour: the heavy-baryon absolute masses $M(\Lambda_Q)=m_Q+O(\sig)$ reduce to the imported scales (A3, A6); the heavy-quark-symmetry and $1/m_Q$ relations derived (C10). -/
theorem p35036 : ∀ (Lc Lb D0 B0 Sc Scs mS mSs : ℚ), Lc = 2286.46 → Lb = 5619.60 → D0 = 1864.84 → B0 = 5279.66 → Sc = 2453.5 → Scs = 2518.4 → mS = (1189.37 + 1192.642 + 1197.449) / (3 : ℚ) → mSs = (1382.8 + 1383.7 + 1387.2) / (3 : ℚ) → -24e-3 < (Lb - Lc - (B0 - D0)) / (B0 - D0) ∧ (Lb - Lc - (B0 - D0)) / (B0 - D0) < -239e-4 ∧ 0.339 < (Scs - Sc) / (mSs - mS) ∧ (Scs - Sc) / (mSs - mS) < 0.3391 :=
  @FRC.LedgerML.p35036
/-- 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 : ((1 : ℚ) / ((2 : ℚ) * (3 : ℚ) ^ (2 : ℕ)) = (1 / 18 : ℚ) ∧ (1 : ℚ) / ((2 : ℚ) * (3 : ℚ)) ^ (2 : ℕ) = (1 / 36 : ℚ)) ∧ ∀ (mN mL mD s : ℚ), mN = 938.9185 → mL = 1115.683 → mD = 1232.0 → s = (440 : ℚ) → 0.822 < FRC.HadronsML.ml mN mD / s ∧ FRC.HadronsML.ml mN mD / s < 0.8224 ∧ 1.488 < FRC.HadronsML.ms mN mL mD / FRC.HadronsML.ml mN mD ∧ FRC.HadronsML.ms mN mL mD / FRC.HadronsML.ml mN mD < 1.489 ∧ 0.444 < FRC.HadronsML.vll mN mD / s ∧ FRC.HadronsML.vll mN mD / s < 0.4441 ∧ 2.133 < mN / s ∧ mN / s < 2.134 ∧ 0.401 < (FRC.HadronsML.ms mN mL mD - FRC.HadronsML.ml mN mD) / s ∧ (FRC.HadronsML.ms mN mL mD - FRC.HadronsML.ml mN mD) / s < 0.402 :=
  @FRC.LedgerML.p35037
/-- 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 : ∀ (M₀ a b : ℚ), (2 : ℚ) * (M₀ + a + b / (2 : ℚ)) + (2 : ℚ) * (M₀ - a + b / (2 : ℚ)) - (3 : ℚ) * M₀ - (M₀ + (2 : ℚ) * b) = (0 : ℚ) :=
  @FRC.LedgerML.p35041
/-- 35:X5 (p35042) — \textbf{The decuplet is equally spaced} because the strange seed enters the wrap additively. -/
theorem p35042 : ∀ (α β : ℚ), α - (2 : ℚ) * (α + β) + (α + (2 : ℚ) * β) = (0 : ℚ) ∧ α + β - (2 : ℚ) * (α + (2 : ℚ) * β) + (α + (3 : ℚ) * β) = (0 : ℚ) :=
  @FRC.LedgerML.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 / 2 : ℚ) * (1 / 2 : ℚ) * ((1 / 2 : ℚ) + (1 : ℚ)) - (9 / 8 : ℚ) = (-3 / 4 : ℚ) ∧ (1 / 2 : ℚ) * (3 / 2 : ℚ) * ((3 / 2 : ℚ) + (1 : ℚ)) - (9 / 8 : ℚ) = (3 / 4 : ℚ) ∧ (3 / 4 : ℚ) - (-3 / 4 : ℚ) = (3 / 2 : ℚ) ∧ (-8 / 3 : ℚ) * (-3 / 4 : ℚ) = (2 : ℚ) ∧ (-8 / 3 : ℚ) * (3 / 4 : ℚ) = (-2 : ℚ)) ∧ ((3 : ℚ) ^ (2 : ℕ) - (1 : ℚ)) / ((2 : ℚ) * (3 : ℚ)) = (4 / 3 : ℚ) ∧ ((0 : ℚ) - (3 : ℚ) * (4 / 3 : ℚ)) / (2 : ℚ) = (-2 : ℚ) ∧ (4 : ℚ) * (-2 : ℚ) = (-8 : ℚ) ∧ (-8 / 3 : ℚ) = (-8 / 3 : ℚ) :=
  @FRC.LedgerML.p35043
/-- 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 : (∀ (p n Sp S0 Sm X0 Xm L : ℚ), p = 938.272 → n = 939.565 → Sp = 1189.37 → S0 = 1192.642 → Sm = 1197.449 → X0 = 1314.86 → Xm = 1321.71 → L = 1115.683 → 79e-4 < (n - p + (Xm - X0) - (Sm - Sp)) / (Sm - Sp) ∧ (n - p + (Xm - X0) - (Sm - Sp)) / (Sm - Sp) < 80e-4 ∧ n - p = 1.293 ∧ (0 : ℚ) < n - p ∧ S0 - L = 76.959 ∧ (0 : ℚ) < S0 - L) ∧ (2 / 3 : ℚ) ^ (2 : ℕ) + (2 / 3 : ℚ) ^ (2 : ℕ) + (-1 / 3 : ℚ) ^ (2 : ℕ) = (1 : ℚ) ∧ (2 / 3 : ℚ) ^ (2 : ℕ) + (-1 / 3 : ℚ) ^ (2 : ℕ) + (-1 / 3 : ℚ) ^ (2 : ℕ) = (2 / 3 : ℚ) ∧ (2 / 3 : ℚ) * (2 / 3 : ℚ) + (2 / 3 : ℚ) * (-1 / 3 : ℚ) + (2 / 3 : ℚ) * (-1 / 3 : ℚ) = (0 : ℚ) ∧ (2 / 3 : ℚ) * (-1 / 3 : ℚ) + (2 / 3 : ℚ) * (-1 / 3 : ℚ) + (-1 / 3 : ℚ) * (-1 / 3 : ℚ) = (-1 / 3 : ℚ) ∧ (1 : ℚ) - (2 / 3 : ℚ) = (1 / 3 : ℚ) ∧ (0 : ℚ) - (-1 / 3 : ℚ) = (1 / 3 : ℚ) :=
  @FRC.LedgerML.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 : ∀ (a r : ℚ), (0 : ℚ) < a → r < (1 : ℚ) → a * ((1 / 4 : ℚ) - (-3 / 4 : ℚ)) + a * r * ((-1 : ℚ) - (0 : ℚ)) = a - a * r ∧ (0 : ℚ) < a - a * r :=
  @FRC.LedgerML.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 : ∀ (δ : ℚ), δ + δ - (2 : ℚ) * δ = (0 : ℚ) :=
  @FRC.LedgerML.p35047
/-- 35:X11 (p35048) — \textbf{The heavy baryons follow heavy-quark symmetry}, $M_{\Lambda_b}-M_{\Lambda_c}=M_B-M_D$ by spin decoupling, so the baryon and meson heavy-mass differences are one quantity. -/
theorem p35048 : ∀ (Lc Lb D0 B0 Sc Scs mS mSs : ℚ), Lc = 2286.46 → Lb = 5619.60 → D0 = 1864.84 → B0 = 5279.66 → Sc = 2453.5 → Scs = 2518.4 → mS = (1189.37 + 1192.642 + 1197.449) / (3 : ℚ) → mSs = (1382.8 + 1383.7 + 1387.2) / (3 : ℚ) → -24e-3 < (Lb - Lc - (B0 - D0)) / (B0 - D0) ∧ (Lb - Lc - (B0 - D0)) / (B0 - D0) < -239e-4 ∧ 0.339 < (Scs - Sc) / (mSs - mS) ∧ (Scs - Sc) / (mSs - mS) < 0.3391 :=
  @FRC.LedgerML.p35048
/-- 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 : ∀ (a b : ℚ), (2 : ℚ) * (a + b) - a - (a + (2 : ℚ) * b) = (0 : ℚ) :=
  @FRC.LedgerML.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 : ∀ (mN mL mD s : ℚ), mN = 938.9185 → mL = 1115.683 → mD = 1232.0 → s = (440 : ℚ) → 0.822 < FRC.HadronsML.ml mN mD / s ∧ FRC.HadronsML.ml mN mD / s < 0.8224 ∧ 1.488 < FRC.HadronsML.ms mN mL mD / FRC.HadronsML.ml mN mD ∧ FRC.HadronsML.ms mN mL mD / FRC.HadronsML.ml mN mD < 1.489 ∧ 0.444 < FRC.HadronsML.vll mN mD / s ∧ FRC.HadronsML.vll mN mD / s < 0.4441 ∧ 2.133 < mN / s ∧ mN / s < 2.134 ∧ 0.401 < (FRC.HadronsML.ms mN mL mD - FRC.HadronsML.ml mN mD) / s ∧ (FRC.HadronsML.ms mN mL mD - FRC.HadronsML.ml mN mD) / s < 0.402 :=
  @FRC.LedgerML.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 : ∀ (mN mL mS mX : ℚ), mN = (938.272 + 939.565) / (2 : ℚ) → mL = 1115.683 → mS = (1189.37 + 1192.642 + 1197.449) / (3 : ℚ) → mX = (1314.86 + 1321.71) / (2 : ℚ) → 56e-4 < (((3 : ℚ) * mL + mS) / (4 : ℚ) - (mN + mX) / (2 : ℚ)) / (((3 : ℚ) * mL + mS) / (4 : ℚ)) ∧ (((3 : ℚ) * mL + mS) / (4 : ℚ) - (mN + mX) / (2 : ℚ)) / (((3 : ℚ) * mL + mS) / (4 : ℚ)) < 58e-4 :=
  @FRC.LedgerML.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 : ∀ (mD mSs mXs mO : ℚ), mD = 1232.0 → mSs = (1382.8 + 1383.7 + 1387.2) / (3 : ℚ) → mXs = (1531.80 + 1535.0) / (2 : ℚ) → mO = 1672.45 → 146.8 < (mO - mD) / (3 : ℚ) ∧ (mO - mD) / (3 : ℚ) < 146.85 ∧ 92e-3 < (mSs - mD - (mO - mXs)) / ((mO - mD) / (3 : ℚ)) ∧ (mSs - mD - (mO - mXs)) / ((mO - mD) / (3 : ℚ)) < 921e-4 ∧ mO - mXs < mXs - mSs ∧ mXs - mSs < mSs - mD :=
  @FRC.LedgerML.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 : (∀ (mN mD mS mSs : ℚ), mN = (938.272 + 939.565) / (2 : ℚ) → mD = 1232.0 → mS = (1189.37 + 1192.642 + 1197.449) / (3 : ℚ) → mSs = (1382.8 + 1383.7 + 1387.2) / (3 : ℚ) → 195.3 < (2 / 3 : ℚ) * (mD - mN) ∧ (2 / 3 : ℚ) * (mD - mN) < 195.4 ∧ 191.4 < mSs - mS ∧ mSs - mS < 191.5) ∧ (1 / 2 : ℚ) * (1 / 2 : ℚ) * ((1 / 2 : ℚ) + (1 : ℚ)) - (9 / 8 : ℚ) = (-3 / 4 : ℚ) ∧ (1 / 2 : ℚ) * (3 / 2 : ℚ) * ((3 / 2 : ℚ) + (1 : ℚ)) - (9 / 8 : ℚ) = (3 / 4 : ℚ) ∧ (3 / 4 : ℚ) - (-3 / 4 : ℚ) = (3 / 2 : ℚ) ∧ (-8 / 3 : ℚ) * (-3 / 4 : ℚ) = (2 : ℚ) ∧ (-8 / 3 : ℚ) * (3 / 4 : ℚ) = (-2 : ℚ) :=
  @FRC.LedgerML.p35053
/-- 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 n Sp S0 Sm X0 Xm L : ℚ), p = 938.272 → n = 939.565 → Sp = 1189.37 → S0 = 1192.642 → Sm = 1197.449 → X0 = 1314.86 → Xm = 1321.71 → L = 1115.683 → 79e-4 < (n - p + (Xm - X0) - (Sm - Sp)) / (Sm - Sp) ∧ (n - p + (Xm - X0) - (Sm - Sp)) / (Sm - Sp) < 80e-4 ∧ n - p = 1.293 ∧ (0 : ℚ) < n - p ∧ S0 - L = 76.959 ∧ (0 : ℚ) < S0 - L :=
  @FRC.LedgerML.p35056
/-- 35:P7 (p35057) — Heavy-quark symmetry $M_{\Lambda_b}-M_{\Lambda_c}=M_B-M_D$ ($2.4\%$) and the $1/m_Q$ hyperfine ratio $(M_{\Sigma_c^{*}}-M_{\Sigma_c})/(M_{\Sigma^{*}}-M_{\Sigma})\simeq m_s/m_c$. Falsifier: a heavy-baryon spectrum off the spin-decoupled, $1/m_Q$-scaled pattern. -/
theorem p35057 : ∀ (Lc Lb D0 B0 Sc Scs mS mSs : ℚ), Lc = 2286.46 → Lb = 5619.60 → D0 = 1864.84 → B0 = 5279.66 → Sc = 2453.5 → Scs = 2518.4 → mS = (1189.37 + 1192.642 + 1197.449) / (3 : ℚ) → mSs = (1382.8 + 1383.7 + 1387.2) / (3 : ℚ) → -24e-3 < (Lb - Lc - (B0 - D0)) / (B0 - D0) ∧ (Lb - Lc - (B0 - D0)) / (B0 - D0) < -239e-4 ∧ 0.339 < (Scs - Sc) / (mSs - mS) ∧ (Scs - Sc) / (mSs - mS) < 0.3391 :=
  @FRC.LedgerML.p35057
/-- 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 : ∀ (mD mSs mXs mO : ℚ), mD = 1232.0 → mSs = (1382.8 + 1383.7 + 1387.2) / (3 : ℚ) → mXs = (1531.80 + 1535.0) / (2 : ℚ) → mO = 1672.45 → 6.0 < mD - (3 : ℚ) * mSs + (3 : ℚ) * mXs - mO ∧ mD - (3 : ℚ) * mSs + (3 : ℚ) * mXs - mO < 6.1 ∧ 36e-4 < (mD - (3 : ℚ) * mSs + (3 : ℚ) * mXs - mO) / mO ∧ (mD - (3 : ℚ) * mSs + (3 : ℚ) * mXs - mO) / mO < 363e-5 :=
  @FRC.LedgerML.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 : ∀ (rho ome Ks phi : ℚ), rho = 775.26 → ome = 782.66 → Ks = (891.67 + 895.55) / (2 : ℚ) → phi = 1019.46 → -42e-4 < ((2 : ℚ) * Ks - rho - phi) / (rho + phi) ∧ ((2 : ℚ) * Ks - rho - phi) / (rho + phi) < -41e-4 ∧ (rho + phi) / (2 : ℚ) = 897.36 ∧ |((rho + phi) / (2 : ℚ) - Ks) / Ks| < 5e-3 ∧ |(rho - ome) / ome| < 1e-2 ∧ (phi - rho) / (2 : ℚ) = 122.1 :=
  @FRC.LedgerML.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 : ∀ (mN mL mS mX mD mSs mXs mO : ℚ), mN = 938.9185 → mL = 1115.683 → mS = (1189.37 + 1192.642 + 1197.449) / (3 : ℚ) → mX = (1314.86 + 1321.71) / (2 : ℚ) → mD = 1232.0 → mSs = (1382.8 + 1383.7 + 1387.2) / (3 : ℚ) → mXs = (1531.80 + 1535.0) / (2 : ℚ) → mO = 1672.45 → |((2 : ℚ) * FRC.HadronsML.ml mN mD + FRC.HadronsML.ms mN mL mD + FRC.HadronsML.vll mN mD / (4 : ℚ) - FRC.HadronsML.vls mN mL mD - mS) / mS| < 112e-4 ∧ 111e-4 < |((2 : ℚ) * FRC.HadronsML.ml mN mD + FRC.HadronsML.ms mN mL mD + FRC.HadronsML.vll mN mD / (4 : ℚ) - FRC.HadronsML.vls mN mL mD - mS) / mS| ∧ |(FRC.HadronsML.ml mN mD + (2 : ℚ) * FRC.HadronsML.ms mN mL mD - FRC.HadronsML.vls mN mL mD + FRC.HadronsML.vss mN mL mD / (4 : ℚ) - mX) / mX| < 112e-4 ∧ |((2 : ℚ) * FRC.HadronsML.ml mN mD + FRC.HadronsML.ms mN mL mD + FRC.HadronsML.vll mN mD / (4 : ℚ) + FRC.HadronsML.vls mN mL mD / (2 : ℚ) - mSs) / mSs| < 112e-4 ∧ |(FRC.HadronsML.ml mN mD + (2 : ℚ) * FRC.HadronsML.ms mN mL mD + FRC.HadronsML.vls mN mL mD / (2 : ℚ) + FRC.HadronsML.vss mN mL mD / (4 : ℚ) - mXs) / mXs| < 112e-4 ∧ |((3 : ℚ) * FRC.HadronsML.ms mN mL mD + (3 / 4 : ℚ) * FRC.HadronsML.vss mN mL mD - mO) / mO| < 112e-4 :=
  @FRC.LedgerML.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 : ∀ (mN mL : ℚ), mN = 938.9185 → mL = 1115.683 → mL - mN = 176.7645 ∧ 176.75 < mL - mN ∧ mL - mN < 176.85 :=
  @FRC.LedgerML.p35061
-- end ledger predicates

end FRC.Hadrons