LatticeStep

formal source

  81
  82/-- A single step on the D-dimensional lattice ℤ^D.
  83    Each step moves ±1 along one axis, or stays put. -/
  84inductive LatticeStep (D : ℕ) where
  85  | plus  (axis : Fin D) : LatticeStep D
  86  | minus (axis : Fin D) : LatticeStep D
  87  | stay  : LatticeStep D
  88  deriving DecidableEq
  89
  90/-- A lattice path: a finite sequence of steps. -/
  91def LatticePath (D : ℕ) := List (LatticeStep D)
  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. -/
  95def step_displacement {D : ℕ} (s : LatticeStep D) (axis : Fin D) : ℤ :=
  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). -/
 107def winding_number {D : ℕ} (path : LatticePath D) (axis : Fin D) : ℤ :=
 108  (path.map (fun s => step_displacement s axis)).sum
 109
 110/-- Winding number of the empty path is zero. -/
 111theorem winding_empty {D : ℕ} (axis : Fin D) :
 112    winding_number ([] : LatticePath D) axis = 0 := rfl
 113
 114/-- Winding number of a single plus-step along the measured axis is +1. -/