charge_to_axis_surjective
plain-language theorem explainer
The map assigning each standard-model charge to an axis of the Q₃ cube is surjective. Researchers deriving conservation from topological linking in three dimensions cite this to confirm that electric, baryon, and lepton charges exhaust the three axes forced by D = 3. The proof is a direct case split on the three possible axis indices that supplies the preimage charge for each.
Claim. The function sending each standard-model charge (electric, baryon, lepton) to its corresponding face-pair axis of the cube $Q_3$ is surjective.
background
The TopologicalConservation module derives conservation laws from linking numbers in D = 3 rather than from continuous symmetries. The function charge_to_axis maps the three standard-model charges to the three axes of Q₃, with electric charge on axis 0, baryon number on axis 1, and lepton number on axis 2. This sits inside the broader claim that D = 3 supports exactly three independent charges through topology.
proof idea
The term proof introduces an arbitrary element of Fin 3 and applies interval_cases to split on its index. Each of the three cases is discharged by supplying the matching charge together with reflexivity.
why it matters
This result supplies the surjectivity half of the bijection charge_to_axis_bijective, which equates the three charges with the three axes of Q₃. It directly supports the module statement that D = 3 supports exactly three independent charges and aligns with the Recognition Science forcing of D = 3 together with the three_charges_at_D3 result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.