winding_stay
plain-language theorem explainer
The winding number along any axis for a single stay step on the D-dimensional lattice is zero. Researchers deriving topological conservation from lattice paths cite this as the base case showing non-moving segments carry no charge. The result supports invariance under variational dynamics that act by local deformations. The proof is a one-line simplification that reduces directly to the definitions of winding_number and step_displacement.
Claim. Let $D$ be a natural number and let $a$ be an element of the finite set with $D$ elements. The winding number of the lattice path consisting of the single stay step equals zero along axis $a$.
background
Module F-013 derives conservation laws from winding numbers of paths on the integer lattice. A lattice step is an inductive type with constructors for unit moves along one axis or a stay. The winding number along axis $k$ is the net signed displacement: number of positive steps minus number of negative steps along that axis. Stay steps contribute zero by definition. The local setting is that variational dynamics update one tick at a time via local deformations, which preserve all winding numbers. Upstream results include the inductive definition of LatticeStep and the step_displacement function used to compute net changes.
proof idea
The proof is a one-line wrapper that applies simplification to the definitions of winding_number and step_displacement. This immediately evaluates the stay case to zero without further case analysis.
why it matters
This anchors the base case for winding numbers in the Recognition Science mechanism for conservation, where exactly D independent charges arise when D equals 3. It feeds the additivity theorem for path concatenation and supports the claim that local deformations leave winding numbers invariant. The module positions this as the topological origin of charge conservation on world-lines.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.