Lambda_RS_zero
plain-language theorem explainer
The RS cosmological constant vanishes when the Hubble-scale input is zero: Λ_RS(0) = 0. Gravity and cosmology workers cite it to recover the baseline Einstein data (Λ = 0) as the H₀² → 0 limit of the dark-energy extension. The proof is a one-line unfold-and-ring on the definition Λ_RS = 3 H₀² Ω_Λ.
Claim. The Recognition Science cosmological constant at vanishing Hubble scale is zero: $\Lambda_{\mathrm{RS}}(0) = 0$, where $\Lambda_{\mathrm{RS}}(H_0^2) := 3 H_0^2 \, \Omega_\Lambda$ and $\Omega_\Lambda$ is the forced RS dark-energy fraction.
background
This module extends the gravity-facing Einstein data so that a nonzero, forced vacuum term enters the EFE chain. Previously the baseline package carried cosmological constant zero; dark energy was blocked from the master chain. The fix introduces $\Lambda_{\mathrm{RS}}(H_0^2) = 3 H_0^2 \Omega_\Lambda$ with the RS-forced fraction $\Omega_\Lambda = 11/16 - \alpha/\pi > 0$.
The absolute scale enters only through the input $H_0^2 > 0$. Structural properties (positivity of $\Omega_\Lambda$, equation of state $w = -1$, covariant conservation of the vacuum stress via metric compatibility) are forced independently of that scale. The zero-input case is the continuity check that the extension collapses back to the old baseline when the Hubble scale is switched off.
Sibling facts already record $\Lambda_{\mathrm{RS}} > 0$ for $H_0^2 > 0$ and $\rho_{\mathrm{vac}} = \Lambda/\kappa$ with $p_{\mathrm{vac}} = -\rho_{\mathrm{vac}}$.
proof idea
One-line algebraic wrapper. Unfold the definition $\Lambda_{\mathrm{RS}}(H_0^2) = 3 H_0^2 \Omega_\Lambda$, substitute $H_0^2 = 0$, and finish by ring: the product is identically zero. No lemmas about $\Omega_\Lambda$ or positivity are needed.
why it matters
Closes the continuity clause in the module's second established claim: the Λ-extended EFE data recovers the baseline when $H_0^2 \to 0$. Downstream, recovers_baseline_lambda rewrites the cosmological-constant slot of rs_efe_data_with_lambda 0 as exactly this identity, matching FullEFE.rs_efe_data.
Without the zero limit, the dark-energy extension would be a permanent fork rather than a controlled lift of the baseline package (coupling $\kappa = 8\varphi^5$, dimension 4 unchanged). The result is pure algebra on the forced form $\Lambda = 3 H_0^2 \Omega_\Lambda$; it does not itself derive $\Omega_\Lambda$ or the eight-tick / $D=3$ chain, but it is the hinge that keeps the QG integration of the vacuum term compatible with the older $\Lambda = 0$ data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.