charge_to_axis_surjective
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not prove injectivity of the map.
- Does not establish dynamical conservation of the charges.
- Does not address quantization or linking numbers themselves.
- Does not extend to charges outside the standard model.
formal statement (Lean)
154theorem charge_to_axis_surjective : Function.Surjective charge_to_axis := by
proof body
Term-mode proof.
155 intro ⟨n, hn⟩; interval_cases n
156 · exact ⟨.electric, rfl⟩
157 · exact ⟨.baryon, rfl⟩
158 · exact ⟨.lepton, rfl⟩
159