Flavour.lean — FrcLedger

1import Mathlib2import FrcLedger.Theme.Flavour3import FrcLedger.Keys.Chart45/-!6# 28-flavour — the chart readings on Mathlib (17 October 2026)78The paper module of *Fermion Flavour Sector over Finite Relational Substrate* (tree `28-flavour-20260626`) on Mathlib:9every declaration is the chart theme's (`FrcLedger/Theme/Flavour.lean`), under the paper's name — the measured Koide10value, the up-quark band, the Gatto terms, the effective powers, the double ratio, the leading-order ratio, the reactor11estimate, the Jarlskog invariant, the TM2 relation at maximal mixing, the exact-TM2 solar value, the neutrino floor and the12Majorana band. Classical (tier 2). The finite content is the core's (`FrcCore/Theme/Flavour.lean`, no axioms); the13predicates `p28NNN` at the end are generated by `make_predicates.py`, aliases of the keys of `Keys/Chart.lean`.14-/1516namespace FRC.Flavour1718open Real1920/-! ## Old names (17 October 2026): every declaration of this module is an alias of the chart theme's (`FRC.FlavourML`,21`FrcLedger/Theme/Flavour.lean`), under the paper's name -/2223/-- 28:P1, 28:X1 — the measured charged-lepton Koide value (`FlavourML.koide_measured`). -/24theorem koide_measured (me mmu mtau : ℝ) (h1 : me = 0.51099895) (h2 : mmu = 105.6583755) (h3 : mtau = 1776.86) :25    |(me + mmu + mtau) / (sqrt me + sqrt mmu + sqrt mtau) ^ 2 - 2 / 3| < 1 / 100000 :=26  FRC.FlavourML.koide_measured me mmu mtau h1 h2 h32728/-- 28:C4, 28:X2, 28:P2 — the up-quark Koide value in three schemes (`FlavourML.koide_up_band`). -/29theorem koide_up_band :30    (0.8489 < (2.16 + 1270 + 172570) / (sqrt 2.16 + sqrt 1270 + sqrt 172570) ^ 2 ∧31      (2.16 + 1270 + 172570) / (sqrt 2.16 + sqrt 1270 + sqrt 172570) ^ 2 < (0.8490 : ℝ)) ∧32    (0.8316 < (2.2 + 1670 + 172800) / (sqrt 2.2 + sqrt 1670 + sqrt 172800) ^ 2 ∧33      (2.2 + 1670 + 172800) / (sqrt 2.2 + sqrt 1670 + sqrt 172800) ^ 2 < (0.8317 : ℝ)) ∧34    (0.8875 < (1.27 + 619 + 168300) / (sqrt 1.27 + sqrt 619 + sqrt 168300) ^ 2 ∧35      (1.27 + 619 + 168300) / (sqrt 1.27 + sqrt 619 + sqrt 168300) ^ 2 < (0.8876 : ℝ)) ∧36    (0.83 : ℝ) < 5 / 6 ∧ (5 / 6 : ℝ) < 0.89 :=37  FRC.FlavourML.koide_up_band3839/-- 28:C6, 28:X4, 28:P3 — the Gatto relation's leading term and its value at φ = π/2 (`FlavourML.gatto_leading`). -/40theorem gatto_leading (md ms mu mc Vus : ℝ) (hd : md = 4.67) (hs : ms = 93.4) (hu : mu = 2.16) (hc : mc = 1270)41    (hV : Vus = 0.2243) :42    0.2236 < sqrt (md / ms) ∧ sqrt (md / ms) < 0.22361 ∧ |sqrt (md / ms) - Vus| < 0.0035 * Vus ∧43    0.2273 < sqrt (md / ms + mu / mc) ∧ sqrt (md / ms + mu / mc) < 0.2275 :=44  FRC.FlavourML.gatto_leading md ms mu mc Vus hd hs hu hc hV4546/-- 28:C7, 28:X3, 28:X6 — the effective Froggatt–Nielsen powers inside their integer brackets (`FlavourML.texture_powers`). -/47theorem texture_powers (lam md ms mb me mmu mtau mu mc mt : ℚ) (hl : lam = 0.2243) (hd : md = 4.67) (hs : ms = 93.4)48    (hb : mb = 4180) (he : me = 0.51099895) (hmu : mmu = 105.6583755) (ht : mtau = 1776.86) (hu : mu = 2.16)49    (hc : mc = 1270) (htop : mt = 172570) :50    (lam ^ 5 < md / mb ∧ md / mb < lam ^ 4) ∧ (lam ^ 3 < ms / mb ∧ ms / mb < lam ^ 2) ∧51    (lam ^ 6 < me / mtau ∧ me / mtau < lam ^ 5) ∧ (lam ^ 2 < mmu / mtau ∧ mmu / mtau < lam) ∧52    (lam ^ 8 < mu / mt ∧ mu / mt < lam ^ 7) ∧ (lam ^ 4 < mc / mt ∧ mc / mt < lam ^ 3) :=53  FRC.FlavourML.texture_powers lam md ms mb me mmu mtau mu mc mt hl hd hs hb he hmu ht hu hc htop5455/-- 28:X5, 00:P3 — the Georgi–Jarlskog double ratio (`FlavourML.gj_ratio`). -/56theorem gj_ratio (me mmu md ms : ℚ) (he : me = 0.51099895) (hmu : mmu = 105.6583755) (hd : md = 4.67) (hs : ms = 93.4) :57    10.3 < (mmu / me) / (ms / md) ∧ (mmu / me) / (ms / md) < 10.5 ∧58    9 * 1.10 < (mmu / me) / (ms / md) ∧ (mmu / me) / (ms / md) < 9 * 1.20 :=59  FRC.FlavourML.gj_ratio me mmu md ms he hmu hd hs6061/-- 28:C3, 28:X7 — the leading-order mass ratio 7 − 4√3 (`FlavourML.lo_ratio`). -/62theorem lo_ratio (mmu mtau : ℝ) (h2 : mmu = 105.6583755) (h3 : mtau = 1776.86) :63    (0.0717 : ℝ) < 7 - 4 * sqrt 3 ∧ 7 - 4 * sqrt 3 < 0.0719 ∧ 0.0594 < mmu / mtau ∧ mmu / mtau < 0.0595 :=64  FRC.FlavourML.lo_ratio mmu mtau h2 h36566/-- 28:C9, 28:X9 — the reactor angle at leading order (`FlavourML.theta13_estimate`). -/67theorem theta13_estimate (Vus s13 : ℝ) (hV : Vus = 0.2243) (hs : s13 = 0.1488) :68    0.1585 < Vus / sqrt 2 ∧ Vus / sqrt 2 < 0.1587 ∧ 1.06 * s13 < Vus / sqrt 2 ∧ Vus / sqrt 2 < 1.07 * s13 :=69  FRC.FlavourML.theta13_estimate Vus s13 hV hs7071/-- 28:C10, 28:X10, 28:P8 — the maximal Jarlskog invariant (`FlavourML.jarlskog`). -/72theorem jarlskog : (1 : ℝ) / (6 * sqrt 3) = sqrt 3 / 18 ∧ ((1 : ℝ) / (6 * sqrt 3)) ^ 2 = 1 / 108 :=73  FRC.FlavourML.jarlskog7475/-- 28:C10, 28:P8 — the TM2 relation at maximal atmospheric mixing (`FlavourML.tm2_at_maximal`). -/76theorem tm2_at_maximal (s13 : ℝ) :77    Real.cos (2 * (π / 4)) / Real.sin (2 * (π / 4)) * ((1 - 2 * s13 ^ 2) / (s13 * sqrt (2 - 3 * s13 ^ 2))) = 0 ∧78    Real.arccos 0 = π / 2 :=79  FRC.FlavourML.tm2_at_maximal s138081/-- 28:C10 — the exact-TM2 solar value (`FlavourML.exact_tm2_solar`). -/82theorem exact_tm2_solar (s13sq : ℚ) (h : s13sq = 0.02215) :83    0.3408 < 1 / (3 * (1 - s13sq)) ∧ 1 / (3 * (1 - s13sq)) < 0.3410 ∧ (0.307 : ℚ) < 1 / (3 * (1 - s13sq)) :=84  FRC.FlavourML.exact_tm2_solar s13sq h8586/-- 28:P5, 28:P6, 28:X11, 00:P3 — the m₁ = 0 floor of the neutrino mass sum (`FlavourML.neutrino_floor`). -/87theorem neutrino_floor (dm21 dm31 : ℝ) (h21 : dm21 = 7.49e-5) (h31 : dm31 = 2.513e-3) :88    0.0587 < sqrt dm21 + sqrt dm31 ∧ sqrt dm21 + sqrt dm31 < 0.0589 :=89  FRC.FlavourML.neutrino_floor dm21 dm31 h21 h319091/-- 28:P7 — the effective Majorana mass band at m₁ = 0 (`FlavourML.majorana_band`). -/92theorem majorana_band (dm21 dm31 s12sq s13sq : ℝ) (h21 : dm21 = 7.49e-5) (h31 : dm31 = 2.513e-3)93    (h12 : s12sq = 0.307) (h13 : s13sq = 0.02215) :94    2.59 < (1 - s13sq) * s12sq * (1000 * sqrt dm21) ∧ (1 - s13sq) * s12sq * (1000 * sqrt dm21) < 2.61 ∧95    1.10 < s13sq * (1000 * sqrt dm31) ∧ s13sq * (1000 * sqrt dm31) < 1.12 ∧96    1.47 < (1 - s13sq) * s12sq * (1000 * sqrt dm21) - s13sq * (1000 * sqrt dm31) ∧97    (1 - s13sq) * s12sq * (1000 * sqrt dm21) + s13sq * (1000 * sqrt dm31) < 3.71 :=98  FRC.FlavourML.majorana_band dm21 dm31 s12sq s13sq h21 h31 h12 h1399100-- Ledger predicates of 28-flavour (generated by make_predicates.py from docs/28-flavour/28-flavour-ledger.json; edit the ledger, not this section)101/-- 28:C3 (p28014) — The leading boundary phase is the framed-rational winding $\delta_{\mathrm{LO}}=\tfrac38-\tfrac13=\tfrac1{24}$ cycle (split-torus boundary $\tfrac38$ minus generation $\tfrac13$; continuum $\pi/12$ [approx]); massless lightest generation. -/102theorem p28014 : ∀ (mmu mtau : ℝ), mmu = 105.6583755 → mtau = 1776.86 → 717e-4 < (7 : ℝ) - (4 : ℝ) * √(3 : ℝ) ∧ (7 : ℝ) - (4 : ℝ) * √(3 : ℝ) < 719e-4 ∧ 594e-4 < mmu / mtau ∧ mmu / mtau < 595e-4 :=103  @FRC.LedgerML.p28014104/-- 28:C4 (p28015) — The squared amplitudes are the cyclotomic norms $r_\ell^2=N(1-i)=2$, $r_u^2=N(1-\omega)=3$ (on B5), hence $Q_\ell=\tfrac23$, $Q_u=\tfrac56$ in framed arithmetic ($Q_u=0.849$ in the working scheme, band $0.83$--$0.89$); the down sector is the GJ-dressed intermediate. -/105theorem p28015 : (0.8489 < (2.16 + (1270 : ℝ) + (172570 : ℝ)) / (√2.16 + √(1270 : ℝ) + √(172570 : ℝ)) ^ (2 : ℕ) ∧ (2.16 + (1270 : ℝ) + (172570 : ℝ)) / (√2.16 + √(1270 : ℝ) + √(172570 : ℝ)) ^ (2 : ℕ) < 0.8490) ∧ (0.8316 < (2.2 + (1670 : ℝ) + (172800 : ℝ)) / (√2.2 + √(1670 : ℝ) + √(172800 : ℝ)) ^ (2 : ℕ) ∧ (2.2 + (1670 : ℝ) + (172800 : ℝ)) / (√2.2 + √(1670 : ℝ) + √(172800 : ℝ)) ^ (2 : ℕ) < 0.8317) ∧ (0.8875 < (1.27 + (619 : ℝ) + (168300 : ℝ)) / (√1.27 + √(619 : ℝ) + √(168300 : ℝ)) ^ (2 : ℕ) ∧ (1.27 + (619 : ℝ) + (168300 : ℝ)) / (√1.27 + √(619 : ℝ) + √(168300 : ℝ)) ^ (2 : ℕ) < 0.8876) ∧ 0.83 < (5 / 6 : ℝ) ∧ (5 / 6 : ℝ) < 0.89 :=106  @FRC.LedgerML.p28015107/-- 28:C6 (p28017) — The Gatto Cabibbo relation $V_{us}=|\sqrt{m_d/m_s}-e^{i\varphi}\sqrt{m_u/m_c}|$, the phase $\varphi$ a kernel datum ($85^\circ\pm10^\circ$ from the data). -/108theorem p28017 : ∀ (md ms mu mc Vus : ℝ), md = 4.67 → ms = 93.4 → mu = 2.16 → mc = (1270 : ℝ) → Vus = 0.2243 → 0.2236 < √(md / ms) ∧ √(md / ms) < 0.22361 ∧ |√(md / ms) - Vus| < 35e-4 * Vus ∧ 0.2273 < √(md / ms + mu / mc) ∧ √(md / ms + mu / mc) < 0.2275 :=109  @FRC.LedgerML.p28017110/-- 28:C7 (p28018) — Up-sector doubling $m^u_i\sim(m^d_i)^2$ from the $\mathbf{10}\cdot\mathbf{10}$ Yukawa. -/111theorem p28018 : ∀ (lam md ms mb me mmu mtau mu mc mt : ℚ), lam = 0.2243 → md = 4.67 → ms = 93.4 → mb = (4180 : ℚ) → me = 0.51099895 → mmu = 105.6583755 → mtau = 1776.86 → mu = 2.16 → mc = (1270 : ℚ) → mt = (172570 : ℚ) → (lam ^ (5 : ℕ) < md / mb ∧ md / mb < lam ^ (4 : ℕ)) ∧ (lam ^ (3 : ℕ) < ms / mb ∧ ms / mb < lam ^ (2 : ℕ)) ∧ (lam ^ (6 : ℕ) < me / mtau ∧ me / mtau < lam ^ (5 : ℕ)) ∧ (lam ^ (2 : ℕ) < mmu / mtau ∧ mmu / mtau < lam) ∧ (lam ^ (8 : ℕ) < mu / mt ∧ mu / mt < lam ^ (7 : ℕ)) ∧ lam ^ (4 : ℕ) < mc / mt ∧ mc / mt < lam ^ (3 : ℕ) :=112  @FRC.LedgerML.p28018113/-- 28:C9 (p28020) — The reactor angle at leading order, $\sin\theta_{13}=\sin\theta_C/\sqrt2\simeq\delta_0/\sqrt2$ (quark--lepton complementarity): $0.159$ against the measured $0.149$, $7\%$, no correction derived. -/114theorem p28020 : ∀ (Vus s13 : ℝ), Vus = 0.2243 → s13 = 0.1488 → 0.1585 < Vus / √(2 : ℝ) ∧ Vus / √(2 : ℝ) < 0.1587 ∧ 1.06 * s13 < Vus / √(2 : ℝ) ∧ Vus / √(2 : ℝ) < 1.07 * s13 :=115  @FRC.LedgerML.p28020116/-- 28:C10 (p28021) — TM2 selected: the trivial $C_3$ character $(1,1,1)/\sqrt3$ is the protected column, so $\cos\delta_{\mathrm{CP}}$ is locked to $\theta_{23}$ by \eqref{eq:tm2}; the magic Jarlskog $J=1/(6\sqrt3)$ is maximal CP, the sign fixed by the drive. -/117theorem p28021 : ((1 : ℝ) / ((6 : ℝ) * √(3 : ℝ)) = √(3 : ℝ) / (18 : ℝ) ∧ ((1 : ℝ) / ((6 : ℝ) * √(3 : ℝ))) ^ (2 : ℕ) = (1 / 108 : ℝ)) ∧ (∀ (s13 : ℝ), Real.cos ((2 : ℝ) * (Real.pi / (4 : ℝ))) / Real.sin ((2 : ℝ) * (Real.pi / (4 : ℝ))) * (((1 : ℝ) - (2 : ℝ) * s13 ^ (2 : ℕ)) / (s13 * √((2 : ℝ) - (3 : ℝ) * s13 ^ (2 : ℕ)))) = (0 : ℝ) ∧ Real.arccos (0 : ℝ) = Real.pi / (2 : ℝ)) ∧ ∀ (s13sq : ℚ), s13sq = 2215e-5 → 0.3408 < (1 : ℚ) / ((3 : ℚ) * ((1 : ℚ) - s13sq)) ∧ (1 : ℚ) / ((3 : ℚ) * ((1 : ℚ) - s13sq)) < 0.3410 ∧ 0.307 < (1 : ℚ) / ((3 : ℚ) * ((1 : ℚ) - s13sq)) :=118  @FRC.LedgerML.p28021119/-- 28:X1 (p28025) — \textbf{The Koide ratio} is exactly $2/3$ given the quarter-turn realisation B5, the cube-root generation orbit bisected at the quarter-turn ($\rho^2=2^{-1}$), an exact value rather than an unexplained empirical coincidence. -/120theorem p28025 : ∀ (me mmu mtau : ℝ), me = 0.51099895 → mmu = 105.6583755 → mtau = 1776.86 → |(me + mmu + mtau) / (√me + √mmu + √mtau) ^ (2 : ℕ) - (2 / 3 : ℝ)| < (1 / 100000 : ℝ) :=121  @FRC.LedgerML.p28025122/-- 28:X2 (p28026) — \textbf{The up-quark Koide value} is $5/6$ in framed arithmetic ($0.849$ in the working scheme, $0.832$ with pole masses), the cube-root colour norm $r_u^2=N(1-\omega)=3$ against the colourless $N(1-i)=2$, a ratio where the Standard Model carries no relation at all. -/123theorem p28026 : (0.8489 < (2.16 + (1270 : ℝ) + (172570 : ℝ)) / (√2.16 + √(1270 : ℝ) + √(172570 : ℝ)) ^ (2 : ℕ) ∧ (2.16 + (1270 : ℝ) + (172570 : ℝ)) / (√2.16 + √(1270 : ℝ) + √(172570 : ℝ)) ^ (2 : ℕ) < 0.8490) ∧ (0.8316 < (2.2 + (1670 : ℝ) + (172800 : ℝ)) / (√2.2 + √(1670 : ℝ) + √(172800 : ℝ)) ^ (2 : ℕ) ∧ (2.2 + (1670 : ℝ) + (172800 : ℝ)) / (√2.2 + √(1670 : ℝ) + √(172800 : ℝ)) ^ (2 : ℕ) < 0.8317) ∧ (0.8875 < (1.27 + (619 : ℝ) + (168300 : ℝ)) / (√1.27 + √(619 : ℝ) + √(168300 : ℝ)) ^ (2 : ℕ) ∧ (1.27 + (619 : ℝ) + (168300 : ℝ)) / (√1.27 + √(619 : ℝ) + √(168300 : ℝ)) ^ (2 : ℕ) < 0.8876) ∧ 0.83 < (5 / 6 : ℝ) ∧ (5 / 6 : ℝ) < 0.89 :=124  @FRC.LedgerML.p28026125/-- 28:X3 (p28027) — \textbf{The flavour charges} are the role depths $(0,1,2)$ of the closed primitive-role ladder, derived as the three generative roles rather than assigned to fit the hierarchy. -/126theorem p28027 : ∀ (lam md ms mb me mmu mtau mu mc mt : ℚ), lam = 0.2243 → md = 4.67 → ms = 93.4 → mb = (4180 : ℚ) → me = 0.51099895 → mmu = 105.6583755 → mtau = 1776.86 → mu = 2.16 → mc = (1270 : ℚ) → mt = (172570 : ℚ) → (lam ^ (5 : ℕ) < md / mb ∧ md / mb < lam ^ (4 : ℕ)) ∧ (lam ^ (3 : ℕ) < ms / mb ∧ ms / mb < lam ^ (2 : ℕ)) ∧ (lam ^ (6 : ℕ) < me / mtau ∧ me / mtau < lam ^ (5 : ℕ)) ∧ (lam ^ (2 : ℕ) < mmu / mtau ∧ mmu / mtau < lam) ∧ (lam ^ (8 : ℕ) < mu / mt ∧ mu / mt < lam ^ (7 : ℕ)) ∧ lam ^ (4 : ℕ) < mc / mt ∧ mc / mt < lam ^ (3 : ℕ) :=127  @FRC.LedgerML.p28027128/-- 28:X4 (p28028) — \textbf{The Cabibbo angle} is the Gatto relation $V_{us}=|\sqrt{m_d/m_s}-e^{i\varphi}\sqrt{m_u/m_c}|$ following from the role-depth texture, the leading term at $0.3\%$ and the phase $\varphi$ a kernel datum, so two otherwise-independent observables are tied rather than measured apart. -/129theorem p28028 : ∀ (md ms mu mc Vus : ℝ), md = 4.67 → ms = 93.4 → mu = 2.16 → mc = (1270 : ℝ) → Vus = 0.2243 → 0.2236 < √(md / ms) ∧ √(md / ms) < 0.22361 ∧ |√(md / ms) - Vus| < 35e-4 * Vus ∧ 0.2273 < √(md / ms + mu / mc) ∧ √(md / ms + mu / mc) < 0.2275 :=130  @FRC.LedgerML.p28028131/-- 28:X5 (p28029) — \textbf{The Georgi--Jarlskog factor} is the colour count $N_c=3$, the $B\!-\!L$ Clebsch of the $\overline{\mathbf{126}}$, not a texture coefficient inserted by hand; its double ratio $9$ against the measured $10.4\pm0.5$ is the open $15\%$ excess of the minimal Clebsch. -/132theorem p28029 : ∀ (me mmu md ms : ℚ), me = 0.51099895 → mmu = 105.6583755 → md = 4.67 → ms = 93.4 → 10.3 < mmu / me / (ms / md) ∧ mmu / me / (ms / md) < 10.5 ∧ (9 : ℚ) * 1.10 < mmu / me / (ms / md) ∧ mmu / me / (ms / md) < (9 : ℚ) * 1.20 :=133  @FRC.LedgerML.p28029134/-- 28:X6 (p28030) — \textbf{The up-sector doubling} $m^u_i\sim(m^d_i)^2$ is forced by the $\mathbf{10}\cdot\mathbf{10}$ Yukawa, so the steeper up hierarchy is a consequence rather than a separate assumption. -/135theorem p28030 : ∀ (lam md ms mb me mmu mtau mu mc mt : ℚ), lam = 0.2243 → md = 4.67 → ms = 93.4 → mb = (4180 : ℚ) → me = 0.51099895 → mmu = 105.6583755 → mtau = 1776.86 → mu = 2.16 → mc = (1270 : ℚ) → mt = (172570 : ℚ) → (lam ^ (5 : ℕ) < md / mb ∧ md / mb < lam ^ (4 : ℕ)) ∧ (lam ^ (3 : ℕ) < ms / mb ∧ ms / mb < lam ^ (2 : ℕ)) ∧ (lam ^ (6 : ℕ) < me / mtau ∧ me / mtau < lam ^ (5 : ℕ)) ∧ (lam ^ (2 : ℕ) < mmu / mtau ∧ mmu / mtau < lam) ∧ (lam ^ (8 : ℕ) < mu / mt ∧ mu / mt < lam ^ (7 : ℕ)) ∧ lam ^ (4 : ℕ) < mc / mt ∧ mc / mt < lam ^ (3 : ℕ) :=136  @FRC.LedgerML.p28030137/-- 28:X7 (p28031) — \textbf{The electron's extreme lightness} is the quarter-turn boundary: the lightest generation sits where the winding amplitude vanishes, massless at leading order, rather than an anomalously small Yukawa tuned by hand. -/138theorem p28031 : ∀ (mmu mtau : ℝ), mmu = 105.6583755 → mtau = 1776.86 → 717e-4 < (7 : ℝ) - (4 : ℝ) * √(3 : ℝ) ∧ (7 : ℝ) - (4 : ℝ) * √(3 : ℝ) < 719e-4 ∧ 594e-4 < mmu / mtau ∧ mmu / mtau < 595e-4 :=139  @FRC.LedgerML.p28031140/-- 28:X9 (p28033) — \textbf{The reactor angle} is, at leading order, $\sin\theta_{13}=\sin\theta_C/\sqrt2=0.159$, quark--lepton complementarity through the quarter-turn, $7\%$ above the observed $0.149$ with no correction derived: a leading-order estimate of the mixing parameter, not a prediction. -/141theorem p28033 : ∀ (Vus s13 : ℝ), Vus = 0.2243 → s13 = 0.1488 → 0.1585 < Vus / √(2 : ℝ) ∧ Vus / √(2 : ℝ) < 0.1587 ∧ 1.06 * s13 < Vus / √(2 : ℝ) ∧ Vus / √(2 : ℝ) < 1.07 * s13 :=142  @FRC.LedgerML.p28033143/-- 28:X10 (p28034) — \textbf{Near-maximal leptonic CP} is the cube-root phase: $\mathrm{Im}\,\omega=\sqrt3/2$ gives the maximal Jarlskog $J=1/(6\sqrt3)$, so the cubic reappears as CP violation rather than a free phase fitted to data. -/144theorem p28034 : (1 : ℝ) / ((6 : ℝ) * √(3 : ℝ)) = √(3 : ℝ) / (18 : ℝ) ∧ ((1 : ℝ) / ((6 : ℝ) * √(3 : ℝ))) ^ (2 : ℕ) = (1 / 108 : ℝ) :=145  @FRC.LedgerML.p28034146/-- 28:X11 (p28035) — \textbf{The neutrino spectrum} (a near-massless lightest state, $\sum m_\nu\simeq59\,$meV on the normal branch) follows from colourlessness fixing $Q_\nu=2/3$, the transpose fixed point under the alignment $M_R\propto m_D$ (Y1) and the boundary branch that selects the ordering (B6), rather than three independent neutrino masses. -/147theorem p28035 : ∀ (dm21 dm31 : ℝ), dm21 = 749e-7 → dm31 = 2513e-6 → 587e-4 < √dm21 + √dm31 ∧ √dm21 + √dm31 < 589e-4 :=148  @FRC.LedgerML.p28035149/-- 28:P1 (p28036) — Charged-lepton Koide $Q_\ell=2/3$ exact on B5 (measured $0.666661\pm0.000007$); $m_e=0.5106$ vs $0.5110$ MeV. Falsifier: a lepton-mass shift of $Q_\ell$ off $2/3$ beyond the $\tau$-mass tolerance. -/150theorem p28036 : ∀ (me mmu mtau : ℝ), me = 0.51099895 → mmu = 105.6583755 → mtau = 1776.86 → |(me + mmu + mtau) / (√me + √mmu + √mtau) ^ (2 : ℕ) - (2 / 3 : ℝ)| < (1 / 100000 : ℝ) :=151  @FRC.LedgerML.p28036152/-- 28:P2 (p28037) — Up-quark Koide $Q_u=5/6$ in framed arithmetic, $r_u^2=N(1-\omega)=3$; continuum $0.849$ in the working scheme, $0.832$ with pole masses, band $0.83$--$0.89$. Falsifier: up/charm/top masses moving $Q_u$ outside the band in every standard scheme. -/153theorem p28037 : (0.8489 < (2.16 + (1270 : ℝ) + (172570 : ℝ)) / (√2.16 + √(1270 : ℝ) + √(172570 : ℝ)) ^ (2 : ℕ) ∧ (2.16 + (1270 : ℝ) + (172570 : ℝ)) / (√2.16 + √(1270 : ℝ) + √(172570 : ℝ)) ^ (2 : ℕ) < 0.8490) ∧ (0.8316 < (2.2 + (1670 : ℝ) + (172800 : ℝ)) / (√2.2 + √(1670 : ℝ) + √(172800 : ℝ)) ^ (2 : ℕ) ∧ (2.2 + (1670 : ℝ) + (172800 : ℝ)) / (√2.2 + √(1670 : ℝ) + √(172800 : ℝ)) ^ (2 : ℕ) < 0.8317) ∧ (0.8875 < (1.27 + (619 : ℝ) + (168300 : ℝ)) / (√1.27 + √(619 : ℝ) + √(168300 : ℝ)) ^ (2 : ℕ) ∧ (1.27 + (619 : ℝ) + (168300 : ℝ)) / (√1.27 + √(619 : ℝ) + √(168300 : ℝ)) ^ (2 : ℕ) < 0.8876) ∧ 0.83 < (5 / 6 : ℝ) ∧ (5 / 6 : ℝ) < 0.89 :=154  @FRC.LedgerML.p28037155/-- 28:P3 (p28038) — Cabibbo $V_{us}=|\sqrt{m_d/m_s}-e^{i\varphi}\sqrt{m_u/m_c}|$: leading term $0.224^{+0.011}_{-0.004}$ vs $0.2243$ ($0.3\%$), the up term $\pm0.04$ with $\varphi$ open. Falsifier: no $\varphi$ satisfying the relation within the input band. -/156theorem p28038 : ∀ (md ms mu mc Vus : ℝ), md = 4.67 → ms = 93.4 → mu = 2.16 → mc = (1270 : ℝ) → Vus = 0.2243 → 0.2236 < √(md / ms) ∧ √(md / ms) < 0.22361 ∧ |√(md / ms) - Vus| < 35e-4 * Vus ∧ 0.2273 < √(md / ms + mu / mc) ∧ √(md / ms + mu / mc) < 0.2275 :=157  @FRC.LedgerML.p28038158/-- 28:P5 (p28039) — Normal neutrino ordering, from $Q_\nu=2/3$, the two $\Delta m^2$ and the boundary branch (B6); the signed circulant solves both orderings (C11b). Falsifier: inverted ordering. -/159theorem p28039 : ∀ (dm21 dm31 : ℝ), dm21 = 749e-7 → dm31 = 2513e-6 → 587e-4 < √dm21 + √dm31 ∧ √dm21 + √dm31 < 589e-4 :=160  @FRC.LedgerML.p28039161/-- 28:P6 (p28040) — Mass-sum floor $\sum m_\nu=58.8$ meV at NuFIT~6.0 ($m_1{=}0$, $m_2{=}8.65$, $m_3{=}50.13$ meV), the $m_1=0$ normal-ordering floor. Falsifier: a cosmological $\sum m_\nu<0.058$ eV. -/162theorem p28040 : ∀ (dm21 dm31 : ℝ), dm21 = 749e-7 → dm31 = 2513e-6 → 587e-4 < √dm21 + √dm31 ∧ √dm21 + √dm31 < 589e-4 :=163  @FRC.LedgerML.p28040164/-- 28:P7 (p28041) — Effective Majorana mass $m_{\beta\beta}{\simeq}1.5$--$3.7$ meV (NO, at $m_1=0$, over the relative Majorana phase; $1.2$--$4.0$ meV with the fitted $m_1=0.36$ meV). Falsifier: a $0\nu\beta\beta$ signal at the inverted scale $15$--$50$ meV. -/165theorem p28041 : ∀ (dm21 dm31 s12sq s13sq : ℝ), dm21 = 749e-7 → dm31 = 2513e-6 → s12sq = 0.307 → s13sq = 2215e-5 → 2.59 < ((1 : ℝ) - s13sq) * s12sq * ((1000 : ℝ) * √dm21) ∧ ((1 : ℝ) - s13sq) * s12sq * ((1000 : ℝ) * √dm21) < 2.61 ∧ 1.10 < s13sq * ((1000 : ℝ) * √dm31) ∧ s13sq * ((1000 : ℝ) * √dm31) < 1.12 ∧ 1.47 < ((1 : ℝ) - s13sq) * s12sq * ((1000 : ℝ) * √dm21) - s13sq * ((1000 : ℝ) * √dm31) ∧ ((1 : ℝ) - s13sq) * s12sq * ((1000 : ℝ) * √dm21) + s13sq * ((1000 : ℝ) * √dm31) < 3.71 :=166  @FRC.LedgerML.p28041167/-- 28:P8 (p28042) — Leptonic CP locked to the octant by \eqref{eq:tm2}: $\delta_{\mathrm{CP}}\in(204^\circ,310^\circ)$ over the $3\sigma$ $\theta_{23}$ range, $\pm124^\circ$/$\pm74^\circ$ at the NuFIT~6.0 best fits, $\sin\delta_{\mathrm{CP}}{<}0$, $J=1/(6\sqrt3)$. Falsifier: CP-conserving $\delta_{\mathrm{CP}}$, $\sin\delta_{\mathrm{CP}}{>}0$, or $(\theta_{23},\delta_{\mathrm{CP}})$ off the relation. -/168theorem p28042 : ((1 : ℝ) / ((6 : ℝ) * √(3 : ℝ)) = √(3 : ℝ) / (18 : ℝ) ∧ ((1 : ℝ) / ((6 : ℝ) * √(3 : ℝ))) ^ (2 : ℕ) = (1 / 108 : ℝ)) ∧ ∀ (s13 : ℝ), Real.cos ((2 : ℝ) * (Real.pi / (4 : ℝ))) / Real.sin ((2 : ℝ) * (Real.pi / (4 : ℝ))) * (((1 : ℝ) - (2 : ℝ) * s13 ^ (2 : ℕ)) / (s13 * √((2 : ℝ) - (3 : ℝ) * s13 ^ (2 : ℕ)))) = (0 : ℝ) ∧ Real.arccos (0 : ℝ) = Real.pi / (2 : ℝ) :=169  @FRC.LedgerML.p28042170-- end ledger predicates171172end FRC.Flavour173