cancelling_pair_closed
plain-language theorem explainer
The theorem establishes that any pair of opposite steps along one axis forms a closed lattice path, with zero net displacement on every coordinate. Researchers deriving topological conservation from winding numbers in three-dimensional lattices would cite it to confirm that cancelling pairs are homotopically trivial. The proof is a direct term-mode simplification that unfolds the winding-number definition and dispatches the axis cases by case analysis.
Claim. For any dimension $D$ and axis $a$, the lattice path consisting of a forward step followed by a backward step along $a$ satisfies $w_k = 0$ for every coordinate $k$, where $w_k$ denotes the net signed count of steps along axis $k$.
background
LatticeStep is the inductive type whose constructors are plus (axis), minus (axis), and stay; each constructor records a unit displacement along one coordinate of the integer lattice. LatticePath is the type of finite lists of such steps. The predicate is_closed on a path requires that the winding number along every axis vanishes, where the winding number for axis $k$ is the difference between the number of plus-$k$ steps and minus-$k$ steps. The module derives conservation laws from the invariance of these winding numbers under local deformations of paths; the same module notes that exactly $D$ independent winding numbers exist and that the case $D=3$ permits non-trivial knots while $D≤2$ does not.
proof idea
The term proof introduces the axis index $k$, then applies simplification on the definitions of winding_number and step_displacement. A case split on the axis equality dispatches the three constructors of LatticeStep; each branch reduces immediately to zero by the arithmetic of signed displacements.
why it matters
The result supplies the elementary closed paths required by the topological mechanism in WindingCharges. It supports the claim that local deformations preserve all winding numbers and therefore that conservation laws arise from the lattice combinatorics. The surrounding comment records the contrast with knotted loops that appear only when $D=3$, the dimension forced by the eight-tick octave in the upstream forcing chain. No downstream use sites are recorded, so the lemma functions as a foundational building block rather than an intermediate step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.