deSitterModel
plain-language theorem explainer
Packages the de Sitter event horizon as a cosmological horizon model: positive comoving radius r, integer rung count s, not causally accumulated, and flagged as requiring future expansion history. Cosmologists comparing vacuum-energy candidates cite it when excluding the event horizon against the particle horizon. The body is a pure structure constructor with fixed Boolean flags.
Claim. For any comoving radius $r > 0$ and any integer rung count $s$, there is a horizon model of de Sitter event-horizon type with that radius and rung count, marked as not causally accumulated and as requiring future information.
background
The module treats vacuum energy as $\rho_\Lambda = \rho_{\mathrm{Pl}} \cdot \varphi^{-2s}$, where $s$ is the $\varphi$-rung count from the substrate scale to a cosmological horizon. Three classical horizons give three answers: particle horizon ($s \approx 294$, ratio $\sim 1$), Hubble radius ($s \approx 289$, ratio $\sim 12.7$), and de Sitter event horizon ($s \approx 290$, ratio $\sim 5.8$).
A horizon model records type, positive comoving radius, rung count, whether the boundary is the maximal past-light-cone contact set (causally accumulated), and whether defining it needs future expansion history. Horizon types are the three candidates above.
The causal-accumulation principle says the vacuum ledger cost is the ground-state total over the maximal region of cells that have already exchanged a comparison. That boundary is the particle horizon by definition. The de Sitter event horizon instead depends on the entire future expansion history, so it is not an accumulated past-contact set.
proof idea
Definitional structure construction, not a proof. The fields are filled directly: type is the de Sitter event-horizon constructor; radius and positivity proof are the input $r$ and $hr$; rung count is the input integer $s$; causal-accumulation is hard-coded false; future-info requirement is hard-coded true. No lemmas are applied.
why it matters
Supplies the third of the three candidate horizon packages used by the vacuum-horizon forcing argument. The module's selection theorem chain (causal accumulation selects the particle horizon; Hubble radius excludes past contacts; de Sitter requires future) needs a uniform HorizonModel carrier so each candidate can be typed, flagged, and compared on the same $\varphi$-ladder rung count.
In the Recognition framework this sits under cosmology rather than the T0–T8 forcing chain, but it inherits the $\varphi$-ladder mass/scale bookkeeping: vacuum energy falls as $\varphi^{-2s}$ once $s$ is fixed. The de Sitter package is the explicit witness that the event horizon fails the causal-accumulation principle because it needs future information, matching the module table entry (ratio $\sim 5.8$ versus unity for the particle horizon).
No downstream theorems currently depend on this definition in the graph; it is infrastructure for the §3 selection results and any later vacuum-energy numerics that instantiate the three models side by side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.