fermion_count
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not include neutrinos or any other particles.
- Does not compute or verify any mass values.
- Does not address experimental PDG comparisons.
- Assumes the listed nine species exhaust the charged fermion sector.
Lean usage
def sm_verification_cert : SMVerificationCert where all_positive := all_fermion_masses_pos phi_scaling := mass_rung_scaling nine_fermions := fermion_countformal statement (Lean)
156theorem fermion_count : Fintype.card Fermion = 9 := by native_decide
proof body
157