fermion_count
plain-language theorem explainer
The Recognition Science mass framework enumerates exactly nine fermions in its Standard Model sector. Researchers assembling the SM verification certificate cite this result to confirm the complete set of charged leptons and quarks before applying the phi-ladder mass formula. The proof proceeds by direct computation of the Fintype cardinality on the inductive Fermion definition.
Claim. The finite type of Standard Model fermions (electron, muon, tauon, up, charm, top, down, strange, bottom) has cardinality nine: $|F| = 9$.
background
The module states RS mass predictions for Standard Model particles using the law m(particle) = yardstick(Sector) × φ^(r - 8 + gap(Z)), with yardstick, rung r, and gap derived from cube geometry (D=3) and charge structure. Fermion is the inductive type whose nine constructors are exactly the charged leptons and quarks: electron, muon, tauon, up, charm, top, down, strange, bottom. This definition derives a Fintype instance, allowing direct cardinality computation. Upstream results supply analogous Fermion types in RSBridge.Anchor that include neutrinos, confirming the present enumeration deliberately excludes them.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic. This evaluates the cardinality of the derived Fintype instance directly from the nine-constructor inductive definition.
why it matters
The result supplies the nine_fermions field of the SMVerificationCert structure, which certifies the full fermion set for mass-law positivity and phi-scaling checks. It is also referenced by cubeFaceUniversalityCert when establishing six-fold counts across quark, lepton, and other domains. The count anchors the nine fermions to the D=3 cube geometry and eight-tick octave of the forcing chain before numerical PDG comparisons are performed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.