charge_to_axis_injective
The map sending each standard-model charge to one of the three axes of the Q3 cube is injective. Researchers tracing conservation laws to topological linking in three dimensions cite this to confirm that electric, baryon, and lepton charges occupy distinct axes. The proof is a one-line wrapper that performs case analysis on the three charge constructors and simplifies via the explicit axis assignment.
claimThe function $f: SMCharge → Fin 3$ defined by $f(electric)=0$, $f(baryon)=1$, $f(lepton)=2$ is injective.
background
The module establishes that conservation arises from topological linking numbers in D=3 rather than from continuous symmetries. Charges are treated as integer invariants preserved under continuous deformations of trajectories in the variational dynamics. The supporting definition assigns each SM charge to a distinct face-pair axis of the Q3 cube: electric to axis 0, baryon to axis 1, lepton to axis 2.
proof idea
The proof is a one-line wrapper that applies intro to obtain two charges a and b whose images coincide, then cases on both constructors and invokes simp_all on the explicit definition of the axis map to conclude a equals b.
why it matters in Recognition Science
This supplies the injectivity half of the bijection between the three SM charges and the three axes of Q3, which is used directly by the bijective theorem in the same module. It supports the claim that D=3 admits exactly three independent topological charges, consistent with the forcing chain that selects three spatial dimensions and the distinction between topological and Noether conservation.
scope and limits
- Does not prove surjectivity onto Fin 3.
- Does not derive conservation along trajectories.
- Does not compute explicit linking numbers.
- Does not extend to charges outside the standard model.
Lean usage
theorem charge_to_axis_bijective : Function.Bijective charge_to_axis := ⟨charge_to_axis_injective, charge_to_axis_surjective⟩formal statement (Lean)
151theorem charge_to_axis_injective : Function.Injective charge_to_axis := by
proof body
One-line wrapper that applies intro.
152 intro a b h; cases a <;> cases b <;> simp_all [charge_to_axis]
153