Encyclopedia Gravity Gravity Riemann Tensor Algebraic Bianchi
ARTICLE 4 claims 4 theorems
Gravity Riemann Tensor Algebraic Bianchi
The Riemann curvature tensor measures how spacetime bends; the algebraic Bianchi identity is a symmetry it must obey, proved here from the Christoffel symbols.
The algebraic Bianchi identity
The Riemann curvature tensor is the standard object in differential geometry that measures how a space bends. In general relativity, it encodes the gravitational field through the curvature of spacetime. The tensor is built from the Christoffel symbols, which describe how coordinates change from point to point, and from their derivatives. Written in local coordinates, the Riemann tensor takes the form 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 algebraic Bianchi identity is a symmetry relation that this tensor satisfies. It states that the sum of the tensor with its indices cyclically permuted vanishes: R^rho_{sigma mu nu} + R^rho_{mu nu sigma} + R^rho_{nu sigma mu} = 0. This identity holds when the Christoffel symbols are symmetric in their lower two indices, which corresponds to a torsion-free connection, the standard condition in general relativity. The identity is called algebraic because it follows from the definition of the tensor and the symmetry of the symbols, without needing any further geometric input.
The machine-checked library of formal theorems proves this identity as the declaration algebraic_bianchi. The proof assumes the Christoffel symbols and their derivatives are symmetric, then expands the definition of the Riemann tensor and simplifies the resulting sum to zero. The same library also proves that the Riemann tensor is antisymmetric in its last two indices, meaning swapping those indices negates the tensor, and that the tensor vanishes identically in flat spacetime where all Christoffel symbols are zero.
What the declaration does not claim is important. It does not prove the differential Bianchi identity, which involves covariant derivatives and is a separate, deeper result. It does not establish that the Riemann tensor has any particular physical meaning or that spacetime is curved in any actual situation. The theorem is purely algebraic: given symmetric symbols, the cyclic sum is zero. It says nothing about whether those symbols correspond to a real gravitational field, which is a separate physical question about the Einstein field equations.
Within the framework of Recognition Science, this algebraic identity is a building block. The framework's library treats general relativity as itself derived from more basic recognition principles, and this theorem is one of the formal results that the framework's account of gravity relies on. But the algebraic Bianchi identity itself is a classical result of differential geometry, known long before the framework existed. The framework's contribution is to have it machine-checked as part of a larger formal library, not to have discovered the identity.
THEOREM algebraic_bianchi · IndisputableMonolith/Gravity/RiemannTensor.lean
/-- 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 algebraic_bianchi · IndisputableMonolith/Gravity/RiemannTensor.lean
/-- 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_antisymmetric_last_two · IndisputableMonolith/Gravity/RiemannTensor.lean
/-- 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 riemann_flat_vanishes · IndisputableMonolith/Gravity/RiemannTensor.lean
/-- 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 differential Bianchi identity, which involves covariant derivatives, is not proved here. The theorem does not assert that any particular physical spacetime is curved. The framework did not discover the algebraic Bianchi identity; it machine-checked a classical result.
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:
- What is the differential Bianchi identity and how does it differ from the algebraic one?
- How does the Riemann tensor relate to the Einstein field equations and physical spacetime curvature?
- What role does the algebraic Bianchi identity play in the Recognition Science derivation of general relativity?
- Under what conditions do the Christoffel symbols fail to be symmetric, and what physical situation does that describe?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM algebraic_bianchi · IndisputableMonolith/Gravity/RiemannTensor.lean
/-- 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) linarithThe algebraic Bianchi identity states that the cyclic sum of the Riemann tensor vanishes: R^rho_{sigma mu nu} + R^rho_{mu nu sigma} + R^rho_{nu sigma mu} = 0. algebraic_bianchi · IndisputableMonolith/Gravity/RiemannTensor.leanTHEOREM algebraic_bianchi · IndisputableMonolith/Gravity/RiemannTensor.lean
/-- 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) linarithThe identity holds when the Christoffel symbols and their derivatives are symmetric in the lower indices. algebraic_bianchi · IndisputableMonolith/Gravity/RiemannTensor.leanTHEOREM riemann_antisymmetric_last_two · IndisputableMonolith/Gravity/RiemannTensor.lean
/-- 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] ringThe Riemann tensor is antisymmetric in its last two indices. riemann_antisymmetric_last_two · IndisputableMonolith/Gravity/RiemannTensor.leanTHEOREM riemann_flat_vanishes · IndisputableMonolith/Gravity/RiemannTensor.lean
/-- 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]The Riemann tensor vanishes in flat spacetime where all Christoffel symbols are zero. riemann_flat_vanishes · IndisputableMonolith/Gravity/RiemannTensor.lean