three_charges_at_D3

formal source

 111def independent_charge_count (D : ℕ) : ℕ :=
 112  if D = 3 then 3 else 0
 113
 114theorem three_charges_at_D3 : independent_charge_count 3 = 3 := by
 115  simp [independent_charge_count]
 116
 117theorem no_charges_at_other_D (D : ℕ) (hD : D ≠ 3) :
 118    independent_charge_count D = 0 := by
 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