Pith. sign in
module module moderate

IndisputableMonolith.Cosmology.HorizonProblem

show as:
view Lean formalization →

Formalizes the classical CMB horizon problem and an RS-native alternative: a universal clock plus cost minimization that favors homogeneity without inflation. Cosmologists comparing inflationary e-folds to Recognition synchronization would cite it. The module defines particle horizons, patch counts, inflation parameters, and cost-of-inhomogeneity lemmas side by side.

claimThe particle horizon is $d_H(t)=a(t)\int_0^t c\,dt'/a(t')$. At CMB last scattering, $d_H$ is far smaller than the observed sky, so many causally disconnected patches appear. The module states that problem, records standard inflation parameters that solve it by superluminal early expansion, and defines an RS alternative: a universal clock, a synchronization mechanism, and a cost of inhomogeneity minimized by a homogeneous configuration.

background

In standard FLRW cosmology the particle horizon bounds the comoving region that light can have crossed since $t=0$. With $c$ restored only for clarity, $d_H(t)=a(t)\int_0^t c,dt'/a(t')$. At recombination ($t\sim 3.8\times 10^5,\mathrm{yr}$) this scale is only about $1.2$ million light years, while the CMB covers $4\pi$ steradians, implying $\sim 10^4$ or more causally disconnected patches of nearly identical temperature.

The classical fix is inflation: a brief epoch of accelerated expansion that stretches one pre-horizon patch across the whole observable sky. This module imports RS constants (including the fundamental tick $\tau_0$) and the $J$-cost infrastructure so it can state both the textbook horizon problem and a Recognition-side account that does not rely on that epoch.

Sibling definitions cover the geometric objects (particle horizon, CMB horizon scale, causal-patch angle, number of patches), a statement of the problem, inflation parameter packs, an RS universal clock, a synchronization mechanism, and a cost-of-inhomogeneity functional whose minimizer is the homogeneous configuration.

proof idea

Definition-and-statement module rather than a single theorem. It introduces ParticleHorizon and evaluates it at CMB time, derives the causal-patch angle and patch count that quantify the classical puzzle, packages standard inflation parameters as one resolution path, then defines the RS clock, synchronization mechanism, and cost-of-inhomogeneity objects. Homogeneity-minimizes-cost and complementary-explanation results sit at the end as the RS-side closure of the same narrative. No deep tactic proof is the point; the structure is parallel formalization of two explanations.

why it matters in Recognition Science

Places the horizon problem inside the Recognition cosmology layer so later work can cite a single module for both the classical statement and the RS alternative. Downstream consumers (none linked yet in the graph) would use the patch-count and cost lemmas when arguing that eight-tick synchronization plus $J$-cost preference for homogeneity can replace inflationary initial conditions. The cost side ties to the global $J$-uniqueness and RCL landmarks: once cost of spatial mismatch is well-defined, the homogeneous sky is the unique minimizer rather than an anthropic accident. Complements the forcing chain's discrete time structure ($\tau_0$, eight-tick octave) by giving it a cosmological reading.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (15)