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)
38noncomputable def slowRollEpsilon : ℝ := 1 / (2 * phi ^ 5)
proof body
Definition body.
39
40/-- Slow-roll parameter η = 1/φ⁵. -/
used by (5)
From the project-wide theorem graph. These declarations reference this one in their body.
-
slowRollEpsilon
in IndisputableMonolith.Cosmology.Inflation
decl_use
-
spectralIndex
in IndisputableMonolith.Cosmology.Inflation
decl_use
-
tensorScalarRatio
in IndisputableMonolith.Cosmology.Inflation
decl_use
-
InflatonCert
in IndisputableMonolith.Cosmology.InflatonPotentialStructural
decl_use
-
slowRollEpsilon_pos
in IndisputableMonolith.Cosmology.InflatonPotentialStructural
decl_use
depends on (1)
Lean names referenced from this declaration's body.