winding_empty
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove invariance of winding numbers under local deformations.
- Does not compute winding numbers for any non-empty path.
- Does not establish independence of windings across distinct axes.
- Does not relate winding numbers to phi-ladder mass formulas or physical constants.
Lean usage
theorem empty_is_closed {D : ℕ} : is_closed ([] : LatticePath D) := fun k => winding_empty kformal statement (Lean)
111theorem winding_empty {D : ℕ} (axis : Fin D) :
112 winding_number ([] : LatticePath D) axis = 0 := rfl
proof body
Term-mode proof.
113
114/-- Winding number of a single plus-step along the measured axis is +1. -/