Encyclopedia Gravity Gravity Riemann Tensor Riemann Flat Vanishes

ARTICLE 3 claims 2 theorems 1 open

Gravity Riemann Tensor Riemann Flat Vanishes

In general relativity, the Riemann tensor measures how spacetime curves; this theorem confirms that in perfectly flat, Minkowski spacetime, that curvature measure is exactly zero.

Verify this page

The flat spacetime theorem

The Riemann curvature tensor is the standard mathematical object that describes how spacetime bends. In general relativity, gravity is not a force pulling objects; it is the curvature of spacetime itself. The tensor, written as R^rho_{sigma mu nu}, is built from the Christoffel symbols, which encode how coordinates change from point to point. A flat spacetime, such as the Minkowski spacetime of special relativity, has no gravity and no curvature, so its Christoffel symbols are all zero.

The theorem riemann_flat_vanishes states that when all Christoffel symbols and their derivatives are zero, the Riemann tensor is identically zero for every choice of indices. This is a direct, machine-checked result: substituting zero into the defining formula cancels every term, leaving zero. The result is a sanity check, not a discovery. It confirms that the formal definition of curvature behaves exactly as the physics demands: no gravity, no curvature.

In Recognition Science, this theorem is part of a larger machine-checked library of formal theorems about gravity. The library also proves that the tensor is antisymmetric in its last two indices and satisfies the algebraic Bianchi identity, which are structural properties that hold for any connection. The flat spacetime result is the simplest of these: it verifies the boundary case where the machinery produces nothing.

What the theorem does not claim is more interesting. It does not show that a vanishing Riemann tensor implies flat spacetime in all cases. That converse statement, which is true for simply connected regions, is a separate theorem not included here. It also does not address the Ricci tensor, the Ricci scalar, or the Einstein field equations, which are built from contractions of the Riemann tensor. The theorem only handles the specific case where the connection is identically zero.

For a reader, the value is clarity about what a formal proof can and cannot do. The theorem shows that the definition of curvature is consistent with the simplest physical case. It does not explain why gravity curves spacetime, nor does it derive the field equations. It is a small, verified brick in a larger structure, and knowing exactly what that brick supports is what makes the structure trustworthy.

THEOREM riemann_flat_vanishes · IndisputableMonolith/Gravity/RiemannTensor.lean
riemann_flat_vanishes · IndisputableMonolith/Gravity/RiemannTensor.lean:59 
/-- For flat spacetime (all Gamma = 0, all dGamma = 0), the Riemann tensor vanishes. -/
theorem riemann_flat_vanishes (rho sigma mu nu : Idx) :
    riemann_tensor (fun _ _ _ => 0) (fun _ _ _ _ => 0) rho sigma mu nu = 0 := by
  simp [riemann_tensor]
THEOREM riemann_antisymmetric_last_two · algebraic_bianchi · IndisputableMonolith/Gravity/RiemannTensor.lean
riemann_antisymmetric_last_two · IndisputableMonolith/Gravity/RiemannTensor.lean:45 
/-- R^rho_{sigma mu nu} is antisymmetric in the last two indices:
    R^rho_{sigma mu nu} = -R^rho_{sigma nu mu}.

    Proof: swapping mu <-> nu negates the d_mu Gamma - d_nu Gamma terms
    and swaps the quadratic Gamma terms. -/
theorem riemann_antisymmetric_last_two
    (gamma : Idx → Idx → Idx → ℝ)
    (dgamma : Idx → Idx → Idx → Idx → ℝ)
    (rho sigma mu nu : Idx) :
    riemann_tensor gamma dgamma rho sigma mu nu =
    -(riemann_tensor gamma dgamma rho sigma nu mu) := by
  simp only [riemann_tensor]
  ring
algebraic_bianchi · IndisputableMonolith/Gravity/RiemannTensor.lean:66 
/-- The algebraic (first) Bianchi identity:
    R^rho_{sigma mu nu} + R^rho_{mu nu sigma} + R^rho_{nu sigma mu} = 0

    This is a consequence of the torsion-free condition (symmetric Christoffel). -/
