winding_number
plain-language theorem explainer
The winding number along axis k for a lattice path on Z^D equals the sum of signed displacements contributed by each step along that axis. Researchers deriving charge conservation from lattice world-lines cite this when showing invariance under local deformations in variational dynamics. The definition reduces directly to a sum after mapping steps via the displacement function.
Claim. For a lattice path $p$ in $Z^D$ and axis $k$, the winding number is $w_k(p) := sum_{s in p} delta_k(s)$, where $delta_k(s)$ equals +1 for a positive step along $k$, -1 for a negative step, and 0 otherwise.
background
The WindingCharges module supplies the topological mechanism for conservation laws left implicit in TopologicalConservation. A LatticePath D is a finite list of LatticeStep D on the integer lattice Z^D, with each step displacing by one unit along a single axis or remaining stationary. The step_displacement function returns the signed contribution of any given step along a chosen axis. This definition operates downstream of lattice path combinatorics and upstream of results on path deformations.
proof idea
The definition is a one-line wrapper that maps the path to the list of axis-specific displacements via step_displacement and then sums the resulting integers.
why it matters
This definition supplies the primitive used by D_independent_charges to establish exactly D independent winding-number charges and by is_closed to characterize loops. It realizes the module claim that conservation laws arise from winding numbers of lattice paths, supporting the D=3 connection where three spatial dimensions produce three independent topological charges. It bridges variational dynamics to topological invariance without invoking the phi-ladder or J-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.