Gravity Riemann Tensor Riemann Antisymmetric Last Two

The antisymmetry theorem

The Riemann curvature tensor is the standard object in differential geometry that measures how much a space curves. In general relativity, it encodes the gravitational field. Written with four indices as R^rho_{sigma mu nu}, it is built from Christoffel symbols, which describe how coordinates change from point to point, and their derivatives. The tensor's definition is long, but one of its properties is simple: swap the last two indices, mu and nu, and the entire value changes sign. That is, R^rho_{sigma mu nu} = -R^rho_{sigma nu mu}. This is the antisymmetry in the last two indices.

This antisymmetry is not an extra assumption. It follows directly from the definition of the Riemann tensor, which is why it holds for any space, curved or flat, as long as the connection is the standard Levi-Civita one. The proof is a short algebraic check: swapping the indices negates the two derivative terms and swaps the two quadratic terms, leaving a minus sign in front of the whole expression. The same property appears in every textbook on general relativity; it is one of the algebraic identities that make the tensor tractable.

In the Recognition Science framework, this property is not taken on faith. The framework's machine-checked library of formal theorems contains a declaration, riemann_antisymmetric_last_two, that proves the identity for an arbitrary set of indices. The proof script is two lines long and uses only the definition and the ring axiom, meaning the result is checked step by step by the computer. This is a theorem, not a model or a hypothesis: it is a fully verified statement about the Riemann tensor as defined.

The declaration also comes with a companion result: for flat spacetime, where all Christoffel symbols and their derivatives are zero, the Riemann tensor vanishes. Together, these two facts form a certificate, a packaged proof that the antisymmetry and the flat-space vanishing both hold. This certificate is what the framework's library offers: not a new physical claim, but a rigorous guarantee that a standard piece of geometry is correct.

What the declaration does not claim is just as important. It does not say that the Riemann tensor is the only object with this property, nor does it derive the tensor from the framework's own axioms. It proves a property of a definition that already exists in the library. It also does not claim anything about the physical interpretation of curvature, such as whether spacetime is actually curved or how gravity behaves; those are separate questions. The theorem is a piece of pure mathematics, verified in isolation.

The practical consequence is that anyone building on the Riemann tensor in the framework's library can rely on this symmetry without rechecking it. It is a small but solid brick in a larger structure. The antisymmetry is not a deep mystery; it is a fact that any careful student of geometry would expect. The framework's contribution is to make that expectation a formal certainty.

/-- 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

/-- 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 declaration does not derive the Riemann tensor from the framework's own axioms. It does not claim anything about the physical interpretation of curvature or gravity. It does not prove the full set of Riemann tensor symmetries, only the antisymmetry in the last two indices.

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: