einstein_tensor
plain-language theorem explainer
Einstein tensor is defined pointwise as the Ricci tensor minus half the metric times the Ricci scalar. General relativists cite it when writing the left-hand side of the Einstein field equations or varying the Hilbert action. The implementation is a direct algebraic combination of the upstream ricci_tensor and ricci_scalar functions.
Claim. $G(g) = R(g) - (1/2) g R(g)$, where $R(g)$ is the Ricci tensor obtained by contracting the Riemann tensor and $R(g)$ is the Ricci scalar obtained by tracing the Ricci tensor with the inverse metric.
background
The module builds curvature objects from the metric. MetricTensor supplies the components of the spacetime metric at each point, while BilinearForm is the type for the resulting rank-two tensors. Ricci tensor and Ricci scalar are imported from the Gravity.RicciTensor module, where the former contracts the Riemann tensor and the latter traces the result.
proof idea
One-line definition that subtracts half the metric-scaled Ricci scalar from the Ricci tensor using the ricci_tensor and ricci_scalar operations.
why it matters
The definition supplies the Einstein tensor to HilbertVariationCert and to the vacuum and sourced Einstein field equation statements in Gravity.RicciTensor. It completes the geometric side of the Einstein equations, linking curvature quantities to the Recognition framework's metric-based forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.