square_loop_closed
The square loop on the D-dimensional integer lattice, built from steps along any two axes j and k, has vanishing net winding on every axis. Researchers deriving topological conservation from lattice path combinatorics would cite this to confirm that elementary plaquettes are closed. The proof reduces the claim to exhaustive case analysis on the queried axis after unfolding the loop and winding definitions.
claimFor any natural number $D$ and indices $j,k$ in the finite set of size $D$, the square loop path formed by successive unit steps along axes $j$ and $k$ is closed: its net signed displacement (winding number) vanishes on every coordinate axis.
background
The WindingCharges module supplies the topological mechanism for conservation: world-lines are sequences of lattice steps on $Z^D$, each step along one axis or a stay. The winding number along axis $k$ equals the number of $+k$ steps minus the number of $-k$ steps. A path is closed precisely when every winding number is zero. Local deformations of paths preserve all windings, so the variational dynamics leaves them invariant. The module shows there are exactly $D$ independent windings because steps along distinct axes commute and do not interfere.
proof idea
The term-mode proof introduces an arbitrary axis, simplifies the square_loop and winding_number expressions via the step_displacement definition, then splits on whether the axis equals $j$ or $k$ (and on the sign of the step). Each case reduces to an algebraic identity that the net count is zero.
why it matters in Recognition Science
The result verifies that the basic 2D plaquettes used to generate the lattice are closed, thereby grounding the claim that winding numbers are conserved under the dynamics. It feeds directly into the derivation that exactly $D$ independent topological charges exist, which the module uses to recover the $D=3$ case from the forcing chain (T8). No downstream theorems are recorded yet, but the lemma closes a basic combinatorial check required for the topological conservation argument.
scope and limits
- Does not prove closure for arbitrary lattice paths or non-planar loops.
- Does not establish independence of windings on distinct axes.
- Does not address continuous deformations or embedding into spacetime.
- Does not connect windings to mass formulas or coupling constants.
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. -/