winding_plus_self
plain-language theorem explainer
A single positive step along axis k in D-dimensional lattice space yields winding number +1 when measured on that axis. Derivations of topological charge conservation in lattice world-lines cite this unit case as the generator for integer charges. The proof reduces immediately by simplification on the winding number definition and the displacement of a plus step.
Claim. For any natural number $D$ and index $k$ in the finite set of $D$ axes, the winding number of the lattice path consisting of one positive step along axis $k$, evaluated on axis $k$, equals $+1$.
background
The module derives conservation laws from winding numbers on lattice paths in $D$ dimensions. A world-line is a finite sequence of steps, each of which is a plus or minus displacement along one axis or a stay. The winding number along axis $k$ is defined as the difference between the number of positive $k$-steps and the number of negative $k$-steps. This supplies the combinatorial mechanism left implicit in the earlier statement that independent charge count equals $D$ when $D=3$.
proof idea
The proof is a one-line wrapper that applies simplification to the definitions of winding number and step displacement.
why it matters
The result is used by the surjectivity theorem that shows every integer vector in $Z^D$ is realized by some lattice path. It therefore anchors the claim that exactly $D$ independent topological charges arise from the combinatorics of local deformations, which in turn justifies the count of three independent charges when $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.