quarkDoublet
plain-language theorem explainer
The declaration sets quarkDoublet to the natural number 2, encoding the two-component isospin doublet of up and down quarks in the weak sector. Workers on Recognition Science derivations of electroweak structure reference it when counting left-handed fermion representations that arise from 3D ledger geometry. The entry is introduced by direct constant assignment with no reduction steps or external lemmas.
Claim. The quark isospin doublet $(u,d)$ is assigned the dimension $2$.
background
The module derives the weak force from Recognition Science ledger geometry. SU(2)_L symmetry emerges from the three generators of 3D rotations, chiral coupling follows from the orientation of the eight-tick cycle, and massive mediators arise from the J-cost minimum at phi. The module lists weak isospin doublets such as (νe, e−) and (u, d) among its predictions.
proof idea
Direct constant definition that assigns the value 2.
why it matters
The definition supplies the quark representation count required by the weak-force emergence derivation (P-019). It supports the module's enumeration of left-handed doublets that couple to the SU(2) generators obtained from the 3D ledger. No downstream theorems are recorded, so the entry functions as a fixed input to the overall doublet tally.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.