is_cancelling_pair
plain-language theorem explainer
A definition identifying when two lattice steps on ℤ^D form a cancelling pair: opposite signed moves along the identical axis. Workers deriving topological conservation from lattice paths cite it to establish invariance of winding numbers under local deformations. The definition is supplied directly as a disjunction of the two orderings of plus-minus pairs.
Claim. For steps $s_1,s_2$ on the $D$-dimensional lattice, the predicate holds precisely when there exists an axis $a$ such that either $s_1$ is the plus-step and $s_2$ the minus-step along $a$, or the reverse.
background
The WindingCharges module derives conservation laws from winding numbers of lattice paths on ℤ^D. Each path is a sequence of LatticeStep elements, where LatticeStep is the inductive type whose constructors are plus (axis : Fin D), minus (axis : Fin D), and stay. The winding number along axis k is the difference between the number of plus-k and minus-k steps; these integers are additive and invariant under the variational dynamics because the dynamics updates paths by local deformations.
proof idea
The definition is given directly by a disjunction of two existential quantifiers over Fin D, one for each ordering of the opposing steps. No lemmas or tactics are invoked; the body enumerates the two symmetric cases.
why it matters
The definition supplies the primitive notion of local deformation used by cancelling_pair_zero_displacement, insert_cancelling_preserves_winding, and remove_cancelling_preserves_winding. These feed the winding_charges_certificate, which establishes integer, additive, invariant, and independent charges, thereby deriving the count of D independent topological charges for D = 3 from the combinatorics of lattice paths.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.