recovers_baseline_lambda
plain-language theorem explainer
The Λ-extended Einstein data package, at vanishing Hubble input H₀² = 0, returns the same cosmological constant as the baseline Full-EFE package (namely zero). Cosmology and gravity workers citing the dark-energy EFE certificate need this limit identity. The proof is a one-line reduction to the already-proved vanishing of the RS vacuum term at zero input.
Claim. The cosmological constant of the Recognition Science Einstein data extended by a vacuum term, evaluated at $H_0^2 = 0$, equals the cosmological constant of the baseline RS Einstein data. Equivalently both sides are zero: $\Lambda_{\mathrm{RS}}(0) = 0$.
background
This module closes the blocker that the gravity-facing Einstein package carried a vanishing cosmological constant, so dark energy was absent from the quantum-gravity / EFE master chain. It inserts the forced vacuum term $\Lambda_{\mathrm{RS}}(H_0^2) = 3 H_0^2 \cdot \Omega_\Lambda$ with the RS-forced fraction $\Omega_\Lambda = 11/16 - \alpha/\pi$.
The baseline package keeps coupling $\kappa = 8\varphi^5$, spacetime dimension 4, and cosmological constant identically zero. The extended package changes only the cosmological-constant slot to $\Lambda_{\mathrm{RS}}(H_0^2)$, leaving $\kappa$ and dimension untouched. The sibling identity $\Lambda_{\mathrm{RS}}(0) = 0$ is exactly the $H_0^2 \to 0$ (equivalently zero-fraction) limit of that slot.
Status of the module is theorem-level: zero sorry, zero new axiom. Absolute scale enters only through the external input $H_0^2 > 0$; the dimensionless fraction and structural properties are forced.
proof idea
Both sides of the equality are the cosmological-constant fields of the respective data packages. Unfolding the extended package at input $0$ reduces the claim definitionally to $\Lambda_{\mathrm{RS}}(0) = 0$. A show rewrites to that identity, which is discharged by the sibling lemma that $\Lambda_{\mathrm{RS}}$ vanishes at zero. No new algebra is performed; this is a one-line wrapper around that vanishing result.
why it matters
This lemma fills the recovers_baseline field of the master dark-energy EFE certificate. That certificate packages five proved claims: positivity of $\Lambda$ for $H_0^2 > 0$, preservation of the derived coupling $\kappa = 8\varphi^5$, vacuum equation of state $w = -1$, covariant conservation of the vacuum stress (from flat metric compatibility), and this baseline recovery.
Together they establish that a nonzero forced vacuum term now sits in the EFE chain without breaking previously derived structure. The module doc frames the point explicitly: the extended data collapses back to the $\Lambda = 0$ baseline in the zero-input limit, so the dark-energy extension is a conservative enlargement of the gravity package rather than a rewrite of it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.