total_fermions_eq_12
plain-language theorem explainer
The theorem asserts that the total fermion count equals twelve in the Recognition Science particle spectrum. Physicists deriving Standard Model generations from the RS forcing chain would cite this to confirm the 3-by-4 structure matches the cube-edge count. The proof is a direct decision procedure that evaluates the product definition of totalFermions.
Claim. In the Recognition Science model the total number of fermions satisfies $totalFermions = generationCount × fermionsPerGeneration = 12$.
background
The module shows that three generations arise because the number of generations equals the spatial dimension D forced at T8. Each generation contains four fermions (up-type, down-type, charged lepton, neutrino), so the product is twelve. The upstream definition totalFermions := generationCount * fermionsPerGeneration supplies the arithmetic that the theorem evaluates.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the equality after the definition of totalFermions is unfolded.
why it matters
This equality supplies the total_12 field inside the GenerationCert structure that certifies the full fermion generation pattern. It closes the geometric link between D = 3, the eight-tick octave, and the twelve Weyl fermions counted as cube edges. The result therefore sits at the interface between the T8 dimension step and the explicit particle content of the Standard Model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.