LatticePath
plain-language theorem explainer
LatticePath defines a finite sequence of steps on the D-dimensional integer lattice as the basic combinatorial object for world-lines. Researchers deriving topological conservation from path winding numbers cite it when counting independent charges on ℤ^D. The definition is a direct type abbreviation over the inductive LatticeStep constructors.
Claim. A lattice path in dimension $D$ is a finite sequence of steps on the lattice $ℤ^D$, where each step is a unit displacement along one of the $D$ coordinate axes or a stationary step.
background
The WindingCharges module supplies the combinatorial substrate for conservation laws by representing world-lines as sequences on ℤ^D. LatticeStep is the inductive type whose constructors are plus or minus along a Fin D axis, or stay; a lattice path is then the list type over these steps. Winding number along axis k is the net signed count of plus-k minus minus-k steps, and these numbers are invariant under the local deformations that implement variational dynamics.
proof idea
Direct definition: LatticePath D is the type of finite lists whose elements belong to LatticeStep D. No lemmas or tactics are applied.
why it matters
LatticePath is the type on which all winding-number functions and closed-path predicates are defined, feeding directly into D_independent_charges (which proves exactly D independent ℤ-valued charges) and is_closed. It closes the gap noted in the module doc by deriving the D independent topological charges from lattice combinatorics, supporting the framework claim that D=3 yields three conserved charges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.