charge_to_axis_bijective
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the numerical values of the charges themselves.
- Does not prove invariance under the variational dynamics.
- Does not extend the bijection to any dimension other than 3.
- Does not address possible additional charges outside the Standard Model set.
Lean usage
have h : Function.Bijective charge_to_axis := charge_to_axis_bijectiveformal statement (Lean)
160theorem charge_to_axis_bijective : Function.Bijective charge_to_axis :=
proof body
Term-mode proof.
161 ⟨charge_to_axis_injective, charge_to_axis_surjective⟩
162
163/-! ## Part 5: Topological vs. Noether Conservation -/
164
165/-- A **Noether charge**: real-valued, conserved under dynamics. -/