ricci_scalar
plain-language theorem explainer
The ricci_scalar definition supplies the scalar curvature R obtained by contracting the Ricci tensor against the inverse metric at a spacetime point. Relativists assembling the Einstein-Hilbert action or verifying the flat-space limit in Recognition Science cite this contraction. The definition is a direct double summation that implements the standard trace operation on the supplied metric interface.
Claim. $R(g,x) = g^{00}(x) R_{00}(x) + g^{01}(x) R_{01}(x) + g^{02}(x) R_{02}(x) + g^{03}(x) R_{03}(x) + g^{10}(x) R_{10}(x) + g^{11}(x) R_{11}(x) + g^{12}(x) R_{12}(x) + g^{13}(x) R_{13}(x) + g^{20}(x) R_{20}(x) + g^{21}(x) R_{21}(x) + g^{22}(x) R_{22}(x) + g^{23}(x) R_{23}(x) + g^{30}(x) R_{30}(x) + g^{31}(x) R_{31}(x) + g^{32}(x) R_{32}(x) + g^{33}(x) R_{33}(x)$, where $g$ is a metric tensor and $R_{ab}$ is the Ricci tensor at point $x$.
background
The module constructs curvature scalars from the metric tensor, a symmetric bilinear form on four-dimensional spacetime points supplied by the MetricTensor structure in Foundation.Hamiltonian and Gravity.Connection. The Ricci tensor is obtained by contracting the Riemann tensor, as defined upstream in Gravity.RicciTensor.ricci_tensor. The inverse_metric accessor raises indices for the final trace. Module documentation states that Christoffel symbols are derived from the metric, providing the local geometric setting for all curvature quantities.
proof idea
The definition is a direct double sum over Fin 4 indices that contracts the inverse metric with the Ricci tensor. It applies inverse_metric g x on pairs (mu, nu) and ricci_tensor g x with index selectors that fix the first slot to 0 while mapping the second slot to the running indices. No lemmas are invoked; the body is the explicit summation implementing the trace.
why it matters
This definition feeds the Einstein-Hilbert action in Relativity.Fields.Integration and the Einstein tensor in the same module. It closes the curvature chain inside the FlatChain structure for Minkowski space, where the scalar is shown to vanish. In the Recognition framework the scalar supplies the R appearing in the action integral and confirms zero curvature for flat spacetime, consistent with the J-cost expansion to second order.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.