genOf_hyp
plain-language theorem explainer
This definition extends the standard generation index to a hypothetical fourth-generation fermion by mapping the sterile neutrino constructor to the extra slot in Fin 4. Modelers of neutrino spectra under the Recognition Science three-generation assumption would cite it when stating the surjectivity failure. The implementation is a direct pattern match on the HypotheticalFermion inductive that delegates ordinary cases to the upstream genOf.
Claim. Let $f$ range over the inductive type of hypothetical fermions (standard fermions plus the extra constructor for a fourth-generation sterile neutrino). Define $g(f) : Fin 4$ by $g(f) = 3$ when $f$ is the sterile neutrino of generation 4, and $g(f)$ equal to the standard generation index of $f$ (an element of Fin 3) otherwise.
background
The module Physics.SterileExclusion records the modelling decision that only three neutrino generations are admitted, expressed by the surjectivity of genOf onto Fin 3. HypotheticalFermion is the inductive extension of the RSBridge.Fermion type that adds the single extra constructor sterile_nu4. The upstream definition genOf (appearing in both RSBridge.Anchor and Masses.RSBridge.Anchor) assigns each standard fermion a unique index in Fin 3 by rung and sector ordering: first-generation particles receive 0, second-generation receive 1, and third-generation receive 2.
proof idea
The definition proceeds by exhaustive pattern matching on the HypotheticalFermion inductive. The sterile_nu4 case returns the literal value 3 inside Fin 4. Every other case applies the upstream genOf to the underlying RSBridge.Fermion and coerces the resulting Fin 3 element into Fin 4.
why it matters
genOf_hyp supplies the extended map required by the downstream theorem no_sterile, which proves that the map cannot be surjective onto Fin 4 and thereby formalizes the module's three-generation assumption. The construction sits inside the Recognition framework's enforcement of minimality via the eight-tick octave and the phi-ladder; it touches the open modelling question of whether any fourth-generation state could be added without violating the rung ordering already fixed by genOf.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.