deSitter_requires_future
plain-language theorem explainer
Any horizon model typed as a de Sitter event horizon and flagged as needing future information cannot simultaneously carry the opposite flag. Cosmologists forcing the vacuum-energy boundary among particle, Hubble, and de Sitter candidates cite this as the formal exclusion of future-dependent horizons from the past-directed ledger. The proof is a one-line Boolean simplification from the true hypothesis.
Claim. For every cosmological horizon model $H$, if $H$ has de Sitter event-horizon type and $H$ requires future information, then it is not the case that $H$ fails to require future information.
background
The module forces which cosmological horizon bounds the vacuum ledger cost $\rho_\Lambda = \rho_{\mathrm{Pl}},\varphi^{-2s}$. Three candidates give different rung counts $s$ and different $\rho_\Lambda$: particle horizon ($s=294$, match $\sim 1$), Hubble radius ($s=289$, factor $\sim 12.7$), and de Sitter event horizon ($s=290$, factor $\sim 5.8$).
A HorizonModel packages horizon type (particle / Hubble / de Sitter), positive comoving radius, rung count from the substrate scale, and Boolean flags for causal accumulation and future-information dependence. The causal-accumulation principle says the vacuum ledger sums $\mathcal{L}(i,j)$ only over cells that have already exchanged a comparison, so the boundary must be the maximal past light-cone set: the particle horizon.
The de Sitter event horizon is the surface beyond which light emitted now never reaches the observer under eternal dark-energy domination. Its radius therefore depends on the future equation of state, not on completed causal contacts.
proof idea
Term/tactic hybrid: introduce the horizon model $H$, discard the type-equality hypothesis, and keep the Boolean hypothesis requiresFutureInfo = true. A single simp rewrite on that hypothesis discharges requiresFutureInfo ≠ false. No external lemmas are needed; the content is pure Boolean inconsistency of true with false.
why it matters
Closes the de Sitter branch of the vacuum-horizon trichotomy in Cosmology.VacuumHorizonForcing. Together with the sibling results that causal accumulation selects the particle horizon and that the Hubble radius excludes past contacts, it leaves only the particle horizon ($s=294$, $\varphi^{-588}$ suppression) as a valid ledger boundary. That selection is what makes the RS vacuum energy match observation rather than overshoot by factors of order $5$–$13$.
The module is marked structural (0 sorry, 0 RS-internal axioms). Downstream use count is currently zero; the theorem stands as a local consistency gate rather than a lemma consumed by a larger named parent. It encodes the module-doc claim that a future-dependent horizon is not a valid boundary for the past-directed recognition ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.