structure
definition
InflatonCert
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Cosmology.InflatonPotentialStructural on GitHub at line 64.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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