ParticleHorizon
plain-language theorem explainer
ParticleHorizon encodes the particle horizon as a pair of positive reals for cosmic time and light-travel radius. Cosmologists quantifying causal disconnection at CMB formation cite it to measure the scale mismatch between horizon size and observed uniformity. As a structure definition it assembles the time, radius, and positivity fields directly from the integral description of light propagation.
Claim. A particle horizon at cosmic time $t > 0$ consists of a horizon radius $r > 0$ equal to the maximum distance light can travel from the Big Bang, $d_H(t) = a(t) ∫_0^t c dt'/a(t')$.
background
The module frames the horizon problem inside Recognition Science: the CMB is uniform to one part in 10^5, yet standard Big Bang cosmology leaves distant patches causally disconnected. The 8-tick clock supplies universal synchronization without light-speed signals, enforcing homogeneity as a ledger consistency condition. The particle horizon is introduced via its standard integral form. Upstream results supply a unit neighborhood radius from cellular automata and a dominant-strategy incentive theorem from mechanism design; both anchor the broader ledger and cost framework used throughout the cosmology development.
proof idea
Structure definition that directly bundles the four fields: cosmic time, horizon radius, and the two positivity propositions. No lemmas or tactics are applied; the declaration is a pure data constructor with embedded constraints.
why it matters
Supplies the typed object instantiated by cmb_horizon to exhibit the numerical discrepancy at z ~ 1100. It fills the setup step of COS-004 before the 8-tick synchronization argument is introduced. The declaration therefore anchors the claim that homogeneity follows from the universal T7 eight-tick octave rather than from exponential expansion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.