charge_count_equals_face_pairs
plain-language theorem explainer
The equality shows that the number of independent topological charges in three dimensions equals the number of opposite face pairs on a 3-cube. Researchers deriving conservation laws from topology rather than Noether symmetries would cite this to ground the count of Standard Model charges in the geometry of D=3. The proof reduces to reflexivity because both quantities are defined to be three.
Claim. In three spatial dimensions the number of independent conserved charges equals the number of pairs of opposite faces on the three-dimensional cube.
background
This module formalizes conservation laws as topological invariants arising from linking in three dimensions rather than continuous symmetries. The function independent_charge_count D returns the number of independent charges supported at dimension D while face_pairs D counts the pairs of opposite faces on the D-cube and equals D by definition from ParticleGenerations. The module doc states that D=3 supports exactly three independent charges because it allows non-trivial linking, with charge as a linking number that is integer-valued and conserved under continuous deformation.
proof idea
The proof is a one-line reflexivity that equates the two sides by their shared definition as the integer three.
why it matters
This equality supports the claim in F-012 that conservation originates from topology in D=3. It feeds into results such as three_charges_at_D3 and topological_charge_quantized by confirming the charge count matches the geometric face pairs. The framework landmark is the forcing of D=3 to enable linking numbers that quantize charges as integers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.