sourced_efe_coord
plain-language theorem explainer
The declaration defines the sourced Einstein field equation in coordinates as the componentwise condition that the Einstein tensor plus Lambda times the metric equals kappa times the stress-energy tensor. Researchers stating the dynamical equations of matter-coupled gravity within the Recognition Science framework would cite this when working in local coordinates. The definition is a direct forall statement that invokes the precomputed einstein_tensor without further reduction.
Claim. $G_{mu nu} + Lambda g_{mu nu} = kappa T_{mu nu}$ for all indices $mu, nu$, where $G_{mu nu}$ denotes the Einstein tensor obtained from the metric, its inverse, the Christoffel symbols gamma, and their first derivatives dgamma.
background
The module Gravity.RicciTensor constructs the Ricci tensor, scalar curvature, and Einstein tensor from the Riemann tensor in four-dimensional spacetime. It supplies ricci_tensor as the contraction $R_{mu nu} = R^rho_{mu rho nu}$, scalar_curvature as the trace $R = g^{mu nu} R_{mu nu}$, and einstein_tensor as $G_{mu nu} = R_{mu nu} - (1/2) R g_{mu nu}$. The local setting uses coordinate components with Idx = Fin 4. Upstream MetricTensor supplies the bilinear form g while Connection provides the inverse metric and Christoffel symbols.
proof idea
This is a definition that directly states the equality using the einstein_tensor function already defined in the same module. No lemmas are applied; the body is the explicit forall statement over the four indices.
why it matters
This definition encodes the sourced Einstein field equation, the central dynamical law of general relativity with matter. It rests on the einstein_tensor construction in the same module and supports later statements such as vacuum_efe_coord and minkowski_is_vacuum_solution. In the Recognition Science framework it supplies the coordinate form of the gravity equations consistent with the forcing chain that yields D = 3 spatial dimensions and the derived constants c = 1, hbar = phi^{-5}.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.