pith. sign in
module module high

IndisputableMonolith.Cosmology.HorizonProblem

show as:
view Lean formalization →

The Cosmology.HorizonProblem module defines the particle horizon integral in RS-native units and quantifies the mismatch between causal contact at recombination and the full CMB sky. Cosmologists and RS researchers cite these definitions when contrasting standard Big Bang expansion with cost-minimization alternatives. The module builds the argument through successive definitions of horizon distance, patch angle, and patch count that culminate in an explicit problem statement.

claimThe particle horizon distance is $d_H(t) = a(t) ∫_0^t c dt'/a(t')$. At CMB recombination this yields a comoving scale of order 1.2 million light years, while the observed CMB spans a much larger angular diameter.

background

Recognition Science formulates cosmology using the J-cost functional and the phi-ladder. The module imports the fundamental RS time quantum τ₀ = 1 tick from Constants and the cost definitions from Cost. It introduces the scale factor a(t) through the standard horizon integral and contrasts the resulting causal patch size with the uniformity observed across the entire sky.

proof idea

This is a definition module with no proofs. It proceeds by defining ParticleHorizon, then cmb_horizon, causal_patch_angle, number_of_patches, and finally horizon_problem_stated, each building directly on the previous to quantify the discrepancy.

why it matters in Recognition Science

The module supplies the horizon problem statement used by downstream siblings such as homogeneous_minimizes_cost and complementary_explanation to argue that cost minimization selects homogeneity. It fills the standard horizon-problem slot in the cosmology chain, linking causal structure to the eight-tick octave and D = 3 spatial dimensions.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (15)