winding_charge
plain-language theorem explainer
winding_charge assigns to each lattice path in D dimensions the integer winding number along a chosen axis k. Researchers deriving topological conservation from lattice combinatorics cite this when establishing that the charges are independent and determine the full winding vector. The definition is realized as a one-line wrapper delegating directly to the winding_number computation on paths.
Claim. Let $D$ be a natural number and $k$ an index in the set with $D$ elements. For a lattice path $p$ consisting of unit steps on the integer lattice in $D$ dimensions, the winding charge along axis $k$ is the net signed displacement $w_k(p)$ given by the difference between positive and negative steps along that axis.
background
Lattice paths are finite sequences of steps on the integer lattice in dimension $D$, where each step displaces the position by one unit along a single coordinate axis or leaves it unchanged. The winding number along axis $k$ extracts the net crossings: the count of positive steps minus the count of negative steps along that axis. This module supplies the explicit mechanism for topological charges that TopologicalConservation left implicit, showing that local deformations of paths preserve all winding numbers because the variational dynamics update one tick at a time via such deformations.
proof idea
The definition is a one-line wrapper that applies the winding_number function to the given path and axis index $k$.
why it matters
This definition is invoked by the downstream theorems D_independent_charges and three_independent_winding_charges, which prove there are exactly $D$ independent winding-number charges and the special case of three for $D=3$. It fills the combinatorial gap in the derivation of conservation laws from lattice paths, connecting directly to the framework requirement of $D=3$ spatial dimensions and the eight-tick octave structure. The construction shows the charges arise from path combinatorics without extra postulates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.