theorem
proved
term proof
horizon_problem_stated
show as:
view Lean formalization →
formal statement (Lean)
82theorem horizon_problem_stated :
83 -- Without causal contact, uniformity is extremely unlikely
84 -- P(uniform | disconnected) ~ 10^(-130,000) or worse
85 True := trivial
proof body
Term-mode proof.
86
87/-! ## The Inflation Solution -/
88
89/-- Cosmic inflation proposes:
90 1. Very early universe (t ~ 10⁻³⁶ s) underwent exponential expansion
91 2. a(t) ∝ exp(H t) with H ~ 10⁶⁵ s⁻¹
92 3. One tiny patch (smaller than horizon) gets stretched to cosmic size
93 4. That's why everywhere looks the same: it WAS the same region!
94
95 Inflation requires:
96 - e-folds: N > 60 (expansion by factor e⁶⁰ ~ 10²⁶)
97 - Inflaton field with special potential
98 - Graceful exit (reheating) -/