sterile_exclusion_assumption
plain-language theorem explainer
Recognition Science encodes the three-neutrino-generation structure by defining the assumption that the hypothetical fermion generation map fails to be surjective onto four generations. Modelers of neutrino masses cite this to exclude a sterile fourth generation without additional hypotheses. The definition consists of a direct assignment of the proposition to the negation of surjectivity for genOf_hyp.
Claim. The modeling assumption that the generation assignment $genOf_{hyp} : HypotheticalFermion → Fin 4$ is not surjective.
background
The module establishes the modeling choice that neutrino generations are limited to three by requiring non-surjectivity of the generation map. genOf_hyp is the function that assigns generations in Fin 4, placing the sterile neutrino candidate at index 3 while mapping others via the RSBridge.genOf to Fin 3. This assumption is aliased in Masses.Assumptions for integration with mass formulas on the phi-ladder. The upstream result from genOf_hyp defines the attempted fourth generation explicitly.
proof idea
The declaration is a one-line definition that sets sterile_exclusion_assumption to the negation of Function.Surjective applied to genOf_hyp.
why it matters
This definition supplies the central assumption for sterile neutrino exclusion, feeding directly into the lemma no_sterile_of_assumption which recovers the non-surjectivity. It implements the modeling choice documented in the module for consistency with the three-generation structure in Recognition Science. The associated mass bound for any hypothetical sterile neutrino at phi^20 E_coh aligns with the phi-ladder rung assignments and the T5 J-uniqueness in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.