particleHorizonModel
plain-language theorem explainer
Constructor for the particle-horizon instance of a cosmological horizon model: positive comoving radius r and integer rung count s, marked causally accumulated and free of future information. Cosmologists comparing vacuum-energy rung counts cite it as the ledger-compatible horizon. The body is a pure structure literal fixing the two Boolean flags and the HorizonType tag.
Claim. Given a comoving radius $r > 0$ and an integer rung count $s$, form the horizon model whose type is the particle horizon, with that radius and rung count, flagged as causally accumulated and as not requiring future information.
background
The module forces which cosmological horizon enters the vacuum-energy formula $\rho_\Lambda = \rho_{\mathrm{Pl}},\varphi^{-2s}$. Three candidates (particle horizon, Hubble radius, de Sitter event horizon) give different rung counts $s$ and therefore different $\rho_\Lambda$; only the particle horizon matches observation near unity.
A HorizonModel packages type tag, positive comoving radius, rung count from the substrate scale, and two Boolean diagnostics: whether the horizon is the accumulated past light-cone, and whether it needs future data. The causal-accumulation principle states that the recognition ledger sums only over cells that have already exchanged a comparison, so the relevant boundary is the maximal past-connected set.
Upstream, past from TimeEmergence is the set of committed ledger snapshots at earlier ticks; that notion of past contact is what "causally accumulated" encodes here.
proof idea
Definitional structure literal, not a proof. It fills HorizonModel by setting horizonType to particleHorizon, copying the supplied radius and positivity witness, storing the rung count, and hard-coding isCausallyAccumulated := true and requiresFutureInfo := false. No lemmas are applied.
why it matters
This is the positive instance the module's selection theorems compare against the Hubble and de Sitter models. The module doc identifies the particle horizon (~46 Gly, $s=294$) as the unique match to observed vacuum density under causal accumulation: the ledger cost is the ground state over the maximal past-connected region, whose boundary is the particle horizon by definition.
Sibling facts (causal_accumulation_selects_particle_horizon, exclusions of Hubble and de Sitter) use this constructor as the canonical "good" model. It sits in the cosmology layer that feeds RS vacuum-energy numerics on the $\varphi$-ladder, not in the T0–T8 forcing chain itself, but it operationalizes the ledger's past-only discipline at cosmological scales.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.