vacuum_horizon_forcing_one_statement
plain-language theorem explainer
The particle-horizon rung count is fixed at 294, forcing the vacuum-energy exponent to -588 and a factor φ^10 gap versus the Hubble-radius count 289. Cosmologists citing the RS vacuum ledger would use this as the single packaged numerical claim for horizon selection. The proof is a three-component term pairing definitional reflexivity with two one-line ring identities.
Claim. The particle-horizon rung count equals $294$, the vacuum-energy exponent $-2$ times that count equals $-588$, and twice the gap between that count and the Hubble-radius rung count $289$ equals $10$.
background
In this module the vacuum energy is written $\rho_\Lambda = \rho_{\mathrm{Pl}}\cdot\varphi^{-2s}$, with $s$ the rung count from the substrate scale to a cosmological horizon on the $\varphi$-ladder. Three candidate 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 selects the particle horizon: the vacuum ledger cost is the ground-state total $\sum_{i,j}\mathcal{L}(i,j)$ over the maximal causally connected region, whose boundary is the particle horizon by definition. The Hubble radius is only the instantaneous $v=c$ surface; past contacts remain in the ledger. The de Sitter horizon is future-directed and is excluded on the same past-directedness grounds.
Upstream, particleHorizonRungCount is the constant $294$; vacuumExponent_particleHorizon records $-2\cdot 294=-588$; hubble_vs_particle_rung_gap records $2(294-289)=10$, the exponent of the $\varphi^{10}$ discrepancy.
proof idea
Term-mode construction of a three-way conjunction. The first conjunct is definitional reflexivity on the constant rung count $294$. The second is the already-proved identity -2 * particleHorizonRungCount = -588 (unfold the constant, then ring). The third is the already-proved gap identity 2 * (particleHorizonRungCount - 289) = 10 (same unfold-and-ring pattern). The whole theorem is therefore a one-line packaging of three numerical facts, not a new derivation.
why it matters
This is the module's one-statement numerical summary of vacuum-horizon forcing. The surrounding development argues that causal accumulation selects the particle horizon and that past-directedness excludes the Hubble radius and the de Sitter event horizon; the present theorem freezes the three integers that make the selection quantitative: rung count $294$, vacuum exponent $-588$, and Hubble gap exponent $10$ (i.e. a $\varphi^{10}$ energy-density factor).
No downstream theorems currently depend on it; it sits at the end of the VacuumHorizonForcing development as the citation handle for the numerical claim. Within the broader RS framework it instantiates the $\varphi$-ladder mass/energy formula at cosmological scale, converting a horizon choice into a definite vacuum-suppression exponent. It does not itself re-prove the causal-accumulation principle; it only packages the arithmetic that follows once the particle horizon is chosen.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.