linking_iff_D3
plain-language theorem explainer
Linking-based charges exist if and only if the dimension equals three. A physicist deriving conservation from topology in Recognition Science would cite the equivalence to anchor the restriction to three spatial dimensions. The proof unfolds the charge-count definition by case analysis and confirms the biconditional with arithmetic.
Claim. For any natural number $D$, the number of independent topological charges supported by dimension $D$ is positive if and only if $D=3$.
background
TopologicalConservation derives conservation from linking numbers rather than Noether symmetries. The definition independent_charge_count returns 3 when $D=3$ and 0 otherwise, encoding that only three-dimensional space supports non-trivial linking of trajectories. Charge is an abbreviation for real numbers in RS-native units, but the theorem concerns the integer count of independent charges.
proof idea
The proof is a one-line wrapper that simplifies the definition of independent_charge_count, splits on the conditional, and applies omega to verify the arithmetic in each case.
why it matters
The equivalence confirms that topological charges, which supply quantized conservation in the ledger, appear only in $D=3$, matching the framework's forcing of three spatial dimensions. It closes the gap between dimensional forcing and the mechanism for integer invariants under continuous deformation, as stated in module item F-012. No downstream uses appear in the graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.