sterile_exclusion_assumption
plain-language theorem explainer
Researchers modelling neutrino masses on the phi-ladder cite the sterile exclusion assumption to enforce that the generation map remains non-surjective beyond three states. The declaration serves as a module-local alias imported from the physics layer. Its definition consists of a single reference to the upstream predicate.
Claim. The sterile exclusion assumption asserts that the neutrino generation map is not surjective: $¬$ (genOf is surjective).
background
In the Recognition Science masses module, assumptions are kept lightweight and phenomenological. The sterile exclusion assumption is imported as a surrogate from the physics module to document the choice that only three neutrino generations are realized via the RSBridge.genOf map onto Fin 3. This predicate appears in the upstream definition as the negation of surjectivity of genOf_hyp. It is accompanied by a mass bound requiring any sterile neutrino to exceed phi to the 20 times the coherence energy E_coh.
proof idea
One-line alias that directly references the sterile_exclusion_assumption definition from the Physics.SterileExclusion module.
why it matters
It feeds the no_sterile_of_assumption lemma, which extracts the non-surjectivity directly from the hypothesis. This supports the mass ladder by excluding extra generations, aligning with the phi-ladder rung assignments. The assumption addresses the modelling choice of whether additional sterile states appear above the phi^19 threshold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.