three_charges_at_D3
plain-language theorem explainer
The theorem establishes that three spatial dimensions support exactly three independent topological charges. Researchers deriving conservation laws from linking numbers rather than Noether symmetries would cite it to confirm the dimension-forced count matches the three Standard Model charges. The proof is a one-line simplification that unfolds the definition of the charge-count function.
Claim. In three spatial dimensions the number of independent topological charges equals three, where this count is defined to be three precisely when the dimension is three and zero otherwise.
background
The module formalizes the claim that conservation laws arise from topology (linking in D=3) rather than continuous symmetries. The upstream definition states that the number of independent topological charges supported by dimension D is 3 when D=3 and 0 otherwise, with explicit values given for D=1 (0, no linking), D=2 (0, everything unlinks), D=3 (3, one per coordinate plane of Q₃), and D≥4 (0, everything unlinks). This sits inside the broader F-012 development that treats charge, baryon number, and lepton number as integer linking numbers invariant under variational dynamics.
proof idea
The proof is a one-line wrapper that applies simplification to the definition of independent charge count, which directly returns the value 3 for input dimension 3.
why it matters
It supplies the exact count required by the topological conservation certificate (F-012), which asserts integer-valued charges, exact conservation along trajectories, and D=3 as the only dimension permitting three independent charges. The result is invoked in sm_charges_match_D3 to equate the Standard Model charge count with the topological count and in all_threes_unified to identify the common origin of the three winding charges, three face-pairs, and three colors. It directly instantiates the framework landmark that D=3 is forced because it alone supports non-trivial linking.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.