LatticeStep
plain-language theorem explainer
LatticeStep is the inductive type of atomic moves on the D-dimensional integer lattice: a signed unit step along one axis or a stationary step. Researchers building world-line combinatorics in Recognition Science cite it when deriving winding-number charges from lattice paths. The definition enumerates three constructors and derives decidable equality automatically.
Claim. For a natural number $D$, the set of lattice steps consists of the inductive type generated by the constructors $+_i$ and $-_i$ for each axis index $i$ in the finite set of size $D$, together with the stationary step.
background
The WindingCharges module supplies the topological mechanism for conservation laws left implicit in TopologicalConservation. World-lines are finite sequences of positions on the integer lattice Z^D; at each tick the position changes by exactly one LatticeStep. The winding number along axis k is the net signed count of steps along that axis, and these numbers are invariant under local deformations that insert or remove cancelling pairs.
proof idea
The declaration is an inductive definition that introduces three constructors: plus and minus each indexed by an element of Fin D, and the nullary constructor stay. Decidable equality is obtained automatically by the deriving clause.
why it matters
LatticeStep is the atomic unit from which LatticePath, winding_number, step_displacement, and is_cancelling_pair are constructed. It directly enables the downstream theorems that cancelling pairs are closed, preserve windings, and that there exist exactly D independent charges. In the Recognition framework this realizes the claim that conservation laws arise from the combinatorics of lattice paths on Z^D, with the D=3 case supplying the three independent topological charges observed in physics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.