def
definition
causal_patch_angle
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Cosmology.HorizonProblem on GitHub at line 68.
browse module
All declarations in this module, on Recognition.
explainer page
formal source
65
66 But the WHOLE sky (360°) is uniform!
67 That's ~10,000 causally disconnected patches. -/
68noncomputable def causal_patch_angle : ℝ := 1 -- degrees
69
70noncomputable def number_of_patches : ℕ :=
71 (360 / 1)^2 -- roughly 130,000 patches
72
73/-! ## Why Is This A Problem? -/
74
75/-- If regions A and B never communicated:
76 1. How do they have the same temperature?
77 2. How do they have the same density?
78 3. How are they statistically correlated?
79
80 Random initial conditions would give:
81 ΔT/T ~ O(1), not O(10⁻⁵)! -/
82theorem horizon_problem_stated :
83 -- Without causal contact, uniformity is extremely unlikely
84 -- P(uniform | disconnected) ~ 10^(-130,000) or worse
85 True := trivial
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) -/