theorem algebraic_bianchi
    (gamma : Idx → Idx → Idx → ℝ)
    (dgamma : Idx → Idx → Idx → Idx → ℝ)
    (h_sym : ∀ rho mu nu, gamma rho mu nu = gamma rho nu mu)
    (h_dsym : ∀ lambda rho mu nu, dgamma lambda rho mu nu = dgamma lambda rho nu mu)
    (rho sigma mu nu : Idx) :
    riemann_tensor gamma dgamma rho sigma mu nu +
    riemann_tensor gamma dgamma rho mu nu sigma +
    riemann_tensor gamma dgamma rho nu sigma mu = 0 := by
  have anti1 := riemann_antisymmetric_last_two gamma dgamma rho sigma mu nu
  have anti2 := riemann_antisymmetric_last_two gamma dgamma rho mu nu sigma
  have anti3 := riemann_antisymmetric_last_two gamma dgamma rho nu sigma mu
  simp only [riemann_tensor] at *
  have quad_cancel : ∀ x : Idx,
    (gamma rho mu x * gamma x nu sigma - gamma rho nu x * gamma x mu sigma) +
    (gamma rho nu x * gamma x sigma mu - gamma rho sigma x * gamma x nu mu) +
    (gamma rho sigma x * gamma x mu nu - gamma rho mu x * gamma x sigma nu) = 0 := by
    intro x
    rw [h_sym x nu sigma, h_sym x mu sigma, h_sym x sigma mu,
        h_sym x nu mu, h_sym x mu nu, h_sym x sigma nu]; ring
  have h_sums : (∑ x : Idx, (gamma rho mu x * gamma x nu sigma - gamma rho nu x * gamma x mu sigma)) +
    (∑ x : Idx, (gamma rho nu x * gamma x sigma mu - gamma rho sigma x * gamma x nu mu)) +
    (∑ x : Idx, (gamma rho sigma x * gamma x mu nu - gamma rho mu x * gamma x sigma nu)) = 0 := by
    rw [← Finset.sum_add_distrib, ← Finset.sum_add_distrib]
    exact Finset.sum_eq_zero (fun x _ => quad_cancel x)
  have key : ∀ x : Idx,
    (gamma rho mu x * gamma x nu sigma - gamma rho nu x * gamma x mu sigma) +
    (gamma rho nu x * gamma x sigma mu - gamma rho sigma x * gamma x nu mu) +
    (gamma rho sigma x * gamma x mu nu - gamma rho mu x * gamma x sigma nu) = 0 := by
    intro x; rw [h_sym x nu sigma, h_sym x mu sigma, h_sym x sigma mu,
                  h_sym x nu mu, h_sym x mu nu, h_sym x sigma nu]; ring
  have sum_zero :
    (∑ x : Idx, (gamma rho mu x * gamma x nu sigma - gamma rho nu x * gamma x mu sigma)) +
    (∑ x : Idx, (gamma rho nu x * gamma x sigma mu - gamma rho sigma x * gamma x nu mu)) +
    (∑ x : Idx, (gamma rho sigma x * gamma x mu nu - gamma rho mu x * gamma x sigma nu)) = 0 := by
    rw [← Finset.sum_add_distrib, ← Finset.sum_add_distrib]
    exact Finset.sum_eq_zero (fun x _ => key x)
  have neg_flip : ∀ (f g : Idx → ℝ),
    ∑ x : Idx, (f x - g x) = -(∑ x : Idx, (g x - f x)) := by
    intros f g
    have : ∀ x ∈ Finset.univ, f x - g x = -(g x - f x) := by intros; ring
    rw [Finset.sum_congr rfl this, Finset.sum_neg_distrib]
  rw [h_dsym mu rho nu sigma, h_dsym nu rho mu sigma, h_dsym nu rho sigma mu,
      h_dsym sigma rho nu mu, h_dsym sigma rho mu nu, h_dsym mu rho sigma nu]
  have full_sum :
    (∑ x : Idx, (gamma rho mu x * gamma x nu sigma)) -
    (∑ x : Idx, (gamma rho nu x * gamma x mu sigma)) +
    ((∑ x : Idx, (gamma rho nu x * gamma x sigma mu)) -
     (∑ x : Idx, (gamma rho sigma x * gamma x nu mu))) +
    ((∑ x : Idx, (gamma rho sigma x * gamma x mu nu)) -
     (∑ x : Idx, (gamma rho mu x * gamma x sigma nu))) = 0 := by
    rw [← Finset.sum_sub_distrib, ← Finset.sum_sub_distrib, ← Finset.sum_sub_distrib,
        ← Finset.sum_add_distrib, ← Finset.sum_add_distrib]
    exact Finset.sum_eq_zero (fun x _ => key x)
  linarith

What this page does not claim

The theorem does not prove the converse statement that zero curvature always implies flat spacetime. It does not involve the Ricci tensor or the Einstein field equations. It does not explain the physical mechanism by which mass curves spacetime.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/RiemannTensor.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND