theorem
proved
spectralIndex_band
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Cosmology.InflatonPotentialStructural on GitHub at line 60.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
57 exact div_pos one_pos (pow_pos phi_pos 5)
58
59/-- n_s - 1 = -2/45 gives n_s ∈ (0.955, 0.957). -/
60theorem spectralIndex_band :
61 ((0.955 : ℝ) < 1 - 2/45) ∧ (1 - 2/45 < (0.957 : ℝ)) := by
62 refine ⟨?_, ?_⟩ <;> norm_num
63
64structure InflatonCert where
65 five_regimes : Fintype.card InflatonRegime = 5
66 efolds : efoldCount = 44
67 phi5_fibonacci : phi ^ 5 = 5 * phi + 3
68 epsilon_pos : 0 < slowRollEpsilon
69 eta_pos : 0 < slowRollEta
70 spectral_index_in_band : ((0.955 : ℝ) < 1 - 2/45) ∧ (1 - 2/45 < (0.957 : ℝ))
71
72noncomputable def inflatonCert : InflatonCert where
73 five_regimes := inflatonRegime_count
74 efolds := efoldCount_eq
75 phi5_fibonacci := phi5_eq
76 epsilon_pos := slowRollEpsilon_pos
77 eta_pos := slowRollEta_pos
78 spectral_index_in_band := spectralIndex_band
79
80end IndisputableMonolith.Cosmology.InflatonPotentialStructural