Encyclopedia Gravity Gravity Riemann Tensor

ARTICLE 3 claims 3 theorems

Gravity Riemann Tensor

The Riemann tensor is the mathematical object that tells you a space is curved, and a machine-checked library has now proven its core properties from scratch.

Verify this page

The curvature tensor

The Riemann curvature tensor is the standard tool in differential geometry for measuring how much a space curves. In general relativity, it describes how gravity warps spacetime. The tensor takes four indices, written R^rho_{sigma mu nu}, and its value at a point captures how a vector changes when you move it around a tiny loop. If the space is flat, like ordinary Euclidean space or Minkowski spacetime, the tensor is zero everywhere. If it is not zero, the space is genuinely curved, and that curvature is what we feel as gravity.

In local coordinates, the tensor is built from the Christoffel symbols, which encode how the coordinate system twists and stretches. The definition is R^rho_{sigma mu nu} = d_mu Gamma^rho_{nu sigma} - d_nu Gamma^rho_{mu sigma} + Gamma^rho_{mu lambda} Gamma^lambda_{nu sigma} - Gamma^rho_{nu lambda} Gamma^lambda_{mu sigma}. The first two terms measure how the connection changes from point to point; the last two are corrections for how the basis vectors themselves bend. This formula, introduced by Bernhard Riemann in the 1860s and refined by Elwin Christoffel and Gregorio Ricci-Curbastro, is the foundation of Einstein's field equations.

The tensor obeys two important algebraic identities. It is antisymmetric in its last two indices: swapping mu and nu changes the sign, so R^rho_{sigma mu nu} = -R^rho_{sigma nu mu}. It also satisfies the algebraic Bianchi identity, which says that the cyclic sum of the last three indices vanishes: R^rho_{sigma mu nu} + R^rho_{mu nu sigma} + R^rho_{nu sigma mu} = 0. This second identity is a consequence of the connection being torsion-free, meaning the Christoffel symbols are symmetric in their lower indices. These identities are not optional extras; they constrain which curvature patterns can actually arise from a metric.

In Recognition Science, the framework's machine-checked library of formal theorems has taken these classical facts and proven them in a formal proof system. The library defines the Riemann tensor exactly as above, then proves the antisymmetry, the algebraic Bianchi identity, and the fact that the tensor vanishes in flat spacetime. The proofs are checked by the kernel, so they carry the same certainty as the framework's other foundational results. This is not a new physical claim; it is a verification that the standard mathematics of gravity is consistent with the framework's own logical foundations.

What this establishes in plain language is that the framework can reproduce the core mathematical machinery of general relativity without adding extra assumptions. The Riemann tensor, its symmetries, and its flat-space behavior all follow from the definitions. This matters because the framework aims to derive physics from a single principle, and here it shows that the geometric language of gravity is not foreign to that project. The result is a bridge: the same formal system that proves the framework's cost function also proves the standard curvature identities. That is a concrete, checkable step toward showing that gravity, as described by Einstein, fits inside the framework's picture.

THEOREM riemann_antisymmetric_last_two · 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
THEOREM algebraic_bianchi · IndisputableMonolith/Gravity/RiemannTensor.lean
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
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]

What this page does not claim

This answer does not claim the framework derives general relativity's field equations. This answer does not claim the Riemann tensor's symmetries are new physics. This answer does not claim the framework explains why spacetime has four dimensions.

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