su2_from_3d
The declaration sets the count of SU(2) generators to three, matching the three spatial dimensions that arise from the Recognition Science forcing chain. Researchers tracing the weak force to ledger geometry would cite this when identifying the three massive bosons W⁺, W⁻, and Z⁰. The proof is a direct reflexivity step on the definition that hardcodes the generator count.
claimThe generators of SU(2) that arise from three-dimensional rotations number exactly three: $N_{SU(2)} = 3$.
background
The module derives the weak nuclear force from the Recognition Science ledger, where SU(2)_L gauge symmetry emerges directly from three-dimensional geometry. The local definition su2Generators counts these generators as three and identifies them with the three massive weak bosons W⁺, W⁻, and Z⁰. This rests on the upstream definition in IsospinSymmetryFromRS that likewise fixes su2Generators to three, confirming consistency with the spatial dimension count.
proof idea
The proof is a one-line reflexivity step that equates the defined value of su2Generators to the numeral three.
why it matters in Recognition Science
This equality anchors the weak force in the three-dimensional spatial structure (T8 of the forcing chain) that follows from J-uniqueness and the eight-tick octave. It supports the module's predictions of three weak bosons, left-handed chiral coupling, and parity violation. No downstream theorems depend on it in the current graph.
scope and limits
- Does not derive boson masses or the Higgs mechanism.
- Does not compute the Fermi constant or interaction range.
- Does not establish the full electroweak gauge group structure.
- Does not address quark or lepton mixing matrices.
formal statement (Lean)
70theorem su2_from_3d : su2Generators = 3 := rfl
proof body
Term-mode proof.
71
72/-- Weak bosons = SU(2) generators. -/