fermionsPerGeneration
plain-language theorem explainer
Recognition Science defines the number of Weyl fermions per generation as fifteen, obtained by multiplying five electroweak sectors by three color copies. Researchers deriving the fermion kinetic Lagrangian or the phi-ladder mass spectrum in the QRFT module cite this count when assembling the FermionKineticCert structure. The definition is a direct structural assignment with no computation or proof steps required beyond the constant value.
Claim. The number of Weyl fermions per generation is defined to be $15$.
background
In the Fermion Kinetic Sector module the standard-model Lagrangian is reinterpreted on the recognition lattice: the mass term becomes J-cost on the fermion recognition ratio while the derivative term becomes the lattice derivative on H_RS. Fermion masses are predicted to lie on the phi-ladder via the relation m_k = m_0 phi^k, reproducing the observed spectrum from the mass-ratio modules already established upstream. The module states that the standard model contains fifteen Weyl fermions per generation and obtains this number as five electroweak sectors each carrying three color copies, consistent with D=3 spatial dimensions.
proof idea
The declaration is a direct constant definition that sets the value to 15. A companion theorem in the same module unfolds the definition and reduces the equality to 5 * 3 by reflexivity.
why it matters
This definition supplies the fermion multiplicity required by the FermionKineticCert structure, which records the equality to 5 * 3 together with positivity and phi-ratio scaling of the mass function. It completes the structural count for the fermion kinetic sector, aligning with the Recognition Composition Law and the forcing chain that yields D=3. The same count appears in totalFermions and fermions_per_gen_eq_4 in the generations module, where a parallel definition assigns the value 4 for the F_2^2 space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.