square_loop
plain-language theorem explainer
The square_loop definition builds a four-step lattice path on the D-dimensional integer grid that traverses the boundary of a square face spanned by coordinate axes j and k. Researchers studying topological invariants in discrete spacetime models cite this construction when deriving conserved winding numbers from lattice paths. The definition is a direct list literal that assembles the steps +j, +k, -j, -k without invoking any lemmas.
Claim. For a natural number $D$ and indices $j,k$ in the finite set with $D$ elements, the square loop is the lattice path given by the sequence of steps $+e_j$, $+e_k$, $-e_j$, $-e_k$, where $e_i$ is the unit vector along axis $i$.
background
LatticePath is defined as a finite list of LatticeStep elements on the D-dimensional lattice, where each step records a signed unit displacement along one coordinate axis. The module WindingCharges develops the topological mechanism for conservation by showing that winding numbers (net signed steps along each axis) remain invariant under local deformations of paths. This square loop supplies a basic closed example that exists once D is at least 2 and illustrates how independent charges arise along each of the D axes.
proof idea
The declaration is a direct definition that returns the explicit four-element list [.plus j, .plus k, .minus j, .minus k]. No upstream lemmas are applied; the construction simply populates the LatticePath type with the four steps that traverse a square face.
why it matters
This definition supplies the canonical non-trivial closed loop invoked by square_loop_closed (which verifies the path is closed) and square_loop_trivial_when_equal (which shows degeneracy when the axes coincide). In the Recognition framework it concretizes the combinatorial origin of D independent winding numbers, supporting the module's derivation that exactly D topological charges are conserved and the special status of D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.