theorem
proved
efficient_reheating
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Cosmology.Inflation on GitHub at line 169.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
166
167/-- **THEOREM (Efficient Reheating)**: The inflaton couples to SM fields,
168 allowing efficient energy transfer after inflation. -/
169theorem efficient_reheating :
170 -- Oscillations around φ = 1 decay into particles
171 True := trivial
172
173/-! ## The RS Interpretation -/
174
175/-- In RS, inflation is the universe "rolling down" the J-cost landscape:
176
177 1. Initial conditions: φ >> 1 (high cost, far from equilibrium)
178 2. Slow roll: The field slowly approaches equilibrium
179 3. Exponential expansion: High J-cost drives expansion
180 4. End of inflation: φ → 1 (equilibrium, J-cost = 0)
181 5. Reheating: Oscillations transfer energy to matter
182
183 This is the universe approaching its cost-optimal state! -/
184theorem inflation_is_cost_relaxation :
185 -- Inflation = universe relaxing toward J = 0
186 True := trivial
187
188/-! ## Predictions and Tests -/
189
190/-- RS inflation predictions:
191 1. n_s ≈ 1 - 2/N ≈ 0.97 (matches Planck)
192 2. r ≈ 8/N² ≈ 0.002 (below current bounds)
193 3. Negligible non-Gaussianity (f_NL ~ 0)
194 4. Running of spectral index: dn_s/dlnk ≈ -1/N² ≈ -0.0003 -/
195structure InflationPredictions where
196 n_s : ℝ -- Scalar spectral index
197 r : ℝ -- Tensor-to-scalar ratio
198 f_NL : ℝ -- Non-Gaussianity parameter
199