conservation_from_efe_and_bianchi
plain-language theorem explainer
If the Einstein field equations hold with nonzero coupling kappa and the contracted Bianchi identity is satisfied, the divergence of the stress-energy tensor vanishes identically. General relativists who derive conservation laws from geometry would cite this as the formal link between the Einstein tensor and matter sources. The proof is a compact term-mode reduction that substitutes the Bianchi condition, applies zero-multiplication and zero-addition identities, and cancels the nonzero kappa factor.
Claim. Let $G$ and $T$ be the Einstein and stress-energy tensors with divergences $d_G$ and $d_T$. Assume $d_G = 0$ and $d_G + 0 = kappa * d_T$ for all indices, with $kappa ≠ 0$. Then $d_T = 0$ for all indices.
background
The Stress-Energy Tensor module obtains the stress-energy tensor by varying the matter action and derives its conservation from the contracted Bianchi identity together with the Einstein field equations. Idx is the finite set of four spacetime directions. Upstream results from the arithmetic foundation establish that multiplication by zero returns zero and that zero plus any element equals the element; these simplify the divergence expressions after substitution.
proof idea
The term-mode proof introduces an arbitrary index, extracts the Bianchi hypothesis and the diverged field equation, rewrites the latter by replacing the Einstein divergence with zero and invoking the zero-multiplication and zero-addition lemmas, then applies left cancellation with the nonzero hypothesis on kappa to reach the vanishing divergence.
why it matters
This declaration supplies the conservation property required by the stress-energy certificate theorem that follows it in the same module. It completes the formalization of Axiom 3 on matter coupling by showing that conservation follows once the Einstein equations and Bianchi identity are assumed. The argument sits inside the gravity sector of the Recognition Science derivation, where the coupling constant is realized through the phi-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.