totalFermions
plain-language theorem explainer
totalFermions defines the total Weyl fermion count as the product of the generation count and the number of fermions per generation. A researcher deriving Standard Model particle content from Recognition Science would cite this when confirming the 12-fermion total that follows from D=3. The definition is realized as a direct multiplication of the two constants fixed by the spatial dimension and the F₂² structure.
Claim. Let $N_g$ be the number of generations and $n_f$ the number of Weyl fermions per generation. The total number of fermions is defined as the product $N = N_g n_f$.
background
The module derives the three generations of fermions in the Standard Model from Recognition Science. The number of generations equals the spatial dimension D, fixed at 3, while each generation contains four Weyl fermions corresponding to the two-dimensional F₂² space. The module documentation states that three generations equal the cube face-pair count and that 3 times 4 yields 12 Weyl fermions, half of the 15 including right-handed states.
proof idea
The declaration is a one-line definition that multiplies generationCount by the local fermionsPerGeneration.
why it matters
This definition supplies the total fermion count certified in GenerationCert to equal 12 and to match the number of cube edges. It implements the counting step that follows from T8 (D=3) and the eight-tick octave. The downstream theorems total_fermions_eq_12 and total_fermions_eq_cube_edges rely on it to establish the equality to 12 and to cubeEdges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.