loops_eq_face_pairs_D3
plain-language theorem explainer
In three dimensions the count of independent lattice loops equals the number of opposite face pairs on the cube. Researchers counting topological charges from winding numbers in Recognition Science cite this equality to fix the number of conserved charges at three. The proof is a one-line native_decide that evaluates both sides directly to the numeral three.
Claim. In three spatial dimensions the number of independent winding loops on the integer lattice equals the number of pairs of opposite faces on the three-dimensional cube.
background
The module derives conservation laws from winding numbers of lattice paths on ℤ^D. For each axis k the winding number w_k(path) equals the net signed steps along that axis: (# of +k steps) minus (# of -k steps). These numbers are invariant under local deformations and therefore under the variational dynamics. The definition face_pairs(D) returns D, the number of opposite face pairs on the D-cube; for D = 3 this yields three pairs. The upstream result ParticleGenerations.face_pairs supplies the combinatorial count that is here equated to the independent loop count.
proof idea
The proof is a one-line native_decide wrapper. It reduces both sides of the equality by direct evaluation: independent_loop_count 3 computes to 3 and face_pairs 3 also computes to 3, discharging the goal by reflexivity.
why it matters
This theorem supplies the missing combinatorial link inside the F-013 certificate on winding charges. It confirms that the three independent topological charges forced by D = 3 coincide with the three face pairs, which the certificate identifies with the three colors and three generations. The result supports the framework claim that conservation is topological rather than Noether-derived and closes the step that equates loop count to dimension in the D = 3 case.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.