vacuum_eos
plain-language theorem explainer
The static vacuum fluid in the Λ-extended Einstein equations has equation of state w = p/ρ = −1 for any nonzero density. Gravity and cosmology work citing the RS dark-energy EFE certificate uses this as the static vacuum anchor. The proof is a two-step algebraic reduction: unfold the pressure definition and cancel.
Claim. For every real density $\rho \neq 0$, the vacuum pressure satisfies $p_{\mathrm{vac}}(\rho)/\rho = -1$.
background
This module closes the blocker that baseline RS Einstein data carried cosmological constant zero. It installs the forced positive vacuum term $\Lambda_{\mathrm{RS}}(H_0^2) = 3 H_0^2 \cdot \Omega_\Lambda$ with the RS fraction $\Omega_\Lambda = 11/16 - \alpha/\pi$, keeping the derived coupling $\kappa = 8\varphi^5$ and dimension 4.
The vacuum stress is written as a perfect fluid $T^{\mathrm{vac}}{\mu\nu} = -(\Lambda/\kappa), g{\mu\nu}$. Density is then $\rho_{\mathrm{vac}} = \Lambda/\kappa > 0$, and vacuum pressure is defined as the negative of that density, so the equation-of-state parameter is $w = p/\rho$. Metric compatibility and covariant conservation of the vacuum stress are proved as sibling results; this lemma isolates the pure algebraic identity $w = -1$.
proof idea
Short tactic proof. Unfold the definition of vacuum pressure (the map $\rho \mapsto -\rho$). Rewrite with the division identities neg_div and div_self, using the hypothesis $\rho \neq 0$, to obtain $(-\rho)/\rho = -1$. No external lemmas beyond those rewrite rules.
why it matters
Inhabits the vacuum_eos_minus_one field of the dark-energy EFE certificate, which packages every claim needed to put a nonzero forced cosmological constant into the quantum-gravity / EFE master chain: positivity of $\Lambda$, preservation of $\kappa$, recovery of the baseline as $H_0^2 \to 0$, vacuum EOS $w = -1$, and covariant conservation of the vacuum stress.
In the Recognition framework this is the static anchor from which any dynamic $\delta w(z)$ kernel deviates. Together with metric compatibility it is the structural reason a cosmological-constant term is consistent with the Bianchi identity. Absolute scale enters only through the input $H_0^2 > 0$; the dimensionless fraction and all structural properties are forced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.