doubletsPerGeneration
plain-language theorem explainer
Each fermion generation carries two weak isospin doublets in the Recognition Science ledger model of the weak force. The definition fixes this count at the natural number 2. It is cited by any calculation that assembles the full set of left-handed fermion pairs across three generations. The proof shape is a direct constant assignment with no computation or lemmas.
Claim. The number of weak isospin doublets per fermion generation is $2$.
background
The module derives the weak force from 3D ledger geometry, where SU(2)_L gauge structure arises from the three generators of spatial rotations and chirality follows from the orientation of the eight-tick cycle. The upstream structure for in UniversalForcingSelfReference records the meta-realization axioms needed for orbit and step coherence in the forcing chain. This definition supplies the per-generation multiplicity used to count the doublets (νe, e−), (u, d) and their counterparts that appear in the module predictions.
proof idea
Direct definition that assigns the constant natural number 2. No lemmas or tactics are invoked; the value is introduced as a primitive count of isospin doublets per generation.
why it matters
The definition supplies the factor that totalDoublets multiplies by three to obtain the complete doublet inventory. It fills the explicit prediction slot for weak isospin doublets listed in the module predictions. In the larger framework it rests on the D = 3 spatial dimensions and eight-tick octave that generate the SU(2) structure from the ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.