Gravity Ricci Tensor

The Ricci tensor

The Ricci tensor, named for Gregorio Ricci-Curbastro, is a standard object in differential geometry. In a curved space, it is defined by contracting the Riemann curvature tensor: R_μν = R^ρ_μρν. A helpful picture: the Riemann tensor records how a vector changes when carried around a small loop, and the Ricci tensor averages that over all loop orientations. Where the Riemann tensor describes full curvature, the Ricci tensor captures the part that responds to the presence of matter and energy. In general relativity, the vacuum field equation sets the Ricci tensor to zero, meaning empty space has no volume-changing curvature.

The scalar curvature R = g^μνR_μν is the trace of the Ricci tensor, a single number at each point. The Einstein tensor G_μν = R_μν - (1/2)R g_μν combines the Ricci tensor and scalar curvature; it is the left side of the Einstein field equations. These objects were developed through the 1910s as Einstein sought a geometric description of gravity, and the Ricci tensor appears in the field equations because it is the only contraction of the Riemann tensor that preserves the needed symmetries.

In Recognition Science, the framework's machine-checked library of formal theorems defines these same objects from the Riemann tensor and proves the key structural facts. The library shows the Einstein tensor is symmetric when the Ricci tensor is, and that all three objects vanish for flat spacetime. It also defines the vacuum and sourced Einstein field equations and proves that flat Minkowski spacetime satisfies the vacuum equation with zero cosmological constant. The library's certificate bundles these results: flat spacetime has zero Ricci tensor, zero scalar curvature, zero Einstein tensor, and solves the vacuum field equation.

These are formal definitions and proofs about the standard objects, not new physics. The library establishes that the framework's formalism reproduces the classical geometric structure of general relativity. The practical consequence: when the framework later derives gravity from recognition costs, it works with the same Ricci tensor and Einstein equations that describe our universe, so the bridge from the framework's discrete ledger to continuous spacetime is built on familiar ground.

/-- The Ricci tensor: contraction of the Riemann tensor.
    R_{mu nu} = R^rho_{mu rho nu} = sum_rho R^rho_{mu rho nu} -/
noncomputable def ricci_tensor
    (gamma : Idx → Idx → Idx → ℝ)
    (dgamma : Idx → Idx → Idx → Idx → ℝ)
    (mu nu : Idx) : ℝ :=
  ∑ rho : Idx, riemann_tensor gamma dgamma rho mu rho nu

/-- Einstein tensor is symmetric when the Ricci tensor is symmetric
    (which holds when the connection is torsion-free). -/
theorem einstein_symmetric
    (met : MetricTensor) (ginv : InverseMetric)
    (gamma : Idx → Idx → Idx → ℝ)
    (dgamma : Idx → Idx → Idx → Idx → ℝ)
    (h_ricci_sym : ∀ mu nu, ricci_tensor gamma dgamma mu nu =
                            ricci_tensor gamma dgamma nu mu)
    (mu nu : Idx) :
    einstein_tensor met ginv gamma dgamma mu nu =
    einstein_tensor met ginv gamma dgamma nu mu := by
  simp only [einstein_tensor]
  rw [h_ricci_sym mu nu, met.symmetric mu nu]

/-- Flat Minkowski metric satisfies the vacuum EFE with Lambda = 0. -/
theorem minkowski_is_vacuum_solution :
    vacuum_efe_coord minkowski minkowski_inverse
      (fun _ _ _ => 0) (fun _ _ _ _ => 0) 0 := by
  intro mu nu
  simp [einstein_flat]

theorem ricci_cert : RicciCert where
  ricci_flat := RicciTensor.ricci_flat
  scalar_flat := RicciTensor.scalar_flat
  einstein_flat := RicciTensor.einstein_flat
  minkowski_vacuum := minkowski_is_vacuum_solution

What this page does not claim

The library does not prove the Einstein tensor is divergence-free in the cited declarations. The framework does not derive the Ricci tensor from recognition costs in this module. The module does not claim any new physics beyond reproducing standard general relativity.

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/RicciTensor.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: