generationCount
plain-language theorem explainer
generationCount sets the fermion generation count to three, identified with spatial dimension D in the RS framework. Model builders working on the Standard Model within Recognition Science cite this when linking generations to cube face-pairs or computing total Weyl fermions. The definition is introduced by direct constant assignment with no computation or lemmas.
Claim. The number of fermion generations is defined as three, coinciding with the spatial dimension $D$.
background
The module ParticlePhysicsGenerationsFromRS starts from the observation that the Standard Model has three generations of fermions and equates this count with the spatial dimension D from the RS forcing chain. generationCount is the base constant in this module, set to 3 to realize the identification three generations = cube face-pair count = D. Each generation is taken to contain four fermions, yielding the total of twelve Weyl fermions that matches the cube edge count.
proof idea
Direct definition with body := 3. No lemmas or tactics are applied; the declaration is a foundational constant with zero proof obligations.
why it matters
This supplies the value three that is used in GenerationCert (three_generations : generationCount = 3), generations_eq_D, and totalFermions. It realizes the module claim that three generations equal D and the framework landmark T8 that forces D = 3 spatial dimensions from the eight-tick octave. The definition closes the link from the forcing chain to the observed three-generation fermion structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.