square_loop_trivial_when_equal
plain-language theorem explainer
When the two axes of a square loop coincide, its winding numbers along every coordinate equal those of the empty path. Lattice models in Recognition Science cite this to confirm that only distinct-axis pairs produce independent topological charges. The proof reduces by direct simplification of the winding_number and step_displacement definitions, followed by case analysis on the target axis.
Claim. For any dimension $D$ and index $j$, the winding number of the square loop formed by repeating axis $j$ equals the winding number of the empty lattice path, for every target axis.
background
LatticePath D is the type of finite sequences of steps on the integer lattice Z^D. Each step displaces by +1 or -1 along one coordinate axis. The winding number along axis a extracts the net signed displacement: number of +a steps minus number of -a steps. The square_loop construction builds a four-step closed path that advances one axis, advances a second, then reverses both. The module derives conservation from the fact that local deformations (replacing a segment by its reverse) leave all winding numbers invariant, as established in the upstream TopologicalConservation framework.
proof idea
The proof introduces the target axis then applies simp to unfold square_loop, winding_number and step_displacement. A case split on whether the queried axis matches the loop direction, followed by further simp, shows both sides evaluate to zero.
why it matters
This result establishes the triviality of degenerate loops, which is required for the combinatorial count of exactly D(D-1)/2 independent non-trivial square loops. For D=3 the count is three, matching the three independent faces of the 3-cube and the three topological charges in the Recognition framework. It supplies the missing derivation for the independent_charge_count definition left implicit in TopologicalConservation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.