square_loop
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not require or enforce that j and k are distinct.
- Does not prove the path is closed or compute its winding numbers.
- Does not restrict the domain to D greater than or equal to 2.
- Does not address invariance under lattice deformations.
formal statement (Lean)
374def square_loop {D : ℕ} (j k : Fin D) : LatticePath D :=
proof body
Definition body.
375 [.plus j, .plus k, .minus j, .minus k]
376