Species
plain-language theorem explainer
The particle species type enumerates the canonical inputs to the rung constructor as fermions from the RS bridge fermion type together with the W, Z, and Higgs bosons. Researchers constructing Z-maps or running ablation checks on anchor equality cite this enumeration to index the mass assignments. The declaration is a direct inductive definition that introduces the four constructors with no further reduction steps.
Claim. The particle species type is defined inductively by the constructors fermion($f$) for $f$ ranging over the RS bridge fermion type, together with the three constants $W$, $Z$, and $H$.
background
In the rung constructor module the species type serves as the discrete index set for maps that assign rung offsets and gaps on the phi-ladder. Its sibling Sector type supplies the five identifiers lepton, neutrino, up-quark, down-quark, and electroweak, with the explicit remark that neutrinos carry baseline zero while leptons carry baseline two. Upstream the shifted cost function satisfies $H(x)=J(x)+1$, converting the recognition composition law into the d'Alembert equation $H(xy)+H(x/y)=2H(x)H(y)$.
proof idea
The declaration is an inductive definition that directly introduces the four constructors without invoking any lemmas or tactics. It is used as the domain type for the subsequent Z and tildeQ maps that appear in the ablation predicates.
why it matters
This enumeration supplies the fixed domain for the Z-map inside the ablation module, enabling the AnchorEq predicate and the three contradiction statements collected in ablation_contradictions. It anchors the species-specific rung assignments required by the mass formula yardstick times phi to the power of rung offset, and it feeds the lithium insight and extinction-cascade calculations downstream. The definition closes the enumeration step in the T5-T8 forcing chain for the mass sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.