square_loop_trivial_when_equal
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not treat the case of distinct axes.
- Does not compute winding numbers for non-degenerate loops.
- Does not address paths longer than four steps.
- Does not incorporate continuous deformations.
formal statement (Lean)
386theorem square_loop_trivial_when_equal {D : ℕ} (j : Fin D) :
387 ∀ axis : Fin D,
388 winding_number (square_loop j j) axis = winding_number ([] : LatticePath D) axis := by
proof body
Term-mode proof.
389 intro axis
390 simp [square_loop, winding_number, step_displacement]
391 split <;> simp
392
393/-! ## Part 10: Why D = 3 Is Special (Combinatorial) -/
394
395/-- **THEOREM (D Independent Closed Loops)**:
396 In D dimensions, there are exactly D · (D-1) / 2 independent
397 non-trivial square loops (one per pair of axes).
398
399 For D = 3: 3 · 2 / 2 = 3 independent loops.
400 These 3 loops bound the 3 independent faces of Q₃.
401 Each face contributes one topological charge (the flux through it). -/