rs_efe_data_with_lambda
plain-language theorem explainer
RS full Einstein data that inserts the forced cosmological constant Λ_RS(H₀²) while keeping the derived coupling κ = 8φ⁵ and spacetime dimension 4. Gravity and cosmology workers cite it when the vacuum term must sit inside the nonlinear EFE package rather than as an external add-on. The definition reuses baseline κ and positivity witnesses and fills the cosmological-constant slot with Λ_RS.
Claim. For any real Hubble-scale squared $H_0^2$, the RS full Einstein data with dark energy is the package with dimension $4$, coupling $\kappa = 8\varphi^5 > 0$, and cosmological constant $\Lambda_{\mathrm{RS}}(H_0^2) = 3 H_0^2 \Omega_\Lambda$, where $\Omega_\Lambda$ is the RS-forced vacuum density fraction.
background
FullEFEData is the nonlinear 4D Einstein-equation package: a dimension field forced equal to 4, an Einstein coupling κ with a positivity witness, and a cosmological-constant slot. The baseline RS package fills that slot with zero, which the module records as the blocker keeping dark energy out of the quantum-gravity / EFE master chain.
This module supplies the missing vacuum term. Λ_RS(H₀²) is defined as 3 H₀² Ω_Λ with the RS-forced fraction Ω_Λ = 11/16 − α/π. Upstream, Ω_Λ > 0 is already proved, so Λ_RS is positive whenever H₀² > 0. The coupling is the same derived factor κ = 8φ⁵ used by the zero-parameter gravity layer; only the cosmological-constant field changes.
Separately, the module grounds covariant conservation of a constant times the metric in flat metric compatibility, so the vacuum stress with equation of state w = −1 is Bianchi-consistent rather than postulated.
proof idea
Pure structure construction, not a reasoned proof. Dimension is hard-coded to 4 with rfl for the equality witness. Coupling and its positivity proof are copied verbatim from the baseline RS EFE data. The cosmological-constant field is set to Λ_RS applied to the input H₀². No new algebra is performed at this declaration.
why it matters
This is the data carrier that puts the forced vacuum term into the gravity-facing EFE chain. The certificate DarkEnergyEFECert is built directly on it: positivity of Λ for H₀² > 0, preservation of κ = 8φ⁵, recovery of the Λ = 0 baseline at H₀² = 0, and the static w = −1 anchor. Companion projection lemmas (dimension, κ equality, Λ positivity, baseline recovery) are one-line reads off this package.
In the Recognition framework it closes the gap flagged by the dark-energy blocker: cosmology already forces Ω_Λ, but the full nonlinear Einstein data still carried Λ = 0. With this definition, dark energy is no longer external to the master chain. The absolute scale still enters only through the input H₀² > 0; the dimensionless fraction and all structural properties remain forced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.