theorem
proved
winding_empty
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.WindingCharges on GitHub at line 111.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
108 (path.map (fun s => step_displacement s axis)).sum
109
110/-- Winding number of the empty path is zero. -/
111theorem winding_empty {D : ℕ} (axis : Fin D) :
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) :