generationCert
plain-language theorem explainer
generationCert constructs the explicit witness for the GenerationCert structure that certifies exactly three fermion generations in the Standard Model. A physicist embedding the SM inside Recognition Science would cite it to tie generational multiplicity directly to the spatial dimension D. The definition is a structure constructor that plugs the dimension-forcing equality generations_eq_D into the first field and three independent counting lemmas into the remaining fields.
Claim. Let $G$ be the structure whose fields assert that the fermion generation count equals 3, the total number of Weyl fermions equals 12, that total equals the number of cube edges, and that the cardinality of the fermion generation type is 3. Then generationCert is the term obtained by substituting the equality generation count = 3 forced by the spatial-dimension theorem together with the three counting results for the remaining fields.
background
The module states that the Standard Model has three generations of fermions and that RS identifies this number with the spatial dimension: 3 = D = F₂³ axes = cube face-pairs. Each generation contains four fermions (up, down, charged lepton, neutrino), yielding 3 × 4 = 12 Weyl fermions, which equals the number of cube edges. The upstream theorem three_generations records that D = 3 forces exactly three generations, while the sibling lemmas generations_eq_D, total_fermions_eq_12, total_fermions_eq_cube_edges and generationTypeCount supply the four concrete equalities required by the GenerationCert structure.
proof idea
The definition is a one-line structure constructor. It assigns the three_generations field to the theorem generations_eq_D, the total_12 field to total_fermions_eq_12, the cube_edge_match field to total_fermions_eq_cube_edges, and the generation_types field to generationTypeCount. No tactics or reductions are performed; the term simply packages the four already-proved equalities into the required record.
why it matters
The certificate closes the counting argument that links the observed three generations of the Standard Model to the Recognition Science forcing chain step T8 (D = 3). It sits inside the ParticlePhysicsGenerationsFromRS module whose documentation states that three generations equal the spatial dimension D and that 12 fermions equal the cube-edge count. No downstream theorems yet depend on it, but it supplies the concrete witness needed for any later derivation that treats generational multiplicity as an RS-native quantity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.