fermionsPerGeneration
plain-language theorem explainer
fermionsPerGeneration is defined as the constant 4, encoding the four Weyl fermions (up, down, charged lepton, neutrino) per generation via the 2² structure in F₂² space. Researchers deriving Standard Model generations from Recognition Science spatial dimensions cite it when computing the total of 12 fermions. The definition is introduced by direct constant assignment with an explanatory comment on its F₂ origin.
Claim. The number of Weyl fermions per generation is defined as the natural number 4, corresponding to the structure 2² in F₂² space.
background
The module derives three generations of fermions from Recognition Science by identifying the generation count with spatial dimension D, which equals the number of cube face-pairs. Each generation is assigned four fermions (up-type, down-type, charged lepton, neutrino) so that 3 × 4 = 12 matches the cube-edge count. This local definition of fermionsPerGeneration as 4 sits alongside an upstream definition in FermionKineticCert that instead sets the same name to 15 via the structural count 5 EW sectors × 3 colors.
proof idea
The declaration is a direct constant definition assigning the value 4, accompanied only by a comment noting its origin as 2² from F₂² space. No lemmas or tactics are invoked; it functions as a foundational constant for the module's subsequent equality and total-count definitions.
why it matters
This definition supplies the per-generation count used by totalFermions and the theorem fermions_per_gen_eq_4, which together close the module's counting argument that 12 fermions equal the cube edges. It fills the explicit step in the Recognition Science derivation of three generations from D = 3, linking to the framework's T8 landmark on spatial dimensions and the cube structure. It leaves open the reconciliation between the 4-count here and the 15-count in the kinetic certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.