step_displacement
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not define the total winding number of an entire path.
- Does not impose any restriction on the value of D.
- Does not encode the dynamics or deformation rules.
- Does not compute physical masses or coupling constants.
formal statement (Lean)
95def step_displacement {D : ℕ} (s : LatticeStep D) (axis : Fin D) : ℤ :=
proof body
Definition body.
96 match s with
97 | .plus a => if a = axis then 1 else 0
98 | .minus a => if a = axis then -1 else 0
99 | .stay => 0
100
101/-! ## Part 2: Winding Numbers -/
102
103/-- The **winding number** of a lattice path along axis k:
104 the total signed displacement along that axis.
105
106 w_k(path) = ∑ (step displacement along k). -/