einstein_tensor
plain-language theorem explainer
The definition supplies the coordinate expression for the Einstein tensor G_mu nu as the trace-adjusted Ricci tensor. Workers on the Einstein field equations in the Recognition Science coordinate formulation cite it when stating vacuum or sourced solutions. The implementation is a direct subtraction of half the scalar curvature times the metric from the Ricci tensor.
Claim. The Einstein tensor is defined by $G_{mu nu} := R_{mu nu} - (1/2) R g_{mu nu}$, where $R_{mu nu}$ denotes the Ricci tensor obtained by contraction of the Riemann tensor, $R$ is the scalar curvature obtained by further contraction with the inverse metric, and $g_{mu nu}$ is the metric tensor.
background
In the Gravity.RicciTensor module the curvature tensors are introduced in local coordinates on a 4-dimensional spacetime. The metric is represented by the structure MetricTensor whose component function g supplies g_mu nu, while InverseMetric supplies the inverse components g^mu nu. The index type Idx is the finite set Fin 4. The Ricci tensor ricci_tensor is obtained by contracting the Riemann tensor on the first and third indices, and the scalar curvature is the further contraction of the Ricci tensor with the inverse metric.
proof idea
The definition is realized by a one-line expression that subtracts half the product of the scalar curvature and the metric component from the Ricci tensor component.
why it matters
This definition supplies the left-hand side of the Einstein field equations and is invoked by vacuum_efe_coord, sourced_efe_coord, and the HilbertVariationCert that encodes the variation of the Einstein-Hilbert action. It also appears in the RicciCert that records the flat-space solution and in the symmetry theorem einstein_symmetric. Within the Recognition Science framework it furnishes the geometric side of the field equations that must be matched to the stress-energy tensor derived from the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.