su2_from_3d
plain-language theorem explainer
The declaration shows that the SU(2) generator count equals three because the weak force structure arises from three-dimensional rotations in the ledger geometry. A physicist tracing gauge symmetries to the forcing chain would cite this when connecting spatial dimensions to electroweak mediators. The proof is a direct reflexivity on the definition of the generator count.
Claim. The number of generators of the SU(2) symmetry group equals three, matching the three spatial dimensions of the ledger: $N_{SU(2)} = 3$.
background
The Weak Force Emergence module derives the weak nuclear force from the Recognition Science ledger rather than postulating it. SU(2)_L gauge symmetry, which mediates the W and Z bosons, emerges from the three generators of rotations in three-dimensional space. The upstream IsospinSymmetryFromRS module defines the generator count as exactly three; the local definition repeats this value with the explicit note that these correspond to the three massive weak bosons.
proof idea
The proof is a term-mode reflexivity step on the definition of the generator count. It relies on the upstream definition from IsospinSymmetryFromRS that sets the count to three, with no further lemmas or tactics required.
why it matters
This result anchors the weak force derivation in the forcing chain at T8, where three spatial dimensions are forced. It supplies the direct link from ledger geometry to the SU(2) structure that accounts for beta decay and neutrino interactions in the P-019 derivation. The module uses it to ground the subsequent discussion of chiral coupling and short range, even though no downstream applications are yet recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.