IndisputableMonolith.Masses.Assumptions
The module supplies surrogate assumptions that imported measurements satisfy the ladder bound in the Recognition Science masses framework. It is imported by the charged-lepton ladder model and the sterile neutrino exclusion model. This is a definition module with no proofs, acting as a placeholder for data integration.
claimAssumption that imported measurements satisfy the ladder bound on the phi-ladder, together with the modeling choice of three neutrino generations.
background
The module belongs to the Masses domain. It documents pending surrogates for the ladder bound used in mass calculations within Recognition Science. The theoretical setting assumes that real-world measurements already fit within the phi-ladder without explicit verification here. The doc comment states: Pending surrogate: imported measurements already satisfy the ladder bound. It imports only Mathlib and has no upstream dependencies.
proof idea
this is a definition module, no proofs
why it matters in Recognition Science
This module feeds the charged-lepton ladder surrogate model in Masses.Basic and the sterile neutrino exclusion assumption in Physics.SterileExclusion. The latter documents the modelling choice that only three neutrino generations are available via RSBridge.genOf surjective onto Fin 3.
scope and limits
- Does not verify the ladder bound against explicit measurements.
- Does not define the mass formulas or phi-ladder itself.
- Does not prove the assumptions; they remain modeling choices.