zeroCharge

formal source

  91/-! ## Part 2: Trivial Charges -/
  92
  93/-- The trivial topological charge: always zero. -/
  94def zeroCharge (N : ℕ) : TopologicalCharge N where
  95  value := fun _ => 0
  96  conserved := fun _ _ _ => rfl
  97
  98/-- A constant topological charge. -/
  99def constCharge (N : ℕ) (n : ℤ) : TopologicalCharge N where
 100  value := fun _ => n
 101  conserved := fun _ _ _ => rfl
 102
 103/-! ## Part 3: Charge Count from Dimension -/
 104
 105/-- The number of **independent topological charges** supported by dimension D.
 106
 107    - D = 1: 0 (no linking)
 108    - D = 2: 0 (everything unlinks)
 109    - D = 3: 3 (one per coordinate plane of Q₃)
 110    - D ≥ 4: 0 (everything unlinks) -/
 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