einstein_tensor
plain-language theorem explainer
The Einstein tensor is defined pointwise as the Ricci tensor minus half the scalar curvature times the metric component. Researchers stating the coordinate form of the Einstein field equations cite this definition when working with vacuum or sourced solutions. The definition is realized as a direct algebraic subtraction that invokes the sibling Ricci tensor and scalar curvature constructions.
Claim. The Einstein tensor is given by $G_{mu nu} := R_{mu nu} - (1/2) R g_{mu nu}$, where $R_{mu nu}$ is the Ricci tensor obtained by contracting the Riemann tensor on the first and third indices and $R$ is the scalar curvature obtained by contracting the Ricci tensor with the inverse metric.
background
The RicciTensor module defines the Einstein tensor after first introducing the Ricci tensor as the contraction $R_{mu nu} = R^rho_{mu rho nu}$ and the scalar curvature as the further contraction $R = g^{mu nu} R_{mu nu}$. The metric is supplied by the MetricTensor structure whose g component returns the lowered-index bilinear form, while InverseMetric supplies the raised-index inverse satisfying the usual delta relation. Connection coefficients gamma and their first derivatives dgamma serve as the explicit inputs that build the curvature tensors in local coordinates.
proof idea
The definition is a one-line algebraic wrapper that subtracts half the scalar curvature times the metric from the Ricci tensor. It directly applies the sibling definitions ricci_tensor and scalar_curvature with no additional lemmas or tactics required.
why it matters
This definition supplies the left-hand side for the vacuum and sourced Einstein field equations (vacuum_efe_coord and sourced_efe_coord) and is invoked to certify that Minkowski space solves the vacuum equations (RicciCert and einstein_flat). It also enters the HilbertVariationCert that recovers the Einstein tensor from the variation of the Einstein-Hilbert action. Within the Recognition Science framework the construction closes the coordinate expression of the gravitational field equations that follow from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.