sm_charges_match_D3
plain-language theorem explainer
The theorem equates the cardinality of the Standard Model charge set to the number of independent topological charges supported by three-dimensional space. Researchers deriving conservation from lattice linking rather than Noether symmetries would cite it to confirm that electric, baryon, and lepton charges align with the three axes of Q3. The proof is a one-line term rewrite that substitutes the SM charge count definition and the three-charge result at D equals 3.
Claim. Let SMCharge be the set of Standard Model charges consisting of the electric, baryon, and lepton charges. Then the cardinality of SMCharge equals the number of independent topological charges in three spatial dimensions, which is 3.
background
The TopologicalConservation module derives conservation laws from topological linking numbers in D=3 rather than from continuous symmetries. SMCharge is the inductive type enumerating the three Standard Model charges: electric, baryon, and lepton. The auxiliary definition independent_charge_count(D) returns 3 precisely when D=3 and 0 otherwise, because only three-dimensional space permits non-trivial linking, one per coordinate plane of the Q3 lattice.
proof idea
The proof is a one-line term-mode wrapper. It rewrites the left side via the sibling definition sm_charge_count and the right side via the sibling lemma three_charges_at_D3, which together establish the numerical equality.
why it matters
This result bridges the Standard Model charge content to the topological structure forced at D=3 and feeds directly into the winding_charges_certificate theorem, which establishes integer quantization, additivity, and invariance of winding numbers along lattice paths. It realizes one of the main results listed in the module documentation for F-012, confirming that D=3 supports exactly three independent charges from face-pair axes of Q3. In the Recognition Science framework it aligns with the forcing of three dimensions (T8) and the emergence of three charges from the phi-ladder geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.