No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
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
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (6)
Lean names referenced from this declaration's body.
-
ell0
in IndisputableMonolith.Constants
decl_use
-
ell0
in IndisputableMonolith.Constants.Derivation
decl_use
-
alpha_attractor
in IndisputableMonolith.Gravity.Inflation
decl_use
-
Omega_0
in IndisputableMonolith.Gravity.Inflation
decl_use
-
spectral_index
in IndisputableMonolith.Gravity.Inflation
decl_use
-
alpha_positive
in IndisputableMonolith.Unification.ConstantsPredictionsProved
decl_use