VacuumHorizonForcingCert
plain-language theorem explainer
Certificate bundle packing the three horizon-selection flags, the particle-horizon rung count, and the vacuum-energy exponent with the forced relation exponent = -2·rung_count. Cosmologists citing the vacuum-horizon forcing argument use it as the typed witness that causal accumulation selects the particle horizon. As a structure definition there is no proof body; inhabitants supply the concrete Booleans and integers.
Claim. A vacuum-horizon forcing certificate is a record of three Boolean flags (particle horizon is the causal-accumulation boundary; Hubble radius is not; de Sitter event horizon requires future knowledge), an integer rung count $s$, an integer exponent $e$, and a proof that $e = -2s$.
background
The module treats vacuum energy as $\rho_\Lambda = \rho_{\mathrm{Pl}}\cdot\varphi^{-2s}$, with $s$ the rung count on the $\varphi$-ladder from the substrate scale to a cosmological horizon. Three candidate 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$).
The causal-accumulation principle says the recognition ledger $\mathcal{L}(i,j)$ is defined only for substrate cells that have already exchanged a comparison. The vacuum ledger cost is therefore the ground-state total over the maximal causally connected region. By definition that boundary is the particle horizon (maximum comoving distance from which a signal has reached the observer since the initial condition).
The Hubble radius is only the instantaneous $v=c$ surface, so past contacts remain in the ledger. The de Sitter event horizon needs the future light cone and is excluded on that ground. The certificate structure packages those three selection claims together with the exponent identity forced by $\rho_\Lambda\propto\varphi^{-2s}$.
proof idea
No proof body: this is a structure definition. The six fields are data (three Booleans, two integers) plus one propositional field exponent_eq requiring exponent = -2 * rung_count. Downstream, vacuumHorizonForcingCert fills the fields with true/false/true, particleHorizonRungCount, and exponent $-588$, discharging the equality by construction. vacuumHorizonForcingCert_inhabited then wraps that inhabitant to prove Nonempty.
why it matters
This is the master certificate type for §6 of the vacuum-horizon forcing module. It turns the causal-accumulation selection argument into a single typed witness: particle horizon in, Hubble and de Sitter out, with the vacuum exponent locked to $-2s$.
Parents are the concrete inhabitant vacuumHorizonForcingCert and the inhabitation theorem vacuumHorizonForcingCert_inhabited, which feed the one-statement vacuum-horizon forcing claim (particle horizon selected; wrong horizon yields the wrong $\rho_\Lambda$). The $\varphi$-ladder mass/energy bookkeeping and the rung-count table in the module doc make the numerical stakes explicit: only $s$ from the particle horizon lands on the observed vacuum density.
Within Recognition Science this is structural cosmology, not a T0–T8 forcing step, but it applies the same ledger/causal-contact discipline that underlies the eight-tick and dimension arguments: cost is summed only over comparisons that have actually occurred.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.