IndisputableMonolith.Masses.Assumptions
This module supplies surrogate assumptions for the mass ladder bound and sterile neutrino exclusion. It asserts that imported measurements satisfy the phi-ladder bound and that only three neutrino generations are available. Mass modelers building charged-lepton ladders and neutrino physicists would cite it to close gaps in phi-ladder calculations. The module contains no proofs and functions as a placeholder declaration.
claimThe module declares the assumption that imported measurements satisfy the $phi$-ladder bound for masses and the assumption that the generation map is surjective onto three generations for neutrinos.
background
Recognition Science derives particle masses from the phi-ladder using the J-cost function and defect distances under the Recognition Composition Law. This module in the Masses domain supplies pending surrogates, as its doc-comment states: imported measurements already satisfy the ladder bound. It introduces two assumptions for charged-lepton modeling and neutrino generation limits while importing only Mathlib for basic structures.
proof idea
This is a definition module, no proofs. It declares two assumptions as hypotheses for use in downstream mass and physics modules.
why it matters in Recognition Science
This module feeds the charged-lepton ladder surrogate model and the sterile neutrino exclusion assumption documenting that only three neutrino generations are available. It supports the mass formula on the phi-ladder by providing the bound surrogate and closes the modeling choice for neutrino generations in the framework.
scope and limits
- Does not derive the ladder bound from the unified forcing chain.
- Does not compute explicit mass values using the yardstick and rung formula.
- Does not prove the surjectivity onto three generations from first principles.
- Does not extend to more than three neutrino generations or their mass hierarchies.