pith. machine review for the scientific record. sign in
theorem proved term proof

efficient_reheating

show as:
view Lean formalization →

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)

 169theorem efficient_reheating :
 170    -- Oscillations around φ = 1 decay into particles
 171    True := trivial

proof body

Term-mode proof.

 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! -/

depends on (14)

Lean names referenced from this declaration's body.