step_displacement

formal source

  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. -/
 115theorem winding_plus_self {D : ℕ} (axis : Fin D) :
 116    winding_number [LatticeStep.plus axis] axis = 1 := by
 117  simp [winding_number, step_displacement]
 118
 119/-- Winding number of a single minus-step along the measured axis is -1. -/
 120theorem winding_minus_self {D : ℕ} (axis : Fin D) :
 121    winding_number [LatticeStep.minus axis] axis = -1 := by
 122  simp [winding_number, step_displacement]
 123
 124/-- Winding number of a step along a DIFFERENT axis is 0. -/
 125theorem winding_orthogonal {D : ℕ} (axis₁ axis₂ : Fin D) (h : axis₁ ≠ axis₂) :