`Reheating`

definition

show as: view math explainer →

module: IndisputableMonolith.Cosmology.Inflation
domain: Cosmology
line: 161 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Cosmology.Inflation on GitHub at line 161.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 158
 159/-- After inflation ends, the inflaton oscillates around φ = 1
 160    and decays into Standard Model particles. -/
 161structure Reheating where
 162  /-- Reheating temperature. -/
 163  temperature : ℝ
 164  /-- Temperature is positive. -/
 165  temp_pos : temperature > 0
 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)

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.