Species
plain-language theorem explainer
Species aliases the fermionic particle type for use in certified anchor equality checks and gap residue bounds. Ablation studies and nucleosynthesis calculations cite it to keep Z-mapping and Fgap applications uniformly typed. The declaration is a direct one-line type abbreviation with no computational or proof content.
Claim. Let $F$ be the inductive type whose constructors are the six quarks $d,s,b,u,c,t$, the three charged leptons $e,mu,tau$, and the three neutrinos $nu_1,nu_2,nu_3$. The species type is defined to be exactly this $F$.
background
The AnchorPolicyCertified module supplies a certificate-based interface that replaces an earlier axiomatic treatment of Standard-Model renormalization-group residues. Instead of asserting a global equality between residue and gap(Z), the module accepts externally supplied interval tables Ires and Igap together with a validity proof; Lean then derives per-species closeness and equal-Z degeneracy bounds. The Species type supplies the common domain for these statements. Upstream, the Fermion inductive is defined in RSBridge.Anchor as the enumeration of the twelve fermions listed above; the present abbreviation simply re-exports that enumeration under the name used by the physics layer.
proof idea
The declaration is a one-line type abbreviation that directly aliases the Fermion inductive type imported from RSBridge.Anchor.
why it matters
The alias parametrizes the AnchorEq predicate and the family of ablation maps (Z_dropPlus4, Z_dropQ4, Z_break6Q) that appear in the ablation_contradictions definition. Those maps are used to show that any deviation from the original Z assignment violates the certified residue bounds. The same type is threaded through rs_lithium_insight and totalRung_pos, ensuring that the phi-ladder mass formula and the eight-tick octave structure remain consistently applied when the framework is extended to cosmology and ecology. It therefore closes the interface gap described in the module header without embedding RG kernels inside Lean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.