su2_from_3d
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.