sm_charge_count

formal source

 136  | lepton : SMCharge
 137  deriving DecidableEq, Fintype
 138
 139theorem sm_charge_count : Fintype.card SMCharge = 3 := by decide
 140
 141theorem sm_charges_match_D3 :
 142    Fintype.card SMCharge = independent_charge_count 3 := by
 143  rw [sm_charge_count, three_charges_at_D3]
 144
 145/-- Each SM charge corresponds to a face-pair axis of Q₃. -/
 146def charge_to_axis : SMCharge → Fin 3
 147  | .electric => ⟨0, by norm_num⟩
 148  | .baryon => ⟨1, by norm_num⟩
 149  | .lepton => ⟨2, by norm_num⟩
 150
 151theorem charge_to_axis_injective : Function.Injective charge_to_axis := by
 152  intro a b h; cases a <;> cases b <;> simp_all [charge_to_axis]
 153
 154theorem charge_to_axis_surjective : Function.Surjective charge_to_axis := by
 155  intro ⟨n, hn⟩; interval_cases n
 156  · exact ⟨.electric, rfl⟩
 157  · exact ⟨.baryon, rfl⟩
 158  · exact ⟨.lepton, rfl⟩
 159
 160theorem charge_to_axis_bijective : Function.Bijective charge_to_axis :=
 161  ⟨charge_to_axis_injective, charge_to_axis_surjective⟩
 162
 163/-! ## Part 5: Topological vs. Noether Conservation -/
 164
 165/-- A **Noether charge**: real-valued, conserved under dynamics. -/
 166structure NoetherCharge (N : ℕ) where
 167  value : Configuration N → ℝ
 168  conserved : ∀ (c next : Configuration N),
 169    IsVariationalSuccessor c next → value next = value c