winding_cons
Prepending a lattice step to a path adds precisely the signed displacement of that step to the winding number along any chosen axis. Researchers deriving topological charge conservation from lattice world-lines cite this additivity to establish invariance under single-tick updates. The proof is a direct unfolding of the winding_number definition followed by list-cons and sum simplification.
claimLet $D$ be a natural number, $s$ a single step on the $D$-dimensional lattice, $p$ a finite sequence of such steps, and $k$ an axis index. The net signed displacement of the concatenated sequence $s$ followed by $p$, measured along axis $k$, equals the displacement contributed by $s$ along $k$ plus the net signed displacement of $p$ along $k$.
background
Module F-013 supplies the topological mechanism for conservation by defining winding numbers on lattice paths in $Z^D$. A LatticeStep is an elementary move: plus or minus one unit along one axis, or a stay. A LatticePath is the finite list of such steps that records a world-line across ticks. The winding number along axis $k$ is the difference between the number of +k steps and the number of -k steps.
proof idea
The proof is a one-line wrapper that unfolds the definition of winding_number and applies simp to the cons and sum operations on the list of per-step displacements.
why it matters in Recognition Science
The lemma supplies the recursive structure needed to prove that winding numbers remain unchanged under the local deformations generated by variational dynamics. It therefore supports the module claim that exactly D independent topological charges exist, with the D=3 case recovering the three independent charges required by the Recognition Science forcing chain. No downstream theorems are recorded yet, leaving its use in explicit conservation proofs open.
scope and limits
- Does not prove invariance under non-local path changes.
- Does not compute numerical winding values for concrete paths.
- Does not extend to infinite or cyclic paths.
- Does not establish orthogonality of windings on distinct axes.
formal statement (Lean)
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
proof body
Term-mode proof.
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. -/