def
definition
gap45
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Cosmology.InflationSpectralIndexFromJCost on GitHub at line 32.
browse module
All declarations in this module, on Recognition.
explainer page
formal source
29namespace IndisputableMonolith.Cosmology.InflationSpectralIndexFromJCost
30
31/-- Gap-45 = body-plan ceiling = 45. -/
32def gap45 : ℕ := 45
33
34/-- RS spectral index: n_s = 1 - 2/gap45. -/
35noncomputable def nsRS : ℝ := 1 - 2 / (gap45 : ℝ)
36
37theorem nsRS_val : nsRS = 1 - 2 / 45 := by
38 unfold nsRS gap45; norm_cast
39
40theorem nsRS_lt_one : nsRS < 1 := by
41 unfold nsRS gap45; norm_num
42
43theorem nsRS_gt_zero : nsRS > 0 := by
44 unfold nsRS gap45; norm_num
45
46/-- n_s_RS ∈ (0.955, 0.957). -/
47theorem nsRS_band : (0.955 : ℝ) < nsRS ∧ nsRS < 0.957 := by
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