Flavour.lean — FrcCore

1import FrcCore.Theme.Flavour2import FrcCore.Theme.Interactions3import FrcCore.Theme.Ladder4import FrcCore.Keys.Flavour5import FrcCore.Keys.Interactions67/-!8# 28-flavour — the flavour sector on the shell, no axioms (17 October 2026)910The paper module of *Fermion Flavour Sector over Finite Relational Substrate* (tree `28-flavour-20260626`): every11declaration the paper cites is the flavour theme's (`Theme/Flavour.lean`: the circulant and its spectrum, the12quarter-turn boundary and the leading-order spectrum, the norms `2` and `3`, the role-depth texture, the Gatto relation13and the Cabibbo modulus, the transpose identities, the protected column, the trimaximal magic matrix and its Jarlskog14invariant, the trace relations, the seesaw of circulants), the interactions theme's (`Theme/Interactions.lean`: the Koide15form, the reflection algebra and the fifth direction) or the horizon theme's (`Theme/Ladder.lean`: the closed role ladder),16under their own names. The predicates `p28NNN` at the end are generated by `make_predicates.py`, aliases of the keys of17`Keys/Flavour.lean` and `Keys/Interactions.lean`. Every declaration is checked to depend on no axiom18(`check_core_axioms.py`).19-/2021namespace FRC.Flavour2223open FRC.Shell FRC.Extension FRC.Unitary FRC.Interactions2425-- Ledger predicates of 28-flavour (generated by make_predicates.py from docs/28-flavour/28-flavour-ledger.json; edit the ledger, not this section)26/-- 28:C1 (p28012) — Generation universality $\Rightarrow$ the amplitude matrix is a $C_3$-circulant $\Rightarrow$ the Koide functional form. -/27theorem p28012 : (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (a b c ω : FRC.Extension.Ext p ν), ω * ω + ω + (1 : FRC.Extension.Ext p ν) = (0 : FRC.Extension.Ext p ν) → c + a * ω + b * (ω * ω) = ω * (a + b * ω + c * (ω * ω)) ∧ b + c * ω + a * (ω * ω) = ω * ω * (a + b * ω + c * (ω * ω)) ∧ c + a * (ω * ω) + b * ω = ω * ω * (a + b * (ω * ω) + c * ω) ∧ b + c * (ω * ω) + a * ω = ω * (a + b * (ω * ω) + c * ω)) ∧ (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (a b c ω : FRC.Extension.Ext p ν), ω * ω + ω + (1 : FRC.Extension.Ext p ν) = (0 : FRC.Extension.Ext p ν) → a + b + c + (a + b * ω + c * (ω * ω)) + (a + b * (ω * ω) + c * ω) = ((1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν)) * a) ∧ (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (a b c ω : FRC.Extension.Ext p ν), ω * ω + ω + (1 : FRC.Extension.Ext p ν) = (0 : FRC.Extension.Ext p ν) → (a + b + c) * (a + b + c) + (a + b * ω + c * (ω * ω)) * (a + b * ω + c * (ω * ω)) + (a + b * (ω * ω) + c * ω) * (a + b * (ω * ω) + c * ω) = ((1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν)) * (a * a) + ((1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν)) * (b * c)) ∧ ∀ {p : Nat} [FRC.Pos p] (a₀ a₁ a₂ ω : FRC.Shell p), ω * ω + ω + (1 : FRC.Shell p) = (0 : FRC.Shell p) → (3 : FRC.Shell p) * (a₀ * a₀ + a₁ * a₁ + a₂ * a₂) = (a₀ + a₁ + a₂) * (a₀ + a₁ + a₂) + (2 : FRC.Shell p) * ((a₀ + a₁ * ω + a₂ * (ω * ω)) * (a₀ + a₁ * (ω * ω) + a₂ * ω)) :=28  @FRC.Ledger.p2801229/-- 28:C2 (p28013) — $Q=2/3\Leftrightarrow r=\sqrt2\Leftrightarrow\rho^2=\tfrac12$ (the equivalence an identity); the value $\rho^2=\tfrac12$ is the realisation B5. -/30theorem p28013 : (∀ {p : Nat} [FRC.Pos p] (a₀ a₁ a₂ ω : FRC.Shell p), ω * ω + ω + (1 : FRC.Shell p) = (0 : FRC.Shell p) → ((3 : FRC.Shell p) * (a₀ * a₀ + a₁ * a₁ + a₂ * a₂) = (2 : FRC.Shell p) * ((a₀ + a₁ + a₂) * (a₀ + a₁ + a₂)) ↔ (2 : FRC.Shell p) * ((a₀ + a₁ * ω + a₂ * (ω * ω)) * (a₀ + a₁ * (ω * ω) + a₂ * ω)) = (a₀ + a₁ + a₂) * (a₀ + a₁ + a₂))) ∧ (∀ {p : Nat} [FRC.Pos p] {ν h : FRC.Shell p}, h + h = (1 : FRC.Shell p) → ν + (1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p) = (0 : FRC.Shell p) → ∀ (a₀ a₁ a₂ : FRC.Shell p), FRC.Interactions.omega3 ν h * FRC.Interactions.omega3 ν h + FRC.Interactions.omega3 ν h + (1 : FRC.Extension.Ext p ν) = (0 : FRC.Extension.Ext p ν) ∧ FRC.Interactions.hat2 ν h a₀ a₁ a₂ = (FRC.Interactions.hat1 ν h a₀ a₁ a₂).conj ∧ FRC.Interactions.hat1 ν h a₀ a₁ a₂ * FRC.Interactions.hat2 ν h a₀ a₁ a₂ = FRC.Extension.Ext.ofShell (FRC.Interactions.hat1 ν h a₀ a₁ a₂).norm ∧ (3 : FRC.Shell p) * (a₀ * a₀ + a₁ * a₁ + a₂ * a₂) = (a₀ + a₁ + a₂) * (a₀ + a₁ + a₂) + (2 : FRC.Shell p) * (FRC.Interactions.hat1 ν h a₀ a₁ a₂).norm ∧ ((3 : FRC.Shell p) * (a₀ * a₀ + a₁ * a₁ + a₂ * a₂) = (2 : FRC.Shell p) * ((a₀ + a₁ + a₂) * (a₀ + a₁ + a₂)) ↔ (2 : FRC.Shell p) * (FRC.Interactions.hat1 ν h a₀ a₁ a₂).norm = (a₀ + a₁ + a₂) * (a₀ + a₁ + a₂))) ∧ ∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (a b c ω : FRC.Extension.Ext p ν), ω * ω + ω + (1 : FRC.Extension.Ext p ν) = (0 : FRC.Extension.Ext p ν) → (a + b + c) * (a + b + c) + (a + b * ω + c * (ω * ω)) * (a + b * ω + c * (ω * ω)) + (a + b * (ω * ω) + c * ω) * (a + b * (ω * ω) + c * ω) = ((1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν)) * (a * a) + ((1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν)) * (b * c) :=31  @FRC.Ledger.p2801332/-- 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. -/33theorem p28014 : (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (a i ω h : FRC.Extension.Ext p ν), i * i + (1 : FRC.Extension.Ext p ν) = (0 : FRC.Extension.Ext p ν) → ω * ω + ω + (1 : FRC.Extension.Ext p ν) = (0 : FRC.Extension.Ext p ν) → h + h = (1 : FRC.Extension.Ext p ν) → a + -(h * ((1 : FRC.Extension.Ext p ν) + i) * a) * (ω * ω) * ω + -(h * ((1 : FRC.Extension.Ext p ν) + -i) * a) * ω * (ω * ω) = (0 : FRC.Extension.Ext p ν) ∧ ((1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν)) * (-(h * ((1 : FRC.Extension.Ext p ν) + i) * a) * (ω * ω) * (-(h * ((1 : FRC.Extension.Ext p ν) + -i) * a) * ω)) = a * a) ∧ (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (a i ω h : FRC.Extension.Ext p ν), i * i + (1 : FRC.Extension.Ext p ν) = (0 : FRC.Extension.Ext p ν) → ω * ω + ω + (1 : FRC.Extension.Ext p ν) = (0 : FRC.Extension.Ext p ν) → h + h = (1 : FRC.Extension.Ext p ν) → a + -(h * ((1 : FRC.Extension.Ext p ν) + i) * a) * (ω * ω) + -(h * ((1 : FRC.Extension.Ext p ν) + -i) * a) * ω = a * h * ((1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + i * (ω + -(ω * ω))) ∧ a + -(h * ((1 : FRC.Extension.Ext p ν) + i) * a) * (ω * ω) * (ω * ω) + -(h * ((1 : FRC.Extension.Ext p ν) + -i) * a) * ω * ω = a * h * ((1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + -(i * (ω + -(ω * ω)))) ∧ i * (ω + -(ω * ω)) * (i * (ω + -(ω * ω))) = (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν)) ∧ (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (s : FRC.Extension.Ext p ν), s * s + -((1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν)) = (0 : FRC.Extension.Ext p ν) → ((1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + -s) * ((1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + -s) = ((1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + -(((1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν)) * s)) * (((1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + s) * ((1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + s))) ∧ (3 : Nat) * (3 : Nat) = (8 : Nat) + (1 : Nat) ∧ (24 : Nat) = (3 : Nat) * (8 : Nat) :=34  @FRC.Ledger.p2801435/-- 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. -/36theorem p28015 : (∀ {p : Nat} [FRC.Pos p] {i : FRC.Shell p}, i * i + (1 : FRC.Shell p) = (0 : FRC.Shell p) → ((1 : FRC.Shell p) + -i) * ((1 : FRC.Shell p) + i) = (2 : FRC.Shell p)) ∧ (∀ {p : Nat} [FRC.Pos p] {ν h : FRC.Shell p}, h + h = (1 : FRC.Shell p) → ν + (1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p) = (0 : FRC.Shell p) → ((1 : FRC.Extension.Ext p ν) + -FRC.Interactions.omega3 ν h).norm = (3 : FRC.Shell p)) ∧ ∀ {p : Nat} [FRC.Pos p] (a₀ a₁ a₂ ω : FRC.Shell p), ω * ω + ω + (1 : FRC.Shell p) = (0 : FRC.Shell p) → (((1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p)) * (a₀ * a₀ + a₁ * a₁ + a₂ * a₂) = ((1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p)) * ((a₀ + a₁ + a₂) * (a₀ + a₁ + a₂)) ↔ ((1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p)) * ((a₀ + a₁ * ω + a₂ * (ω * ω)) * (a₀ + a₁ * (ω * ω) + a₂ * ω)) = ((1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p)) * ((a₀ + a₁ + a₂) * (a₀ + a₁ + a₂))) :=37  @FRC.Ledger.p2801538/-- 28:C5 (p28016) — The cross-sector phase lock $\delta_\ell:\delta_d:\delta_u=1:\tfrac12:\tfrac13$ is the relation $c_\ell=2c_d^{2}-1=4c_u^{3}-3c_u$ between the cube invariants $c=\cos3\delta$ of the sectors, each read from its masses through the circulant determinant; in the $\overline{\mathrm{MS}}$ working scheme of Table~\ref{tab:sectors} the sectors satisfy it within the quark-mass uncertainty [chart] ($0.496$, $0.335$; $0.388$ for the up ratio with the pole charm mass). -/39theorem p28016 : (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (z : FRC.Extension.Ext p ν), z * z.conj = (1 : FRC.Extension.Ext p ν) → z * z + z.conj * z.conj = (z + z.conj) * (z + z.conj) + -((1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν))) ∧ (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (z : FRC.Extension.Ext p ν), z * z.conj = (1 : FRC.Extension.Ext p ν) → z * z * z + z.conj * z.conj * z.conj = (z + z.conj) * ((z + z.conj) * (z + z.conj)) + -(((1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν)) * (z + z.conj))) ∧ ∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (a b c : FRC.Extension.Ext p ν), FRC.Unitary.det (FRC.Flavour.circ a b c) = a * a * a + b * b * b + c * c * c + -(((1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν)) * (a * b * c)) :=40  @FRC.Ledger.p2801641/-- 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). -/42theorem p28017 : (∀ {p : Nat} [FRC.Pos p] (c s m₁ m₂ : FRC.Shell p), c * c + s * s = (1 : FRC.Shell p) → m₁ * (c * c) + m₂ * (s * s) = (0 : FRC.Shell p) → m₂ * (s * s) = -(m₁ * (c * c))) ∧ ∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (sd cu cd su z : FRC.Extension.Ext p ν), z * z.conj = (1 : FRC.Extension.Ext p ν) → (sd * cu + -(cd * su * z)) * (sd * cu + -(cd * su * z.conj)) = sd * cu * (sd * cu) + cd * su * (cd * su) + -(sd * cu * (cd * su) * (z + z.conj)) :=43  @FRC.Ledger.p2801744/-- 28:C7 (p28018) — Up-sector doubling $m^u_i\sim(m^d_i)^2$ from the $\mathbf{10}\cdot\mathbf{10}$ Yukawa. -/45theorem p28018 : List.map (fun k => (2 : Nat) * k) [(2 : Nat), (1 : Nat), (0 : Nat)] = [(4 : Nat), (2 : Nat), (0 : Nat)] ∧ List.map (fun k => (4 : Nat) * k) [(2 : Nat), (1 : Nat), (0 : Nat)] = [(8 : Nat), (4 : Nat), (0 : Nat)] ∧ List.map (fun k => (2 : Nat) * k) [(4 : Nat), (2 : Nat), (0 : Nat)] = [(8 : Nat), (4 : Nat), (0 : Nat)] ∧ ((List.range (3 : Nat)).all fun i => (List.range (3 : Nat)).all fun j => FRC.Flavour.expo [(2 : Nat), (1 : Nat), (0 : Nat)] i j == FRC.Flavour.expo [(2 : Nat), (1 : Nat), (0 : Nat)] j i) = true ∧ ((List.range (3 : Nat)).all fun i => (List.range (3 : Nat)).all fun j => FRC.Flavour.expo [(4 : Nat), (2 : Nat), (0 : Nat)] i j == FRC.Flavour.expo [(4 : Nat), (2 : Nat), (0 : Nat)] j i) = true :=46  @FRC.Ledger.p2801847/-- 28:C8 (p28019) — Lopsided $M_e=M_d^{\mathsf T}$ splits CKM (small) from PMNS (large); the CKM angle values reduce to the winding kernel and the shared $\sigma$. -/48theorem p28019 : (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (L R : FRC.Unitary.M3 p ν) (x y z : FRC.Extension.Ext p ν), FRC.Flavour.transpose (FRC.Unitary.mmul (FRC.Unitary.mmul L (FRC.Flavour.diag x y z)) (FRC.Flavour.transpose R)) = FRC.Unitary.mmul (FRC.Unitary.mmul R (FRC.Flavour.diag x y z)) (FRC.Flavour.transpose L)) ∧ ∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (A B : FRC.Unitary.M3 p ν), FRC.Flavour.transpose (FRC.Unitary.mmul A B) = FRC.Unitary.mmul (FRC.Flavour.transpose B) (FRC.Flavour.transpose A) :=49  @FRC.Ledger.p2801950/-- 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. -/51theorem p28021 : (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p}, FRC.Flavour.mulvec FRC.Flavour.shift (1 : FRC.Extension.Ext p ν) (1 : FRC.Extension.Ext p ν) (1 : FRC.Extension.Ext p ν) = ((1 : FRC.Extension.Ext p ν), (1 : FRC.Extension.Ext p ν), (1 : FRC.Extension.Ext p ν)) ∧ FRC.Flavour.mulvec FRC.Flavour.shift ((1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν)) (-1 : FRC.Extension.Ext p ν) (-1 : FRC.Extension.Ext p ν) = ((-1 : FRC.Extension.Ext p ν), (-1 : FRC.Extension.Ext p ν), (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν)) ∧ ∀ (l : FRC.Extension.Ext p ν), l * ((1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν)) = (-1 : FRC.Extension.Ext p ν) → l * (-1 : FRC.Extension.Ext p ν) = (-1 : FRC.Extension.Ext p ν) → l * (-1 : FRC.Extension.Ext p ν) = (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) → (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) = (0 : FRC.Extension.Ext p ν)) ∧ (∀ {p : Nat} [FRC.Pos p] {ν h : FRC.Shell p}, h + h = (1 : FRC.Shell p) → ν + (1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p) = (0 : FRC.Shell p) → (FRC.Interactions.omega3 ν h).norm = (1 : FRC.Shell p) ∧ (FRC.Interactions.omega3 ν h * FRC.Interactions.omega3 ν h).norm = (1 : FRC.Shell p)) ∧ ∀ {p : Nat} [FRC.Pos p] {ν h : FRC.Shell p}, h + h = (1 : FRC.Shell p) → ν + (1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p) = (0 : FRC.Shell p) → ((1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p)) * -(ν * (h * h)) = (1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p) :=52  @FRC.Ledger.p2802153/-- 28:C11 (p28022) — Seesaw of circulants $\Rightarrow$ Koide-form (theorem); with $M_R\propto m_D$ (Y1) the seesaw gives $m_\nu=m_D^{\mathsf T}$, $r_\nu=\sqrt2$ (transpose fixed point). -/54theorem p28022 : (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (a b c a' b' c' : FRC.Extension.Ext p ν), FRC.Unitary.mmul (FRC.Flavour.circ a b c) (FRC.Flavour.circ a' b' c') = FRC.Flavour.circ (a * a' + b * c' + c * b') (a * b' + b * a' + c * c') (a * c' + b * b' + c * a')) ∧ (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (a b c : FRC.Extension.Ext p ν), FRC.Unitary.adj (FRC.Flavour.circ a b c) = FRC.Flavour.circ (a * a + -(b * c)) (c * c + -(a * b)) (b * b + -(a * c))) ∧ (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (a b c a' b' c' : FRC.Extension.Ext p ν), ∃ x y z, FRC.Unitary.mmul (FRC.Unitary.mmul (FRC.Flavour.circ a b c) (FRC.Unitary.adj (FRC.Flavour.circ a' b' c'))) (FRC.Flavour.transpose (FRC.Flavour.circ a b c)) = FRC.Flavour.circ x y z) ∧ (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (c : FRC.Extension.Ext p ν) (M : FRC.Unitary.M3 p ν), FRC.Unitary.mmul (FRC.Unitary.mmul M (FRC.Unitary.adj (FRC.Unitary.smul c M))) (FRC.Flavour.transpose M) = FRC.Unitary.smul (c * c * FRC.Unitary.det M) (FRC.Flavour.transpose M)) ∧ ∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (a b c : FRC.Extension.Ext p ν), FRC.Flavour.transpose (FRC.Flavour.circ a b c) = FRC.Flavour.circ a c b :=55  @FRC.Ledger.p2802256/-- 28:C11b (p28050) — Both orderings solved: the signed $r_\nu=\sqrt2$ circulant solves both neutrino orderings exactly, so the boundary branch (B6) is the sole ordering assumption. -/57theorem p28050 : (∀ {p : Nat} [FRC.Pos p] (a₀ a₁ a₂ ω : FRC.Shell p), ω * ω + ω + (1 : FRC.Shell p) = (0 : FRC.Shell p) → ((3 : FRC.Shell p) * (a₀ * a₀ + a₁ * a₁ + a₂ * a₂) = (2 : FRC.Shell p) * ((a₀ + a₁ + a₂) * (a₀ + a₁ + a₂)) ↔ (2 : FRC.Shell p) * ((a₀ + a₁ * ω + a₂ * (ω * ω)) * (a₀ + a₁ * (ω * ω) + a₂ * ω)) = (a₀ + a₁ + a₂) * (a₀ + a₁ + a₂))) ∧ ∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (a b c ω : FRC.Extension.Ext p ν), ω * ω + ω + (1 : FRC.Extension.Ext p ν) = (0 : FRC.Extension.Ext p ν) → (a + b + c) * (a + b + c) + (a + b * ω + c * (ω * ω)) * (a + b * ω + c * (ω * ω)) + (a + b * (ω * ω) + c * ω) * (a + b * (ω * ω) + c * ω) = ((1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν)) * (a * a) + ((1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν)) * (b * c) :=58  @FRC.Ledger.p2805059/-- 28:C12 (p28024) — The generation $\mathbf{16}$ is the four-chart reflection algebra $\Lambda^{\bullet}(\C^4)\cong\Lambda^{\mathrm{even}}(\C^5)$, the quarter-turn the fifth direction; projection anchored at $\nu^c=\Lambda^0$. -/60theorem p28024 : (((List.range (16 : Nat)).all fun S => (List.range (16 : Nat)).all fun T => decide ((FRC.Interactions.emul S T).snd < (16 : Nat))) = true ∧ ((List.range (16 : Nat)).all fun S => (List.range (16 : Nat)).all fun T => (List.range (16 : Nat)).all fun U => FRC.Interactions.assocL S T U == FRC.Interactions.assocR S T U) = true ∧ ((List.range (4 : Nat)).all fun i => (List.range (4 : Nat)).all fun j => if (i == j) = true then FRC.Interactions.emul ((2 : Nat) ^ i) ((2 : Nat) ^ j) == ((0 : Int), (0 : Nat)) else FRC.Interactions.emul ((2 : Nat) ^ i) ((2 : Nat) ^ j) == (-(FRC.Interactions.emul ((2 : Nat) ^ j) ((2 : Nat) ^ i)).fst, (FRC.Interactions.emul ((2 : Nat) ^ j) ((2 : Nat) ^ i)).snd)) = true) ∧ FRC.Interactions.gen16.length = (16 : Nat) ∧ ((List.range (16 : Nat)).all fun S => FRC.Interactions.gen16.contains (FRC.Interactions.fifth S)) = true ∧ ((List.range (16 : Nat)).all fun S => (List.range (16 : Nat)).all fun T => decide ((FRC.Interactions.fifth S == FRC.Interactions.fifth T) = true → (S == T) = true)) = true ∧ (FRC.Interactions.gen16.all fun R => (List.range (16 : Nat)).any fun S => FRC.Interactions.fifth S == R) = true ∧ ((List.range (16 : Nat)).all fun S => FRC.Interactions.cnt S (0 : Nat) (4 : Nat) % (2 : Nat) == (0 : Nat) || FRC.Interactions.emul S (16 : Nat) == ((1 : Int), FRC.Interactions.fifth S)) = true :=61  @FRC.Ledger.p2802462/-- 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. -/63theorem p28025 : (∀ {p : Nat} [FRC.Pos p] (a₀ a₁ a₂ ω : FRC.Shell p), ω * ω + ω + (1 : FRC.Shell p) = (0 : FRC.Shell p) → (3 : FRC.Shell p) * (a₀ * a₀ + a₁ * a₁ + a₂ * a₂) = (a₀ + a₁ + a₂) * (a₀ + a₁ + a₂) + (2 : FRC.Shell p) * ((a₀ + a₁ * ω + a₂ * (ω * ω)) * (a₀ + a₁ * (ω * ω) + a₂ * ω))) ∧ (∀ {p : Nat} [FRC.Pos p] (a₀ a₁ a₂ ω : FRC.Shell p), ω * ω + ω + (1 : FRC.Shell p) = (0 : FRC.Shell p) → ((3 : FRC.Shell p) * (a₀ * a₀ + a₁ * a₁ + a₂ * a₂) = (2 : FRC.Shell p) * ((a₀ + a₁ + a₂) * (a₀ + a₁ + a₂)) ↔ (2 : FRC.Shell p) * ((a₀ + a₁ * ω + a₂ * (ω * ω)) * (a₀ + a₁ * (ω * ω) + a₂ * ω)) = (a₀ + a₁ + a₂) * (a₀ + a₁ + a₂))) ∧ (∀ {p : Nat} [FRC.Pos p] {ν h : FRC.Shell p}, h + h = (1 : FRC.Shell p) → ν + (1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p) = (0 : FRC.Shell p) → ∀ (a₀ a₁ a₂ : FRC.Shell p), FRC.Interactions.omega3 ν h * FRC.Interactions.omega3 ν h + FRC.Interactions.omega3 ν h + (1 : FRC.Extension.Ext p ν) = (0 : FRC.Extension.Ext p ν) ∧ FRC.Interactions.hat2 ν h a₀ a₁ a₂ = (FRC.Interactions.hat1 ν h a₀ a₁ a₂).conj ∧ FRC.Interactions.hat1 ν h a₀ a₁ a₂ * FRC.Interactions.hat2 ν h a₀ a₁ a₂ = FRC.Extension.Ext.ofShell (FRC.Interactions.hat1 ν h a₀ a₁ a₂).norm ∧ (3 : FRC.Shell p) * (a₀ * a₀ + a₁ * a₁ + a₂ * a₂) = (a₀ + a₁ + a₂) * (a₀ + a₁ + a₂) + (2 : FRC.Shell p) * (FRC.Interactions.hat1 ν h a₀ a₁ a₂).norm ∧ ((3 : FRC.Shell p) * (a₀ * a₀ + a₁ * a₁ + a₂ * a₂) = (2 : FRC.Shell p) * ((a₀ + a₁ + a₂) * (a₀ + a₁ + a₂)) ↔ (2 : FRC.Shell p) * (FRC.Interactions.hat1 ν h a₀ a₁ a₂).norm = (a₀ + a₁ + a₂) * (a₀ + a₁ + a₂))) ∧ ∀ {p : Nat} [FRC.Pos p] {κ : Nat}, p = (4 : Nat) * κ + (1 : Nat) → FRC.Shell.ofNat ((2 : Nat) * κ + (1 : Nat)) + FRC.Shell.ofNat ((2 : Nat) * κ + (1 : Nat)) = (1 : FRC.Shell p) ∧ (-3 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p) = (0 : FRC.Shell p) :=64  @FRC.Ledger.p2802565/-- 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. -/66theorem p28026 : (∀ {p : Nat} [FRC.Pos p] {ν h : FRC.Shell p}, h + h = (1 : FRC.Shell p) → ν + (1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p) = (0 : FRC.Shell p) → ((1 : FRC.Extension.Ext p ν) + -FRC.Interactions.omega3 ν h).norm = (3 : FRC.Shell p)) ∧ ∀ {p : Nat} [FRC.Pos p] (a₀ a₁ a₂ ω : FRC.Shell p), ω * ω + ω + (1 : FRC.Shell p) = (0 : FRC.Shell p) → (((1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p)) * (a₀ * a₀ + a₁ * a₁ + a₂ * a₂) = ((1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p)) * ((a₀ + a₁ + a₂) * (a₀ + a₁ + a₂)) ↔ ((1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p)) * ((a₀ + a₁ * ω + a₂ * (ω * ω)) * (a₀ + a₁ * (ω * ω) + a₂ * ω)) = ((1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p)) * ((a₀ + a₁ + a₂) * (a₀ + a₁ + a₂))) :=67  @FRC.Ledger.p2802668/-- 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. -/69theorem p28027 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (j : Nat), g ^ (g ^ j).val = g ^ ((g ^ j).val % (p - (1 : Nat)))) ∧ List.map (fun k => (2 : Nat) * k) [(2 : Nat), (1 : Nat), (0 : Nat)] = [(4 : Nat), (2 : Nat), (0 : Nat)] ∧ List.map (fun k => (4 : Nat) * k) [(2 : Nat), (1 : Nat), (0 : Nat)] = [(8 : Nat), (4 : Nat), (0 : Nat)] ∧ List.map (fun k => (2 : Nat) * k) [(4 : Nat), (2 : Nat), (0 : Nat)] = [(8 : Nat), (4 : Nat), (0 : Nat)] ∧ ((List.range (3 : Nat)).all fun i => (List.range (3 : Nat)).all fun j => FRC.Flavour.expo [(2 : Nat), (1 : Nat), (0 : Nat)] i j == FRC.Flavour.expo [(2 : Nat), (1 : Nat), (0 : Nat)] j i) = true ∧ ((List.range (3 : Nat)).all fun i => (List.range (3 : Nat)).all fun j => FRC.Flavour.expo [(4 : Nat), (2 : Nat), (0 : Nat)] i j == FRC.Flavour.expo [(4 : Nat), (2 : Nat), (0 : Nat)] j i) = true :=70  @FRC.Ledger.p2802771/-- 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. -/72theorem p28028 : (∀ {p : Nat} [FRC.Pos p] (c s m₁ m₂ : FRC.Shell p), c * c + s * s = (1 : FRC.Shell p) → m₁ * (c * c) + m₂ * (s * s) = (0 : FRC.Shell p) → m₂ * (s * s) = -(m₁ * (c * c))) ∧ ∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (sd cu cd su z : FRC.Extension.Ext p ν), z * z.conj = (1 : FRC.Extension.Ext p ν) → (sd * cu + -(cd * su * z)) * (sd * cu + -(cd * su * z.conj)) = sd * cu * (sd * cu) + cd * su * (cd * su) + -(sd * cu * (cd * su) * (z + z.conj)) :=73  @FRC.Ledger.p2802874/-- 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. -/75theorem p28029 : (List.filter (fun S => FRC.Interactions.col S == (2 : Nat) && FRC.Interactions.wk S == (2 : Nat) && FRC.Interactions.y6 S == (2 : Int)) FRC.Interactions.gen16).length = (3 : Nat) ∧ (List.filter (fun S => FRC.Interactions.col S == (0 : Nat) && FRC.Interactions.wk S == (2 : Nat) && FRC.Interactions.y6 S == (6 : Int)) FRC.Interactions.gen16).length = (1 : Nat) ∧ (3 : Nat) * (3 : Nat) = (9 : Nat) :=76  @FRC.Ledger.p2802977/-- 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. -/78theorem p28030 : List.map (fun k => (2 : Nat) * k) [(2 : Nat), (1 : Nat), (0 : Nat)] = [(4 : Nat), (2 : Nat), (0 : Nat)] ∧ List.map (fun k => (4 : Nat) * k) [(2 : Nat), (1 : Nat), (0 : Nat)] = [(8 : Nat), (4 : Nat), (0 : Nat)] ∧ List.map (fun k => (2 : Nat) * k) [(4 : Nat), (2 : Nat), (0 : Nat)] = [(8 : Nat), (4 : Nat), (0 : Nat)] ∧ ((List.range (3 : Nat)).all fun i => (List.range (3 : Nat)).all fun j => FRC.Flavour.expo [(2 : Nat), (1 : Nat), (0 : Nat)] i j == FRC.Flavour.expo [(2 : Nat), (1 : Nat), (0 : Nat)] j i) = true ∧ ((List.range (3 : Nat)).all fun i => (List.range (3 : Nat)).all fun j => FRC.Flavour.expo [(4 : Nat), (2 : Nat), (0 : Nat)] i j == FRC.Flavour.expo [(4 : Nat), (2 : Nat), (0 : Nat)] j i) = true :=79  @FRC.Ledger.p2803080/-- 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. -/81theorem p28031 : (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (a i ω h : FRC.Extension.Ext p ν), i * i + (1 : FRC.Extension.Ext p ν) = (0 : FRC.Extension.Ext p ν) → ω * ω + ω + (1 : FRC.Extension.Ext p ν) = (0 : FRC.Extension.Ext p ν) → h + h = (1 : FRC.Extension.Ext p ν) → a + -(h * ((1 : FRC.Extension.Ext p ν) + i) * a) * (ω * ω) * ω + -(h * ((1 : FRC.Extension.Ext p ν) + -i) * a) * ω * (ω * ω) = (0 : FRC.Extension.Ext p ν) ∧ ((1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν)) * (-(h * ((1 : FRC.Extension.Ext p ν) + i) * a) * (ω * ω) * (-(h * ((1 : FRC.Extension.Ext p ν) + -i) * a) * ω)) = a * a) ∧ (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (a i ω h : FRC.Extension.Ext p ν), i * i + (1 : FRC.Extension.Ext p ν) = (0 : FRC.Extension.Ext p ν) → ω * ω + ω + (1 : FRC.Extension.Ext p ν) = (0 : FRC.Extension.Ext p ν) → h + h = (1 : FRC.Extension.Ext p ν) → a + -(h * ((1 : FRC.Extension.Ext p ν) + i) * a) * (ω * ω) + -(h * ((1 : FRC.Extension.Ext p ν) + -i) * a) * ω = a * h * ((1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + i * (ω + -(ω * ω))) ∧ a + -(h * ((1 : FRC.Extension.Ext p ν) + i) * a) * (ω * ω) * (ω * ω) + -(h * ((1 : FRC.Extension.Ext p ν) + -i) * a) * ω * ω = a * h * ((1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + -(i * (ω + -(ω * ω)))) ∧ i * (ω + -(ω * ω)) * (i * (ω + -(ω * ω))) = (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν)) ∧ ∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (s : FRC.Extension.Ext p ν), s * s + -((1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν)) = (0 : FRC.Extension.Ext p ν) → ((1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + -s) * ((1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + -s) = ((1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + -(((1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν)) * s)) * (((1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + s) * ((1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + s)) :=82  @FRC.Ledger.p2803183/-- 28:X8 (p28032) — \textbf{The large-lepton, small-quark mixing split} is the lopsided $M_e=M_d^{\mathsf T}$: one off-diagonal feeds the invisible right-handed quark rotation and, transposed, the visible left-handed lepton rotation, so the two mixing matrices are one structure rather than two unrelated ones. -/84theorem p28032 : (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (L R : FRC.Unitary.M3 p ν) (x y z : FRC.Extension.Ext p ν), FRC.Flavour.transpose (FRC.Unitary.mmul (FRC.Unitary.mmul L (FRC.Flavour.diag x y z)) (FRC.Flavour.transpose R)) = FRC.Unitary.mmul (FRC.Unitary.mmul R (FRC.Flavour.diag x y z)) (FRC.Flavour.transpose L)) ∧ ∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (A B : FRC.Unitary.M3 p ν), FRC.Flavour.transpose (FRC.Unitary.mmul A B) = FRC.Unitary.mmul (FRC.Flavour.transpose B) (FRC.Flavour.transpose A) :=85  @FRC.Ledger.p2803286/-- 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. -/87theorem p28034 : (∀ {p : Nat} [FRC.Pos p] {ν h : FRC.Shell p}, h + h = (1 : FRC.Shell p) → ν + (1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p) = (0 : FRC.Shell p) → (FRC.Interactions.omega3 ν h).norm = (1 : FRC.Shell p) ∧ (FRC.Interactions.omega3 ν h * FRC.Interactions.omega3 ν h).norm = (1 : FRC.Shell p)) ∧ ∀ {p : Nat} [FRC.Pos p] {ν h : FRC.Shell p}, h + h = (1 : FRC.Shell p) → ν + (1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p) = (0 : FRC.Shell p) → ((1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p)) * -(ν * (h * h)) = (1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p) :=88  @FRC.Ledger.p2803489/-- 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. -/90theorem p28035 : (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (c : FRC.Extension.Ext p ν) (M : FRC.Unitary.M3 p ν), FRC.Unitary.mmul (FRC.Unitary.mmul M (FRC.Unitary.adj (FRC.Unitary.smul c M))) (FRC.Flavour.transpose M) = FRC.Unitary.smul (c * c * FRC.Unitary.det M) (FRC.Flavour.transpose M)) ∧ (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (a b c a' b' c' : FRC.Extension.Ext p ν), ∃ x y z, FRC.Unitary.mmul (FRC.Unitary.mmul (FRC.Flavour.circ a b c) (FRC.Unitary.adj (FRC.Flavour.circ a' b' c'))) (FRC.Flavour.transpose (FRC.Flavour.circ a b c)) = FRC.Flavour.circ x y z) ∧ ∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (a b c ω : FRC.Extension.Ext p ν), ω * ω + ω + (1 : FRC.Extension.Ext p ν) = (0 : FRC.Extension.Ext p ν) → c + a * ω + b * (ω * ω) = ω * (a + b * ω + c * (ω * ω)) ∧ b + c * ω + a * (ω * ω) = ω * ω * (a + b * ω + c * (ω * ω)) ∧ c + a * (ω * ω) + b * ω = ω * ω * (a + b * (ω * ω) + c * ω) ∧ b + c * (ω * ω) + a * ω = ω * (a + b * (ω * ω) + c * ω) :=91  @FRC.Ledger.p2803592/-- 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. -/93theorem p28036 : (∀ {p : Nat} [FRC.Pos p] (a₀ a₁ a₂ ω : FRC.Shell p), ω * ω + ω + (1 : FRC.Shell p) = (0 : FRC.Shell p) → ((3 : FRC.Shell p) * (a₀ * a₀ + a₁ * a₁ + a₂ * a₂) = (2 : FRC.Shell p) * ((a₀ + a₁ + a₂) * (a₀ + a₁ + a₂)) ↔ (2 : FRC.Shell p) * ((a₀ + a₁ * ω + a₂ * (ω * ω)) * (a₀ + a₁ * (ω * ω) + a₂ * ω)) = (a₀ + a₁ + a₂) * (a₀ + a₁ + a₂))) ∧ ∀ {p : Nat} [FRC.Pos p] {ν h : FRC.Shell p}, h + h = (1 : FRC.Shell p) → ν + (1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p) = (0 : FRC.Shell p) → ∀ (a₀ a₁ a₂ : FRC.Shell p), FRC.Interactions.omega3 ν h * FRC.Interactions.omega3 ν h + FRC.Interactions.omega3 ν h + (1 : FRC.Extension.Ext p ν) = (0 : FRC.Extension.Ext p ν) ∧ FRC.Interactions.hat2 ν h a₀ a₁ a₂ = (FRC.Interactions.hat1 ν h a₀ a₁ a₂).conj ∧ FRC.Interactions.hat1 ν h a₀ a₁ a₂ * FRC.Interactions.hat2 ν h a₀ a₁ a₂ = FRC.Extension.Ext.ofShell (FRC.Interactions.hat1 ν h a₀ a₁ a₂).norm ∧ (3 : FRC.Shell p) * (a₀ * a₀ + a₁ * a₁ + a₂ * a₂) = (a₀ + a₁ + a₂) * (a₀ + a₁ + a₂) + (2 : FRC.Shell p) * (FRC.Interactions.hat1 ν h a₀ a₁ a₂).norm ∧ ((3 : FRC.Shell p) * (a₀ * a₀ + a₁ * a₁ + a₂ * a₂) = (2 : FRC.Shell p) * ((a₀ + a₁ + a₂) * (a₀ + a₁ + a₂)) ↔ (2 : FRC.Shell p) * (FRC.Interactions.hat1 ν h a₀ a₁ a₂).norm = (a₀ + a₁ + a₂) * (a₀ + a₁ + a₂)) :=94  @FRC.Ledger.p2803695/-- 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. -/96theorem p28037 : (∀ {p : Nat} [FRC.Pos p] {ν h : FRC.Shell p}, h + h = (1 : FRC.Shell p) → ν + (1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p) = (0 : FRC.Shell p) → ((1 : FRC.Extension.Ext p ν) + -FRC.Interactions.omega3 ν h).norm = (3 : FRC.Shell p)) ∧ ∀ {p : Nat} [FRC.Pos p] (a₀ a₁ a₂ ω : FRC.Shell p), ω * ω + ω + (1 : FRC.Shell p) = (0 : FRC.Shell p) → (((1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p)) * (a₀ * a₀ + a₁ * a₁ + a₂ * a₂) = ((1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p)) * ((a₀ + a₁ + a₂) * (a₀ + a₁ + a₂)) ↔ ((1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p)) * ((a₀ + a₁ * ω + a₂ * (ω * ω)) * (a₀ + a₁ * (ω * ω) + a₂ * ω)) = ((1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p)) * ((a₀ + a₁ + a₂) * (a₀ + a₁ + a₂))) :=97  @FRC.Ledger.p2803798/-- 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. -/99theorem p28038 : (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (sd cu cd su z : FRC.Extension.Ext p ν), z * z.conj = (1 : FRC.Extension.Ext p ν) → (sd * cu + -(cd * su * z)) * (sd * cu + -(cd * su * z.conj)) = sd * cu * (sd * cu) + cd * su * (cd * su) + -(sd * cu * (cd * su) * (z + z.conj))) ∧ ∀ {p : Nat} [FRC.Pos p] (c s m₁ m₂ : FRC.Shell p), c * c + s * s = (1 : FRC.Shell p) → m₁ * (c * c) + m₂ * (s * s) = (0 : FRC.Shell p) → m₂ * (s * s) = -(m₁ * (c * c)) :=100  @FRC.Ledger.p28038101/-- 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. -/102theorem p28039 : (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (c : FRC.Extension.Ext p ν) (M : FRC.Unitary.M3 p ν), FRC.Unitary.mmul (FRC.Unitary.mmul M (FRC.Unitary.adj (FRC.Unitary.smul c M))) (FRC.Flavour.transpose M) = FRC.Unitary.smul (c * c * FRC.Unitary.det M) (FRC.Flavour.transpose M)) ∧ ∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (a b c : FRC.Extension.Ext p ν), FRC.Flavour.transpose (FRC.Flavour.circ a b c) = FRC.Flavour.circ a c b :=103  @FRC.Ledger.p28039104/-- 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. -/105theorem p28042 : (∀ {p : Nat} [FRC.Pos p] {ν h : FRC.Shell p}, h + h = (1 : FRC.Shell p) → ν + (1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p) = (0 : FRC.Shell p) → ((1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p)) * -(ν * (h * h)) = (1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p)) ∧ (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p}, FRC.Flavour.mulvec FRC.Flavour.shift (1 : FRC.Extension.Ext p ν) (1 : FRC.Extension.Ext p ν) (1 : FRC.Extension.Ext p ν) = ((1 : FRC.Extension.Ext p ν), (1 : FRC.Extension.Ext p ν), (1 : FRC.Extension.Ext p ν)) ∧ FRC.Flavour.mulvec FRC.Flavour.shift ((1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν)) (-1 : FRC.Extension.Ext p ν) (-1 : FRC.Extension.Ext p ν) = ((-1 : FRC.Extension.Ext p ν), (-1 : FRC.Extension.Ext p ν), (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν)) ∧ ∀ (l : FRC.Extension.Ext p ν), l * ((1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν)) = (-1 : FRC.Extension.Ext p ν) → l * (-1 : FRC.Extension.Ext p ν) = (-1 : FRC.Extension.Ext p ν) → l * (-1 : FRC.Extension.Ext p ν) = (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) → (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) + (1 : FRC.Extension.Ext p ν) = (0 : FRC.Extension.Ext p ν)) ∧ ∀ {p : Nat} [FRC.Pos p] {ν h : FRC.Shell p}, h + h = (1 : FRC.Shell p) → ν + (1 : FRC.Shell p) + (1 : FRC.Shell p) + (1 : FRC.Shell p) = (0 : FRC.Shell p) → (FRC.Interactions.omega3 ν h).norm = (1 : FRC.Shell p) ∧ (FRC.Interactions.omega3 ν h * FRC.Interactions.omega3 ν h).norm = (1 : FRC.Shell p) :=106  @FRC.Ledger.p28042107-- end ledger predicates108109end FRC.Flavour110