def
definition
nsPlanck
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Cosmology.InflationSpectralIndexFromJCost on GitHub at line 51.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
48 rw [nsRS_val]; norm_num
49
50/-- Planck observed value 0.965 is close to RS prediction within 0.01. -/
51def nsPlanck : ℝ := 0.965
52theorem nsRS_near_planck : |nsRS - nsPlanck| < 0.015 := by
53 rw [nsRS_val]
54 unfold nsPlanck
55 rw [abs_lt]
56 constructor <;> norm_num
57
58structure SpectralIndexCert where
59 nsRS_band : (0.955 : ℝ) < nsRS ∧ nsRS < 0.957
60 nsRS_near_planck : |nsRS - nsPlanck| < 0.015
61
62def spectralIndexCert : SpectralIndexCert where
63 nsRS_band := nsRS_band
64 nsRS_near_planck := nsRS_near_planck
65
66end IndisputableMonolith.Cosmology.InflationSpectralIndexFromJCost