import FrcCore.Theme.Interactions
import FrcCore.Theme.Unitary
import FrcCore.Theme.Fields
import FrcCore.Keys.Interactions
import FrcCore.Keys.Horizon

/-!
# 27-fields — the Standard-Model interactions on the shell, no axioms (16 October 2026)

The paper module of *Gauge Interactions over Finite Holographic Substrate* (tree `27-fields-20260625`): every
declaration is the interactions theme's (`Theme/Interactions.lean`, `Theme/Unitary.lean`, `Theme/Fields.lean`), under
the paper's name — the electroweak counts and the neutral Hessian, the lattice identities, the V − A cancellation, the
drive's adjoint on `𝔽₁₃`, the Hermitian determinants, and the kernel-decided certificates (`2T` over `𝔽₉`, the `4³`
Green's function, the admissible actions at `L = 4`, the colour sector over `𝔽₄`, the mass matrices over `𝔽_p[√−3]`);
`one_generation` and `fifth_direction` keep the theme's names. The predicates `p27NNN` at the end are generated by
`make_predicates.py`, aliases of the keys of `Keys/Interactions.lean`. Every declaration is checked to depend on no
axiom (`check_core_axioms.py`).
-/

namespace FRC.Fields

open FRC.Shell FRC.Extension FRC.Unitary FRC.Interactions

/-! ## The paper's names for the theme's certificates -/

/-- 27:C1, 27:C4 — `SU(2, 𝔽₃) = 2T` over `𝔽₉` (`Interactions.tetrahedral_group`). -/
theorem tetrahedral_group :
    su2.length = 24 ∧ 24 = 3 * (3 * 3 - 1) ∧
    su2.all (fun x => su2.all (fun y => su2.contains (qmul x y))) = true ∧
    su2.any (fun x => su2.any (fun y => qmul x y != qmul y x)) = true ∧
    su2.all (fun x => (x.1 + Ext.conj x.1).im == 0) = true ∧
    [1, 2, 3, 4, 6].map (fun k => (su2.filter (fun x => qord x == k)).length) = [1, 1, 8, 6, 8] ∧
    [0, 1, 2].map (fun t => (su2.filter (fun x => (x.1 + Ext.conj x.1).re == ofNat t)).length) = [6, 9, 9] ∧
    su2.contains (⟨0, 1⟩, 0) = true ∧
    (su2.filter (fun x => qmul x (⟨0, 1⟩, 0) == qmul (⟨0, 1⟩, 0) x)).length = 4 :=
  FRC.Interactions.tetrahedral_group
/-- 27:C3 — the `L = 4` Coulomb Green's function (`Interactions.green_torus`). -/
theorem green_torus :
    greenTable.length = 64 ∧
    (List.range 64).all (fun n => greenLap (n % 4) (n / 4 % 4) (n / 16) == if n == 0 then 7680 - 120 else -120) = true ∧
    green 1 0 0 = 257 ∧ green 0 1 0 = 257 ∧ green 0 0 1 = 257 ∧ green 3 0 0 = 257 ∧
    green 0 0 0 > green 1 0 0 ∧ green 1 0 0 > green 2 0 0 ∧
    greenTable.foldl (· + ·) 0 = 0 ∧ 7680 / 64 = 120 :=
  FRC.Interactions.green_torus
/-- 27:C2, 27:X3 — the two admissible actions at `L = 4` (`Interactions.admissible_two`). -/
theorem admissible_two :
    constraintRows.length = 1023 ∧ admissibleA.length = 123 ∧ admissibleB.length = 123 ∧ maxwellForm.length = 123 ∧
    constraintRows.all (fun r => rowDot r admissibleA == 0) = true ∧
    constraintRows.all (fun r => rowDot r admissibleB == 0) = true ∧
    constraintRows.all (fun r => rowDot r maxwellForm == 0) = true ∧
    maxwellForm.map (fun c => 2 * c) = List.zipWith (fun b a => b - a) admissibleB admissibleA ∧
    admissibleA ≠ admissibleB :=
  FRC.Interactions.admissible_two
/-- 27:X11 — the Hermitian mass matrices over `𝔽₁₇[√−3]`, `𝔽₅₃[√−3]` (`Interactions.ckm_free`). -/
theorem ckm_free :
    ents (dag mu17) = ents mu17 ∧ ents (dag md17) = ents md17 ∧ ents (dag mc17) = ents mc17 ∧
    (det mu17).im = 0 ∧ (det md17).im = 0 ∧ (det mc17).im = 0 ∧ (det (mmul mu17 md17)).im = 0 ∧
    (det mu17).re ≠ 0 ∧ (det md17).re ≠ 0 ∧ (det mc17).re ≠ 0 ∧
    ents (mmul mu17 md17) ≠ ents (mmul md17 mu17) ∧
    ents (dag mu53) = ents mu53 ∧ ents (dag md53) = ents md53 ∧ ents (dag mc53) = ents mc53 ∧
    (det mu53).im = 0 ∧ (det md53).im = 0 ∧ (det mc53).im = 0 ∧ (det (mmul mu53 md53)).im = 0 ∧
    (det mu53).re ≠ 0 ∧ (det md53).re ≠ 0 ∧ (det mc53).re ≠ 0 ∧
    ents (mmul mu53 md53) ≠ ents (mmul md53 mu53) ∧
    nu17 + 3 = 0 ∧ nu53 + 3 = 0 :=
  FRC.Interactions.ckm_free
open FRC.Interactions.F4 in
/-- 27:C7, 27:X7 — the centre of `SU(3, 2)` over `𝔽₄` (`Interactions.su3_centre`). -/
theorem su3_centre :
    ([o, w, w2].all (fun x => x * conj x == o && x * x * x == o)) = true ∧
    (z * conj z == o) = false ∧ [o, w, w2].length = 3 ∧ 2 + 1 = 3 ∧
    ([o, w, w2].all (fun x => mm (scal x) [z, z, o, z, o, z, o, z, z] == mm [z, z, o, z, o, z, o, z, z] (scal x) &&
      mm (scal x) [z, z, o, z, w, z, w2, z, z] == mm [z, z, o, z, w, z, w2, z, z] (scal x))) = true :=
  FRC.Interactions.su3_centre
open FRC.Interactions.F4 in
/-- 27:C7, 27:X7, 27:X1 — the gluon self-coupling over `𝔽₄` (`Interactions.gluon_commutator`). -/
theorem gluon_commutator :
    let U₁ : M := [z, z, o, z, o, z, o, z, z]
    let U₂ : M := [z, z, o, z, w, z, w2, z, z]
    let D₁ : M := [o, z, z, z, w, z, z, z, w2]
    let D₂ : M := [w, z, z, z, o, z, z, z, w2]
    mm (dg U₁) U₁ = one ∧ mm (dg U₂) U₂ = one ∧ det U₁ = o ∧ det U₂ = o ∧
    mm U₁ U₂ ≠ mm U₂ U₁ ∧
    mm (mm U₁ U₂) (mm (dg U₁) (dg U₂)) = [w2, z, z, z, o, z, z, z, w] ∧
    mm (mm U₁ U₂) (mm (dg U₁) (dg U₂)) ≠ one ∧
    mm (mm D₁ D₂) (mm (dg D₁) (dg D₂)) = one :=
  FRC.Interactions.gluon_commutator

/-! ## The paper's names for the theme's theorems -/

/-- 27:C6, 27:X4 — `sin²θ_W = 3/8` from the sixteen's charges (`Interactions.weinberg_angle`). -/
theorem weinberg_angle : isum (gen16.map (fun S => (3 * t3h S) * (3 * t3h S))) = 72 ∧ isum (gen16.map (fun S => q6 S * q6 S)) = 192 ∧ 72 * 8 = 192 * 3 :=
  @FRC.Interactions.weinberg_angle
/-- 27:C9 — the unification counts (`Interactions.unification_counts`). -/
theorem unification_counts : 24 - (8 + 3 + 1) = 12 ∧ 12 = 2 * (3 * 2) ∧ 1 + 5 + 10 = 16 ∧ 10 * 9 = 2 * 45 :=
  @FRC.Interactions.unification_counts
/-- 27:C11 — `Ω ≡ 5 (mod 12)` as the conjunction (`Interactions.residue_five`). -/
theorem residue_five : ∀ n : Nat, n % 12 = 5 ↔ n % 4 = 1 ∧ n % 3 = 2 :=
  @FRC.Interactions.residue_five
/-- 27:C7, 27:X7 — the rank tower (`Interactions.rank_tower`). -/
theorem rank_tower : ∀ n : Nat, n % 12 = 5 → (n + 1) % 2 = 0 ∧ (n + 1) % 3 = 0 ∧ (n + 1) % 4 = 2 :=
  @FRC.Interactions.rank_tower
/-- 27:C5, 27:X3, 27:X5 — the neutral Hessian (`Interactions.hessian_neutral`). -/
theorem hessian_neutral : ∀ {p : Nat} [Pos p] (g g' v : Shell p), g * g * (v * v) * (g' * g' * (v * v)) + -(-(g * g' * (v * v)) * -(g * g' * (v * v))) = 0 ∧ g * g * (v * v) * g' + -(g * g' * (v * v)) * g = 0 ∧ -(g * g' * (v * v)) * g' + g' * g' * (v * v) * g = 0 ∧ g * g * (v * v) * g + -(g * g' * (v * v)) * -g' = (g * g + g' * g') * (v * v) * g ∧ -(g * g' * (v * v)) * g + g' * g' * (v * v) * -g' = (g * g + g' * g') * (v * v) * -g' :=
  @FRC.Interactions.hessian_neutral
