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)
137noncomputable def spectralIndex (φ : ℝ) (hφ : φ > 0) : ℝ :=
proof body
Definition body.
138 1 - 6 * slowRollEpsilon φ hφ + 2 * slowRollEta φ hφ
139
140/-- **THEOREM (Nearly Scale-Invariant Spectrum)**: n_s ≈ 1 for slow-roll.
141 Planck measures n_s = 0.965 ± 0.004. -/
used by (4)
From the project-wide theorem graph. These declarations reference this one in their body.
-
CMBObservable
in IndisputableMonolith.Physics.CosmicMicrowaveBackgroundTemperatureFromRS
decl_use
-
CosmicRayCert
in IndisputableMonolith.Physics.CosmicRaysFromPhiLadder
decl_use
-
spectralIndex
in IndisputableMonolith.Physics.CosmicRaysFromPhiLadder
decl_use
-
spectralIndexBand
in IndisputableMonolith.Physics.CosmicRaysFromPhiLadder
decl_use
depends on (6)
Lean names referenced from this declaration's body.
-
slowRollEpsilon
in IndisputableMonolith.Cosmology.Inflation
decl_use
-
slowRollEta
in IndisputableMonolith.Cosmology.Inflation
decl_use
-
slowRollEpsilon
in IndisputableMonolith.Cosmology.InflatonPotentialStructural
decl_use
-
slowRollEta
in IndisputableMonolith.Cosmology.InflatonPotentialStructural
decl_use
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
-
spectralIndex
in IndisputableMonolith.Physics.CosmicRaysFromPhiLadder
decl_use