totalDoublets
plain-language theorem explainer
The definition computes the aggregate count of weak isospin doublets across three fermion generations by scaling the per-generation value. A physicist enumerating left-handed representations in the electroweak sector of Recognition Science would cite this count when tallying neutrino-electron and up-down pairs. The proof is a direct arithmetic definition that multiplies the constant 3 by the upstream per-generation doublet count of 2.
Claim. The total number of weak isospin doublets is given by $3d$, where $d=2$ denotes the number of isospin doublets per generation.
background
The Weak Force Emergence module derives the weak interaction from ledger geometry that produces SU(2) symmetry with three generators, chiral couplings from eight-tick cycle orientation, and massive mediators from the J-cost minimum at phi. Upstream results include the doubletsPerGeneration definition, which fixes two isospin doublets per generation corresponding to lepton and quark pairs. Additional dependencies on collision-free ledger properties and simplicial edge lengths supply the combinatorial substrate for counting these representations.
proof idea
This is a one-line definition that multiplies the number of generations by the per-generation doublet count supplied by the sibling definition doubletsPerGeneration.
why it matters
This definition supports the enumeration of fermion representations in the P-019 derivation of weak force predictions, including left-handed doublets for neutrinos, electrons, and quarks. It connects to the SU(2)_L structure emerging from three-dimensional ledger geometry and the eight-tick octave periodicity. No downstream uses are recorded, leaving its integration into larger electroweak calculations as an open step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.