flat_vacuum_stress_conserved
plain-language theorem explainer
On flat Minkowski spacetime, any constant multiple of the metric is covariantly conserved: ∇_λ(c η_μν) = 0 for every index triple. Gravity and cosmology workers cite this when placing a vacuum (Λ) stress tensor into the Einstein equation without spoiling Bianchi identity. The proof is a one-line specialization of the general vacuum-stress conservation lemma, discharging metric compatibility via the already-proved Minkowski case.
Claim. For every real constant $c$ and all index triples $(\lambda,\mu,\nu)$, the $(0,2)$ covariant derivative of the tensor $c\,\eta_{\mu\nu}$ vanishes when the connection is the Christoffel connection of Minkowski spacetime (whose Christoffel symbols are identically zero). Equivalently, $\nabla^{(\eta)}(c\,\eta)=0$.
background
This module closes the dark-energy gap in the Recognition Science Einstein data: the baseline FullEFE package still carried cosmological constant zero. Here a forced positive vacuum term $\Lambda_{\mathrm{RS}}=3H_0^2\Omega_\Lambda$ with $\Omega_\Lambda=11/16-\alpha/\pi$ is inserted, written as a perfect fluid $T^{\mathrm{vac}}{\mu\nu}=-(\Lambda/\kappa)g{\mu\nu}$ with $w=-1$.
Covariant conservation of that term is not an extra postulate. It follows from metric compatibility: a constant times the metric has vanishing covariant derivative precisely because $\nabla g=0$. The module already proves the flat reference case (minkowski_metric_compatible) and the scalar-linearity of the $(0,2)$ covariant derivative, then obtains $\nabla(c\cdot g)=0$ for any constant $c$.
The present statement is the grounded flat specialization: connection built from the Minkowski inverse metric with vanishing partials of $g$, stress tensor $c,\eta_{\mu\nu}$, and zero partials of that tensor.
proof idea
One-line term proof. Apply the general lemma that any constant multiple of a metric is covariantly conserved whenever the connection is the Christoffel connection of that metric and metric compatibility holds. Instantiate the metric to Minkowski, the Christoffel symbols to those computed from the Minkowski inverse with zero partial derivatives of $g$ (hence identically zero), the partials of the stress tensor to zero, and discharge the compatibility hypothesis by the already-proved Minkowski metric-compatibility theorem. No new algebra is performed here.
why it matters
This is the structural Bianchi/U9 anchor for a cosmological constant inside the RS gravity chain: $\nabla^\mu G_{\mu\nu}=0$ remains consistent once the vacuum term is present. Downstream, the dark-energy EFE certificate wires vacuum_conserved directly to this theorem, so the inhabited certificate records that every dark-energy claim (positive $\Lambda$, preserved $\kappa=8\varphi^5$, baseline recovery at $H_0^2\to 0$, $w=-1$, and conservation) is proved with zero sorry.
Together with the forced fraction $\Omega_\Lambda=11/16-\alpha/\pi$ and the vacuum equation of state, it removes the blocker that previously kept dark energy out of the quantum-gravity / EFE master data. The absolute scale still enters only through an external $H_0^2>0$; the conservation identity itself is scale-free and holds for every real $c$, including $c=-\Lambda/\kappa$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.