winding_cons
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.