import FrcCore.Theme.Interactions
import FrcCore.Theme.Ladder
import FrcCore.Theme.Flavour

/-!
# FrcCore.Keys.Flavour — the keyed theorems of the flavour theme (ledger migration, task LM19)

One declaration per key, `FRC.Ledger.p<key>`, generated by `make_keys.py` from the ledgers' Lean bindings: the theorem
that every row carrying the key asserts, proved from the themes alone. The paper's module keeps its declaration
`FRC.<Module>.p<key>` as an alias. Every declaration has no axioms (`check_core_axioms.py`).
-/

namespace FRC.Ledger

-- Keys of the flavour theme (generated by make_keys.py from the ledgers' Lean bindings; edit the ledgers, not this file)
/-- p00080 — 00:G15. \textbf{Flavour} (structure): the seesaw scale, $b$--$\tau$ unification and the role-ladder mass ordering are derived; the observed spectrum is the projection of the one $\mathbf{16}$. The mixing angles and phases reduce to the role-depth texture, the lopsided $\sigma$, the trimaximal $C_3$ column and quark--lepton complementarity (28-flav C9), leaving the $\Om$-hard phases $\{\delta_0,\delta_\nu,\delta_{\mathrm{CP}}\}$ (Z6); the seesaw fixes $Q_\nu{=}2/3$. -/
theorem p00080 : (∀ {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] (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] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (j : Nat), g ^ (g ^ j).val = g ^ ((g ^ j).val % (p - (1 : Nat))) :=
  And.intro @FRC.Flavour.transpose_fixed_point (And.intro @FRC.Flavour.seesaw_circulant (And.intro @FRC.Interactions.koide_two_thirds (@FRC.Ladder.tower_reduces)))
/-- p00179 — 00:G17. \textbf{Flavour} (exact ratios): Koide $2/3$ (G16), the factor $3$ of Georgi--Jarlskog, the squared amplitudes the split/non-split norms $N(1{-}\im){=}2$, $N(1{-}\omega){=}3$ on the realisation 28:B5 (G1, G4), trimaximal $|F_{jk}|^2{=}\tfrac13$, maximal Jarlskog $J^2{=}\tfrac1{108}$, the $\lambda$-texture from role depths, and the charged sectors locked by $\delta_\ell{:}\delta_d{:}\delta_u=1{:}\tfrac12{:}\tfrac13$ to $\delta_0$. -/
theorem p00179 : (∀ {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] {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)) ∧ ((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)) ∧ (∀ {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)) ∧ (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) ∧ (∀ {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)) :=
  And.intro @FRC.Interactions.koide_two_thirds (And.intro @FRC.Flavour.norm_one_sub_i (And.intro @FRC.Flavour.norm_one_sub_omega (And.intro @FRC.Flavour.colour_count (And.intro @FRC.Flavour.trimaximal (And.intro @FRC.Flavour.jarlskog_sq (And.intro @FRC.Flavour.texture_exponents (And.intro @FRC.Flavour.trace_double (@FRC.Flavour.trace_triple))))))))
/-- p28012 — 28:C1. Generation universality $\Rightarrow$ the amplitude matrix is a $C_3$-circulant $\Rightarrow$ the Koide functional form. -/
theorem 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₂ * ω)) :=
  And.intro @FRC.Flavour.circ_eigen (And.intro @FRC.Flavour.eigen_sum (And.intro @FRC.Flavour.eigen_sumsq (@FRC.Interactions.koide_parseval)))
/-- p28013 — 28:C2. $Q=2/3\Leftrightarrow r=\sqrt2\Leftrightarrow\rho^2=\tfrac12$ (the equivalence an identity); the value $\rho^2=\tfrac12$ is the realisation B5. -/
theorem 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) :=
  And.intro @FRC.Interactions.koide_two_thirds (And.intro @FRC.Interactions.koide_extension (@FRC.Flavour.eigen_sumsq))
/-- p28014 — 28:C3. 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. -/
theorem 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) :=
  And.intro @FRC.Flavour.quarter_turn_boundary (And.intro @FRC.Flavour.lo_eigen (And.intro @FRC.Flavour.lo_ratio_sq (@FRC.Flavour.delta_lo)))
/-- p28015 — 28:C4. 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. -/
theorem 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₂))) :=
  And.intro @FRC.Flavour.norm_one_sub_i (And.intro @FRC.Flavour.norm_one_sub_omega (@FRC.Flavour.koide_five_sixths))
