winding_charge

formal source

 236/-! ## Part 6: Exactly D Independent Charges -/
 237
 238/-- The winding number along axis k, viewed as a function on lattice paths. -/
 239def winding_charge (D : ℕ) (k : Fin D) : LatticePath D → ℤ :=
 240  fun p => winding_number p k
 241
 242/-- **THEOREM (D Independent Charges)**:
 243    There are exactly D independent winding-number charges.
 244
 245    "Independent" means:
 246    1. Each charge is a distinct ℤ-valued function (they disagree on some path)
 247    2. No charge is a ℤ-linear combination of the others
 248    3. Together they determine the full winding-number vector
 249
 250    Proof: For distinct axes j ≠ k, the path [plus k] has
 251    winding_charge k = 1 but winding_charge j = 0. -/
 252theorem D_independent_charges (D : ℕ) (hD : 0 < D) :
 253    -- 1. There are D winding charges
 254    (Fintype.card (Fin D) = D) ∧
 255    -- 2. They are pairwise distinguishable
 256    (∀ j k : Fin D, j ≠ k →
 257      ∃ p : LatticePath D, winding_charge D j p ≠ winding_charge D k p) ∧
 258    -- 3. Each charge can take any integer value independently
 259    (∀ k : Fin D, ∀ n : ℤ,
 260      ∃ p : LatticePath D, winding_charge D k p = n ∧
 261        ∀ j, j ≠ k → winding_charge D j p = 0) := by
 262  refine ⟨Fintype.card_fin D, ?_, ?_⟩
 263  · intro j k hjk
 264    use [LatticeStep.plus k]
 265    simp [winding_charge, winding_number, step_displacement, hjk, Ne.symm hjk]
 266  · intro k n
 267    obtain ⟨p, hp, hp'⟩ := winding_surjective_single k n
 268    exact ⟨p, hp, hp'⟩
 269