doublet_from_isospin
plain-language theorem explainer
The declaration establishes that the lepton doublet size equals 2, matching the weak isospin doublet for I = 1/2. Physicists deriving SU(2)_L representations from ledger geometry would cite this when linking Recognition Science to chiral fermion structure. The proof is a direct reflexivity step on the definition of the lepton doublet.
Claim. The lepton doublet size satisfies $2I + 1 = 2$ for weak isospin $I = 1/2$.
background
The Weak Force Emergence module derives the weak interaction from 3D ledger geometry that produces SU(2) symmetry with three generators. Chirality and parity violation arise from the orientation of the eight-tick cycle. The lepton doublet is defined directly as the pair consisting of the electron neutrino and electron, with its cardinality fixed at 2. Upstream results supply the explicit definition of this doublet cardinality together with topological counts (wallpaper groups) used in mass derivations.
proof idea
The proof is a one-line reflexivity step that applies the definition of the lepton doublet.
why it matters
This anchors the weak isospin doublet structure inside the Recognition Science derivation of the weak force. It supports emergence of SU(2)_L from the eight-tick octave and D = 3 spatial dimensions, feeding predictions of left-handed coupling and massive W and Z bosons. The result closes a direct link from the phi-forcing chain to electroweak representations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.