lambda_efe_lambda_pos
plain-language theorem explainer
For any positive Hubble scale squared, the cosmological-constant slot of the Λ-extended RS Einstein data is strictly positive. Gravity and cosmology proofs that need a forced nonzero vacuum term in the EFE package cite this. The argument is a one-line term application of the positivity of Λ_RS.
Claim. If $H_0^2 > 0$, then the cosmological constant carried by the Recognition-Science full Einstein data with vacuum term at scale $H_0^2$ is strictly positive: $0 < \Lambda_{\mathrm{RS}}(H_0^2)$.
background
This module closes the gravity-facing blocker that the baseline RS Einstein data had cosmological constant zero. It installs a 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 the derived coupling $\kappa = 8\varphi^5$ and spacetime dimension 4.
The extended data package rs_efe_data_with_lambda is the baseline FullEFE record with only the cosmological-constant field replaced by $\Lambda_{\mathrm{RS}}(H_0^2)$. Upstream, Lambda_RS_pos already shows $0 < \Lambda_{\mathrm{RS}}(H_0^2)$ whenever $H_0^2 > 0$, using positivity of the constant 3, of $H_0^2$, and of $\Omega_\Lambda$. Absolute scale enters only through the hypothesis $H_0^2 > 0$; the dimensionless fraction and structural properties are forced.
proof idea
One-line term proof. The cosmological-constant projection of rs_efe_data_with_lambda H0sq is definitionally Lambda_RS H0sq, so the goal is exactly the statement of Lambda_RS_pos h, which is applied directly.
why it matters
This is the positivity leg of the dark-energy EFE certificate. Downstream, darkEnergyEFECert fills its lambda_pos field by fun h => lambda_efe_lambda_pos h, together with kappa preservation, baseline recovery, $w = -1$ vacuum equation of state, and covariant conservation of the vacuum stress.
In the module narrative, the vacuum term must be forced positive so dark energy enters the quantum-gravity / EFE master chain rather than remaining an external add-on. The absolute scale is the sole free input ($H_0^2 > 0$); $\Omega_\Lambda > 0$ is already proved. This does not itself derive the numerical value of $H_0$, only that any positive Hubble scale yields a positive $\Lambda$ slot in the EFE data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.