winding_additive

formal source

 138    sum of their individual winding numbers.
 139
 140    This is the formal content of "charge is additive." -/
 141theorem winding_additive {D : ℕ} (p₁ p₂ : LatticePath D) (axis : Fin D) :
 142    winding_number (List.append p₁ p₂) axis =
 143    winding_number p₁ axis + winding_number p₂ axis := by
 144  simp [winding_number, List.map_append, List.sum_append]
 145
 146/-- Prepending a step adds its displacement. -/
 147theorem winding_cons {D : ℕ} (s : LatticeStep D) (p : LatticePath D) (axis : Fin D) :
 148    winding_number (s :: p) axis = step_displacement s axis + winding_number p axis := by
 149  unfold winding_number
 150  simp [List.map_cons, List.sum_cons]
 151
 152/-! ## Part 4: Invariance Under Local Deformations -/
 153
 154/-- A **local deformation** is a pair of steps that cancel each other:
 155    a plus-step followed by a minus-step along the same axis (or vice versa).
 156
 157    Inserting or removing such pairs from a path does not change any
 158    winding number. This is the discrete analogue of homotopy invariance. -/
 159def is_cancelling_pair {D : ℕ} (s₁ s₂ : LatticeStep D) : Prop :=
 160  (∃ a : Fin D, s₁ = .plus a ∧ s₂ = .minus a) ∨
 161  (∃ a : Fin D, s₁ = .minus a ∧ s₂ = .plus a)
 162
 163/-- A cancelling pair has zero total displacement along every axis. -/
 164theorem cancelling_pair_zero_displacement {D : ℕ} (s₁ s₂ : LatticeStep D)
 165    (h : is_cancelling_pair s₁ s₂) (axis : Fin D) :
 166    step_displacement s₁ axis + step_displacement s₂ axis = 0 := by
 167  rcases h with ⟨a, h₁, h₂⟩ | ⟨a, h₁, h₂⟩
 168  · subst h₁; subst h₂
 169    simp [step_displacement]
 170    split <;> simp
 171  · subst h₁; subst h₂