charge_to_axis_bijective
plain-language theorem explainer
The map sending each of the three Standard Model charges to one of the three axes of the cube Q₃ is bijective. Researchers tracing conservation laws to topological linking in D = 3 would cite this result to confirm a one-to-one correspondence between electric charge, baryon number, and lepton number and the three spatial axes. The proof is a one-line wrapper that pairs the already-proved injectivity and surjectivity statements for the same map.
Claim. The function that assigns the electric charge to axis 0, the baryon number to axis 1, and the lepton number to axis 2 of the three-dimensional cube $Q_3$ is a bijection between the set of Standard Model charges and the set of three axes.
background
In Recognition Science, conservation arises from topological linking numbers that are invariant under continuous deformation in exactly three spatial dimensions. The module defines the map that sends each Standard Model charge (electric, baryon, lepton) to a distinct face-pair axis of the cube $Q_3$. Upstream lemmas establish that this assignment is injective by exhaustive case analysis on the three charges and surjective by checking that every axis in Fin 3 is hit by exactly one charge. The local setting is the claim that topological invariants, not Noether symmetries, enforce integer-valued conservation in the ledger.
proof idea
The proof is a one-line wrapper that applies the pair constructor to the two prior theorems: charge_to_axis_injective (proved by cases on the charges) and charge_to_axis_surjective (proved by interval cases on the target axes). No additional tactics or reductions are required.
why it matters
This bijection supplies the final piece of the F-012 certificate, which states that exactly three independent charges exist only in D = 3 and correspond to the three axes of $Q_3$. It is invoked directly in the topological_conservation_certificate theorem that lists integer quantization, exact conservation along trajectories, and the requirement for D = 3. The result aligns with the framework's T8 forcing of three dimensions and the three-charge structure at the Berry threshold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.