efe_with_source
plain-language theorem explainer
The declaration defines the sourced Einstein field equations in coordinate form as the statement that the Einstein tensor plus Lambda times the metric equals kappa times the stress-energy tensor for every pair of indices. Researchers working on the Recognition Science derivation of the conservation law from the Einstein equations would cite this definition when establishing matter coupling. It is realized as a direct equational definition that simply unfolds the Einstein tensor and the stress-energy components.
Claim. The sourced Einstein field equations hold when, for all coordinate indices $mu$ and $nu$, the Einstein tensor $G_{mu nu}$ computed from the metric $g$ and its first derivatives satisfies $G_{mu nu} + Lambda g_{mu nu} = kappa T_{mu nu}$, where $T_{mu nu}$ is the symmetric stress-energy tensor obtained from the variation of the matter action.
background
The module defines the stress-energy tensor as the symmetric bilinear form $T_{mu nu}$ arising from the matter action variation: $T_{mu nu} = -(2/sqrt(-g)) delta S_matter / delta g^{mu nu}$. The Einstein tensor is constructed from the Ricci tensor and scalar curvature derived from the metric and Christoffel symbols (gamma and dgamma). This definition sits inside the conservation chain that derives nabla^mu T_{mu nu} = 0 from the contracted Bianchi identity and the Einstein equations, thereby proving Axiom 3 on matter coupling.
proof idea
This is a definition, not a theorem. It directly encodes the equality einstein_tensor met ginv gamma dgamma mu nu + Lambda * met.g mu nu = kappa * T.T mu nu inside a universal quantifier over indices. No lemmas are applied; the body is the explicit statement of the sourced EFE.
why it matters
This definition is the central object in the conservation chain of the module. It is used by the StressEnergyCert structure to certify that for kappa = 8 phi^5 the conservation law holds, and by the vacuum_is_special_case theorem to recover the vacuum equations when T vanishes. It fills the role of the sourced Einstein equations in the Recognition Science derivation of gravity, linking the geometric Einstein tensor to the matter stress-energy tensor and enabling the proof that nabla^mu T_mu nu = 0 follows from the Bianchi identity. The framework sets kappa to 8 phi^5 in RS-native units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.