independent_charge_count
plain-language theorem explainer
The definition counts the independent topological charges permitted by spatial dimension D. Researchers deriving conservation laws from topology rather than symmetry would cite it when establishing that only three dimensions support quantized charges. The definition proceeds by direct case distinction on whether D equals three.
Claim. Let $n(D)$ denote the number of independent topological charges supported in dimension $D$. Then $n(D)=3$ if $D=3$, and $n(D)=0$ otherwise.
background
This definition appears in the module formalizing topological conservation, where conservation laws originate from linking invariants in three dimensions rather than Noether symmetries. Topological charges are integer-valued linking numbers that remain invariant under continuous deformations of trajectories in the ledger. The module contrasts topological conservation (quantized, dimension-dependent) with Noether conservation (real-valued, symmetry-dependent). It builds on the prior result from DimensionForcing that only D equals three supports non-trivial linking, now quantified by the count of independent charges.
proof idea
The definition is given directly by cases on the value of D: it returns three when the dimension equals three and zero for all other natural numbers.
why it matters
This definition supplies the count used throughout the topological conservation results, including the certificate asserting that conservation is topological, requires D equals three, and yields exactly three charges matching the Standard Model. It fills the gap left by DimensionForcing by making explicit the number of charges supported only in three dimensions. The construction aligns with the Recognition Science forcing chain, where D equals three emerges as the unique dimension permitting the required linking for conservation laws.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.