cmb_horizon
plain-language theorem explainer
cmb_horizon supplies concrete numerical values for the particle horizon at CMB formation: cosmic time 1.2e13 seconds and radius 3.6e22 meters. Cosmologists working on the horizon problem in Recognition Science would cite these to quantify the mismatch between causal patches and observed uniformity. The definition constructs the ParticleHorizon record directly and verifies positivity conditions via norm_num.
Claim. The particle horizon at cosmic microwave background formation is given by cosmic time $t = 1.2 times 10^{13}$ seconds and horizon radius $r = 3.6 times 10^{22}$ meters, with $t > 0$ and $r > 0$.
background
The module COS-004 frames the horizon problem as the tension between CMB uniformity to 1 part in 10^5 and the limited causal reach in standard Big Bang expansion. The ParticleHorizon structure encodes the maximum distance light could have traveled since the Big Bang via the integral form $d_H(t) = a(t) int_0^t c dt'/a(t')$, instantiated here at $z sim 1100$ where the horizon spans roughly 1.2 million light years while the observable sky is far larger. Upstream results supply supporting structures such as nuclear density tiers from NucleosynthesisTiers and ledger factorization from DAlembert, but the present definition focuses on numerical scale-setting rather than derivation.
proof idea
One-line wrapper that directly constructs the ParticleHorizon record with the supplied time and radius literals, then applies norm_num to discharge the two positivity fields.
why it matters
This definition anchors the numerical scale for the horizon problem statement in the module, which contrasts the small causal horizon against full-sky uniformity and motivates the 8-tick synchronization alternative to inflation. It supplies the concrete values referenced by sibling declarations such as horizon_problem_stated and complementary_explanation. The placement ties directly to the T7 eight-tick octave landmark, where the universal clock enforces homogeneity as a ledger consistency condition without requiring light-speed communication.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.