lambda_efe_kappa
plain-language theorem explainer
The Einstein coupling in the dark-energy-extended EFE data equals $8\varphi^5$, independent of the input $H_0^2$. Anyone citing the RS vacuum term in the gravity chain needs this to confirm $\kappa$ is unchanged when $\Lambda$ is switched on. The proof is a one-line appeal to the baseline $\kappa$ identity, since the extended data copies that field verbatim.
Claim. For every real $H_0^2$, the Einstein coupling $\kappa$ carried by the RS full-EFE data with forced cosmological constant $\Lambda_{\mathrm{RS}}(H_0^2)$ equals $8\varphi^5$.
background
This module extends the gravity-facing Einstein data so that the cosmological-constant slot is no longer forced to zero. The baseline package rs_efe_data already fixes spacetime dimension 4 and the derived coupling $\kappa=8\varphi^5$; the blocker recorded elsewhere was only that $\Lambda=0$ kept dark energy out of the EFE master chain.
The extended package rs_efe_data_with_lambda(H_0^2) keeps the same dimension and the same $\kappa$ field (copied from the baseline), and fills the cosmological-constant slot with the forced value $\Lambda_{\mathrm{RS}}(H_0^2)=3H_0^2\cdot\Omega_\Lambda$, where $\Omega_\Lambda=11/16-\alpha/\pi$. Upstream, rs_efe_kappa already proves the baseline identity $\kappa=8\varphi^5$ (via the RS lattice derivation of the coupling). The constant $\varphi$ is the golden ratio fixed by the self-similarity step of the forcing chain; the factor $8\varphi^5$ is the RS-native Einstein coupling in the units used throughout the monolith.
proof idea
One-line wrapper. By definition the extended data sets its $\kappa$ field equal to the baseline rs_efe_data.kappa. The goal therefore reduces exactly to the upstream theorem rs_efe_kappa, which states that baseline value is $8\varphi^5$. No new algebra is performed; the $H_0^2$ parameter never enters the $\kappa$ slot.
why it matters
This lemma is the $\kappa$-preservation half of the dark-energy EFE certificate. Downstream, darkEnergyEFECert wires it in as kappa_preserved, alongside positivity of $\Lambda$, recovery of the baseline when $H_0^2\to 0$, the vacuum equation of state $w=-1$, and covariant conservation of the vacuum stress. Together those facts discharge the blocker that the gravity-facing EFE data carried a zero cosmological constant, and put a nonzero, forced, Bianchi-consistent vacuum term into the quantum-gravity / EFE master chain.
Framework-wise it locks the coupling side of the RS constants package: with $c=1$ and $\hbar=\varphi^{-5}$, the Einstein coupling $\kappa=8\varphi^5$ is the gravity dual of that ladder, unchanged by the vacuum term. Only the $\Lambda$ slot moves; dimension and $\kappa$ stay fixed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.