theorem
proved
homogeneous_minimizes_cost
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Cosmology.HorizonProblem on GitHub at line 153.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
150 Jcost (1 + abs δρ) -- Cost increases with density contrast
151
152/-- **THEOREM**: Homogeneous configurations minimize J-cost. -/
153theorem homogeneous_minimizes_cost :
154 costOfInhomogeneity 0 < costOfInhomogeneity 0.01 := by
155 unfold costOfInhomogeneity
156 simp only [abs_zero, add_zero]
157 -- J(1) < J(1.01) because J(1) = 0 and J(1.01) > 0
158 rw [Jcost_unit0]
159 -- Need: 0 < Jcost(1 + |0.01|) = Jcost(1.01)
160 rw [Jcost_eq_sq (by norm_num : (1 : ℝ) + |0.01| ≠ 0)]
161 -- (1.01 - 1)² / (2 × 1.01) = 0.0001 / 2.02 > 0
162 simp only [abs_of_pos (by norm_num : (0.01 : ℝ) > 0)]
163 norm_num
164
165/-! ## Combining Inflation and RS -/
166
167/-- Inflation and RS are complementary:
168
169 - Inflation: Explains HOW uniform regions got stretched
170 - RS: Explains WHY uniformity was favored in the first place
171
172 Together:
173 1. J-cost minimization selected homogeneous initial conditions
174 2. Inflation stretched one homogeneous patch to observable universe
175 3. 8-tick synchronization maintained coherence during expansion -/
176def complementary_explanation : List String := [
177 "RS explains why low-entropy initial state",
178 "Inflation explains stretching mechanism",
179 "Together give complete picture",
180 "J-cost constrains inflaton potential"
181]
182
183/-! ## Predictions -/