leptonDoublet
leptonDoublet assigns the natural number 2 to represent the cardinality of the left-handed lepton pair. Electroweak model builders in Recognition Science cite it when fixing the weak isospin doublet structure that follows from three-dimensional ledger geometry. The definition is a direct constant assignment requiring no computation or lemmas.
claimThe lepton doublet consisting of the electron neutrino and the electron has cardinality 2.
background
The module derives the weak force from ledger geometry, with SU(2)_L emerging from three spatial dimensions and chiral coupling from the orientation of the eight-tick cycle. The lepton doublet is the left-handed pair participating in weak interactions, sized consistently with isospin 1/2. The upstream Quark inductive type in CubeFaceUniversality supplies the parallel six-flavor structure for quarks, confirming the same doublet pattern across fermion sectors.
proof idea
The definition is a direct constant assignment of the natural number 2.
why it matters in Recognition Science
This supplies the numerical size used by the downstream theorem doublet_from_isospin, which states 2I + 1 = 2 for I = 1/2. It anchors the weak-force predictions of massive W and Z bosons, parity violation, and short range arising from the J-cost minimum at phi within the eight-tick octave and D = 3 framework. The definition closes the interface between the 3D ledger and the observed fermion doublets listed in the module predictions.
scope and limits
- Does not derive the value 2 from the forcing chain or Recognition Composition Law.
- Does not list explicit particle fields or charge assignments.
- Does not address CKM mixing or higher-generation doublets.
- Does not compute masses or coupling strengths.
Lean usage
theorem doublet_size : leptonDoublet = 2 := rflformal statement (Lean)
90def leptonDoublet : ℕ := 2
proof body
Definition body.
91
92/-- Quark doublet: (u, d). -/