theorem
proved
efficient_reheating
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
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