vacuumExponent_particleHorizon
plain-language theorem explainer
The vacuum-energy exponent attached to the particle horizon equals −588: twice the rung count 294 with a minus sign. Cosmologists citing the RS vacuum-horizon selection use this identity when writing ρ_Λ/ρ_Pl = φ^(−588). The proof is a one-line unfold-and-ring of the constant definition.
Claim. If $s_{\mathrm{PH}}$ denotes the ΛCDM particle-horizon rung count (the integer $294$), then the vacuum-energy exponent is $-2 s_{\mathrm{PH}} = -588$. Equivalently, $\rho_\Lambda / \rho_{\mathrm{Pl}} = \varphi^{-588}$ when the horizon is the particle horizon.
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 up to a chosen cosmological horizon on the $\varphi$-ladder. Three candidate horizons give three integers: particle horizon $s=294$, Hubble radius $s=289$, de Sitter event horizon $s=290$. Only the particle horizon yields a ratio near the observed vacuum energy.
The local setting is the causal-accumulation principle: the recognition ledger is summed only over substrate cells that have already exchanged a comparison, i.e. over the maximal past-directed causal contact set. By definition that set is bounded by the particle horizon. The definition particleHorizonRungCount simply records the integer $294$ that this horizon contributes on the ladder.
The factor $-2s$ is therefore the pure exponent that multiplies $\log\varphi$ in the vacuum-energy formula once the horizon has been fixed.
proof idea
Term-mode one-liner. Unfold the definition particleHorizonRungCount (the constant integer $294$), then close by ring, which reduces $-2\cdot 294$ to $-588$ in $\mathbb{Z}$. No external lemmas are required beyond the definition itself.
why it matters
This identity is the second conjunct of the package theorem vacuum_horizon_forcing_one_statement, which states in one place that the particle horizon is selected, its rung count is $294$, the vacuum exponent is $-588$, and the gap to the Hubble-radius count is $10$ rungs (a $\varphi^{10}$ energy ratio). Without the exponent identity the one-statement cannot quote the numerical vacuum suppression that matches observation.
In the broader RS picture the result sits downstream of the $\varphi$-ladder mass/energy formula and of the eight-tick / three-dimensional forcing chain only indirectly: it uses the same rung arithmetic that converts geometric scales into $\varphi$-powers. It does not itself invoke T5–T8; it is a pure bookkeeping step that makes the causal-accumulation selection numerically usable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.