linking_iff_D3

formal source

 119  simp [independent_charge_count, hD]
 120
 121/-- Linking-based charges exist iff D = 3. -/
 122theorem linking_iff_D3 (D : ℕ) :
 123    0 < independent_charge_count D ↔ D = 3 := by
 124  simp [independent_charge_count]; split <;> omega
 125
 126/-- Charge count = face pairs = colors = generations. -/
 127theorem charge_count_equals_face_pairs :
 128    independent_charge_count 3 = face_pairs 3 := rfl
 129
 130/-! ## Part 4: The Three Standard Model Charges -/
 131
 132/-- The three conserved charges of the Standard Model. -/
 133inductive SMCharge where
 134  | electric : SMCharge
 135  | baryon : SMCharge
 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]