HorizonModel
plain-language theorem explainer
A data bundle for one cosmological horizon candidate: type tag, positive comoving radius, integer rung count on the phi ladder, and two Boolean flags (past-light-cone accumulation vs future-dependent). Cosmologists comparing particle, Hubble, and de Sitter cutoffs for the vacuum ledger cite it. Pure structure definition; no proof obligations beyond field types and positivity.
Claim. A horizon model is a record $(T, R, s, A, F)$ where $T$ is one of $\{\text{particle},\ \text{Hubble},\ \text{de Sitter event}\}$, $R > 0$ is the comoving radius in substrate units, $s \in \mathbb{Z}$ is the rung count from the substrate scale $\ell_{\mathrm{sub}}$ to radius $R$, $A$ is true iff the horizon is the accumulated past light cone, and $F$ is true iff defining the horizon needs future expansion data.
background
The module treats vacuum energy as $\rho_\Lambda = \rho_{\mathrm{Pl}} \cdot \varphi^{-2s}$, with $s$ the rung count from the substrate scale to a cosmological horizon. Three standard cutoffs give different $s$ and different $\rho_\Lambda/\rho_{\mathrm{obs}}$: particle horizon ($\sim 46,\mathrm{Gly}$, $s=294$, ratio $\sim 1$), Hubble radius ($\sim 14,\mathrm{Gly}$, $s=289$, ratio $\sim 12.7$), and de Sitter event horizon ($\sim 17,\mathrm{Gly}$, $s=290$, ratio $\sim 5.8$).
The causal-accumulation principle says the recognition ledger $\mathcal{L}(i,j)$ is defined only for substrate cells that have already exchanged a comparison, i.e. that lie in causal contact since the initial condition. The vacuum ledger cost is then the ground-state total over the maximal causally connected region; its boundary is the particle horizon by definition.
HorizonType is the three-way tag. The Boolean fields encode the two selection criteria used later: past-directed accumulation versus instantaneous Hubble flow, and independence from future expansion history (cf. the module's past/future ledger snapshots).
proof idea
No proof: this is a structure declaration. It packages five fields (type tag, positive real radius, integer rung count, two Bools) so that concrete models and selection lemmas can quantify over a single object rather than loose tuples. Downstream constructors fill the fields; selection theorems pattern-match on the Bools and the type tag.
why it matters
This is the carrier type for the vacuum-horizon forcing argument. The three constructors particleHorizonModel, hubbleRadiusModel, and deSitterModel inhabit it with the canonical flag patterns (particle: accumulated, no future; Hubble: not accumulated; de Sitter: requires future). The structural selection theorem causal_accumulation_selects_particle_horizon then takes three such models and, from the flag hypotheses alone, isolates the particle horizon as the unique valid ledger boundary.
That selection feeds the rung count $s$ into $\rho_\Lambda = \rho_{\mathrm{Pl}}\varphi^{-2s}$, explaining why the observed vacuum density tracks the particle-horizon rung ($s\approx 294$) rather than Hubble or de Sitter. Companion lemmas hubbleRadius_excludes_past_contacts and deSitter_requires_future discharge the two exclusion routes. In the broader RS chain this is cosmology-side structure sitting on the phi ladder and the past-directed ledger, not a new forcing axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.