three_charges_at_D3
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.
claimIn 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 in Recognition Science
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.
scope and limits
- Does not prove that charges are quantized or integer-valued.
- Does not derive the explicit values or assignments of the three charges.
- Does not address conservation of charges along individual trajectories.
- Does not compare topological charges to Noether charges beyond the dimension count.
Lean usage
rw [three_charges_at_D3]formal statement (Lean)
114theorem three_charges_at_D3 : independent_charge_count 3 = 3 := by
proof body
One-line wrapper that applies simp.
115 simp [independent_charge_count]
116