/-- p28016 — 28:C5. 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). -/
theorem 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)) :=
  And.intro @FRC.Flavour.trace_double (And.intro @FRC.Flavour.trace_triple (@FRC.Flavour.circ_det))
/-- p28017 — 28:C6. 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). -/
theorem 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)) :=
  And.intro @FRC.Flavour.gst_relation (@FRC.Flavour.cabibbo_modulus)
/-- p28018 — 28:C7. Up-sector doubling $m^u_i\sim(m^d_i)^2$ from the $\mathbf{10}\cdot\mathbf{10}$ Yukawa. -/
theorem 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 :=
  @FRC.Flavour.texture_exponents
/-- p28019 — 28:C8. 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$. -/
theorem 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) :=
  And.intro @FRC.Flavour.transpose_exchanges (@FRC.Flavour.transpose_mul)
/-- p28021 — 28:C10. 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. -/
theorem 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) :=
  And.intro @FRC.Flavour.protected_column (And.intro @FRC.Flavour.trimaximal (@FRC.Flavour.jarlskog_sq))
/-- p28022 — 28:C11. 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). -/
theorem 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 :=
  And.intro @FRC.Flavour.circ_mul (And.intro @FRC.Flavour.circ_adj (And.intro @FRC.Flavour.seesaw_circulant (And.intro @FRC.Flavour.transpose_fixed_point (@FRC.Flavour.circ_transpose))))
/-- p28026 — 28:X2. \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. -/
theorem 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₂))) :=
  And.intro @FRC.Flavour.norm_one_sub_omega (@FRC.Flavour.koide_five_sixths)
/-- p28027 — 28:X3. \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. -/
theorem 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 :=
  And.intro @FRC.Ladder.tower_reduces (@FRC.Flavour.texture_exponents)
/-- p28028 — 28:X4. \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. -/
theorem 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)) :=
  And.intro @FRC.Flavour.gst_relation (@FRC.Flavour.cabibbo_modulus)
/-- p28029 — 28:X5. \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. -/
theorem 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) :=
  @FRC.Flavour.colour_count
/-- p28030 — 28:X6. \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. -/
theorem 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 :=
  @FRC.Flavour.texture_exponents
/-- p28031 — 28:X7. \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. -/
theorem 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)) :=
  And.intro @FRC.Flavour.quarter_turn_boundary (And.intro @FRC.Flavour.lo_eigen (@FRC.Flavour.lo_ratio_sq))
/-- p28032 — 28:X8. \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. -/
theorem 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) :=
  And.intro @FRC.Flavour.transpose_exchanges (@FRC.Flavour.transpose_mul)
/-- p28034 — 28:X10. \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. -/
theorem 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) :=
  And.intro @FRC.Flavour.trimaximal (@FRC.Flavour.jarlskog_sq)
/-- p28035 — 28:X11. \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. -/
theorem 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 * ω) :=
  And.intro @FRC.Flavour.transpose_fixed_point (And.intro @FRC.Flavour.seesaw_circulant (@FRC.Flavour.circ_eigen))
/-- p28037 — 28:P2. 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. -/
theorem 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₂))) :=
  And.intro @FRC.Flavour.norm_one_sub_omega (@FRC.Flavour.koide_five_sixths)
/-- p28038 — 28:P3. 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. -/
theorem 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)) :=
  And.intro @FRC.Flavour.cabibbo_modulus (@FRC.Flavour.gst_relation)
/-- p28039 — 28:P5. 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. -/
theorem 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 :=
  And.intro @FRC.Flavour.transpose_fixed_point (@FRC.Flavour.circ_transpose)
/-- p28042 — 28:P8. 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. -/
theorem 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) :=
  And.intro @FRC.Flavour.jarlskog_sq (And.intro @FRC.Flavour.protected_column (@FRC.Flavour.trimaximal))
/-- p28050 — 28:C11b. Both orderings solved: the signed $r_\nu=\sqrt2$ circulant solves both neutrino orderings exactly, so the boundary branch (B6) is the sole ordering assumption. -/
theorem 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) :=
  And.intro @FRC.Interactions.koide_two_thirds (@FRC.Flavour.eigen_sumsq)
-- end keys

end FRC.Ledger