square_loop_closed
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.