no_charges_at_other_D
plain-language theorem explainer
The theorem shows that the count of independent topological charges is zero for every natural number D other than 3. Researchers deriving conservation laws from linking numbers in Recognition Science cite it to enforce the dimension restriction. The proof is a one-line simplification that invokes the piecewise definition of the charge count under the hypothesis D ≠ 3.
Claim. Let $D$ be a natural number satisfying $D ≠ 3$. Then the number of independent topological charges supported by dimension $D$ equals zero.
background
The TopologicalConservation module derives conservation from topological linking in three dimensions rather than from continuous symmetries. The central definition independent_charge_count returns 3 precisely when D = 3 and 0 otherwise, because only three-dimensional space admits non-trivial linking numbers, one per coordinate plane of the cube Q₃. This rests on the upstream result from DimensionForcing that D = 3 is the unique dimension permitting stable links.
proof idea
The proof is a one-line wrapper that applies the simp tactic to the definition of independent_charge_count together with the hypothesis D ≠ 3, which selects the else branch and yields zero.
why it matters
The result is invoked inside topological_conservation_certificate, the F-012 certificate asserting that conservation laws are topological: integer-valued, exactly conserved along trajectories, and possible only in D = 3. It thereby confirms the framework step T8 that forces three spatial dimensions because only that dimension supports three independent charges from linking.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.