Lambda_RS
plain-language theorem explainer
Defines the RS cosmological constant at a given squared Hubble scale by the standard Friedmann conversion Λ = 3 H₀² Ω_Λ, with Ω_Λ the forced RS density fraction 11/16 − α/π. Gravity and cosmology workers cite it when wiring dark energy into the Einstein data. The body is a one-line product of three scalars.
Claim. For a real squared Hubble scale $H_0^2$, set $\Lambda_{\mathrm{RS}}(H_0^2) := 3\, H_0^2\, \Omega_\Lambda^{\mathrm{RS}}$, where the RS density parameter is the fixed real $\Omega_\Lambda^{\mathrm{RS}} = 11/16 - \alpha/\pi$.
background
This module closes the gravity-facing gap that the baseline Einstein data carried cosmological constant zero. Dark energy is restored by a forced vacuum term that stays covariantly conserved and recovers the old data when the Hubble scale vanishes.
The dimensionless fraction comes from CosmologicalConstantDerivation: $\Omega_\Lambda^{\mathrm{RS}} = 11/16 - \alpha/\pi$, with geometric seed $11/16$ from the $D=3$ ledger and one measured input $\alpha$. The classical Friedmann relation then converts that fraction into a dimensionful $\Lambda$ once an absolute scale $H_0^2$ is supplied.
Sibling material in the same file proves $\Omega_\Lambda^{\mathrm{RS}} > 0$, metric compatibility on the flat reference, and that a constant multiple of the metric has vanishing covariant derivative, so the vacuum stress is Bianchi-consistent.
proof idea
Pure definition: expand as the product $3 \cdot H_0^2 \cdot \Omega_\Lambda^{\mathrm{RS}}$. No tactics, no lemmas. Downstream positivity and zero-limit facts unfold this def and apply arithmetic plus the already-proved sign of $\Omega_\Lambda^{\mathrm{RS}}$.
why it matters
This is the single scalar that turns the baseline FullEFE package into dark-energy-aware data. It is the cosmological_constant field of rs_efe_data_with_lambda, which keeps $\kappa = 8\varphi^5$ and dimension 4 while replacing $\Lambda = 0$ by $\Lambda_{\mathrm{RS}}(H_0^2)$.
Parents: Lambda_RS_pos (strict positivity for $H_0^2 > 0$), Lambda_RS_zero (collapse at vanishing Hubble scale), recovers_baseline_lambda (the extended data matches the old slot when $H_0^2 = 0$). Together they discharge DarkEnergyStatus.blocker_efe_lambda_zero and put a nonzero forced vacuum term into the QG/EFE master chain.
Framework link: $\Omega_\Lambda$ is RS-forced (geometric 11/16 minus $\alpha/\pi$); only the absolute scale $H_0^2$ is an external positive input. The vacuum equation of state read off later is exactly $w = -1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.