Encyclopedia Gravity Gravity Riemann Tensor Riemann Tensor

ARTICLE 4 claims 4 theorems

Gravity Riemann Tensor Riemann Tensor

The Riemann curvature tensor measures how much a space bends by tracking how parallel lines twist when carried around a loop.

Verify this page

The Riemann tensor in coordinates

The Riemann curvature tensor is the standard mathematical tool for describing how a space is curved. In general relativity, gravity is not a force pulling objects together but the curvature of spacetime itself, and this tensor is the precise way to express that curvature. The definition starts with the Christoffel symbols, which describe how coordinate directions change from point to point, and then combines those symbols and their derivatives to produce a four-index object R^rho_{sigma mu nu} that encodes the local geometry.

In local coordinates the tensor is defined by a specific formula: 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}. This expression combines the derivatives of the Christoffel symbols with products of the symbols themselves. The result is a quantity that vanishes exactly when the space is flat, meaning when the geometry is the same everywhere as ordinary Euclidean space or Minkowski spacetime.

The definition was introduced by Bernhard Riemann in the 1850s as a way to distinguish curved spaces from flat ones without needing to embed them in a higher-dimensional space. It became the central object of general relativity when Albert Einstein used it to formulate the field equations in 1915. The tensor's key property is that it measures curvature intrinsically, using only measurements made within the space itself, not from outside it.

The tensor satisfies several algebraic identities that constrain its structure. It is antisymmetric in its last two indices, meaning swapping those indices changes the sign: R^rho_{sigma mu nu} = -R^rho_{sigma nu mu}. It also satisfies the algebraic Bianchi identity, which states that the cyclic sum R^rho_{sigma mu nu} + R^rho_{mu nu sigma} + R^rho_{nu sigma mu} vanishes, provided the Christoffel symbols are symmetric in their lower indices, a condition known as torsion-free. In flat spacetime, where all Christoffel symbols and their derivatives are zero, the tensor vanishes identically.

In Recognition Science, the framework's machine-checked library of formal theorems defines this tensor in coordinates and proves these algebraic properties. The declaration riemann_tensor establishes the coordinate formula, and the theorems riemann_antisymmetric_last_two and algebraic_bianchi prove the antisymmetry and the Bianchi identity respectively. The framework also proves riemann_flat_vanishes, showing the tensor is zero in flat spacetime. These are formal results about the algebraic structure of the tensor, checked mechanically by the library's proof checker.

What the framework does not claim is equally important. The declaration does not derive the Riemann tensor from the Recognition Science forcing chain; it simply defines the standard coordinate expression and proves its algebraic properties. It does not prove that this tensor is the unique or necessary curvature object for the framework's physical claims. It does not establish the physical interpretation of curvature as gravity, nor does it connect the tensor to the framework's other results about dimensions or constants. The theorems are about the mathematics of the tensor as it appears in standard differential geometry, not about the framework's distinctive physical predictions.

The practical consequence is that a reader can trust the algebraic identities as machine-checked facts, while understanding that the framework's broader claims about gravity, such as how curvature relates to the forced constants or dimensions, remain separate targets. The tensor definition and its symmetries are a solid foundation, but they are not the whole story of how the framework treats gravity.

THEOREM riemann_tensor · IndisputableMonolith/Gravity/RiemannTensor.lean
riemann_tensor · IndisputableMonolith/Gravity/RiemannTensor.lean:27 
/-- The Riemann curvature tensor in local coordinates:
    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}

    Inputs:
    - gamma: Christoffel symbols Gamma^rho_{mu nu}
    - dgamma: derivatives d_lambda Gamma^rho_{mu nu} -/
noncomputable def riemann_tensor
    (gamma : Idx → Idx → Idx → ℝ)
    (dgamma : Idx → Idx → Idx → Idx → ℝ)
    (rho sigma mu nu : Idx) : ℝ :=
  dgamma mu rho nu sigma - dgamma nu rho mu sigma +
  ∑ lambda : Idx, (gamma rho mu lambda * gamma lambda nu sigma) -
  ∑ lambda : Idx, (gamma rho nu lambda * gamma lambda mu sigma)
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

The Riemann tensor is not derived from the Recognition Science forcing chain. The declaration does not prove that this tensor is the unique curvature object for the framework. No physical interpretation of curvature as gravity is established by these theorems.

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