three_independent_loops_D3
plain-language theorem explainer
The theorem establishes that the combinatorial count of independent loops on the three-dimensional lattice equals three. Researchers deriving the number of conserved topological charges from winding numbers in Recognition Science cite this when fixing the D=3 case. The proof is a one-line native decision procedure that evaluates the loop-counting definition directly.
Claim. In three spatial dimensions the number of independent winding numbers on lattice paths equals three: $N(3)=3$.
background
The module derives conservation laws from winding numbers of lattice paths on ℤ^D. For each axis k the winding number w_k counts net signed steps along that axis. Local deformations of a path preserve all winding numbers, so they remain invariant under the variational dynamics. The axes are independent because a change along one axis leaves the others untouched, yielding exactly D independent charges. Upstream SpectralEmergence.of states that the same face-pair count on Q₃ produces three particle generations.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate independent_loop_count at argument 3 from its definition.
why it matters
This supplies the explicit D=3 value required by the winding-charge mechanism left implicit in TopologicalConservation. It aligns with the face-pair count in SpectralEmergence.of that yields three generations and realizes the T8 forcing of three spatial dimensions. The result closes the count of independent topological charges for the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.