vacuumEnergyExponent
plain-language theorem explainer
Maps a cosmological horizon model to the integer vacuum-energy exponent −2s, where s is the φ-rung count from the substrate scale to the horizon radius. Vacuum energy density then scales as φ to that power. Cosmologists comparing particle, Hubble, and de Sitter horizons cite this packing. The body is a one-line arithmetic definition from the model’s rung field.
Claim. For a horizon model $H$ with rung count $s = H.\mathrm{rungCount}$ (integer number of $\varphi$-rungs from the substrate length to the comoving horizon radius), the vacuum energy exponent is the integer $-2s$. Equivalently, vacuum energy density scales as $\rho_\Lambda \propto \varphi^{-2s}$.
background
The module treats vacuum energy as $\rho_\Lambda = \rho_{\mathrm{Pl}} \cdot \varphi^{-2s}$, with $s$ the rung count from the substrate scale to a cosmological horizon. Three candidate horizons give different $s$ (particle $\sim 294$, Hubble $\sim 289$, de Sitter $\sim 290$) and thus different $\rho_\Lambda$ relative to observation; only the particle horizon matches order unity.
A horizon model packages horizon type, positive comoving radius, integer rung count, and a flag for causal accumulation (past light cone versus instantaneous recession or future expansion). The causal-accumulation principle says the vacuum ledger cost is the ground-state total over the maximal causally connected region, whose boundary is the particle horizon by definition.
The $\varphi$-ladder and cost algebra ($J$, shifted $H = J+1$) sit upstream as the RS scale and functional backbone; this definition only extracts the exponent $-2s$ from the model’s rung field.
proof idea
Pure definition: return $-2$ times the model’s integer rungCount. No lemmas, tactics, or nontrivial computation. Noncomputable only because the ambient real/horizon infrastructure is.
why it matters
Packs the module’s scaling law $\rho_\Lambda / \rho_{\mathrm{Pl}} = \varphi^{-2s}$ into a single integer attached to each horizon model. Downstream selection theorems (causal accumulation picks the particle horizon; Hubble excludes past contacts; de Sitter needs future data) compare exponents across models; this is the common numeric handle.
It sits in the cosmology layer that forces which horizon enters the vacuum ledger, consistent with RS φ-ladder mass/energy bookkeeping and the eight-tick / D=3 forcing chain only indirectly (via the same φ scale). No open sorry: structural definition supporting the 0-sorry selection argument in the module doc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.