IndisputableMonolith.Physics.SterileExclusion
The SterileExclusion module shows that surjectivity of the generation map genOf onto three generations rules out a fourth fermion generation or sterile states without violating minimality. BSM model builders would cite it when deriving upper bounds on sterile neutrino masses or extra generations. The structure proceeds by introducing a hypothetical fourth fermion and deriving a direct contradiction with the imported surjectivity condition.
claimIf the generation map is surjective onto the set of three generations, then no hypothetical fourth-generation fermion exists without violating minimality.
background
This module sits in the Physics layer and imports the core bridge from RSBridge.Anchor, where Fermion denotes the twelve Standard Model species, ZOf assigns the charge-indexed integer Z_i = q̃² + q̃⁴ (+4 for quarks), and gap(F) = ln(1 + Z/φ)/ln(φ) supplies the display function used for the phi-ladder. It also pulls in the lightweight mass_ladder_assumption from Masses.Assumptions as the central phenomenological predicate. The local definitions introduce HypotheticalFermion together with predicates that enforce exclusion once genOf is assumed surjective onto Fin 3.
proof idea
This is a definition module whose main theorems are one-line wrappers that apply the surjectivity assumption imported from the anchor bridge to the hypothetical-fermion predicate, immediately yielding the no_sterile and sterile_bound statements.
why it matters in Recognition Science
The module closes a potential loophole for extra generations that would otherwise require adjustments to the phi-ladder mass formula and the eight-tick octave structure. It supports the minimality claim that feeds the forcing chain steps fixing D = 3 and the observed fermion spectrum.
scope and limits
- Does not establish surjectivity of genOf.
- Does not treat scalar or vector extensions.
- Does not derive numerical mass bounds.
- Does not address mixing or oscillation data.