step_displacement
plain-language theorem explainer
The definition computes the signed integer displacement contributed by one lattice step along a chosen coordinate axis in D dimensions. Researchers working on topological conservation laws and winding-number invariants cite it when decomposing path sums into per-axis contributions. It is realized by exhaustive case analysis on the three constructors of LatticeStep.
Claim. Let $s$ be a step on the integer lattice $Z^D$ and let $k$ be a coordinate axis. The displacement along $k$ equals $+1$ when $s$ advances positively along $k$, equals $-1$ when it retreats along $k$, and equals zero for any other step.
background
In the Winding Charges module the lattice is equipped with steps that change position by $pm 1$ along one axis or remain fixed. LatticeStep is the inductive type whose constructors are plus(axis), minus(axis) and stay. The module derives conservation laws from the invariance of winding numbers under local deformations of world-lines on $Z^D$ (see MODULE_DOC).
proof idea
The definition performs pattern matching on the LatticeStep constructors. For a plus step it returns 1 when the axis matches and 0 otherwise; for a minus step it returns -1 on match and 0 otherwise; the stay constructor always returns 0.
why it matters
This definition supplies the primitive building block for all winding-number calculations in the module. It is invoked directly by the proofs of cancelling-pair zero displacement and of D independent charges, which establish that exactly D topological charges exist when the spatial dimension is 3. The construction realizes the claim in the module documentation that each axis contributes one independent winding number, thereby grounding the topological mechanism for conservation laws.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.