pith. machine review for the scientific record. sign in
theorem

homogeneous_minimizes_cost

proved
show as:
view math explainer →
module
IndisputableMonolith.Cosmology.HorizonProblem
domain
Cosmology
line
153 · github
papers citing
none yet

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

A cached Ask Recognition explainer exists for this declaration.

open explainer

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 -/