winding_empty
plain-language theorem explainer
The winding number of the empty lattice path is zero along any axis in dimension D. Researchers deriving topological conservation from lattice path combinatorics cite this as the base case. The proof holds immediately by reflexivity on the definition of winding number as net signed steps.
Claim. For any natural number $D$ and axis $k$ in Fin $D$, the winding number of the empty path satisfies $w_k([]) = 0$.
background
In the WindingCharges module a LatticePath in dimension $D$ is defined as a finite list of LatticeStep elements. Each step contributes a signed displacement of $+1$, $-1$, or $0$ along a chosen axis. The winding number $w_k$ along axis $k$ is the difference between the number of $+k$ steps and $-k$ steps. The module derives conservation laws from the invariance of these integers under local path deformations, supplying the explicit mechanism left implicit in TopologicalConservation.
proof idea
The proof is a one-line term that applies reflexivity, since the winding number of the empty list is definitionally zero by the recursive definition of winding_number.
why it matters
This supplies the zero case for the induction in winding_surjective_single, which establishes surjectivity of winding numbers onto integer vectors, and is invoked directly in empty_is_closed to show the empty path is closed. It anchors the combinatorial derivation of exactly $D$ independent charges in F-013, linking to the forcing chain step that forces $D=3$ and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.