IndisputableMonolith.Gravity.FullEFEWithDarkEnergy
Module assembling the Einstein field equations with an RS-derived vacuum sector: a coordinate covariant derivative on (0,2) tensors, metric compatibility, conserved vacuum stress, and the RS cosmological constant Λ_RS with density and pressure. Gravity and cosmology workers cite it when wiring dark energy into the sourced EFE chain. Structure is definitional plus short positivity and conservation lemmas on top of FullEFE, Connection, and CosmologicalConstantDerivation.
claimIn local coordinates, the covariant derivative $\nabla_\lambda T_{\mu\nu}$ of a $(0,2)$ tensor is built from ordinary derivatives and Christoffel symbols so that metric compatibility is $\nabla_\lambda g_{\mu\nu}=0$. The module defines the RS vacuum density $\rho_{\mathrm{vac}}$, pressure, and cosmological constant $\Lambda_{\mathrm{RS}}$ (with $\Omega_\Lambda^{\mathrm{RS}}>0$), and records conservation of the vacuum stress-energy on Minkowski and flat backgrounds for use in the full Einstein equations with dark energy.
background
Recognition Science derives the nonlinear sourced Einstein equations from a discrete ledger (FullEFE), conditional on Regge-style continuum limits. The connection layer supplies Christoffel symbols in a coordinate patch $g:\mathbb{R}^4\to\mathbb{R}^{4\times 4}$, avoiding Mathlib's missing abstract connections while keeping the usual GR calculus.
Dark energy enters through CosmologicalConstantDerivation (registry C-010): QFT overpredicts $\Lambda$ by $\sim 10^{120}$; RS instead fixes a vacuum scale from the ledger and constants (native tick $\tau_0=1$). This module is the glue: it states the $(0,2)$ covariant derivative matching the metric-compatibility identity term-for-term, then packages $\Lambda_{\mathrm{RS}}$, $\rho_{\mathrm{vac}}$, and vacuum pressure so the EFE can carry a cosmological term without an external $\Lambda$ postulate.
Sibling names mark the local API: covDeriv02 and metric compatibility on Minkowski, vacuum-stress conservation (flat and general), and positivity/zero lemmas for $\Lambda_{\mathrm{RS}}$ and $\rho_{\mathrm{vac}}$.
proof idea
Not a single theorem: a small gravity+vacuum library. Covariant derivative of a $(0,2)$ tensor is defined from partials plus Christoffel contractions so it agrees with the Connection metric-compatibility expression; compatibility is then $\forall\lambda\mu\nu,,\nabla_\lambda g_{\mu\nu}=0$. Scalar-multiplication and Minkowski specializations are short algebraic checks.
Vacuum stress conservation on flat/Minkowski backgrounds follows from that derivative vanishing on the vacuum $T_{\mu\nu}$ built from $\rho_{\mathrm{vac}}$ and isotropic pressure. $\Lambda_{\mathrm{RS}}$, $\rho_{\mathrm{vac}}$, and $\Omega_\Lambda^{\mathrm{RS}}$ are definitions or thin wrappers over CosmologicalConstantDerivation and Constants, with positivity (and a zero case) discharged by the upstream sign facts rather than a long local proof.
why it matters in Recognition Science
Closes the gap between the ledger-derived full EFE and an RS-native cosmological term: without a conserved vacuum stress and an explicit $\Lambda_{\mathrm{RS}}$, the sourced equations cannot host dark energy in the same coordinate calculus as ordinary matter. It sits on FullEFE (nonlinear sourced Einstein system), Connection (Levi-Civita in patches), and C-010 (what fixes $\Lambda$), and exposes $\rho_{\mathrm{vac}}$, pressure, and $\Omega_\Lambda^{\mathrm{RS}}>0$ for cosmology and late-universe matching.
No downstream edges are recorded yet in the mirror graph, so this module is presently a leaf API: parent consumers would be continuum GR limits, Friedmann/acceleration identities, or observational $\Omega_\Lambda$ bounds expressed in RS units ($c=1$, and the usual RS ladder for other constants). Framework-wise it is the gravity-side counterpart of the cosmological-constant derivation, not a new forcing-chain step (T0–T8).
scope and limits
- Does not prove the full nonlinear EFE; that lives in FullEFE under Regge convergence axioms.
- Does not derive $\Lambda$ from QFT vacuum sums; it imports the RS C-010 construction.
- Does not work on abstract Mathlib manifolds; calculus is local coordinate patches only.
- Does not claim observational fits to $w$ or structure-growth data beyond positivity of $\Omega_\Lambda^{\mathrm{RS}}$.
- Does not establish global energy conditions or singularity theorems with the vacuum term.
depends on (4)
declarations in this module (20)
-
def
covDeriv02 -
theorem
covDeriv02_smul -
theorem
minkowski_metric_compatible -
theorem
vacuum_stress_conserved -
theorem
flat_vacuum_stress_conserved -
theorem
Omega_Lambda_RS_pos -
def
Lambda_RS -
theorem
Lambda_RS_pos -
theorem
Lambda_RS_zero -
def
rho_vac -
theorem
rho_vac_pos -
def
vacuum_pressure -
theorem
vacuum_eos -
def
rs_efe_data_with_lambda -
theorem
lambda_efe_kappa -
theorem
lambda_efe_dimension -
theorem
lambda_efe_lambda_pos -
theorem
recovers_baseline_lambda -
structure
DarkEnergyEFECert -
def
darkEnergyEFECert