IndisputableMonolith.Masses.Assumptions

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4namespace Masses
   5
   6/-!
   7# Masses Assumptions (Model Layer)
   8
   9Centralises phenomenological assumptions used by the masses modules. These
  10predicates are intentionally lightweight and sit in the `Model` portion of the
  11codebase.
  12
  13Definitions
  14* `mass_ladder_assumption` – current placeholder for the ladder audit.
  15* `sterile_exclusion_assumption` – imported from physics (surrogate).
  16
  17See `docs/Assumptions.md` §Masses for context.
  18-/
  19
  20open IndisputableMonolith
  21
  22/-- Pending surrogate: imported measurements already satisfy the ladder bound. -/
  23noncomputable def mass_ladder_assumption : Prop :=
  24  ∀ m ∈ Data.import_measurements,
  25    |m.value - Constants.phi ^ Basic.rung_exponent m.name| ≤ m.error
  26
  27/-- Alias for the physics-side sterile exclusion assumption. -/
  28abbrev sterile_exclusion_assumption : Prop :=
  29  Physics.sterile_exclusion_assumption
  30
  31end Masses
  32end IndisputableMonolith
  33