generations_eq_D
plain-language theorem explainer
The theorem equates the number of fermion generations to three, identified with the spatial dimension D in Recognition Science. Model builders extending the Standard Model from the Recognition framework would cite this for the structural origin of three generations. The proof is a direct reflexivity step that follows immediately from the constant definition of generationCount.
Claim. The number of fermion generations equals the spatial dimension: $N_g = 3 = D$, where $N_g$ is fixed by the Recognition Science construction to match the three spatial dimensions.
background
The module derives three generations of fermions directly from Recognition Science, identifying the generation count with spatial dimension D and with the three face-pairs of a cube. Each generation is assigned four fermions (up-type, down-type, charged lepton, neutrino), yielding twelve Weyl fermions that match the twelve edges of the cube. The upstream definition fixes generationCount as the natural number 3, explicitly annotated as equal to D.
proof idea
The proof is a one-line reflexivity wrapper. Because generationCount is defined to be exactly the constant 3, the equality holds definitionally and rfl closes the goal without further steps.
why it matters
This equality supplies the three-generations field of the downstream GenerationCert, which also records the total fermion count of twelve and the cube-edge match. It realizes the Recognition Science landmark that D equals three spatial dimensions, thereby accounting for the observed three generations within the framework. The module states that the construction contains zero sorry or axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.