winding_plus_self

formal source

 112    winding_number ([] : LatticePath D) axis = 0 := rfl
 113
 114/-- Winding number of a single plus-step along the measured axis is +1. -/
 115theorem winding_plus_self {D : ℕ} (axis : Fin D) :
 116    winding_number [LatticeStep.plus axis] axis = 1 := by
 117  simp [winding_number, step_displacement]
 118
 119/-- Winding number of a single minus-step along the measured axis is -1. -/
 120theorem winding_minus_self {D : ℕ} (axis : Fin D) :
 121    winding_number [LatticeStep.minus axis] axis = -1 := by
 122  simp [winding_number, step_displacement]
 123
 124/-- Winding number of a step along a DIFFERENT axis is 0. -/
 125theorem winding_orthogonal {D : ℕ} (axis₁ axis₂ : Fin D) (h : axis₁ ≠ axis₂) :
 126    winding_number [LatticeStep.plus axis₁] axis₂ = 0 := by
 127  simp [winding_number, step_displacement, h]
 128
 129/-- Winding number of a stay step is 0. -/
 130theorem winding_stay {D : ℕ} (axis : Fin D) :
 131    winding_number [LatticeStep.stay] axis = 0 := by
 132  simp [winding_number, step_displacement]
 133
 134/-! ## Part 3: Additivity Under Concatenation -/
 135
 136/-- **THEOREM (Winding Numbers Are Additive)**:
 137    The winding number of the concatenation of two paths equals the
 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