structure
definition
InflationCert
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Gravity.Inflation on GitHub at line 112.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
109
110/-! ## Certificate -/
111
112structure InflationCert where
113 alpha_derived : alpha_attractor = phi + 1
114 alpha_positive : 0 < alpha_attractor
115 spectral_ok : 0.96 < spectral_index 55 ∧ spectral_index 55 < 0.97
116 modulation_positive : 0 < Omega_0
117 curvature_bounded : (1 : ℝ) / ell0 ^ 2 = 1
118
119theorem inflation_cert : InflationCert where
120 alpha_derived := alpha_attractor_eq_phi_plus_one
121 alpha_positive := alpha_attractor_pos
122 spectral_ok := n_s_at_55
123 modulation_positive := Omega_0_pos
124 curvature_bounded := curvature_bounded_at_R0
125
126end
127
128end RSInflation
129end Gravity
130end IndisputableMonolith