doublet_from_isospin
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the Fermi constant or boson masses.
- Does not address quark mixing or the CKM matrix.
- Does not detail the Higgs mechanism or J-cost minimization.
formal statement (Lean)
213theorem doublet_from_isospin : leptonDoublet = 2 := rfl
proof body
Term-mode proof.
214
215/-! ## Decay Processes -/
216
217/-- Beta decay: n → p + e⁻ + ν̄e via W⁻. -/