IndisputableMonolith.Physics.SterileExclusion
The SterileExclusion module shows that surjectivity of the generation map onto three generations rules out a fourth fermion species without violating minimality of the recognition model. Particle physicists seeking BSM constraints would cite the result to exclude sterile neutrinos. The argument rests on the HypotheticalFermion definition combined with the surjectivity hypothesis to reach a contradiction.
claimIf the generation map is surjective onto the set of three generations, then no fourth-generation fermion exists that preserves minimality of the mass ladder.
background
The module sits in the physics layer and imports the RSBridge.Anchor definitions of Fermion (the twelve Standard Model species), ZOf (charge-indexed integer), and the gap function F(Z) = ln(1 + Z/φ)/ln(φ). It also draws the mass_ladder_assumption placeholder from Masses.Assumptions. The DOC_COMMENT states the central claim: genOf surjective to Fin 3 implies no 4th gen possible without breaking minimality.
proof idea
This is a module collecting definitions and theorems on sterile exclusion; the structure centers on the HypotheticalFermion type, the genOf_hyp assumption, and the derived no_sterile statement.
why it matters in Recognition Science
The module enforces minimality in the Recognition framework by excluding extra fermion generations, directly supporting the phi-ladder mass formula and the T5 J-uniqueness step. It fills the exclusion claim stated in the module DOC_COMMENT and prepares the ground for downstream mass and anchor results even though no used_by edges are recorded yet.
scope and limits
- Does not derive numerical masses for the twelve fermions.
- Does not treat gauge bosons or scalar sectors.
- Does not incorporate direct experimental limits on sterile states.
- Does not extend the argument to non-minimal extensions of the phi-ladder.