pith. machine review for the scientific record. sign in
def definition def or abbrev high

LatticePath

show as:
view Lean formalization →

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.

claimA 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  91def LatticePath (D : ℕ) := List (LatticeStep D)

proof body

Definition body.

  92
  93/-- The displacement of a single step along a specific axis.
  94    +1 for a plus-step along that axis, -1 for a minus-step, 0 otherwise. -/

used by (16)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (9)

Lean names referenced from this declaration's body.