pith. machine review for the scientific record. sign in
theorem proved term proof

square_loop_closed

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 377theorem square_loop_closed {D : ℕ} (j k : Fin D) :
 378    is_closed (square_loop j k) := by

proof body

Term-mode proof.

 379  intro axis
 380  simp [square_loop, winding_number, step_displacement]
 381  split <;> split <;> simp
 382
 383/-- The square loop can be decomposed into two cancelling pairs
 384    when j = k (trivial case). When j ≠ k, the loop is genuinely
 385    2-dimensional — it bounds a square face of the lattice. -/

depends on (14)

Lean names referenced from this declaration's body.