vacuum_stress_conserved
plain-language theorem explainer
Any constant multiple of a metric-compatible metric has vanishing (0,2) covariant derivative. In the RS gravity chain this is the structural reason the static vacuum stress T^vac = −(Λ/κ)g is covariantly conserved, so a cosmological-constant term is consistent with the contracted Bianchi identity. The proof is a three-line rewrite: scale out the constant via covDeriv02_smul, apply metric compatibility, then ring.
Claim. Let $g$ be a metric tensor with Christoffel data $\Gamma$ and partial derivatives $\partial g$, and assume metric compatibility $\nabla_\lambda g_{\mu\nu}=0$. Then for every real constant $c$ and all indices $\lambda,\mu,\nu$, $$\nabla_\lambda(c\, g_{\mu\nu})=0.$$ In particular, with $c=-\Lambda/\kappa$ the vacuum stress $T^{\mathrm{vac}}_{\mu\nu}=-({\Lambda}/{\kappa})g_{\mu\nu}$ satisfies $\nabla_\lambda T^{\mathrm{vac}}_{\mu\nu}=0$.
background
This module closes the dark-energy blocker on the RS Einstein data: the baseline FullEFE package carried cosmological_constant = 0. Here a forced positive $\Lambda_{\mathrm{RS}}(H_0^2)=3H_0^2\Omega_\Lambda$ with $\Omega_\Lambda=11/16-\alpha/\pi$ is inserted, the vacuum equation of state is fixed at $w=-1$, and covariant conservation of the vacuum term is proved rather than assumed.
The local differential-geometry layer is Connection: MetricTensor supplies $g_{\mu\nu}$, ChristoffelData holds $\Gamma^\rho_{\mu\nu}$, and metric_compatibility asserts that the (0,2) covariant derivative of $g$ vanishes once the partials $\partial g$ are supplied. The operator covDeriv02 is that covariant derivative on symmetric (0,2) tensors; covDeriv02_smul records its $\mathbb{R}$-linearity in the tensor argument.
Metric compatibility is the classical identity $\nabla_\lambda g_{\mu\nu}=0$. The module proves it for the flat (Minkowski) reference separately; the present theorem keeps it as a hypothesis so the same algebra applies to any compatible chart.
proof idea
Fix indices $\lambda,\mu,\nu$. Rewrite the target covariant derivative of $c\cdot g$ by covDeriv02_smul, which pulls the constant scalar out of covDeriv02. The remaining factor is exactly covDeriv02 of the bare metric, which metric_compatibility sets to $0$. The resulting expression $c\cdot 0$ is cleared by ring. No curvature identities or Bianchi identities are invoked; only linearity of the connection and the compatibility hypothesis.
why it matters
Covariant conservation of $T^{\mathrm{vac}}$ is the structural reason a cosmological constant is always consistent with $\nabla^\mu G_{\mu\nu}=0$ (the contracted Bianchi / U9 side of the EFE). The module doc lists this as item 4 of what is established: conservation is grounded in metric compatibility plus linearity, not postulated.
The sole direct consumer is flat_vacuum_stress_conserved, which discharges the compatibility hypothesis via the proved minkowski_metric_compatible and thereby anchors the vacuum term on the flat reference used by the RS gravity chain. Together with $\Lambda_{\mathrm{RS}}>0$, $\rho_{\mathrm{vac}}=\Lambda/\kappa$, and $w=-1$, this puts a nonzero, forced, conserved vacuum term into the QG/EFE master data that previously carried $\Lambda=0$.
No new axiom is introduced; the absolute scale enters only through the external input $H_0^2>0$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.