vacuum_is_special_case
plain-language theorem explainer
The theorem shows that the Einstein field equations with source reduce directly to the vacuum form when the stress-energy tensor is identically zero. Researchers working on conservation laws or empty-spacetime limits inside the Recognition Science gravity module would cite it. The proof is a direct substitution of the zero tensor definition into the sourced equation followed by coordinate-wise simplification.
Claim. Let $g$ be a metric with inverse $g^{-1}$, Christoffel symbols and their derivatives given. If the sourced Einstein equations $G + Lambda g = kappa T$ hold with $T=0$ (the vacuum stress-energy tensor), then the vacuum equations $G + Lambda g = 0$ hold in coordinates.
background
The module defines the stress-energy tensor via variation of the matter action and derives conservation of $T$ from the contracted Bianchi identity together with the Einstein field equations. MetricTensor supplies a local bilinear-form interface for $g_{mu nu}$. The upstream Hamiltonian result supplies the concrete MetricTensor structure used here. The module document states that the overall development proves Axiom 3 on matter coupling via the chain: Bianchi identity implies nabla G = 0, EFE gives G proportional to T, metric compatibility gives nabla T = 0.
proof idea
The term proof introduces the hypothesis that the sourced equations hold, extracts the mu-nu component, and applies simp on the definitions of vacuum_stress_energy (identically zero) and efe_with_source to obtain the vacuum coordinate equation directly.
why it matters
The result is referenced inside stress_energy_cert to certify the vacuum special case of the stress-energy properties. It closes the vacuum limit inside the conservation chain that runs from the geometric Bianchi identity through the EFE to nabla^mu T_{mu nu} = 0. In the Recognition framework it supplies the T=0 endpoint of the sourced equations before the eight-tick octave and D=3 geometry are imposed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.