darkEnergyEFECert
plain-language theorem explainer
Packages five proved facts into a single dark-energy EFE certificate: positive forced Λ, preserved κ = 8φ⁵, recovery of the Λ = 0 baseline, vacuum equation of state w = −1, and covariant conservation of the vacuum stress on the flat reference. Gravity and QG auditors cite it to confirm the vacuum term is fully in the Einstein-data chain. The body is a pure structure inhabitant wiring existing lemmas.
Claim. There exists a dark-energy EFE certificate asserting: (i) for every $H_0^2 > 0$, the cosmological constant in the $\Lambda$-extended RS Einstein data is positive; (ii) the coupling remains $\kappa = 8\varphi^5$ for every $H_0^2$; (iii) at $H_0^2 = 0$ the cosmological constant equals the baseline (zero) value; (iv) vacuum pressure over density equals $-1$ whenever density is nonzero; (v) any constant multiple of the flat metric has vanishing $(0,2)$ covariant derivative.
background
This module closes the gravity-facing blocker that the baseline RS Einstein data carried cosmological constant zero. It installs a nonzero forced 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 dimension 4 and the derived coupling $\kappa = 8\varphi^5$.
The certificate structure bundles five structural claims: positivity of $\Lambda$ for $H_0^2 > 0$; preservation of $\kappa$; recovery of the $\Lambda = 0$ baseline at vanishing $H_0^2$; the static vacuum equation of state $w = -1$ obtained by writing $T^{\mathrm{vac}}{\mu\nu} = -(\Lambda/\kappa) g{\mu\nu}$; and covariant conservation of that vacuum stress on the flat reference.
Conservation is grounded, not assumed: metric compatibility of Minkowski plus linearity of the $(0,2)$ covariant derivative imply $\nabla(c\cdot g) = 0$ for any constant $c$, in particular $c = -\Lambda/\kappa$. Absolute scale enters only through the input $H_0^2 > 0$; the dimensionless fraction and every structural property are forced.
proof idea
One-line structure inhabitant. Each field is filled by a named upstream theorem:
lambda_posislambda_efe_lambda_pos, itself a thin wrapper ofLambda_RS_pos.kappa_preservedislambda_efe_kappa, which reduces to the baselineFullEFE.rs_efe_kappa.recovers_baselineisrecovers_baseline_lambda, proved by reducing toLambda_RS_zero.vacuum_eos_minus_oneisvacuum_eos: unfold pressure, rewrite $p/\rho = -\rho/\rho = -1$.vacuum_conservedisflat_vacuum_stress_conserved, the specialization ofvacuum_stress_conservedthat discharges Minkowski metric compatibility.
No new algebra is performed at this site; the certificate merely records that every slot is already proved.
why it matters
This is the inhabited certificate that the module doc advertises: every dark-energy EFE claim is proved, with zero sorry and zero new axiom. It resolves DarkEnergyStatus.blocker_efe_lambda_zero by placing a forced, positive, covariantly conserved vacuum term into the quantum-gravity / EFE master chain while preserving $\kappa = 8\varphi^5$ (the RS-native coupling tied to $G = \varphi^5/\pi$ in RS units).
Downstream consumers of the gravity chain can now treat dark energy as an installed structural fact rather than an external add-on. The $w = -1$ slot is the static anchor from which any dynamic $\delta w(z)$ kernel is meant to deviate. Used-by is currently empty, so this is a terminal packaging node for the module rather than an intermediate lemma.
Framework landmarks: the forced positive $\Omega_\Lambda$ fraction, the derived $\kappa = 8\varphi^5$, and Bianchi consistency via metric compatibility (the structural reason a cosmological constant never breaks $\nabla^\mu G_{\mu\nu} = 0$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.