winding_minus_self
plain-language theorem explainer
A single negative lattice step along a chosen axis yields winding number -1 along that axis. Lattice modelers deriving topological charges from path combinatorics cite this as the base case for signed displacements. The proof reduces directly by unfolding the winding number definition on the singleton path.
Claim. For any natural number $D$ and axis $a$ in the finite set of $D$ coordinates, the winding number of the singleton path consisting of one negative step along $a$ equals $-1$ when evaluated on coordinate $a$.
background
The Winding Charges module treats world-lines as finite sequences of steps on the integer lattice $Z^D$. Each step is either a unit displacement along one coordinate axis or a stay. The winding number along axis $k$ is defined as the difference between the number of positive and negative steps along that axis. This construction supplies the explicit mechanism left implicit in TopologicalConservation, where independent charge count equals $D$ precisely because the $D$ winding numbers are separately conserved under local path deformations.
proof idea
The term-mode proof applies simp to the definitions of winding_number and step_displacement. These unfold the net signed count for the singleton list containing only the minus step, yielding exactly $-1$ on the target axis.
why it matters
This base case is invoked by the surjectivity theorem winding_surjective_single, which establishes that every integer vector in $Z^D$ is realized by some lattice path. It thereby completes the combinatorial step showing exactly $D$ independent topological charges, aligning with the framework's derivation of three spatial dimensions from the eight-tick octave and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.