generationCount
plain-language theorem explainer
generationCount fixes the number of fermion generations at exactly 3 to match the spatial dimension D. Researchers deriving Standard Model fermion counts from Recognition Science cite it when verifying the cube face-pair correspondence or computing total Weyl fermions. The definition is a direct constant assignment with no lemmas or computation.
Claim. The number of fermion generations is defined to be 3, equal to the spatial dimension $D$.
background
In the Recognition Science framework the Standard Model fermion content is obtained from the spatial dimension. Module documentation states: 'Three generations of fermions from RS — A1 SM Depth. The Standard Model has three generations of fermions. RS: 3 = D (spatial dimension) = F₂³ axes = cube face-pairs.' Each generation is assigned four fermions (up, down, charged lepton, neutrino), yielding twelve Weyl fermions that equal the number of cube edges.
proof idea
This is a direct definition that assigns the constant 3. No lemmas are applied and no tactics are used.
why it matters
The definition supplies the generation count required by the GenerationCert structure, which asserts three_generations : generationCount = 3 together with totalFermions = 12 and the cube-edge match. It realizes the module claim that three generations equal D, closing the link from forcing-chain step T8 (D = 3) to observed fermion generations. The sibling theorem generations_eq_D simply reflects the definition via rfl.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.