structure
definition
def or abbrev
NumericalPredictionsCert
show as:
view Lean formalization →
formal statement (Lean)
170structure NumericalPredictionsCert where
171 deriving Repr
172
173@[simp] def NumericalPredictionsCert.verified (_ : NumericalPredictionsCert) : Prop :=
proof body
Definition body.
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