GenerationCert
plain-language theorem explainer
GenerationCert bundles the assertions that fermion generations number exactly three, total fermions equal twelve, this total matches the twelve edges of the unit cube, and the FermionGeneration type has cardinality three. A physicist deriving Standard Model content from the Recognition Science forcing chain would cite the certificate to confirm the D=3 implication. The declaration is a direct structure record of four equalities already established by sibling definitions and upstream theorems.
Claim. The certificate asserting that the generation count equals three, the total fermion count equals twelve, the total fermion count equals the unit cube edge count, and the cardinality of the three-element FermionGeneration type equals three.
background
The module derives three generations of fermions from the Recognition Science framework where spatial dimension D equals three, corresponding to the three face-pairs of the cube. Each generation has four fermions, so three generations yield twelve fermions matching the twelve edges of the unit cube. Upstream results include the theorem three_generations establishing that face_pairs 3 equals 3 and the definition of cubeEdges as 12. The FermionGeneration is defined as an inductive type with constructors first, second, and third.
proof idea
As a structure definition with no proof body, it simply declares the four fields holding the equalities generationCount = 3, totalFermions = 12, totalFermions = cubeEdges, and Fintype.card FermionGeneration = 3. These equalities are supplied by sibling definitions and upstream theorems such as three_generations and cubeEdges.
why it matters
It provides the bundled certificate used by the generationCert definition to witness the three-generation structure. This realizes the T8 step where D equals 3 forces three generations, with the total of twelve fermions aligning with the cube geometry. It leaves open the embedding of these generations into the full phi-ladder mass spectrum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.