independent_loop_count
plain-language theorem explainer
The definition counts independent closed loops in D dimensions by the formula D(D-1)/2, which equals the number of unordered axis pairs. Researchers deriving topological conservation from lattice path windings cite it to obtain the exact number of independent charges. It is realized as a direct arithmetic expression with no auxiliary lemmas.
Claim. In $D$ spatial dimensions the number of independent non-trivial square loops is exactly $D(D-1)/2$.
background
This definition sits inside the F-013 module that supplies the topological mechanism for conservation laws. World-lines are sequences of lattice steps on $Z^D$; each axis $k$ carries a winding number $w_k$ equal to the net signed steps along that axis. Local deformations of a path preserve all winding numbers, so the variational dynamics leaves them invariant. The module isolates the combinatorial count of independent square loops formed by pairs of axes, which later specializes to three loops when $D=3$.
proof idea
The declaration is a direct definition that encodes the binomial coefficient via integer arithmetic. No lemmas or tactics are invoked; the expression $D * (D-1)/2$ is the standard count of unordered pairs of distinct axes.
why it matters
It supplies the loop count used by three_independent_loops_D3, loops_eq_face_pairs_D3, and the winding_charges_certificate theorem. The certificate lists four properties (integer, additive, invariant, independent) that together derive conservation from windings; this definition closes the combinatorial step that earlier independent_charge_count left as a postulate. In the Recognition framework it supports the emergence of exactly three independent charges for $D=3$, consistent with the eight-tick octave and the topological protection of charge quantization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.