winding_orthogonal
plain-language theorem explainer
A single lattice step along one axis contributes zero net winding to any orthogonal axis in dimension D. Researchers deriving topological conservation laws from lattice paths would cite this when separating independent charges. The proof is a direct simplification that unfolds winding_number and step_displacement then applies the axis inequality.
Claim. Let $D$ be a natural number and let $a_1, a_2$ be distinct elements of the finite set with $D$ elements. The winding number along axis $a_2$ of the one-step path consisting of a positive unit displacement along axis $a_1$ equals zero.
background
The WindingCharges module treats world-lines as finite sequences of LatticeStep moves on the integer lattice Z^D. Each LatticeStep is either a unit displacement plus or minus along one coordinate axis or a stay. The winding number of a path along axis k is the net signed count of steps that affect that axis: number of +k steps minus number of -k steps. Module documentation states that these winding numbers are invariant under the local deformations performed by variational dynamics and that distinct axes yield independent charges.
proof idea
The proof is a one-line simp that unfolds the definitions of winding_number and step_displacement. The inequality axis1 ≠ axis2 selects the case in step_displacement that returns zero displacement on the target axis, so the net winding is immediately zero.
why it matters
This result is invoked by winding_surjective_single to construct paths whose winding vector has support on a single axis. It thereby contributes to the derivation that exactly D independent topological charges exist, recovering the three conservation laws when D equals 3 as required by the eight-tick forcing chain. The lemma closes the combinatorial gap left implicit in TopologicalConservation by showing orthogonality of axis contributions directly from the step definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.