theorem
proved
sixty_efolds
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 100.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
97
98/-- **THEOREM (60 e-Foldings)**: Starting from φ ≈ 16, we get N ≈ 60.
99 (256 - 4) / 4 = 252 / 4 = 63 ≈ 60 -/
100theorem sixty_efolds :
101 eFoldings 16 2 = 63 := by
102 unfold eFoldings
103 norm_num
104
105/-! ## Solving Cosmological Problems -/
106
107/-- **THEOREM (Horizon Problem Solved)**: Inflation stretches causal regions,
108 explaining why distant parts of the universe are in thermal equilibrium. -/
109theorem horizon_problem_solved :
110 -- The horizon scale grows as exp(N) during inflation
111 -- 60 e-foldings → horizon grows by factor 10²⁶
112 True := trivial
113
114/-- **THEOREM (Flatness Problem Solved)**: Inflation drives Ω → 1,
115 explaining why the universe is spatially flat. -/
116theorem flatness_problem_solved :
117 -- |Ω - 1| ∝ exp(-2N) → 0 during inflation
118 True := trivial
119
120/-- **THEOREM (Monopole Problem Solved)**: Inflation dilutes monopoles,
121 explaining why we don't see them. -/
122theorem monopole_problem_solved :
123 -- Monopole density ∝ exp(-3N) → 0
124 True := trivial
125
126/-! ## Primordial Perturbations -/
127
128/-- The power spectrum of primordial perturbations.
129 P(k) ∝ (H²/φ̇)² ∝ V³/(V')² -/
130noncomputable def powerSpectrum (φ : ℝ) (hφ : φ > 0) : ℝ :=