homogeneous_minimizes_cost
plain-language theorem explainer
Homogeneous density configurations have strictly lower J-cost than those with a 1% density contrast. Cosmologists using Recognition Science to address the horizon problem would cite this to show uniformity is selected by cost minimization. The proof is a direct algebraic reduction that unfolds the cost definition, applies the unit and squared-form lemmas for Jcost, and verifies positivity by norm_num.
Claim. Let $J(x) = (x-1)^2/(2x)$ for $x>0$. Then $J(1) < J(1.01)$.
background
The Cosmology.HorizonProblem module frames the horizon problem as resolved by 8-tick synchronization providing universal coherence without light-speed contact. costOfInhomogeneity(δρ) is defined as Jcost(1 + |δρ|), so the theorem compares the cost at zero contrast to a small nonzero contrast. Upstream lemmas establish Jcost(1) = 0 and the explicit squared form Jcost(x) = (x-1)^2/(2x) for x ≠ 0; tick supplies the fundamental RS time quantum.
proof idea
The term proof unfolds costOfInhomogeneity, simplifies absolutes and zeros, rewrites the left side to zero via Jcost_unit0, applies Jcost_eq_sq with a non-zero guard, simplifies the absolute value on the right, and closes with norm_num to confirm the positive difference.
why it matters
The result supports the module's claim that J-cost minimization favors homogeneous initial conditions, complementing inflation by explaining why uniformity is selected in the first place. It fills the cost-minimization step in the RS solution to the horizon problem and aligns with J-uniqueness in the forcing chain. No downstream uses are recorded, leaving its integration with the full 8-tick octave and D=3 structure open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.