/-- 27:C5 — `cos²θ_W = 5/8` (`Interactions.five_eighths`). -/
theorem five_eighths : ∀ {p : Nat} [Pos p] (g g' : Shell p), 8 * (g' * g') = 3 * (g * g + g' * g') → 8 * (g * g) = 5 * (g * g + g' * g') :=
  @FRC.Interactions.five_eighths
/-- 27:C2, 27:X3 — the photon's operator forced (`Interactions.projector_forced`). -/
theorem projector_forced : ∀ {p : Nat} [Pos p] (a b c : Shell p), (a + b) * 1 + c = 0 → (a + b) * (1 + 1) + c = 0 → a + b = 0 ∧ c = 0 :=
  @FRC.Interactions.projector_forced
/-- 27:X2 — discrete Stokes (`Interactions.holonomy_stokes`). -/
theorem holonomy_stokes : ∀ {p : Nat} [Pos p] (A₁ A₂ B₃ A₄ A₅ B₀ B₁ : Shell p), A₁ + A₂ + B₃ + -A₄ + -A₅ + -B₀ = A₁ + B₁ + -A₅ + -B₀ + (A₂ + B₃ + -A₄ + -B₁) :=
  @FRC.Interactions.holonomy_stokes
/-- 27:C2, 27:X1 — gauge invariance of the flux (`Interactions.gauge_flux_invariant`). -/
theorem gauge_flux_invariant : ∀ {p : Nat} [Pos p] (A B C D φ₀ φ₁ φ₂ φ₃ : Shell p), A + φ₁ + -φ₀ + (B + φ₂ + -φ₁) + -(C + φ₂ + -φ₃) + -(D + φ₃ + -φ₀) = A + B + -C + -D :=
  @FRC.Interactions.gauge_flux_invariant
/-- 27:C4, 27:X6 — the V − A cancellation (`Interactions.va_cancel`). -/
theorem va_cancel : ∀ {p : Nat} [Pos p], FRC.Nat.isPrime p → ∀ {u : Shell p} {N : Nat}, u ^ N = 1 → ∀ {δ : Nat}, u ^ (2 * δ) ≠ 1 → sumRange (fun τ => u ^ (2 * δ * τ)) N = 0 ∧ sumRange (fun _ => (1 : Shell p)) N = ofNat N :=
  @FRC.Interactions.va_cancel
/-- The chiral projector, corroboration (`Interactions.projector_idempotent`). -/
theorem projector_idempotent : ∀ {p : Nat} [Pos p] (x y : Shell p), (1 : Shell p) * 1 = 1 ∧ (0 : Shell p) * 0 = 0 ∧ 1 * x = x ∧ 0 * y = 0 :=
  @FRC.Interactions.projector_idempotent
/-- 27:C4, 27:X6 — the orientation relabelling (`Interactions.orientation_flip`). -/
theorem orientation_flip : ∀ {p : Nat} [Pos p], FRC.Nat.isPrime p → ∀ {u : Shell p} {N : Nat}, u ^ N = 1 → ∀ {δ : Nat}, δ ≤ N → u ^ (2 * δ) ≠ 1 → sumRange (fun τ => u ^ (2 * (N - δ) * τ)) N = 0 ∧ ((1 : Int) ≠ -1 ∧ (1 : Int) * 1 > 0 ∧ (-1 : Int) * -1 > 0) :=
  @FRC.Interactions.orientation_flip
/-- 27:C4, 27:X1 — the drive's adjoint action on `𝔽₁₃` (`Interactions.drive_adjoint`). -/
theorem drive_adjoint :
    m2 (2, 0, 0, 7) (7, 0, 0, (2 : Shell 13)) = (1, 0, 0, 1) ∧
    m2 (m2 (2, 0, 0, 7) (1, 0, 0, 12)) (7, 0, 0, (2 : Shell 13)) = (1, 0, 0, 12) ∧
    m2 (m2 (2, 0, 0, 7) (0, 1, 0, 0)) (7, 0, 0, (2 : Shell 13)) = (0, 4, 0, 0) ∧
    m2 (m2 (2, 0, 0, 7) (0, 0, 1, 0)) (7, 0, 0, (2 : Shell 13)) = (0, 0, 10, 0) ∧
    (4 : Shell 13) * 10 = 1 ∧
    ((List.range (13 * 13 * 13 * 13)).filter (fun n =>
      let X := m2of (p := 13) n
      X.1 * X.2.2.2 + -(X.2.1 * X.2.2.1) == 1 && m2 X (2, 0, 0, 7) == m2 (2, 0, 0, 7) X)).length = 12 ∧
    m2 (3, 4, 2, 3) (2, 0, 0, 7) ≠ m2 (2, 0, 0, 7) (3, 4, 2, (3 : Shell 13)) :=
  FRC.Interactions.drive_adjoint
/-- 27:X11, 27:P9 — Hermitian determinants are their own conjugates (`Unitary.hermitian_det_real`). -/
theorem hermitian_det_real : ∀ {p : Nat} [Pos p] {ν : Shell p} (A : M3 p ν), dag A = A → Ext.conj (det A) = det A :=
  @FRC.Unitary.hermitian_det_real
/-- 27:C5, 27:X5 — the full Hessian on `𝔽₁₃` and `𝔽₅` (`Interactions.hessian_full`). -/
theorem hessian_full :
    ((List.range 4).all (fun a => hess (5 : Shell 13) 1 2 2 7 a 2 * 2 + hess (5 : Shell 13) 1 2 2 7 a 3 * 1 == 0)) = true ∧
    hess (5 : Shell 13) 1 2 2 7 2 2 * hess (5 : Shell 13) 1 2 2 7 3 3 + -(hess (5 : Shell 13) 1 2 2 7 2 3 * hess (5 : Shell 13) 1 2 2 7 3 2) = 0 ∧
    hess (5 : Shell 13) 1 2 2 7 0 0 = hess (5 : Shell 13) 1 2 2 7 1 1 ∧
    hess (5 : Shell 13) 1 2 2 7 2 2 + hess (5 : Shell 13) 1 2 2 7 3 3 = (1 * 1 + 2 * 2) * (2 * 2) * (7 * 7) ∧
    hess (5 : Shell 13) 1 2 2 7 0 0 * (1 * 1 + 2 * 2) = (hess (5 : Shell 13) 1 2 2 7 2 2 + hess (5 : Shell 13) 1 2 2 7 3 3) * (1 * 1) ∧
    (5 : Shell 13) * 5 = -1 ∧ (7 : Shell 13) + 7 = 1 ∧
    ((List.range 4).all (fun a => hess (2 : Shell 5) 1 1 2 3 a 2 * 1 + hess (2 : Shell 5) 1 1 2 3 a 3 * 1 == 0)) = true ∧
    hess (2 : Shell 5) 1 1 2 3 2 2 * hess (2 : Shell 5) 1 1 2 3 3 3 + -(hess (2 : Shell 5) 1 1 2 3 2 3 * hess (2 : Shell 5) 1 1 2 3 3 2) = 0 ∧
    hess (2 : Shell 5) 1 1 2 3 0 0 = hess (2 : Shell 5) 1 1 2 3 1 1 ∧
    hess (2 : Shell 5) 1 1 2 3 2 2 + hess (2 : Shell 5) 1 1 2 3 3 3 = (1 * 1 + 1 * 1) * (2 * 2) * (3 * 3) ∧
    hess (2 : Shell 5) 1 1 2 3 0 0 * (1 * 1 + 1 * 1) = (hess (2 : Shell 5) 1 1 2 3 2 2 + hess (2 : Shell 5) 1 1 2 3 3 3) * (1 * 1) ∧
    (2 : Shell 5) * 2 = -1 ∧ (3 : Shell 5) + 3 = 1 :=
  FRC.Interactions.hessian_full
/-- 27:C9, 27:X8 — the colour–isospin transpositions as automorphisms (`Interactions.offblock_automorphism`). -/
theorem offblock_automorphism :
    offblock.all (fun cw => (List.range 32).all (fun S => (List.range 32).all (fun T =>
      let a := emul S T
      let b := emul (act cw.1 cw.2 S) (act cw.1 cw.2 T)
      b.1 * b.1 == a.1 * a.1 && (a.1 == 0 || b.2 == act cw.1 cw.2 a.2)))) = true ∧
    offblock.all (fun cw => (List.range 32).all (fun S => (List.range 32).all (fun T =>
      act cw.1 cw.2 S == act cw.1 cw.2 T → S == T)) && (List.range 32).all (fun S => act cw.1 cw.2 S < 32)) = true :=
  FRC.Interactions.offblock_automorphism
/-- 27:X11, 27:P9 — the Hermitian determinant's imaginary part is `2`-torsion (`Unitary.hermitian_det_shell`). -/
theorem hermitian_det_shell : ∀ {p : Nat} [Pos p] {ν : Shell p} (A : M3 p ν), dag A = A → (det A).im + (det A).im = 0 :=
  @FRC.Unitary.hermitian_det_shell
/-- 27:C1, 27:C4 — the trace is a class function (`Unitary.class_function`). -/
theorem class_function : ∀ {p : Nat} [Pos p] {ν : Shell p} (g M : M2 p ν), det2 g = 1 → tr2 (mmul2 (mmul2 g M) (adj2 g)) = tr2 M :=
  @FRC.Unitary.class_function

-- Ledger predicates of 27-fields (generated by make_predicates.py from docs/27-fields/27-fields-ledger.json; edit the ledger, not this section)
/-- 27:C1 (p27013) — The finite gauge correspondence, its exact clauses: the abelian inclusion $\Z/M\hookrightarrow\U(1)$ as the $M$-th roots of unity, the positive cyclotomic action (the Wilson weight $1-\Re\zeta\ge0$), and the exact $q{=}3$ embedding $\SU(2,\F_3)\cong2T$ with the Wilson trace a class function (Theorems~\ref{thm:corrU1},~\ref{thm:corrpos},~\ref{thm:corr2T}); the resolvable-window reconstruction is C12 and the cross-scale running $\Omega$-hard (Z1). -/
theorem p27013 : (FRC.Interactions.su2.length = (24 : Nat) ∧ (24 : Nat) = (3 : Nat) * ((3 : Nat) * (3 : Nat) - (1 : Nat)) ∧ (FRC.Interactions.su2.all fun x => FRC.Interactions.su2.all fun y => FRC.Interactions.su2.contains (FRC.Interactions.qmul x y)) = true ∧ (FRC.Interactions.su2.any fun x => FRC.Interactions.su2.any fun y => FRC.Interactions.qmul x y != FRC.Interactions.qmul y x) = true ∧ (FRC.Interactions.su2.all fun x => (x.fst + x.fst.conj).im == (0 : FRC.Shell (3 : Nat))) = true ∧ List.map (fun k => (List.filter (fun x => FRC.Interactions.qord x == k) FRC.Interactions.su2).length) [(1 : Nat), (2 : Nat), (3 : Nat), (4 : Nat), (6 : Nat)] = [(1 : Nat), (1 : Nat), (8 : Nat), (6 : Nat), (8 : Nat)] ∧ List.map (fun t => (List.filter (fun x => (x.fst + x.fst.conj).re == FRC.Shell.ofNat t) FRC.Interactions.su2).length) [(0 : Nat), (1 : Nat), (2 : Nat)] = [(6 : Nat), (9 : Nat), (9 : Nat)] ∧ FRC.Interactions.su2.contains ({ re := (0 : FRC.Shell (3 : Nat)), im := (1 : FRC.Shell (3 : Nat)) }, (0 : FRC.Extension.Ext (3 : Nat) (2 : FRC.Shell (3 : Nat)))) = true ∧ (List.filter (fun x => FRC.Interactions.qmul x ({ re := (0 : FRC.Shell (3 : Nat)), im := (1 : FRC.Shell (3 : Nat)) }, (0 : FRC.Extension.Ext (3 : Nat) (2 : FRC.Shell (3 : Nat)))) == FRC.Interactions.qmul ({ re := (0 : FRC.Shell (3 : Nat)), im := (1 : FRC.Shell (3 : Nat)) }, (0 : FRC.Extension.Ext (3 : Nat) (2 : FRC.Shell (3 : Nat)))) x) FRC.Interactions.su2).length = (4 : Nat)) ∧ ∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (g M : FRC.Unitary.M2 p ν), FRC.Unitary.det2 g = (1 : FRC.Extension.Ext p ν) → FRC.Unitary.tr2 (FRC.Unitary.mmul2 (FRC.Unitary.mmul2 g M) (FRC.Unitary.adj2 g)) = FRC.Unitary.tr2 M :=
  @FRC.Ledger.p27013
/-- 27:C2 (p27014) — Electromagnetism: charge as a quantised winding index, the massless photon by drive-invariance, the repulsive sign, the unique Maxwell operator, and $\al_{\mathrm{bare}}=1/4\pi$ as the phase-channel capacity normalisation. -/
theorem p27014 : (∀ {p : Nat} [FRC.Pos p] (A B C D φ₀ φ₁ φ₂ φ₃ : FRC.Shell p), A + φ₁ + -φ₀ + (B + φ₂ + -φ₁) + -(C + φ₂ + -φ₃) + -(D + φ₃ + -φ₀) = A + B + -C + -D) ∧ (∀ {p : Nat} [FRC.Pos p] (a b c : FRC.Shell p), (a + b) * (1 : FRC.Shell p) + c = (0 : FRC.Shell p) → (a + b) * ((1 : FRC.Shell p) + (1 : FRC.Shell p)) + c = (0 : FRC.Shell p) → a + b = (0 : FRC.Shell p) ∧ c = (0 : FRC.Shell p)) ∧ FRC.Interactions.constraintRows.length = (1023 : Nat) ∧ FRC.Interactions.admissibleA.length = (123 : Nat) ∧ FRC.Interactions.admissibleB.length = (123 : Nat) ∧ FRC.Interactions.maxwellForm.length = (123 : Nat) ∧ (FRC.Interactions.constraintRows.all fun r => FRC.Interactions.rowDot r FRC.Interactions.admissibleA == (0 : Int)) = true ∧ (FRC.Interactions.constraintRows.all fun r => FRC.Interactions.rowDot r FRC.Interactions.admissibleB == (0 : Int)) = true ∧ (FRC.Interactions.constraintRows.all fun r => FRC.Interactions.rowDot r FRC.Interactions.maxwellForm == (0 : Int)) = true ∧ List.map (fun c => (2 : Int) * c) FRC.Interactions.maxwellForm = List.zipWith (fun b a => b - a) FRC.Interactions.admissibleB FRC.Interactions.admissibleA ∧ FRC.Interactions.admissibleA ≠ FRC.Interactions.admissibleB :=
  @FRC.Ledger.p27014
/-- 27:C3 (p27015) — The Coulomb law and Maxwell dynamics, as corollaries of the correspondence on the resolvable window. -/
theorem p27015 : FRC.Interactions.greenTable.length = (64 : Nat) ∧ ((List.range (64 : Nat)).all fun n => FRC.Interactions.greenLap (n % (4 : Nat)) (n / (4 : Nat) % (4 : Nat)) (n / (16 : Nat)) == if (n == (0 : Nat)) = true then (7680 : Int) - (120 : Int) else (-120 : Int)) = true ∧ FRC.Interactions.green (1 : Nat) (0 : Nat) (0 : Nat) = (257 : Int) ∧ FRC.Interactions.green (0 : Nat) (1 : Nat) (0 : Nat) = (257 : Int) ∧ FRC.Interactions.green (0 : Nat) (0 : Nat) (1 : Nat) = (257 : Int) ∧ FRC.Interactions.green (3 : Nat) (0 : Nat) (0 : Nat) = (257 : Int) ∧ FRC.Interactions.green (0 : Nat) (0 : Nat) (0 : Nat) > FRC.Interactions.green (1 : Nat) (0 : Nat) (0 : Nat) ∧ FRC.Interactions.green (1 : Nat) (0 : Nat) (0 : Nat) > FRC.Interactions.green (2 : Nat) (0 : Nat) (0 : Nat) ∧ List.foldl (fun x1 x2 => x1 + x2) (0 : Int) FRC.Interactions.greenTable = (0 : Int) ∧ (7680 / 64 : Nat) = (120 : Nat) :=
  @FRC.Ledger.p27015
/-- 27:C4 (p27016) — The weak sector: the cell-local $\SU(2)$ Wilson connection, electroweak breaking as drive-torus misalignment with the photon kept massless, and maximal $V\!-\!A$ parity violation with the Frobenius branch decoupling exactly. -/
theorem p27016 : (FRC.Interactions.m2 ((2 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (7 : FRC.Shell (13 : Nat))) ((7 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (2 : FRC.Shell (13 : Nat))) = ((1 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (1 : FRC.Shell (13 : Nat))) ∧ FRC.Interactions.m2 (FRC.Interactions.m2 ((2 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (7 : FRC.Shell (13 : Nat))) ((1 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (12 : FRC.Shell (13 : Nat)))) ((7 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (2 : FRC.Shell (13 : Nat))) = ((1 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (12 : FRC.Shell (13 : Nat))) ∧ FRC.Interactions.m2 (FRC.Interactions.m2 ((2 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (7 : FRC.Shell (13 : Nat))) ((0 : FRC.Shell (13 : Nat)), (1 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)))) ((7 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (2 : FRC.Shell (13 : Nat))) = ((0 : FRC.Shell (13 : Nat)), (4 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat))) ∧ FRC.Interactions.m2 (FRC.Interactions.m2 ((2 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (7 : FRC.Shell (13 : Nat))) ((0 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (1 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)))) ((7 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (2 : FRC.Shell (13 : Nat))) = ((0 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (10 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat))) ∧ (4 : FRC.Shell (13 : Nat)) * (10 : FRC.Shell (13 : Nat)) = (1 : FRC.Shell (13 : Nat)) ∧ (List.filter (fun n => have X := FRC.Interactions.m2of n; X.fst * X.snd.snd.snd + -(X.snd.fst * X.snd.snd.fst) == (1 : FRC.Shell (13 : Nat)) && FRC.Interactions.m2 X ((2 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (7 : FRC.Shell (13 : Nat))) == FRC.Interactions.m2 ((2 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (7 : FRC.Shell (13 : Nat))) X) (List.range ((13 : Nat) * (13 : Nat) * (13 : Nat) * (13 : Nat)))).length = (12 : Nat) ∧ FRC.Interactions.m2 ((3 : FRC.Shell (13 : Nat)), (4 : FRC.Shell (13 : Nat)), (2 : FRC.Shell (13 : Nat)), (3 : FRC.Shell (13 : Nat))) ((2 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (7 : FRC.Shell (13 : Nat))) ≠ FRC.Interactions.m2 ((2 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (7 : FRC.Shell (13 : Nat))) ((3 : FRC.Shell (13 : Nat)), (4 : FRC.Shell (13 : Nat)), (2 : FRC.Shell (13 : Nat)), (3 : FRC.Shell (13 : Nat)))) ∧ (∀ {p : Nat} [FRC.Pos p], FRC.Nat.isPrime p → ∀ {u : FRC.Shell p} {N : Nat}, u ^ N = (1 : FRC.Shell p) → ∀ {δ : Nat}, u ^ ((2 : Nat) * δ) ≠ (1 : FRC.Shell p) → FRC.Shell.sumRange (fun τ => u ^ ((2 : Nat) * δ * τ)) N = (0 : FRC.Shell p) ∧ FRC.Shell.sumRange (fun x => (1 : FRC.Shell p)) N = FRC.Shell.ofNat N) ∧ (∀ {p : Nat} [FRC.Pos p], FRC.Nat.isPrime p → ∀ {u : FRC.Shell p} {N : Nat}, u ^ N = (1 : FRC.Shell p) → ∀ {δ : Nat}, δ ≤ N → u ^ ((2 : Nat) * δ) ≠ (1 : FRC.Shell p) → FRC.Shell.sumRange (fun τ => u ^ ((2 : Nat) * (N - δ) * τ)) N = (0 : FRC.Shell p) ∧ (1 : Int) ≠ (-1 : Int) ∧ (1 : Int) * (1 : Int) > (0 : Int) ∧ (-1 : Int) * (-1 : Int) > (0 : Int)) ∧ (FRC.Interactions.su2.length = (24 : Nat) ∧ (24 : Nat) = (3 : Nat) * ((3 : Nat) * (3 : Nat) - (1 : Nat)) ∧ (FRC.Interactions.su2.all fun x => FRC.Interactions.su2.all fun y => FRC.Interactions.su2.contains (FRC.Interactions.qmul x y)) = true ∧ (FRC.Interactions.su2.any fun x => FRC.Interactions.su2.any fun y => FRC.Interactions.qmul x y != FRC.Interactions.qmul y x) = true ∧ (FRC.Interactions.su2.all fun x => (x.fst + x.fst.conj).im == (0 : FRC.Shell (3 : Nat))) = true ∧ List.map (fun k => (List.filter (fun x => FRC.Interactions.qord x == k) FRC.Interactions.su2).length) [(1 : Nat), (2 : Nat), (3 : Nat), (4 : Nat), (6 : Nat)] = [(1 : Nat), (1 : Nat), (8 : Nat), (6 : Nat), (8 : Nat)] ∧ List.map (fun t => (List.filter (fun x => (x.fst + x.fst.conj).re == FRC.Shell.ofNat t) FRC.Interactions.su2).length) [(0 : Nat), (1 : Nat), (2 : Nat)] = [(6 : Nat), (9 : Nat), (9 : Nat)] ∧ FRC.Interactions.su2.contains ({ re := (0 : FRC.Shell (3 : Nat)), im := (1 : FRC.Shell (3 : Nat)) }, (0 : FRC.Extension.Ext (3 : Nat) (2 : FRC.Shell (3 : Nat)))) = true ∧ (List.filter (fun x => FRC.Interactions.qmul x ({ re := (0 : FRC.Shell (3 : Nat)), im := (1 : FRC.Shell (3 : Nat)) }, (0 : FRC.Extension.Ext (3 : Nat) (2 : FRC.Shell (3 : Nat)))) == FRC.Interactions.qmul ({ re := (0 : FRC.Shell (3 : Nat)), im := (1 : FRC.Shell (3 : Nat)) }, (0 : FRC.Extension.Ext (3 : Nat) (2 : FRC.Shell (3 : Nat)))) x) FRC.Interactions.su2).length = (4 : Nat)) ∧ ∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (g M : FRC.Unitary.M2 p ν), FRC.Unitary.det2 g = (1 : FRC.Extension.Ext p ν) → FRC.Unitary.tr2 (FRC.Unitary.mmul2 (FRC.Unitary.mmul2 g M) (FRC.Unitary.adj2 g)) = FRC.Unitary.tr2 M :=
  @FRC.Ledger.p27016
/-- 27:C5 (p27017) — The propagating neutral spectrum and custodial $\rho=1$: the Hessian of $S_\rho$ at the broken vacuum gives massive $W^\pm,Z$ against a massless photon, $\rho=1$ as $\det\equiv0$, $M_W^2/M_Z^2=\cos^2\sW$, which is $5/8$ at the unification point (Prop.~\ref{prop:running}); the imported electroweak template (A4) evaluated on the realisation B3. -/
theorem p27017 : (∀ {p : Nat} [FRC.Pos p] (g g' v : FRC.Shell p), g * g * (v * v) * (g' * g' * (v * v)) + -(-(g * g' * (v * v)) * -(g * g' * (v * v))) = (0 : FRC.Shell p) ∧ g * g * (v * v) * g' + -(g * g' * (v * v)) * g = (0 : FRC.Shell p) ∧ -(g * g' * (v * v)) * g' + g' * g' * (v * v) * g = (0 : FRC.Shell p) ∧ g * g * (v * v) * g + -(g * g' * (v * v)) * -g' = (g * g + g' * g') * (v * v) * g ∧ -(g * g' * (v * v)) * g + g' * g' * (v * v) * -g' = (g * g + g' * g') * (v * v) * -g') ∧ (((List.range (4 : Nat)).all fun a => FRC.Interactions.hess (5 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (7 : FRC.Shell (13 : Nat)) a (2 : Nat) * (2 : FRC.Shell (13 : Nat)) + FRC.Interactions.hess (5 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (7 : FRC.Shell (13 : Nat)) a (3 : Nat) * (1 : FRC.Shell (13 : Nat)) == (0 : FRC.Shell (13 : Nat))) = true ∧ FRC.Interactions.hess (5 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (7 : FRC.Shell (13 : Nat)) (2 : Nat) (2 : Nat) * FRC.Interactions.hess (5 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (7 : FRC.Shell (13 : Nat)) (3 : Nat) (3 : Nat) + -(FRC.Interactions.hess (5 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (7 : FRC.Shell (13 : Nat)) (2 : Nat) (3 : Nat) * FRC.Interactions.hess (5 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (7 : FRC.Shell (13 : Nat)) (3 : Nat) (2 : Nat)) = (0 : FRC.Shell (13 : Nat)) ∧ FRC.Interactions.hess (5 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (7 : FRC.Shell (13 : Nat)) (0 : Nat) (0 : Nat) = FRC.Interactions.hess (5 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (7 : FRC.Shell (13 : Nat)) (1 : Nat) (1 : Nat) ∧ FRC.Interactions.hess (5 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (7 : FRC.Shell (13 : Nat)) (2 : Nat) (2 : Nat) + FRC.Interactions.hess (5 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (7 : FRC.Shell (13 : Nat)) (3 : Nat) (3 : Nat) = ((1 : FRC.Shell (13 : Nat)) * (1 : FRC.Shell (13 : Nat)) + (2 : FRC.Shell (13 : Nat)) * (2 : FRC.Shell (13 : Nat))) * ((2 : FRC.Shell (13 : Nat)) * (2 : FRC.Shell (13 : Nat))) * ((7 : FRC.Shell (13 : Nat)) * (7 : FRC.Shell (13 : Nat))) ∧ FRC.Interactions.hess (5 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (7 : FRC.Shell (13 : Nat)) (0 : Nat) (0 : Nat) * ((1 : FRC.Shell (13 : Nat)) * (1 : FRC.Shell (13 : Nat)) + (2 : FRC.Shell (13 : Nat)) * (2 : FRC.Shell (13 : Nat))) = (FRC.Interactions.hess (5 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (7 : FRC.Shell (13 : Nat)) (2 : Nat) (2 : Nat) + FRC.Interactions.hess (5 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (7 : FRC.Shell (13 : Nat)) (3 : Nat) (3 : Nat)) * ((1 : FRC.Shell (13 : Nat)) * (1 : FRC.Shell (13 : Nat))) ∧ (5 : FRC.Shell (13 : Nat)) * (5 : FRC.Shell (13 : Nat)) = (-1 : FRC.Shell (13 : Nat)) ∧ (7 : FRC.Shell (13 : Nat)) + (7 : FRC.Shell (13 : Nat)) = (1 : FRC.Shell (13 : Nat)) ∧ ((List.range (4 : Nat)).all fun a => FRC.Interactions.hess (2 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (2 : FRC.Shell (5 : Nat)) (3 : FRC.Shell (5 : Nat)) a (2 : Nat) * (1 : FRC.Shell (5 : Nat)) + FRC.Interactions.hess (2 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (2 : FRC.Shell (5 : Nat)) (3 : FRC.Shell (5 : Nat)) a (3 : Nat) * (1 : FRC.Shell (5 : Nat)) == (0 : FRC.Shell (5 : Nat))) = true ∧ FRC.Interactions.hess (2 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (2 : FRC.Shell (5 : Nat)) (3 : FRC.Shell (5 : Nat)) (2 : Nat) (2 : Nat) * FRC.Interactions.hess (2 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (2 : FRC.Shell (5 : Nat)) (3 : FRC.Shell (5 : Nat)) (3 : Nat) (3 : Nat) + -(FRC.Interactions.hess (2 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (2 : FRC.Shell (5 : Nat)) (3 : FRC.Shell (5 : Nat)) (2 : Nat) (3 : Nat) * FRC.Interactions.hess (2 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (2 : FRC.Shell (5 : Nat)) (3 : FRC.Shell (5 : Nat)) (3 : Nat) (2 : Nat)) = (0 : FRC.Shell (5 : Nat)) ∧ FRC.Interactions.hess (2 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (2 : FRC.Shell (5 : Nat)) (3 : FRC.Shell (5 : Nat)) (0 : Nat) (0 : Nat) = FRC.Interactions.hess (2 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (2 : FRC.Shell (5 : Nat)) (3 : FRC.Shell (5 : Nat)) (1 : Nat) (1 : Nat) ∧ FRC.Interactions.hess (2 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (2 : FRC.Shell (5 : Nat)) (3 : FRC.Shell (5 : Nat)) (2 : Nat) (2 : Nat) + FRC.Interactions.hess (2 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (2 : FRC.Shell (5 : Nat)) (3 : FRC.Shell (5 : Nat)) (3 : Nat) (3 : Nat) = ((1 : FRC.Shell (5 : Nat)) * (1 : FRC.Shell (5 : Nat)) + (1 : FRC.Shell (5 : Nat)) * (1 : FRC.Shell (5 : Nat))) * ((2 : FRC.Shell (5 : Nat)) * (2 : FRC.Shell (5 : Nat))) * ((3 : FRC.Shell (5 : Nat)) * (3 : FRC.Shell (5 : Nat))) ∧ FRC.Interactions.hess (2 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (2 : FRC.Shell (5 : Nat)) (3 : FRC.Shell (5 : Nat)) (0 : Nat) (0 : Nat) * ((1 : FRC.Shell (5 : Nat)) * (1 : FRC.Shell (5 : Nat)) + (1 : FRC.Shell (5 : Nat)) * (1 : FRC.Shell (5 : Nat))) = (FRC.Interactions.hess (2 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (2 : FRC.Shell (5 : Nat)) (3 : FRC.Shell (5 : Nat)) (2 : Nat) (2 : Nat) + FRC.Interactions.hess (2 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (2 : FRC.Shell (5 : Nat)) (3 : FRC.Shell (5 : Nat)) (3 : Nat) (3 : Nat)) * ((1 : FRC.Shell (5 : Nat)) * (1 : FRC.Shell (5 : Nat))) ∧ (2 : FRC.Shell (5 : Nat)) * (2 : FRC.Shell (5 : Nat)) = (-1 : FRC.Shell (5 : Nat)) ∧ (3 : FRC.Shell (5 : Nat)) + (3 : FRC.Shell (5 : Nat)) = (1 : FRC.Shell (5 : Nat))) ∧ ∀ {p : Nat} [FRC.Pos p] (g g' : FRC.Shell p), (8 : FRC.Shell p) * (g' * g') = (3 : FRC.Shell p) * (g * g + g' * g') → (8 : FRC.Shell p) * (g * g) = (5 : FRC.Shell p) * (g * g + g' * g') :=
  @FRC.Ledger.p27017
/-- 27:C6 (p27018) — The Weinberg trace formula $\sin^2\sW=\Tr(T_3^2)/\Tr(Q^2)=3/8$ for a complete generation, the unification-point value, and the four-fermion amplitude with $G_F=1/(\sqrt2\,v^2)$; the imported template (A4) evaluated on the realisations B3, B5. -/
theorem p27018 : (FRC.Interactions.isum (List.map (fun S => (3 : Int) * FRC.Interactions.t3h S * ((3 : Int) * FRC.Interactions.t3h S)) FRC.Interactions.gen16) = (72 : Int) ∧ FRC.Interactions.isum (List.map (fun S => FRC.Interactions.q6 S * FRC.Interactions.q6 S) FRC.Interactions.gen16) = (192 : Int) ∧ (72 : Nat) * (8 : Nat) = (192 : Nat) * (3 : Nat)) ∧ (List.filter (fun S => FRC.Interactions.col S == (0 : Nat) && FRC.Interactions.wk S == (0 : Nat) && FRC.Interactions.y6 S == (0 : Int)) FRC.Interactions.gen16).length = (1 : Nat) ∧ (List.filter (fun S => FRC.Interactions.col S == (2 : Nat) && FRC.Interactions.wk S == (0 : Nat) && FRC.Interactions.y6 S == (-4 : Int)) FRC.Interactions.gen16).length = (3 : Nat) ∧ (List.filter (fun S => FRC.Interactions.col S == (1 : Nat) && FRC.Interactions.wk S == (1 : Nat) && FRC.Interactions.y6 S == (1 : Int)) FRC.Interactions.gen16).length = (6 : 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) ∧ (List.filter (fun S => FRC.Interactions.col S == (3 : Nat) && FRC.Interactions.wk S == (1 : Nat) && FRC.Interactions.y6 S == (-3 : Int)) FRC.Interactions.gen16).length = (2 : Nat) ∧ (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.map FRC.Interactions.q6 FRC.Interactions.gen16 = [(0 : Int), (-4 : Int), (-4 : Int), (-4 : Int), (4 : Int), (4 : Int), (4 : Int), (0 : Int), (-2 : Int), (-2 : Int), (-2 : Int), (-6 : Int), (6 : Int), (2 : Int), (2 : Int), (2 : Int)] ∧ FRC.Interactions.isum (List.map FRC.Interactions.y6 FRC.Interactions.gen16) = (0 : Int) ∧ FRC.Interactions.isum (List.map (fun S => FRC.Interactions.y6 S ^ (3 : Nat)) FRC.Interactions.gen16) = (0 : Int) ∧ FRC.Interactions.isum (List.map FRC.Interactions.y6 (List.filter (fun S => FRC.Interactions.col S == (1 : Nat) || FRC.Interactions.col S == (2 : Nat)) FRC.Interactions.gen16)) = (0 : Int) ∧ FRC.Interactions.isum (List.map FRC.Interactions.y6 (List.filter (fun S => FRC.Interactions.wk S == (1 : Nat)) FRC.Interactions.gen16)) = (0 : Int) ∧ (List.filter (fun S => FRC.Interactions.col S == (1 : Nat)) FRC.Interactions.gen16).length = (List.filter (fun S => FRC.Interactions.col S == (2 : Nat)) FRC.Interactions.gen16).length ∧ (List.filter (fun S => FRC.Interactions.wk S == (1 : Nat)) FRC.Interactions.gen16).length % (4 : Nat) = (0 : Nat) ∧ (FRC.Interactions.gen16.contains (0 : Nat) && FRC.Interactions.y6 (0 : Nat) == (0 : Int) && FRC.Interactions.q6 (0 : Nat) == (0 : Int) && FRC.Interactions.col (0 : Nat) == (0 : Nat) && FRC.Interactions.wk (0 : Nat) == (0 : Nat)) = true :=
  @FRC.Ledger.p27018
/-- 27:C7 (p27019) — The strong sector: the colour $\SU(3,\Omega)$ frame forced as the minimal triality-carrying rank, the exact $\Z_3$ centre, the gluon connection, and the confinement area law $\sigma>0$ from positivity, with the string tension $\sigma(\beta)=-\ln c_1(\beta)$ computed in finite units (closed form on $2T$; $c_1^{\SU(3)}=\tfrac\beta{18}+\tfrac{\beta^2}{216}+\cdots$). -/
theorem p27019 : (([FRC.Interactions.F4.o, FRC.Interactions.F4.w, FRC.Interactions.F4.w2].all fun x => x * x.conj == FRC.Interactions.F4.o && x * x * x == FRC.Interactions.F4.o) = true ∧ (FRC.Interactions.F4.z * FRC.Interactions.F4.z.conj == FRC.Interactions.F4.o) = false ∧ [FRC.Interactions.F4.o, FRC.Interactions.F4.w, FRC.Interactions.F4.w2].length = (3 : Nat) ∧ (2 : Nat) + (1 : Nat) = (3 : Nat) ∧ ([FRC.Interactions.F4.o, FRC.Interactions.F4.w, FRC.Interactions.F4.w2].all fun x => FRC.Interactions.F4.mm x.scal [FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.z] == FRC.Interactions.F4.mm [FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.z] x.scal && FRC.Interactions.F4.mm x.scal [FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.w, FRC.Interactions.F4.z, FRC.Interactions.F4.w2, FRC.Interactions.F4.z, FRC.Interactions.F4.z] == FRC.Interactions.F4.mm [FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.w, FRC.Interactions.F4.z, FRC.Interactions.F4.w2, FRC.Interactions.F4.z, FRC.Interactions.F4.z] x.scal) = true) ∧ (have U₁ := [FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.z]; have U₂ := [FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.w, FRC.Interactions.F4.z, FRC.Interactions.F4.w2, FRC.Interactions.F4.z, FRC.Interactions.F4.z]; have D₁ := [FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.w, FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.w2]; have D₂ := [FRC.Interactions.F4.w, FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.w2]; FRC.Interactions.F4.mm (FRC.Interactions.F4.dg U₁) U₁ = FRC.Interactions.F4.one ∧ FRC.Interactions.F4.mm (FRC.Interactions.F4.dg U₂) U₂ = FRC.Interactions.F4.one ∧ FRC.Interactions.F4.det U₁ = FRC.Interactions.F4.o ∧ FRC.Interactions.F4.det U₂ = FRC.Interactions.F4.o ∧ FRC.Interactions.F4.mm U₁ U₂ ≠ FRC.Interactions.F4.mm U₂ U₁ ∧ FRC.Interactions.F4.mm (FRC.Interactions.F4.mm U₁ U₂) (FRC.Interactions.F4.mm (FRC.Interactions.F4.dg U₁) (FRC.Interactions.F4.dg U₂)) = [FRC.Interactions.F4.w2, FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.w] ∧ FRC.Interactions.F4.mm (FRC.Interactions.F4.mm U₁ U₂) (FRC.Interactions.F4.mm (FRC.Interactions.F4.dg U₁) (FRC.Interactions.F4.dg U₂)) ≠ FRC.Interactions.F4.one ∧ FRC.Interactions.F4.mm (FRC.Interactions.F4.mm D₁ D₂) (FRC.Interactions.F4.mm (FRC.Interactions.F4.dg D₁) (FRC.Interactions.F4.dg D₂)) = FRC.Interactions.F4.one) ∧ ∀ (n : Nat), n % (12 : Nat) = (5 : Nat) → (n + (1 : Nat)) % (2 : Nat) = (0 : Nat) ∧ (n + (1 : Nat)) % (3 : Nat) = (0 : Nat) ∧ (n + (1 : Nat)) % (4 : Nat) = (2 : Nat) :=
  @FRC.Ledger.p27019
/-- 27:C8 (p27020) — One complete Standard-Model generation as the spinor $\mathbf{16}$ of the rank-five frame: field content, hypercharges, charges, and full anomaly freedom; the imported $\SO(10)$ template (A4) evaluated on the realisation B5. -/
theorem p27020 : (List.filter (fun S => FRC.Interactions.col S == (0 : Nat) && FRC.Interactions.wk S == (0 : Nat) && FRC.Interactions.y6 S == (0 : Int)) FRC.Interactions.gen16).length = (1 : Nat) ∧ (List.filter (fun S => FRC.Interactions.col S == (2 : Nat) && FRC.Interactions.wk S == (0 : Nat) && FRC.Interactions.y6 S == (-4 : Int)) FRC.Interactions.gen16).length = (3 : Nat) ∧ (List.filter (fun S => FRC.Interactions.col S == (1 : Nat) && FRC.Interactions.wk S == (1 : Nat) && FRC.Interactions.y6 S == (1 : Int)) FRC.Interactions.gen16).length = (6 : 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) ∧ (List.filter (fun S => FRC.Interactions.col S == (3 : Nat) && FRC.Interactions.wk S == (1 : Nat) && FRC.Interactions.y6 S == (-3 : Int)) FRC.Interactions.gen16).length = (2 : Nat) ∧ (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.map FRC.Interactions.q6 FRC.Interactions.gen16 = [(0 : Int), (-4 : Int), (-4 : Int), (-4 : Int), (4 : Int), (4 : Int), (4 : Int), (0 : Int), (-2 : Int), (-2 : Int), (-2 : Int), (-6 : Int), (6 : Int), (2 : Int), (2 : Int), (2 : Int)] ∧ FRC.Interactions.isum (List.map FRC.Interactions.y6 FRC.Interactions.gen16) = (0 : Int) ∧ FRC.Interactions.isum (List.map (fun S => FRC.Interactions.y6 S ^ (3 : Nat)) FRC.Interactions.gen16) = (0 : Int) ∧ FRC.Interactions.isum (List.map FRC.Interactions.y6 (List.filter (fun S => FRC.Interactions.col S == (1 : Nat) || FRC.Interactions.col S == (2 : Nat)) FRC.Interactions.gen16)) = (0 : Int) ∧ FRC.Interactions.isum (List.map FRC.Interactions.y6 (List.filter (fun S => FRC.Interactions.wk S == (1 : Nat)) FRC.Interactions.gen16)) = (0 : Int) ∧ (List.filter (fun S => FRC.Interactions.col S == (1 : Nat)) FRC.Interactions.gen16).length = (List.filter (fun S => FRC.Interactions.col S == (2 : Nat)) FRC.Interactions.gen16).length ∧ (List.filter (fun S => FRC.Interactions.wk S == (1 : Nat)) FRC.Interactions.gen16).length % (4 : Nat) = (0 : Nat) ∧ (FRC.Interactions.gen16.contains (0 : Nat) && FRC.Interactions.y6 (0 : Nat) == (0 : Int) && FRC.Interactions.q6 (0 : Nat) == (0 : Int) && FRC.Interactions.col (0 : Nat) == (0 : Nat) && FRC.Interactions.wk (0 : Nat) == (0 : Nat)) = true :=
  @FRC.Ledger.p27020
/-- 27:C9 (p27021) — Simple $\SO(10)$ unification forced: the colour--isospin off-block reframings are gauge automorphisms, and the torsion that distinguishes the blocks needs more coherent steps than any horizon count admits ($3s<\Omega+1$ for $s^2\le\Omega$); the horizon itself is the master's (00:Z2--Z4). -/
theorem p27021 : ((24 : Nat) - ((8 : Nat) + (3 : Nat) + (1 : Nat)) = (12 : Nat) ∧ (12 : Nat) = (2 : Nat) * ((3 : Nat) * (2 : Nat)) ∧ (1 : Nat) + (5 : Nat) + (10 : Nat) = (16 : Nat) ∧ (10 : Nat) * (9 : Nat) = (2 : Nat) * (45 : Nat)) ∧ (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) ∧ ((FRC.Interactions.offblock.all fun cw => (List.range (32 : Nat)).all fun S => (List.range (32 : Nat)).all fun T => have a := FRC.Interactions.emul S T; have b := FRC.Interactions.emul (FRC.Interactions.act cw.fst cw.snd S) (FRC.Interactions.act cw.fst cw.snd T); b.fst * b.fst == a.fst * a.fst && (a.fst == (0 : Int) || b.snd == FRC.Interactions.act cw.fst cw.snd a.snd)) = true ∧ (FRC.Interactions.offblock.all fun cw => ((List.range (32 : Nat)).all fun S => (List.range (32 : Nat)).all fun T => decide ((FRC.Interactions.act cw.fst cw.snd S == FRC.Interactions.act cw.fst cw.snd T) = true → (S == T) = true)) && (List.range (32 : Nat)).all fun S => decide (FRC.Interactions.act cw.fst cw.snd S < (32 : Nat))) = true) ∧ ∀ (Ω s : Nat), (7 : Nat) ≤ Ω → s * s ≤ Ω → (3 : Nat) * s < Ω + (1 : Nat) :=
  @FRC.Ledger.p27021
/-- 27:C10 (p27022) — The closure of the four primitive roles ($5\!\to\!1$): four interactions and no fifth, three generations and no fourth, the boson/fermion split, and the generation ordering, given the role-to-matter realisation (B6). -/
theorem p27022 : ∀ {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))) :=
  @FRC.Ledger.p27022
/-- 27:C11 (p27023) — The admissible substrate residue $\Omega\equiv5\!\pmod{12}$ forced by self-consistency. -/
theorem p27023 : (∀ (n : Nat), n % (12 : Nat) = (5 : Nat) ↔ n % (4 : Nat) = (1 : Nat) ∧ n % (3 : Nat) = (2 : Nat)) ∧ ([(5 : Nat), (17 : Nat), (29 : Nat), (41 : Nat), (53 : Nat), (89 : Nat), (101 : Nat), (113 : Nat), (2408561 : Nat)].all fun n => n % (12 : Nat) == (5 : Nat) && n % (4 : Nat) == (1 : Nat) && n % (3 : Nat) == (2 : Nat)) = true ∧ ([(13 : Nat), (61 : Nat), (157 : Nat), (421 : Nat)].all fun n => n % (12 : Nat) == (1 : Nat) && n % (4 : Nat) == (1 : Nat) && n % (3 : Nat) == (1 : Nat)) = true :=
  @FRC.Ledger.p27023
/-- 27:X1 (p27024) — \textbf{The gauge group} $\U(1)\times\SU(2)\times\SU(3)$ is the gauging of the substrate's three frame data, the phase, spinor, and colour frames read by the one recipe, not a product of groups chosen to fit. -/
theorem p27024 : (∀ {p : Nat} [FRC.Pos p] (A B C D φ₀ φ₁ φ₂ φ₃ : FRC.Shell p), A + φ₁ + -φ₀ + (B + φ₂ + -φ₁) + -(C + φ₂ + -φ₃) + -(D + φ₃ + -φ₀) = A + B + -C + -D) ∧ (FRC.Interactions.m2 ((2 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (7 : FRC.Shell (13 : Nat))) ((7 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (2 : FRC.Shell (13 : Nat))) = ((1 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (1 : FRC.Shell (13 : Nat))) ∧ FRC.Interactions.m2 (FRC.Interactions.m2 ((2 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (7 : FRC.Shell (13 : Nat))) ((1 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (12 : FRC.Shell (13 : Nat)))) ((7 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (2 : FRC.Shell (13 : Nat))) = ((1 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (12 : FRC.Shell (13 : Nat))) ∧ FRC.Interactions.m2 (FRC.Interactions.m2 ((2 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (7 : FRC.Shell (13 : Nat))) ((0 : FRC.Shell (13 : Nat)), (1 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)))) ((7 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (2 : FRC.Shell (13 : Nat))) = ((0 : FRC.Shell (13 : Nat)), (4 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat))) ∧ FRC.Interactions.m2 (FRC.Interactions.m2 ((2 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (7 : FRC.Shell (13 : Nat))) ((0 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (1 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)))) ((7 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (2 : FRC.Shell (13 : Nat))) = ((0 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (10 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat))) ∧ (4 : FRC.Shell (13 : Nat)) * (10 : FRC.Shell (13 : Nat)) = (1 : FRC.Shell (13 : Nat)) ∧ (List.filter (fun n => have X := FRC.Interactions.m2of n; X.fst * X.snd.snd.snd + -(X.snd.fst * X.snd.snd.fst) == (1 : FRC.Shell (13 : Nat)) && FRC.Interactions.m2 X ((2 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (7 : FRC.Shell (13 : Nat))) == FRC.Interactions.m2 ((2 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (7 : FRC.Shell (13 : Nat))) X) (List.range ((13 : Nat) * (13 : Nat) * (13 : Nat) * (13 : Nat)))).length = (12 : Nat) ∧ FRC.Interactions.m2 ((3 : FRC.Shell (13 : Nat)), (4 : FRC.Shell (13 : Nat)), (2 : FRC.Shell (13 : Nat)), (3 : FRC.Shell (13 : Nat))) ((2 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (7 : FRC.Shell (13 : Nat))) ≠ FRC.Interactions.m2 ((2 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (0 : FRC.Shell (13 : Nat)), (7 : FRC.Shell (13 : Nat))) ((3 : FRC.Shell (13 : Nat)), (4 : FRC.Shell (13 : Nat)), (2 : FRC.Shell (13 : Nat)), (3 : FRC.Shell (13 : Nat)))) ∧ have U₁ := [FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.z]; have U₂ := [FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.w, FRC.Interactions.F4.z, FRC.Interactions.F4.w2, FRC.Interactions.F4.z, FRC.Interactions.F4.z]; have D₁ := [FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.w, FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.w2]; have D₂ := [FRC.Interactions.F4.w, FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.w2]; FRC.Interactions.F4.mm (FRC.Interactions.F4.dg U₁) U₁ = FRC.Interactions.F4.one ∧ FRC.Interactions.F4.mm (FRC.Interactions.F4.dg U₂) U₂ = FRC.Interactions.F4.one ∧ FRC.Interactions.F4.det U₁ = FRC.Interactions.F4.o ∧ FRC.Interactions.F4.det U₂ = FRC.Interactions.F4.o ∧ FRC.Interactions.F4.mm U₁ U₂ ≠ FRC.Interactions.F4.mm U₂ U₁ ∧ FRC.Interactions.F4.mm (FRC.Interactions.F4.mm U₁ U₂) (FRC.Interactions.F4.mm (FRC.Interactions.F4.dg U₁) (FRC.Interactions.F4.dg U₂)) = [FRC.Interactions.F4.w2, FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.w] ∧ FRC.Interactions.F4.mm (FRC.Interactions.F4.mm U₁ U₂) (FRC.Interactions.F4.mm (FRC.Interactions.F4.dg U₁) (FRC.Interactions.F4.dg U₂)) ≠ FRC.Interactions.F4.one ∧ FRC.Interactions.F4.mm (FRC.Interactions.F4.mm D₁ D₂) (FRC.Interactions.F4.mm (FRC.Interactions.F4.dg D₁) (FRC.Interactions.F4.dg D₂)) = FRC.Interactions.F4.one :=
  @FRC.Ledger.p27024
/-- 27:X2 (p27025) — \textbf{Charge quantisation} is automatic: electric charge is an integer winding index, so the electron and proton charges match exactly and no fractional residue survives, with no quantisation condition imposed. -/
theorem p27025 : (∀ {p : Nat} [FRC.Pos p] (A₁ A₂ B₃ A₄ A₅ B₀ B₁ : FRC.Shell p), A₁ + A₂ + B₃ + -A₄ + -A₅ + -B₀ = A₁ + B₁ + -A₅ + -B₀ + (A₂ + B₃ + -A₄ + -B₁)) ∧ (List.filter (fun S => FRC.Interactions.col S == (0 : Nat) && FRC.Interactions.wk S == (0 : Nat) && FRC.Interactions.y6 S == (0 : Int)) FRC.Interactions.gen16).length = (1 : Nat) ∧ (List.filter (fun S => FRC.Interactions.col S == (2 : Nat) && FRC.Interactions.wk S == (0 : Nat) && FRC.Interactions.y6 S == (-4 : Int)) FRC.Interactions.gen16).length = (3 : Nat) ∧ (List.filter (fun S => FRC.Interactions.col S == (1 : Nat) && FRC.Interactions.wk S == (1 : Nat) && FRC.Interactions.y6 S == (1 : Int)) FRC.Interactions.gen16).length = (6 : 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) ∧ (List.filter (fun S => FRC.Interactions.col S == (3 : Nat) && FRC.Interactions.wk S == (1 : Nat) && FRC.Interactions.y6 S == (-3 : Int)) FRC.Interactions.gen16).length = (2 : Nat) ∧ (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.map FRC.Interactions.q6 FRC.Interactions.gen16 = [(0 : Int), (-4 : Int), (-4 : Int), (-4 : Int), (4 : Int), (4 : Int), (4 : Int), (0 : Int), (-2 : Int), (-2 : Int), (-2 : Int), (-6 : Int), (6 : Int), (2 : Int), (2 : Int), (2 : Int)] ∧ FRC.Interactions.isum (List.map FRC.Interactions.y6 FRC.Interactions.gen16) = (0 : Int) ∧ FRC.Interactions.isum (List.map (fun S => FRC.Interactions.y6 S ^ (3 : Nat)) FRC.Interactions.gen16) = (0 : Int) ∧ FRC.Interactions.isum (List.map FRC.Interactions.y6 (List.filter (fun S => FRC.Interactions.col S == (1 : Nat) || FRC.Interactions.col S == (2 : Nat)) FRC.Interactions.gen16)) = (0 : Int) ∧ FRC.Interactions.isum (List.map FRC.Interactions.y6 (List.filter (fun S => FRC.Interactions.wk S == (1 : Nat)) FRC.Interactions.gen16)) = (0 : Int) ∧ (List.filter (fun S => FRC.Interactions.col S == (1 : Nat)) FRC.Interactions.gen16).length = (List.filter (fun S => FRC.Interactions.col S == (2 : Nat)) FRC.Interactions.gen16).length ∧ (List.filter (fun S => FRC.Interactions.wk S == (1 : Nat)) FRC.Interactions.gen16).length % (4 : Nat) = (0 : Nat) ∧ (FRC.Interactions.gen16.contains (0 : Nat) && FRC.Interactions.y6 (0 : Nat) == (0 : Int) && FRC.Interactions.q6 (0 : Nat) == (0 : Int) && FRC.Interactions.col (0 : Nat) == (0 : Nat) && FRC.Interactions.wk (0 : Nat) == (0 : Nat)) = true :=
  @FRC.Ledger.p27025
/-- 27:X3 (p27026) — \textbf{The photon and its dynamics} are forced: masslessness is drive-invariance and the exact rank-one kernel of the broken vacuum, and Maxwell is the unique adjacency-local gauge-invariant quadratic operator, neither put in by hand. -/
theorem p27026 : (∀ {p : Nat} [FRC.Pos p] (g g' v : FRC.Shell p), g * g * (v * v) * (g' * g' * (v * v)) + -(-(g * g' * (v * v)) * -(g * g' * (v * v))) = (0 : FRC.Shell p) ∧ g * g * (v * v) * g' + -(g * g' * (v * v)) * g = (0 : FRC.Shell p) ∧ -(g * g' * (v * v)) * g' + g' * g' * (v * v) * g = (0 : FRC.Shell p) ∧ g * g * (v * v) * g + -(g * g' * (v * v)) * -g' = (g * g + g' * g') * (v * v) * g ∧ -(g * g' * (v * v)) * g + g' * g' * (v * v) * -g' = (g * g + g' * g') * (v * v) * -g') ∧ (∀ {p : Nat} [FRC.Pos p] (a b c : FRC.Shell p), (a + b) * (1 : FRC.Shell p) + c = (0 : FRC.Shell p) → (a + b) * ((1 : FRC.Shell p) + (1 : FRC.Shell p)) + c = (0 : FRC.Shell p) → a + b = (0 : FRC.Shell p) ∧ c = (0 : FRC.Shell p)) ∧ FRC.Interactions.constraintRows.length = (1023 : Nat) ∧ FRC.Interactions.admissibleA.length = (123 : Nat) ∧ FRC.Interactions.admissibleB.length = (123 : Nat) ∧ FRC.Interactions.maxwellForm.length = (123 : Nat) ∧ (FRC.Interactions.constraintRows.all fun r => FRC.Interactions.rowDot r FRC.Interactions.admissibleA == (0 : Int)) = true ∧ (FRC.Interactions.constraintRows.all fun r => FRC.Interactions.rowDot r FRC.Interactions.admissibleB == (0 : Int)) = true ∧ (FRC.Interactions.constraintRows.all fun r => FRC.Interactions.rowDot r FRC.Interactions.maxwellForm == (0 : Int)) = true ∧ List.map (fun c => (2 : Int) * c) FRC.Interactions.maxwellForm = List.zipWith (fun b a => b - a) FRC.Interactions.admissibleB FRC.Interactions.admissibleA ∧ FRC.Interactions.admissibleA ≠ FRC.Interactions.admissibleB :=
  @FRC.Ledger.p27026
/-- 27:X4 (p27027) — \textbf{The Weinberg angle} is the exact rational $\sin^2\sW=3/8$ at the unification point, fixed by the charge spectrum of the realised generation (B5) with the group-theoretic step imported (A4), not a free parameter measured into the theory. -/
theorem p27027 : FRC.Interactions.isum (List.map (fun S => (3 : Int) * FRC.Interactions.t3h S * ((3 : Int) * FRC.Interactions.t3h S)) FRC.Interactions.gen16) = (72 : Int) ∧ FRC.Interactions.isum (List.map (fun S => FRC.Interactions.q6 S * FRC.Interactions.q6 S) FRC.Interactions.gen16) = (192 : Int) ∧ (72 : Nat) * (8 : Nat) = (192 : Nat) * (3 : Nat) :=
  @FRC.Ledger.p27027
/-- 27:X5 (p27028) — \textbf{The custodial relation} $\rho=1$ is the rank-one identity $\det\equiv0$ forced by the spinor-doublet Higgs, not a tree-level accident. -/
theorem p27028 : (∀ {p : Nat} [FRC.Pos p] (g g' v : FRC.Shell p), g * g * (v * v) * (g' * g' * (v * v)) + -(-(g * g' * (v * v)) * -(g * g' * (v * v))) = (0 : FRC.Shell p) ∧ g * g * (v * v) * g' + -(g * g' * (v * v)) * g = (0 : FRC.Shell p) ∧ -(g * g' * (v * v)) * g' + g' * g' * (v * v) * g = (0 : FRC.Shell p) ∧ g * g * (v * v) * g + -(g * g' * (v * v)) * -g' = (g * g + g' * g') * (v * v) * g ∧ -(g * g' * (v * v)) * g + g' * g' * (v * v) * -g' = (g * g + g' * g') * (v * v) * -g') ∧ ((List.range (4 : Nat)).all fun a => FRC.Interactions.hess (5 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (7 : FRC.Shell (13 : Nat)) a (2 : Nat) * (2 : FRC.Shell (13 : Nat)) + FRC.Interactions.hess (5 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (7 : FRC.Shell (13 : Nat)) a (3 : Nat) * (1 : FRC.Shell (13 : Nat)) == (0 : FRC.Shell (13 : Nat))) = true ∧ FRC.Interactions.hess (5 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (7 : FRC.Shell (13 : Nat)) (2 : Nat) (2 : Nat) * FRC.Interactions.hess (5 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (7 : FRC.Shell (13 : Nat)) (3 : Nat) (3 : Nat) + -(FRC.Interactions.hess (5 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (7 : FRC.Shell (13 : Nat)) (2 : Nat) (3 : Nat) * FRC.Interactions.hess (5 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (7 : FRC.Shell (13 : Nat)) (3 : Nat) (2 : Nat)) = (0 : FRC.Shell (13 : Nat)) ∧ FRC.Interactions.hess (5 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (7 : FRC.Shell (13 : Nat)) (0 : Nat) (0 : Nat) = FRC.Interactions.hess (5 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (7 : FRC.Shell (13 : Nat)) (1 : Nat) (1 : Nat) ∧ FRC.Interactions.hess (5 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (7 : FRC.Shell (13 : Nat)) (2 : Nat) (2 : Nat) + FRC.Interactions.hess (5 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (7 : FRC.Shell (13 : Nat)) (3 : Nat) (3 : Nat) = ((1 : FRC.Shell (13 : Nat)) * (1 : FRC.Shell (13 : Nat)) + (2 : FRC.Shell (13 : Nat)) * (2 : FRC.Shell (13 : Nat))) * ((2 : FRC.Shell (13 : Nat)) * (2 : FRC.Shell (13 : Nat))) * ((7 : FRC.Shell (13 : Nat)) * (7 : FRC.Shell (13 : Nat))) ∧ FRC.Interactions.hess (5 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (7 : FRC.Shell (13 : Nat)) (0 : Nat) (0 : Nat) * ((1 : FRC.Shell (13 : Nat)) * (1 : FRC.Shell (13 : Nat)) + (2 : FRC.Shell (13 : Nat)) * (2 : FRC.Shell (13 : Nat))) = (FRC.Interactions.hess (5 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (7 : FRC.Shell (13 : Nat)) (2 : Nat) (2 : Nat) + FRC.Interactions.hess (5 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) (7 : FRC.Shell (13 : Nat)) (3 : Nat) (3 : Nat)) * ((1 : FRC.Shell (13 : Nat)) * (1 : FRC.Shell (13 : Nat))) ∧ (5 : FRC.Shell (13 : Nat)) * (5 : FRC.Shell (13 : Nat)) = (-1 : FRC.Shell (13 : Nat)) ∧ (7 : FRC.Shell (13 : Nat)) + (7 : FRC.Shell (13 : Nat)) = (1 : FRC.Shell (13 : Nat)) ∧ ((List.range (4 : Nat)).all fun a => FRC.Interactions.hess (2 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (2 : FRC.Shell (5 : Nat)) (3 : FRC.Shell (5 : Nat)) a (2 : Nat) * (1 : FRC.Shell (5 : Nat)) + FRC.Interactions.hess (2 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (2 : FRC.Shell (5 : Nat)) (3 : FRC.Shell (5 : Nat)) a (3 : Nat) * (1 : FRC.Shell (5 : Nat)) == (0 : FRC.Shell (5 : Nat))) = true ∧ FRC.Interactions.hess (2 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (2 : FRC.Shell (5 : Nat)) (3 : FRC.Shell (5 : Nat)) (2 : Nat) (2 : Nat) * FRC.Interactions.hess (2 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (2 : FRC.Shell (5 : Nat)) (3 : FRC.Shell (5 : Nat)) (3 : Nat) (3 : Nat) + -(FRC.Interactions.hess (2 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (2 : FRC.Shell (5 : Nat)) (3 : FRC.Shell (5 : Nat)) (2 : Nat) (3 : Nat) * FRC.Interactions.hess (2 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (2 : FRC.Shell (5 : Nat)) (3 : FRC.Shell (5 : Nat)) (3 : Nat) (2 : Nat)) = (0 : FRC.Shell (5 : Nat)) ∧ FRC.Interactions.hess (2 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (2 : FRC.Shell (5 : Nat)) (3 : FRC.Shell (5 : Nat)) (0 : Nat) (0 : Nat) = FRC.Interactions.hess (2 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (2 : FRC.Shell (5 : Nat)) (3 : FRC.Shell (5 : Nat)) (1 : Nat) (1 : Nat) ∧ FRC.Interactions.hess (2 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (2 : FRC.Shell (5 : Nat)) (3 : FRC.Shell (5 : Nat)) (2 : Nat) (2 : Nat) + FRC.Interactions.hess (2 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (2 : FRC.Shell (5 : Nat)) (3 : FRC.Shell (5 : Nat)) (3 : Nat) (3 : Nat) = ((1 : FRC.Shell (5 : Nat)) * (1 : FRC.Shell (5 : Nat)) + (1 : FRC.Shell (5 : Nat)) * (1 : FRC.Shell (5 : Nat))) * ((2 : FRC.Shell (5 : Nat)) * (2 : FRC.Shell (5 : Nat))) * ((3 : FRC.Shell (5 : Nat)) * (3 : FRC.Shell (5 : Nat))) ∧ FRC.Interactions.hess (2 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (2 : FRC.Shell (5 : Nat)) (3 : FRC.Shell (5 : Nat)) (0 : Nat) (0 : Nat) * ((1 : FRC.Shell (5 : Nat)) * (1 : FRC.Shell (5 : Nat)) + (1 : FRC.Shell (5 : Nat)) * (1 : FRC.Shell (5 : Nat))) = (FRC.Interactions.hess (2 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (2 : FRC.Shell (5 : Nat)) (3 : FRC.Shell (5 : Nat)) (2 : Nat) (2 : Nat) + FRC.Interactions.hess (2 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (1 : FRC.Shell (5 : Nat)) (2 : FRC.Shell (5 : Nat)) (3 : FRC.Shell (5 : Nat)) (3 : Nat) (3 : Nat)) * ((1 : FRC.Shell (5 : Nat)) * (1 : FRC.Shell (5 : Nat))) ∧ (2 : FRC.Shell (5 : Nat)) * (2 : FRC.Shell (5 : Nat)) = (-1 : FRC.Shell (5 : Nat)) ∧ (3 : FRC.Shell (5 : Nat)) + (3 : FRC.Shell (5 : Nat)) = (1 : FRC.Shell (5 : Nat)) :=
  @FRC.Ledger.p27028
/-- 27:X6 (p27029) — \textbf{Maximal parity violation} is the exact decoupling of the Frobenius branch from the drive, so the $V\!-\!A$ current is derived rather than the left-handed doublets assigned by hand. -/
theorem p27029 : (∀ {p : Nat} [FRC.Pos p], FRC.Nat.isPrime p → ∀ {u : FRC.Shell p} {N : Nat}, u ^ N = (1 : FRC.Shell p) → ∀ {δ : Nat}, u ^ ((2 : Nat) * δ) ≠ (1 : FRC.Shell p) → FRC.Shell.sumRange (fun τ => u ^ ((2 : Nat) * δ * τ)) N = (0 : FRC.Shell p) ∧ FRC.Shell.sumRange (fun x => (1 : FRC.Shell p)) N = FRC.Shell.ofNat N) ∧ ∀ {p : Nat} [FRC.Pos p], FRC.Nat.isPrime p → ∀ {u : FRC.Shell p} {N : Nat}, u ^ N = (1 : FRC.Shell p) → ∀ {δ : Nat}, δ ≤ N → u ^ ((2 : Nat) * δ) ≠ (1 : FRC.Shell p) → FRC.Shell.sumRange (fun τ => u ^ ((2 : Nat) * (N - δ) * τ)) N = (0 : FRC.Shell p) ∧ (1 : Int) ≠ (-1 : Int) ∧ (1 : Int) * (1 : Int) > (0 : Int) ∧ (-1 : Int) * (-1 : Int) > (0 : Int) :=
  @FRC.Ledger.p27029
/-- 27:X7 (p27030) — \textbf{The colour sector} is fixed: three colours is the minimal triality-carrying frame, confinement is the compact-group area law from positivity, and asymptotic freedom is the gluon self-coupling, not $N_c=3$ supplemented by an assumed confining phase. -/
theorem p27030 : (([FRC.Interactions.F4.o, FRC.Interactions.F4.w, FRC.Interactions.F4.w2].all fun x => x * x.conj == FRC.Interactions.F4.o && x * x * x == FRC.Interactions.F4.o) = true ∧ (FRC.Interactions.F4.z * FRC.Interactions.F4.z.conj == FRC.Interactions.F4.o) = false ∧ [FRC.Interactions.F4.o, FRC.Interactions.F4.w, FRC.Interactions.F4.w2].length = (3 : Nat) ∧ (2 : Nat) + (1 : Nat) = (3 : Nat) ∧ ([FRC.Interactions.F4.o, FRC.Interactions.F4.w, FRC.Interactions.F4.w2].all fun x => FRC.Interactions.F4.mm x.scal [FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.z] == FRC.Interactions.F4.mm [FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.z] x.scal && FRC.Interactions.F4.mm x.scal [FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.w, FRC.Interactions.F4.z, FRC.Interactions.F4.w2, FRC.Interactions.F4.z, FRC.Interactions.F4.z] == FRC.Interactions.F4.mm [FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.w, FRC.Interactions.F4.z, FRC.Interactions.F4.w2, FRC.Interactions.F4.z, FRC.Interactions.F4.z] x.scal) = true) ∧ (have U₁ := [FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.z]; have U₂ := [FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.w, FRC.Interactions.F4.z, FRC.Interactions.F4.w2, FRC.Interactions.F4.z, FRC.Interactions.F4.z]; have D₁ := [FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.w, FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.w2]; have D₂ := [FRC.Interactions.F4.w, FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.w2]; FRC.Interactions.F4.mm (FRC.Interactions.F4.dg U₁) U₁ = FRC.Interactions.F4.one ∧ FRC.Interactions.F4.mm (FRC.Interactions.F4.dg U₂) U₂ = FRC.Interactions.F4.one ∧ FRC.Interactions.F4.det U₁ = FRC.Interactions.F4.o ∧ FRC.Interactions.F4.det U₂ = FRC.Interactions.F4.o ∧ FRC.Interactions.F4.mm U₁ U₂ ≠ FRC.Interactions.F4.mm U₂ U₁ ∧ FRC.Interactions.F4.mm (FRC.Interactions.F4.mm U₁ U₂) (FRC.Interactions.F4.mm (FRC.Interactions.F4.dg U₁) (FRC.Interactions.F4.dg U₂)) = [FRC.Interactions.F4.w2, FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.o, FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.z, FRC.Interactions.F4.w] ∧ FRC.Interactions.F4.mm (FRC.Interactions.F4.mm U₁ U₂) (FRC.Interactions.F4.mm (FRC.Interactions.F4.dg U₁) (FRC.Interactions.F4.dg U₂)) ≠ FRC.Interactions.F4.one ∧ FRC.Interactions.F4.mm (FRC.Interactions.F4.mm D₁ D₂) (FRC.Interactions.F4.mm (FRC.Interactions.F4.dg D₁) (FRC.Interactions.F4.dg D₂)) = FRC.Interactions.F4.one) ∧ ∀ (n : Nat), n % (12 : Nat) = (5 : Nat) → (n + (1 : Nat)) % (2 : Nat) = (0 : Nat) ∧ (n + (1 : Nat)) % (3 : Nat) = (0 : Nat) ∧ (n + (1 : Nat)) % (4 : Nat) = (2 : Nat) :=
  @FRC.Ledger.p27030
/-- 27:X8 (p27031) — \textbf{One complete generation} is the spinor $\mathbf{16}$ of the rank-five internal frame, so its hypercharges, charges, and anomaly freedom follow and a right-handed neutrino is present, with $\SO(10)$ unification forced, rather than a hypercharge assignment whose anomaly cancellation is a coincidence; given B5, the anomaly cancellation is the imported $\SO(10)$ fact (A4) evaluated on the realised content. -/
theorem p27031 : ((List.filter (fun S => FRC.Interactions.col S == (0 : Nat) && FRC.Interactions.wk S == (0 : Nat) && FRC.Interactions.y6 S == (0 : Int)) FRC.Interactions.gen16).length = (1 : Nat) ∧ (List.filter (fun S => FRC.Interactions.col S == (2 : Nat) && FRC.Interactions.wk S == (0 : Nat) && FRC.Interactions.y6 S == (-4 : Int)) FRC.Interactions.gen16).length = (3 : Nat) ∧ (List.filter (fun S => FRC.Interactions.col S == (1 : Nat) && FRC.Interactions.wk S == (1 : Nat) && FRC.Interactions.y6 S == (1 : Int)) FRC.Interactions.gen16).length = (6 : 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) ∧ (List.filter (fun S => FRC.Interactions.col S == (3 : Nat) && FRC.Interactions.wk S == (1 : Nat) && FRC.Interactions.y6 S == (-3 : Int)) FRC.Interactions.gen16).length = (2 : Nat) ∧ (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.map FRC.Interactions.q6 FRC.Interactions.gen16 = [(0 : Int), (-4 : Int), (-4 : Int), (-4 : Int), (4 : Int), (4 : Int), (4 : Int), (0 : Int), (-2 : Int), (-2 : Int), (-2 : Int), (-6 : Int), (6 : Int), (2 : Int), (2 : Int), (2 : Int)] ∧ FRC.Interactions.isum (List.map FRC.Interactions.y6 FRC.Interactions.gen16) = (0 : Int) ∧ FRC.Interactions.isum (List.map (fun S => FRC.Interactions.y6 S ^ (3 : Nat)) FRC.Interactions.gen16) = (0 : Int) ∧ FRC.Interactions.isum (List.map FRC.Interactions.y6 (List.filter (fun S => FRC.Interactions.col S == (1 : Nat) || FRC.Interactions.col S == (2 : Nat)) FRC.Interactions.gen16)) = (0 : Int) ∧ FRC.Interactions.isum (List.map FRC.Interactions.y6 (List.filter (fun S => FRC.Interactions.wk S == (1 : Nat)) FRC.Interactions.gen16)) = (0 : Int) ∧ (List.filter (fun S => FRC.Interactions.col S == (1 : Nat)) FRC.Interactions.gen16).length = (List.filter (fun S => FRC.Interactions.col S == (2 : Nat)) FRC.Interactions.gen16).length ∧ (List.filter (fun S => FRC.Interactions.wk S == (1 : Nat)) FRC.Interactions.gen16).length % (4 : Nat) = (0 : Nat) ∧ (FRC.Interactions.gen16.contains (0 : Nat) && FRC.Interactions.y6 (0 : Nat) == (0 : Int) && FRC.Interactions.q6 (0 : Nat) == (0 : Int) && FRC.Interactions.col (0 : Nat) == (0 : Nat) && FRC.Interactions.wk (0 : Nat) == (0 : Nat)) = true) ∧ ((FRC.Interactions.offblock.all fun cw => (List.range (32 : Nat)).all fun S => (List.range (32 : Nat)).all fun T => have a := FRC.Interactions.emul S T; have b := FRC.Interactions.emul (FRC.Interactions.act cw.fst cw.snd S) (FRC.Interactions.act cw.fst cw.snd T); b.fst * b.fst == a.fst * a.fst && (a.fst == (0 : Int) || b.snd == FRC.Interactions.act cw.fst cw.snd a.snd)) = true ∧ (FRC.Interactions.offblock.all fun cw => ((List.range (32 : Nat)).all fun S => (List.range (32 : Nat)).all fun T => decide ((FRC.Interactions.act cw.fst cw.snd S == FRC.Interactions.act cw.fst cw.snd T) = true → (S == T) = true)) && (List.range (32 : Nat)).all fun S => decide (FRC.Interactions.act cw.fst cw.snd S < (32 : Nat))) = true) ∧ ∀ (Ω s : Nat), (7 : Nat) ≤ Ω → s * s ≤ Ω → (3 : Nat) * s < Ω + (1 : Nat) :=
  @FRC.Ledger.p27031
/-- 27:X9 (p27032) — \textbf{The interaction and generation counts} are the $1+3$ split of the closed primitive-role ladder, so four forces and three families are fixed and a fifth force and a fourth generation are forbidden, not left unexplained. -/
theorem p27032 : ∀ {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))) :=
  @FRC.Ledger.p27032
/-- 27:X10 (p27033) — \textbf{The Koide ratio} is exactly $2/3$, the cube-root generation orbit at the self-dual quarter-turn $\rho^2=2^{-1}$, an exact value rather than an unexplained numerical coincidence. -/
theorem p27033 : (∀ {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) :=
  @FRC.Ledger.p27033
/-- 27:X11 (p27034) — \textbf{The strong-CP angle} vanishes with no axion: the Wilson action class carries no orientation-odd term (B2), and Hermitian quark masses have real determinant, so $\bar\theta=0$ arises nowhere rather than being tuned away. -/
theorem p27034 : (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (U : FRC.Unitary.M3 p ν), FRC.Unitary.SU FRC.Unitary.mone U → FRC.Unitary.tr (FRC.Unitary.adj U) = (FRC.Unitary.tr U).conj ∧ FRC.Unitary.tr (FRC.Unitary.adj U) + (FRC.Unitary.tr (FRC.Unitary.adj U)).conj = FRC.Unitary.tr U + (FRC.Unitary.tr U).conj) ∧ (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (A : FRC.Unitary.M3 p ν), FRC.Unitary.dag A = A → (FRC.Unitary.det A).conj = FRC.Unitary.det A) ∧ (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (A : FRC.Unitary.M3 p ν), FRC.Unitary.dag A = A → (FRC.Unitary.det A).im + (FRC.Unitary.det A).im = (0 : FRC.Shell p)) ∧ FRC.Unitary.ents (FRC.Unitary.dag FRC.Interactions.mu17) = FRC.Unitary.ents FRC.Interactions.mu17 ∧ FRC.Unitary.ents (FRC.Unitary.dag FRC.Interactions.md17) = FRC.Unitary.ents FRC.Interactions.md17 ∧ FRC.Unitary.ents (FRC.Unitary.dag FRC.Interactions.mc17) = FRC.Unitary.ents FRC.Interactions.mc17 ∧ (FRC.Unitary.det FRC.Interactions.mu17).im = (0 : FRC.Shell (17 : Nat)) ∧ (FRC.Unitary.det FRC.Interactions.md17).im = (0 : FRC.Shell (17 : Nat)) ∧ (FRC.Unitary.det FRC.Interactions.mc17).im = (0 : FRC.Shell (17 : Nat)) ∧ (FRC.Unitary.det (FRC.Unitary.mmul FRC.Interactions.mu17 FRC.Interactions.md17)).im = (0 : FRC.Shell (17 : Nat)) ∧ (FRC.Unitary.det FRC.Interactions.mu17).re ≠ (0 : FRC.Shell (17 : Nat)) ∧ (FRC.Unitary.det FRC.Interactions.md17).re ≠ (0 : FRC.Shell (17 : Nat)) ∧ (FRC.Unitary.det FRC.Interactions.mc17).re ≠ (0 : FRC.Shell (17 : Nat)) ∧ FRC.Unitary.ents (FRC.Unitary.mmul FRC.Interactions.mu17 FRC.Interactions.md17) ≠ FRC.Unitary.ents (FRC.Unitary.mmul FRC.Interactions.md17 FRC.Interactions.mu17) ∧ FRC.Unitary.ents (FRC.Unitary.dag FRC.Interactions.mu53) = FRC.Unitary.ents FRC.Interactions.mu53 ∧ FRC.Unitary.ents (FRC.Unitary.dag FRC.Interactions.md53) = FRC.Unitary.ents FRC.Interactions.md53 ∧ FRC.Unitary.ents (FRC.Unitary.dag FRC.Interactions.mc53) = FRC.Unitary.ents FRC.Interactions.mc53 ∧ (FRC.Unitary.det FRC.Interactions.mu53).im = (0 : FRC.Shell (53 : Nat)) ∧ (FRC.Unitary.det FRC.Interactions.md53).im = (0 : FRC.Shell (53 : Nat)) ∧ (FRC.Unitary.det FRC.Interactions.mc53).im = (0 : FRC.Shell (53 : Nat)) ∧ (FRC.Unitary.det (FRC.Unitary.mmul FRC.Interactions.mu53 FRC.Interactions.md53)).im = (0 : FRC.Shell (53 : Nat)) ∧ (FRC.Unitary.det FRC.Interactions.mu53).re ≠ (0 : FRC.Shell (53 : Nat)) ∧ (FRC.Unitary.det FRC.Interactions.md53).re ≠ (0 : FRC.Shell (53 : Nat)) ∧ (FRC.Unitary.det FRC.Interactions.mc53).re ≠ (0 : FRC.Shell (53 : Nat)) ∧ FRC.Unitary.ents (FRC.Unitary.mmul FRC.Interactions.mu53 FRC.Interactions.md53) ≠ FRC.Unitary.ents (FRC.Unitary.mmul FRC.Interactions.md53 FRC.Interactions.mu53) ∧ FRC.Interactions.nu17 + (3 : FRC.Shell (17 : Nat)) = (0 : FRC.Shell (17 : Nat)) ∧ FRC.Interactions.nu53 + (3 : FRC.Shell (53 : Nat)) = (0 : FRC.Shell (53 : Nat)) :=
  @FRC.Ledger.p27034
/-- 27:P1 (p27035) — \textbf{No fourth generation and no fifth interaction} \emph{[forced]}. The role ladder closes, the fifth step returns to counting, and the Carrier is the entire substrate, so a fourth chiral family and a fifth fundamental force are forbidden, not merely absent (Tier~4). \emph{Falsifier:} any fourth-generation fermion, or any new fundamental interaction. -/
theorem p27035 : ∀ {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))) :=
  @FRC.Ledger.p27035
/-- 27:P2 (p27036) — \textbf{A desert to the substrate scale} \emph{[forced]}. The gauge group is exactly $\SU(3)\times\SU(2)\times\U(1)$ until the substrate resolves the colour--isospin split; no new gauge boson, vector-like fermion, or extra scalar lies between the electroweak and substrate ($\sim10^{16}$--$10^{19}\,$GeV) scales. \emph{Falsifier:} a $Z'$, $W'$, leptoquark, second Higgs doublet, or compositeness signature at the LHC or a future collider. This is the sharpest divergence from supersymmetry, extra dimensions, and composite-Higgs scenarios. -/
theorem p27036 : (List.filter (fun S => FRC.Interactions.col S == (0 : Nat) && FRC.Interactions.wk S == (0 : Nat) && FRC.Interactions.y6 S == (0 : Int)) FRC.Interactions.gen16).length = (1 : Nat) ∧ (List.filter (fun S => FRC.Interactions.col S == (2 : Nat) && FRC.Interactions.wk S == (0 : Nat) && FRC.Interactions.y6 S == (-4 : Int)) FRC.Interactions.gen16).length = (3 : Nat) ∧ (List.filter (fun S => FRC.Interactions.col S == (1 : Nat) && FRC.Interactions.wk S == (1 : Nat) && FRC.Interactions.y6 S == (1 : Int)) FRC.Interactions.gen16).length = (6 : 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) ∧ (List.filter (fun S => FRC.Interactions.col S == (3 : Nat) && FRC.Interactions.wk S == (1 : Nat) && FRC.Interactions.y6 S == (-3 : Int)) FRC.Interactions.gen16).length = (2 : Nat) ∧ (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.map FRC.Interactions.q6 FRC.Interactions.gen16 = [(0 : Int), (-4 : Int), (-4 : Int), (-4 : Int), (4 : Int), (4 : Int), (4 : Int), (0 : Int), (-2 : Int), (-2 : Int), (-2 : Int), (-6 : Int), (6 : Int), (2 : Int), (2 : Int), (2 : Int)] ∧ FRC.Interactions.isum (List.map FRC.Interactions.y6 FRC.Interactions.gen16) = (0 : Int) ∧ FRC.Interactions.isum (List.map (fun S => FRC.Interactions.y6 S ^ (3 : Nat)) FRC.Interactions.gen16) = (0 : Int) ∧ FRC.Interactions.isum (List.map FRC.Interactions.y6 (List.filter (fun S => FRC.Interactions.col S == (1 : Nat) || FRC.Interactions.col S == (2 : Nat)) FRC.Interactions.gen16)) = (0 : Int) ∧ FRC.Interactions.isum (List.map FRC.Interactions.y6 (List.filter (fun S => FRC.Interactions.wk S == (1 : Nat)) FRC.Interactions.gen16)) = (0 : Int) ∧ (List.filter (fun S => FRC.Interactions.col S == (1 : Nat)) FRC.Interactions.gen16).length = (List.filter (fun S => FRC.Interactions.col S == (2 : Nat)) FRC.Interactions.gen16).length ∧ (List.filter (fun S => FRC.Interactions.wk S == (1 : Nat)) FRC.Interactions.gen16).length % (4 : Nat) = (0 : Nat) ∧ (FRC.Interactions.gen16.contains (0 : Nat) && FRC.Interactions.y6 (0 : Nat) == (0 : Int) && FRC.Interactions.q6 (0 : Nat) == (0 : Int) && FRC.Interactions.col (0 : Nat) == (0 : Nat) && FRC.Interactions.wk (0 : Nat) == (0 : Nat)) = true :=
  @FRC.Ledger.p27036
/-- 27:P3 (p27037) — \textbf{No TeV supersymmetry} \emph{[forced]}. The Standard-Model content alone runs the measured couplings to a meeting of the first two near $10^{13}\,$GeV, where the Weinberg angle is $3/8$ by the normalisation. The strong coupling misses by $13\%$. The content has no superpartner. Where the completion closes the miss is the $\Omega$-hard running (Z1). \emph{Falsifier:} superpartners. -/
theorem p27037 : (List.filter (fun S => FRC.Interactions.col S == (0 : Nat) && FRC.Interactions.wk S == (0 : Nat) && FRC.Interactions.y6 S == (0 : Int)) FRC.Interactions.gen16).length = (1 : Nat) ∧ (List.filter (fun S => FRC.Interactions.col S == (2 : Nat) && FRC.Interactions.wk S == (0 : Nat) && FRC.Interactions.y6 S == (-4 : Int)) FRC.Interactions.gen16).length = (3 : Nat) ∧ (List.filter (fun S => FRC.Interactions.col S == (1 : Nat) && FRC.Interactions.wk S == (1 : Nat) && FRC.Interactions.y6 S == (1 : Int)) FRC.Interactions.gen16).length = (6 : 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) ∧ (List.filter (fun S => FRC.Interactions.col S == (3 : Nat) && FRC.Interactions.wk S == (1 : Nat) && FRC.Interactions.y6 S == (-3 : Int)) FRC.Interactions.gen16).length = (2 : Nat) ∧ (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.map FRC.Interactions.q6 FRC.Interactions.gen16 = [(0 : Int), (-4 : Int), (-4 : Int), (-4 : Int), (4 : Int), (4 : Int), (4 : Int), (0 : Int), (-2 : Int), (-2 : Int), (-2 : Int), (-6 : Int), (6 : Int), (2 : Int), (2 : Int), (2 : Int)] ∧ FRC.Interactions.isum (List.map FRC.Interactions.y6 FRC.Interactions.gen16) = (0 : Int) ∧ FRC.Interactions.isum (List.map (fun S => FRC.Interactions.y6 S ^ (3 : Nat)) FRC.Interactions.gen16) = (0 : Int) ∧ FRC.Interactions.isum (List.map FRC.Interactions.y6 (List.filter (fun S => FRC.Interactions.col S == (1 : Nat) || FRC.Interactions.col S == (2 : Nat)) FRC.Interactions.gen16)) = (0 : Int) ∧ FRC.Interactions.isum (List.map FRC.Interactions.y6 (List.filter (fun S => FRC.Interactions.wk S == (1 : Nat)) FRC.Interactions.gen16)) = (0 : Int) ∧ (List.filter (fun S => FRC.Interactions.col S == (1 : Nat)) FRC.Interactions.gen16).length = (List.filter (fun S => FRC.Interactions.col S == (2 : Nat)) FRC.Interactions.gen16).length ∧ (List.filter (fun S => FRC.Interactions.wk S == (1 : Nat)) FRC.Interactions.gen16).length % (4 : Nat) = (0 : Nat) ∧ (FRC.Interactions.gen16.contains (0 : Nat) && FRC.Interactions.y6 (0 : Nat) == (0 : Int) && FRC.Interactions.q6 (0 : Nat) == (0 : Int) && FRC.Interactions.col (0 : Nat) == (0 : Nat) && FRC.Interactions.wk (0 : Nat) == (0 : Nat)) = true :=
  @FRC.Ledger.p27037
/-- 27:P4 (p27038) — \textbf{The proton is effectively stable} \emph{[forced]}. The $X,Y$ leptoquarks are the twelve colour--isospin off-block generators. With their mass at the substrate scale (the $\Omega$-hard scale of Z1) the lifetime exceeds $10^{45}$ years, orders beyond the reach of Hyper-Kamiokande. At $10^{16}\,$GeV it already exceeds the Super-Kamiokande bound. \emph{Falsifier:} an observed proton decay near $10^{34}$--$10^{35}$ years. -/
theorem p27038 : (24 : Nat) - ((8 : Nat) + (3 : Nat) + (1 : Nat)) = (12 : Nat) ∧ (12 : Nat) = (2 : Nat) * ((3 : Nat) * (2 : Nat)) ∧ (1 : Nat) + (5 : Nat) + (10 : Nat) = (16 : Nat) ∧ (10 : Nat) * (9 : Nat) = (2 : Nat) * (45 : Nat) :=
  @FRC.Ledger.p27038
/-- 27:P5 (p27039) — \textbf{Majorana neutrinos, heavy singlets, no light sterile neutrino} \emph{[sector]}. Exactly one of the sixteen states is a full singlet, the right-handed neutrino. It admits a Majorana mass at the unification scale (A4), and the seesaw then places the light masses in the observed band for singlet masses of $10^{14}$--$10^{15}\,$GeV. \emph{Falsifier:} a confirmed eV-scale sterile neutrino, or Dirac neutrinos. -/
theorem p27039 : (List.filter (fun S => FRC.Interactions.col S == (0 : Nat) && FRC.Interactions.wk S == (0 : Nat) && FRC.Interactions.y6 S == (0 : Int)) FRC.Interactions.gen16).length = (1 : Nat) ∧ (List.filter (fun S => FRC.Interactions.col S == (2 : Nat) && FRC.Interactions.wk S == (0 : Nat) && FRC.Interactions.y6 S == (-4 : Int)) FRC.Interactions.gen16).length = (3 : Nat) ∧ (List.filter (fun S => FRC.Interactions.col S == (1 : Nat) && FRC.Interactions.wk S == (1 : Nat) && FRC.Interactions.y6 S == (1 : Int)) FRC.Interactions.gen16).length = (6 : 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) ∧ (List.filter (fun S => FRC.Interactions.col S == (3 : Nat) && FRC.Interactions.wk S == (1 : Nat) && FRC.Interactions.y6 S == (-3 : Int)) FRC.Interactions.gen16).length = (2 : Nat) ∧ (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.map FRC.Interactions.q6 FRC.Interactions.gen16 = [(0 : Int), (-4 : Int), (-4 : Int), (-4 : Int), (4 : Int), (4 : Int), (4 : Int), (0 : Int), (-2 : Int), (-2 : Int), (-2 : Int), (-6 : Int), (6 : Int), (2 : Int), (2 : Int), (2 : Int)] ∧ FRC.Interactions.isum (List.map FRC.Interactions.y6 FRC.Interactions.gen16) = (0 : Int) ∧ FRC.Interactions.isum (List.map (fun S => FRC.Interactions.y6 S ^ (3 : Nat)) FRC.Interactions.gen16) = (0 : Int) ∧ FRC.Interactions.isum (List.map FRC.Interactions.y6 (List.filter (fun S => FRC.Interactions.col S == (1 : Nat) || FRC.Interactions.col S == (2 : Nat)) FRC.Interactions.gen16)) = (0 : Int) ∧ FRC.Interactions.isum (List.map FRC.Interactions.y6 (List.filter (fun S => FRC.Interactions.wk S == (1 : Nat)) FRC.Interactions.gen16)) = (0 : Int) ∧ (List.filter (fun S => FRC.Interactions.col S == (1 : Nat)) FRC.Interactions.gen16).length = (List.filter (fun S => FRC.Interactions.col S == (2 : Nat)) FRC.Interactions.gen16).length ∧ (List.filter (fun S => FRC.Interactions.wk S == (1 : Nat)) FRC.Interactions.gen16).length % (4 : Nat) = (0 : Nat) ∧ (FRC.Interactions.gen16.contains (0 : Nat) && FRC.Interactions.y6 (0 : Nat) == (0 : Int) && FRC.Interactions.q6 (0 : Nat) == (0 : Int) && FRC.Interactions.col (0 : Nat) == (0 : Nat) && FRC.Interactions.wk (0 : Nat) == (0 : Nat)) = true :=
  @FRC.Ledger.p27039
/-- 27:P6 (p27040) — \textbf{No new particle of dark matter} \emph{[sector]}. The matter content is exactly one Standard-Model generation, triplicated, with heavy $\nu^c$; the construction contains no weakly-interacting massive particle and no axion. \emph{Falsifier:} a positive signal in a direct-detection (LZ, XENONnT) or axion (ADMX) experiment. Dark matter, if not a Standard-Model state, must then reside in the gravitational/substrate sector, a residual burden of the programme. -/
theorem p27040 : (List.filter (fun S => FRC.Interactions.col S == (0 : Nat) && FRC.Interactions.wk S == (0 : Nat) && FRC.Interactions.y6 S == (0 : Int)) FRC.Interactions.gen16).length = (1 : Nat) ∧ (List.filter (fun S => FRC.Interactions.col S == (2 : Nat) && FRC.Interactions.wk S == (0 : Nat) && FRC.Interactions.y6 S == (-4 : Int)) FRC.Interactions.gen16).length = (3 : Nat) ∧ (List.filter (fun S => FRC.Interactions.col S == (1 : Nat) && FRC.Interactions.wk S == (1 : Nat) && FRC.Interactions.y6 S == (1 : Int)) FRC.Interactions.gen16).length = (6 : 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) ∧ (List.filter (fun S => FRC.Interactions.col S == (3 : Nat) && FRC.Interactions.wk S == (1 : Nat) && FRC.Interactions.y6 S == (-3 : Int)) FRC.Interactions.gen16).length = (2 : Nat) ∧ (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.map FRC.Interactions.q6 FRC.Interactions.gen16 = [(0 : Int), (-4 : Int), (-4 : Int), (-4 : Int), (4 : Int), (4 : Int), (4 : Int), (0 : Int), (-2 : Int), (-2 : Int), (-2 : Int), (-6 : Int), (6 : Int), (2 : Int), (2 : Int), (2 : Int)] ∧ FRC.Interactions.isum (List.map FRC.Interactions.y6 FRC.Interactions.gen16) = (0 : Int) ∧ FRC.Interactions.isum (List.map (fun S => FRC.Interactions.y6 S ^ (3 : Nat)) FRC.Interactions.gen16) = (0 : Int) ∧ FRC.Interactions.isum (List.map FRC.Interactions.y6 (List.filter (fun S => FRC.Interactions.col S == (1 : Nat) || FRC.Interactions.col S == (2 : Nat)) FRC.Interactions.gen16)) = (0 : Int) ∧ FRC.Interactions.isum (List.map FRC.Interactions.y6 (List.filter (fun S => FRC.Interactions.wk S == (1 : Nat)) FRC.Interactions.gen16)) = (0 : Int) ∧ (List.filter (fun S => FRC.Interactions.col S == (1 : Nat)) FRC.Interactions.gen16).length = (List.filter (fun S => FRC.Interactions.col S == (2 : Nat)) FRC.Interactions.gen16).length ∧ (List.filter (fun S => FRC.Interactions.wk S == (1 : Nat)) FRC.Interactions.gen16).length % (4 : Nat) = (0 : Nat) ∧ (FRC.Interactions.gen16.contains (0 : Nat) && FRC.Interactions.y6 (0 : Nat) == (0 : Int) && FRC.Interactions.q6 (0 : Nat) == (0 : Int) && FRC.Interactions.col (0 : Nat) == (0 : Nat) && FRC.Interactions.wk (0 : Nat) == (0 : Nat)) = true :=
  @FRC.Ledger.p27040
/-- 27:P7 (p27041) — \textbf{No new-physics contribution to the muon anomaly} \emph{[sector]}. With no states beyond the Standard Model, $(g-2)_\mu$ must be accounted for by Standard-Model (notably hadronic) contributions. \emph{Falsifier:} a robustly established beyond-Standard-Model excess; the current lattice and experimental trend toward the Standard-Model value favours this prediction. -/
theorem p27041 : (List.filter (fun S => FRC.Interactions.col S == (0 : Nat) && FRC.Interactions.wk S == (0 : Nat) && FRC.Interactions.y6 S == (0 : Int)) FRC.Interactions.gen16).length = (1 : Nat) ∧ (List.filter (fun S => FRC.Interactions.col S == (2 : Nat) && FRC.Interactions.wk S == (0 : Nat) && FRC.Interactions.y6 S == (-4 : Int)) FRC.Interactions.gen16).length = (3 : Nat) ∧ (List.filter (fun S => FRC.Interactions.col S == (1 : Nat) && FRC.Interactions.wk S == (1 : Nat) && FRC.Interactions.y6 S == (1 : Int)) FRC.Interactions.gen16).length = (6 : 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) ∧ (List.filter (fun S => FRC.Interactions.col S == (3 : Nat) && FRC.Interactions.wk S == (1 : Nat) && FRC.Interactions.y6 S == (-3 : Int)) FRC.Interactions.gen16).length = (2 : Nat) ∧ (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.map FRC.Interactions.q6 FRC.Interactions.gen16 = [(0 : Int), (-4 : Int), (-4 : Int), (-4 : Int), (4 : Int), (4 : Int), (4 : Int), (0 : Int), (-2 : Int), (-2 : Int), (-2 : Int), (-6 : Int), (6 : Int), (2 : Int), (2 : Int), (2 : Int)] ∧ FRC.Interactions.isum (List.map FRC.Interactions.y6 FRC.Interactions.gen16) = (0 : Int) ∧ FRC.Interactions.isum (List.map (fun S => FRC.Interactions.y6 S ^ (3 : Nat)) FRC.Interactions.gen16) = (0 : Int) ∧ FRC.Interactions.isum (List.map FRC.Interactions.y6 (List.filter (fun S => FRC.Interactions.col S == (1 : Nat) || FRC.Interactions.col S == (2 : Nat)) FRC.Interactions.gen16)) = (0 : Int) ∧ FRC.Interactions.isum (List.map FRC.Interactions.y6 (List.filter (fun S => FRC.Interactions.wk S == (1 : Nat)) FRC.Interactions.gen16)) = (0 : Int) ∧ (List.filter (fun S => FRC.Interactions.col S == (1 : Nat)) FRC.Interactions.gen16).length = (List.filter (fun S => FRC.Interactions.col S == (2 : Nat)) FRC.Interactions.gen16).length ∧ (List.filter (fun S => FRC.Interactions.wk S == (1 : Nat)) FRC.Interactions.gen16).length % (4 : Nat) = (0 : Nat) ∧ (FRC.Interactions.gen16.contains (0 : Nat) && FRC.Interactions.y6 (0 : Nat) == (0 : Int) && FRC.Interactions.q6 (0 : Nat) == (0 : Int) && FRC.Interactions.col (0 : Nat) == (0 : Nat) && FRC.Interactions.wk (0 : Nat) == (0 : Nat)) = true :=
  @FRC.Ledger.p27041
/-- 27:P8 (p27042) — \textbf{The charged-lepton Koide relation is exactly $2/3$} \emph{[structural]}: $(m_e+m_\mu+m_\tau)/(\sqrt{m_e}+\sqrt{m_\mu}+\sqrt{m_\tau})^2=2/3$, empirically to one part in $10^{5}$, is the cube-root generation orbit at the self-dual value $\rho^2=2^{-1}$ --- $Q=\tfrac13+\tfrac23\rho^2$ exact, $\rho^2$ the quarter-turn ($4\mid\Omega-1$) self-dual amplitude on the cubic ($3\mid\Omega+1$) plane. Form and value derived; the selection of the mass vector onto that orientation is the $\Omega$-hard flavour residual (28:Z1). \emph{Falsifier:} a measured $Q$ displaced from $2/3$ beyond the per-mille winding-phase corrections. -/
theorem p27042 : (∀ {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) :=
  @FRC.Ledger.p27042
/-- 27:P9 (p27043) — \textbf{Vanishing strong-CP angle without an axion} \emph{[structural]}. The QCD vacuum angle vanishes on the substrate, $\bar\theta=0$ with no axion: the Wilson action class carries no orientation-odd term (B2) and colour is drive-invariant, so the bare $\theta=0$, and the Hermitian quark mass matrices have real determinant, so $\arg\det M_q=0$, while the Cabibbo--Kobayashi--Maskawa phase sits in the up--down misalignment. \emph{Falsifier:} a neutron electric dipole moment above the QCD floor, or a discovered axion. -/
theorem p27043 : (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (U : FRC.Unitary.M3 p ν), FRC.Unitary.SU FRC.Unitary.mone U → FRC.Unitary.tr (FRC.Unitary.adj U) = (FRC.Unitary.tr U).conj ∧ FRC.Unitary.tr (FRC.Unitary.adj U) + (FRC.Unitary.tr (FRC.Unitary.adj U)).conj = FRC.Unitary.tr U + (FRC.Unitary.tr U).conj) ∧ (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (A : FRC.Unitary.M3 p ν), FRC.Unitary.dag A = A → (FRC.Unitary.det A).conj = FRC.Unitary.det A) ∧ ∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (A : FRC.Unitary.M3 p ν), FRC.Unitary.dag A = A → (FRC.Unitary.det A).im + (FRC.Unitary.det A).im = (0 : FRC.Shell p) :=
  @FRC.Ledger.p27043
-- end ledger predicates

end FRC.Fields