scalar_flat
Scalar curvature vanishes for Minkowski spacetime when the Riemann tensor is identically zero. Researchers deriving vacuum solutions or flat-space baselines in Recognition Science gravity would cite this result. The proof is a one-line simplification that unfolds the scalar curvature definition and invokes the prior ricci_flat lemma.
claimFor the Minkowski inverse metric with vanishing connection coefficients and Riemann tensor, the scalar curvature satisfies $R = g^{mu nu} R_{mu nu} = 0$.
background
The Gravity.RicciTensor module defines the Ricci tensor as the contraction $R_{mu nu} = R^rho{}{mu rho nu}$ of the Riemann tensor and the scalar curvature as the trace $R = g^{mu nu} R{mu nu}$ with the inverse metric. Flat spacetime is represented by zero Riemann tensor input, which forces both Ricci and scalar quantities to vanish. This provides the vacuum baseline before curvature or sources are introduced.
proof idea
The proof is a one-line wrapper that applies simp to the scalar_curvature definition, which reduces directly to the Ricci tensor, and substitutes the ricci_flat result already established for zero Riemann input.
why it matters in Recognition Science
This theorem feeds einstein_flat and the RicciCert structure that certifies Minkowski spacetime as a vacuum solution to the Einstein field equations with zero cosmological constant. It anchors the gravity sector to the Recognition Science base case, consistent with T8 forcing of three spatial dimensions and the zero point of the phi-ladder before J-cost defects appear.
scope and limits
- Does not address nonzero Riemann tensors or curved metrics.
- Does not derive sourced Einstein field equations.
- Does not verify the divergence-free property of the Einstein tensor.
- Does not incorporate Recognition Science constants such as phi or alpha.
formal statement (Lean)
57theorem scalar_flat :
58 scalar_curvature minkowski_inverse (fun _ _ _ => 0) (fun _ _ _ _ => 0) = 0 := by
proof body
Term-mode proof.
59 simp [scalar_curvature, ricci_flat]
60
61/-! ## Einstein Tensor -/
62
63/-- The Einstein tensor: G_{mu nu} = R_{mu nu} - (1/2) R g_{mu nu}.
64 This is the LHS of the Einstein field equations. -/