cancelling_pair_zero_displacement
plain-language theorem explainer
A pair of lattice steps that cancel each other along the same axis produces zero net displacement on any coordinate. Researchers working on topological conservation in lattice models cite this to establish invariance of winding numbers under local deformations. The proof uses case analysis on the two orderings of the cancelling pair followed by simplification of the displacement function.
Claim. Let $D$ be a natural number. For steps $s_1,s_2$ on the lattice $Z^D$ that form a cancelling pair (one positive and one negative along the same axis) and any axis $k$, the displacement of $s_1$ along $k$ plus the displacement of $s_2$ along $k$ equals zero.
background
The WindingCharges module models world-lines as sequences of LatticeStep on $Z^D$, where each step is plus or minus along one axis or stay. The step_displacement function computes the signed contribution (+1, -1, or 0) of a step to a chosen axis. The is_cancelling_pair predicate identifies pairs that are opposites on the same axis. This local result on displacement is the key algebraic fact underlying homotopy invariance of winding numbers.
proof idea
The term proof cases on the disjunction in the cancelling-pair hypothesis. For each branch it substitutes the step equalities, unfolds step_displacement, and applies split followed by simplification to confirm the sum is zero.
why it matters
This theorem is invoked by insert_cancelling_preserves_winding to show that appending a cancelling pair to a path prefix does not alter the winding number. It supplies the local mechanism for the global conservation of topological charges in the Recognition framework, where exactly D independent winding numbers arise for dimension D, with the case D=3 yielding three charges as required by the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.