def definition def or abbrev

`mass_ladder_assumption`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  23noncomputable def mass_ladder_assumption : Prop :=

proof body

Definition body.

  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. -/

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

mass_ladder_holds in IndisputableMonolith.Masses.Basic decl_use
mass_ladder_matches_pdg in IndisputableMonolith.Masses.Basic decl_use
proton_relative_error in IndisputableMonolith.Masses.Verification decl_use

depends on (5)

Lean names referenced from this declaration's body.

Constants in IndisputableMonolith.CPM.LawOfExistence decl_use
import_measurements in IndisputableMonolith.Data.Import decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
rung_exponent in IndisputableMonolith.Masses.Basic decl_use
value in IndisputableMonolith.QFT.SpinStatistics decl_use