Fermion
plain-language theorem explainer
The declaration enumerates the twelve Standard Model fermion species as an inductive type in the Recognition Science bridge to masses. Researchers mapping particle masses to the phi-ladder via ZOf and gap functions cite it when fixing the species list for anchor-scale calculations. The definition is a direct inductive enumeration that automatically derives decidable equality, representation, and inhabited structure.
Claim. Let Fermion be the inductive type whose constructors are the twelve species $d,s,b,u,c,t,e,mu,tau,nu_1,nu_2,nu_3$, equipped with decidable equality, a representation instance, and an inhabited instance.
background
The RSBridge.Anchor module supplies the core bridge between the recognition framework and particle physics. It introduces the type Fermion for the twelve Standard Model species (six quarks, three charged leptons, three neutrinos), the charge-indexed integer map ZOf, the display function gap(F) = ln(1 + Z/phi)/ln(phi), and the anchor-scale massAtAnchor. The module states that gap(ZOf i) is the closed-form value claimed to equal the integrated RG residue at the anchor scale mu-star, with tolerance approximately 1e-6. Upstream, the definition re-uses the mu projector coefficient from Cost.Ndim.Projector and the generation torsion tau from Masses.Anchor, together with the SMVerification.Fermion enumeration.
proof idea
The declaration is an inductive definition that directly lists the twelve constructors and derives DecidableEq, Repr, and Inhabited by the deriving clause. No tactics or lemmas are applied; the structure is generated automatically by Lean.
why it matters
This enumeration is the species index used by SpectralEmergenceCert to obtain three generations from D = 3 and by FermionKineticCert to certify that fermion masses at successive phi-ladder rungs differ by exact factors of phi. It therefore supplies the concrete list required for the single-anchor phenomenology claim that integrated RG residues equal gap(ZOf i). The definition closes the interface between the Recognition Science forcing chain (T8 fixing D = 3) and the mass formula yardstick * phi^(rung - 8 + gap(Z)).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.