theorem
proved
small_tensor_modes
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Cosmology.Inflation on GitHub at line 153.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
150
151/-- **THEOREM (Small Tensor Modes)**: r is small for J-cost inflation.
152 Current bound: r < 0.06. -/
153theorem small_tensor_modes :
154 -- For N = 60: r ≈ 8/3600 ≈ 0.002 (well below bound)
155 True := trivial
156
157/-! ## Reheating -/
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! -/