`NumericalPredictionsCert`

definition

show as: view math explainer →

module: IndisputableMonolith.Masses.NumericalPredictions
domain: Masses
line: 170 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Masses.NumericalPredictions on GitHub at line 170.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 167/-! ## Summary: all predictions in one structure -/
 168
 169/-- Master certificate: all numerical predictions are proved. -/
 170structure NumericalPredictionsCert where
 171  deriving Repr
 172
 173@[simp] def NumericalPredictionsCert.verified (_ : NumericalPredictionsCert) : Prop :=
 174  -- Alpha
 175  (137.030 < alphaInv ∧ alphaInv < 137.039)
 176  -- Gravity (κ = 8φ⁵)
 177  ∧ (85.6 < 8 * phi ^ 5 ∧ 8 * phi ^ 5 < 90.4)
 178  -- Planck (ℏ = φ⁻⁵)
 179  ∧ ((0.088 : ℝ) < hbar ∧ hbar < (0.093 : ℝ))
 180  -- Mass ratios
 181  ∧ (17 < phi ^ 6 ∧ phi ^ 6 < 18)    -- generation step
 182  ∧ (29 < phi ^ 7 ∧ phi ^ 7 < 30)    -- neutrino ratio
 183  ∧ (198 < phi ^ 11 ∧ phi ^ 11 < 200) -- quark/lepton ratio
 184  -- Phi itself
 185  ∧ (1.61 < phi ∧ phi < 1.62)
 186
 187@[simp] theorem NumericalPredictionsCert.verified_any (c : NumericalPredictionsCert) :
 188    NumericalPredictionsCert.verified c := by
 189  refine ⟨⟨alphaInv_gt, alphaInv_lt⟩,
 190         kappa_bounds,
 191         hbar_bounds,
 192         phi_pow_6_bounds,
 193         neutrino_squared_mass_ratio,
 194         phi_pow_11_bounds,
 195         ⟨phi_gt_onePointSixOne, phi_lt_onePointSixTwo⟩⟩
 196
 197end
 198end NumericalPredictions
 199end Masses
 200end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.