vacuumHorizonForcingCert
plain-language theorem explainer
Canonical certificate that the vacuum-energy rung is the particle horizon: rung count 294 and exponent −588, with the algebraic check exponent = −2·rung. Cosmologists citing the causal-accumulation selection of ρ_Λ use this witness. It is a structure instance: three Boolean flags, the particle-horizon rung constant, and a one-line ring proof of the exponent identity.
Claim. There is a vacuum-horizon forcing certificate with particle horizon marked causal, Hubble-radius non-causality flag set false, de Sitter event horizon flagged as requiring future knowledge, rung count equal to the $\Lambda$CDM particle-horizon rung $294$, vacuum exponent $-588$, and the identity $\mathrm{exponent}=-2\cdot\mathrm{rung\_count}$.
background
In this module the vacuum density is written $\rho_\Lambda=\rho_{\mathrm{Pl}}\cdot\varphi^{-2s}$, where $s$ is the rung count from the substrate scale to a cosmological horizon on the $\varphi$-ladder. Three standard horizons give three answers: particle horizon ($s=294$, ratio $\sim 1$), Hubble radius ($s=289$, ratio $\sim 12.7$), and de Sitter event horizon ($s=290$, ratio $\sim 5.8$).
The causal-accumulation principle fixes the choice. 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 therefore the ground-state sum over the maximal causally connected region, whose boundary is the particle horizon by definition.
particleHorizonRungCount is the constant $294$, giving the suppression $\varphi^{-588}$. The structure VacuumHorizonForcingCert packages the three selection flags, the rung, the exponent, and the obligatory identity $\mathrm{exponent}=-2\cdot\mathrm{rung_count}$.
proof idea
Pure structure construction, not a tactic proof of a proposition. The three Boolean fields are filled with the literal values true, false, true. The rung field is the upstream definition particleHorizonRungCount ($294$). The exponent is the literal $-588$. The only proof obligation is exponent_eq: unfold the rung constant and discharge $-588=-2\cdot 294$ by ring.
why it matters
This is the concrete inhabitant that makes the vacuum-horizon forcing certificate inhabited. Downstream, vacuumHorizonForcingCert_inhabited is the one-line Nonempty witness $\langle\texttt{vacuumHorizonForcingCert}\rangle$, and the module's one-statement summary records that the particle horizon is selected by causal accumulation while Hubble and de Sitter are excluded.
In the broader RS cosmology story this pins the vacuum-energy exponent to $-588$ on the $\varphi$-ladder (mass/cost yardstick with $\varphi$-rungs), matching the observed $\rho_\Lambda$ when the ledger is summed only over the accumulated causal set. It does not itself re-prove the three horizon lemmas; it freezes their Boolean outcome and the arithmetic into a single cert value the rest of the stack can quote.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.