horizon_problem_stated
plain-language theorem explainer
The horizon problem asserts that CMB uniformity to one part in 10^5 occurs across regions that remained causally disconnected under standard Big Bang expansion, with the probability of such uniformity from random initial conditions falling below 10^{-130000}. Cosmologists cite the statement when motivating either inflation or intrinsic synchronization mechanisms. The proof is a direct term reduction to the trivial proposition.
Claim. In the absence of causal contact between cosmic regions, the probability of observed uniformity satisfies $P($uniform$|$disconnected$) ≲ 10^{-130000}$.
background
Module COS-004 frames the horizon problem as the tension between observed CMB uniformity (ΔT/T ~ 10^{-5}) and the causal disconnection of distant patches in standard cosmology. Recognition Science supplies an alternative via the universal 8-tick clock, which enforces homogeneity as a ledger consistency condition without requiring light-speed signals. Upstream definitions include the shifted cost H(x) = J(x) + 1, which converts the Recognition Composition Law into d'Alembert form, and related cost-algebra structures used to quantify synchronization.
proof idea
The declaration is a one-line term proof that applies the trivial proposition to the stated claim.
why it matters
The theorem records the horizon problem that the module addresses through the eight-tick octave (T7) of the forcing chain. It precedes declarations on inflation parameters, the RS universal clock, and cost-of-inhomogeneity comparisons. The module doc states that the ledger structure enforces homogeneity as a consistency condition, leaving open whether 8-tick synchronization fully replaces inflation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.