charge_to_axis
plain-language theorem explainer
The definition assigns the electric charge to axis 0, baryon number to axis 1, and lepton number to axis 2 among the three face-pair axes of the three-dimensional cube. Researchers establishing the topological origin of conservation laws cite this map when proving that exactly three charges exist and that they stand in bijection with the axes. It is realized by exhaustive case analysis on the three constructors of the charge type.
Claim. Define the map from the set of Standard Model charges to the three axes by electric charge maps to 0, baryon number maps to 1, and lepton number maps to 2.
background
The module formalizes the claim that conservation arises from topological linking in three spatial dimensions rather than from continuous symmetries. SMCharge is the inductive type whose constructors are electric, baryon, and lepton. The three face-pair axes of the cube Q₃ supply the topological invariants whose linking numbers remain unchanged under continuous deformation of trajectories.
proof idea
Defined by direct pattern matching on the three constructors of SMCharge, returning the corresponding element of Fin 3 with bounds discharged by norm_num.
why it matters
The map is invoked by the bijective, injective, and surjective theorems that together establish the one-to-one correspondence between charges and axes. It is required by the topological conservation certificate, which records that exactly three independent charges exist only in D = 3 and that they equal the number of face pairs. The definition therefore supplies the concrete link between the F-012 registry item and the dimension-forcing result that selects D = 3 for non-trivial linking.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.