winding_surjective_single
plain-language theorem explainer
The winding-number map along any fixed axis from lattice paths in D dimensions onto the integers is surjective, with the realizing path carrying zero winding on all other axes. A physicist constructing conserved topological charges on a discrete spacetime lattice would cite the result to guarantee every integer charge value is attainable. The argument proceeds by induction on the target integer, constructing the path through successive single-axis steps and invoking additivity together with axis orthogonality.
Claim. For any natural number $D$, any coordinate axis $k$ in the finite set of $D$ directions, and any integer $n$, there exists a finite lattice path $p$ on the integer lattice such that the net signed displacement of $p$ along axis $k$ equals $n$ while the net signed displacement along every other axis equals zero.
background
A lattice path is a finite list of steps on the D-dimensional integer lattice, where each step is a plus or minus unit displacement along one coordinate axis or a stay. The winding number along a chosen axis is the algebraic sum of the individual step displacements along that axis, yielding the net signed count of traversals. This supplies the topological charges whose invariance under local deformations yields conservation laws, as set out in the module's account of world-lines and the earlier TopologicalConservation development.
proof idea
The proof uses integer induction on the target value n. The zero case is given directly by the empty path, which has vanishing winding on every axis. For the successor step the inductive hypothesis supplies a path realizing k; concatenation with a single plus step along the target axis raises the winding by 1 while leaving orthogonal windings at zero, by additivity and the orthogonality of distinct axes. The predecessor case appends a minus step and applies the corresponding minus lemma with a ring simplification on the integers.
why it matters
The statement is invoked by the downstream theorem establishing exactly D independent winding charges. Within the Recognition framework it supplies the combinatorial realization of the D spatial dimensions forced by the eight-tick octave, ensuring the topological charges match the number of independent conservation laws required by the lattice model. The module thereby replaces an earlier definitional count with a derivation from path combinatorics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.