no_sterile_of_assumption
plain-language theorem explainer
The lemma records that the sterile exclusion assumption directly forces the hypothetical fermion map genOf_hyp to miss surjectivity onto four slots. Neutrino model builders working inside Recognition Science would cite it to lock in the three-generation structure before computing mass ladders. The argument is a one-line term that returns the supplied hypothesis verbatim.
Claim. Let genOf_hyp map each hypothetical fermion to an element of the four-element set Fin 4. If the sterile exclusion assumption holds, then genOf_hyp is not surjective.
background
The SterileExclusion module encodes the modelling decision that only three neutrino generations are permitted, expressed by requiring RSBridge.genOf to be surjective onto Fin 3. Two central definitions appear: genOf_hyp, which sends the sterile candidate to the fourth slot of Fin 4 while routing the others through the existing three-generation map, and sterile_exclusion_assumption, the predicate asserting that genOf_hyp fails to be surjective. The upstream alias in Masses.Assumptions simply forwards the same predicate from the physics layer.
proof idea
The proof is a one-line term that returns the hypothesis h, which is definitionally identical to the non-surjectivity statement.
why it matters
It closes the modelling interface for the three-generation neutrino sector, ensuring downstream mass formulae on the phi-ladder remain consistent with minimality. The declaration supports the placeholder bound sterile_bound by excluding a fourth generation outright. No further parent theorems are recorded, but the step aligns with the overall forcing chain that fixes D = 3 and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.