ricci_tensor
open lean source
IndisputableMonolith.Relativity.Geometry.Curvature on GitHub at line 51.
browse module
All declarations in this module, on Recognition.
plain-language theorem explainer
The Ricci tensor arises as the contraction of the Riemann tensor on its first and third indices, producing the bilinear form R_mu nu from a given metric. Relativists deriving the Einstein field equations or the Hilbert action cite this step when reducing the full curvature to the trace needed for the Einstein tensor. The definition implements the contraction by direct summation over the four index values using the supplied Riemann tensor on the input metric.
Claim. For a metric tensor $g$, the Ricci tensor is the bilinear form $R(x, low) = sum_{rho=0}^3 R^rho{}_{mu rho nu}(x)$ where $mu$ and $nu$ are read from the two-index vector $low$ and $R^rho{}_{sigma mu nu}$ is the Riemann tensor constructed from $g$.
background
The module treats curvature quantities derived from the metric in four-dimensional spacetime. The MetricTensor structure supplies a local bilinear form $g$ on vectors indexed by Fin 4, while BilinearForm provides the codomain type for the resulting curvature objects. Christoffel symbols are obtained from the metric and its derivatives; the Riemann tensor is then built from those symbols before contraction yields the Ricci tensor.
proof idea
The definition is a direct functional wrapper. It extracts mu and nu from the low argument, then sums the Riemann tensor over rho in Fin 4 by constructing the appropriate three-index vector for each term.
why it matters
This supplies the Ricci tensor to the Einstein tensor definition and the HilbertVariationCert structure that certifies the vacuum Einstein equations for Minkowski space. It appears in the RicciCert that confirms flat spacetime satisfies the vacuum field equations with zero cosmological constant. The construction sits inside the geometric layer that ultimately connects to the eight-tick octave and D=3 spatial dimensions in the forcing chain.
depends on
-
of -
last -
mu -
of -
BilinearForm -
MetricTensor -
is -
of -
from -
is -
of -
is -
MetricTensor -
ricci_tensor -
riemann_tensor -
of -
is -
MetricTensor -
two -
last -
riemann_tensor -
MetricTensor -
BilinearForm
used by
formal source
48 Finset.univ.sum (fun (lambda : Fin 4) => Γ x rho nu lambda * Γ x lambda mu sigma)
49
50/-- **Ricci Tensor** $R_{\mu\nu} = R^{\rho}_{\mu\rho\nu}$. -/
51noncomputable def ricci_tensor (g : MetricTensor) : BilinearForm :=
52 fun x _ low =>
53 let mu := low 0
54 let nu := low 1
55 Finset.univ.sum (fun (rho : Fin 4) =>
56 riemann_tensor g x (fun _ => rho) (fun i => if i.val = 0 then mu else if i.val = 1 then rho else nu))
57
58/-- **THEOREM (Riemann Antisymmetry)**: The Riemann tensor is antisymmetric in its last two indices.
59 R^ρ_{σμν} = -R^ρ_{σνμ}
60
61 This follows directly from the definition of the Riemann tensor in terms of
62 Christoffel symbols. -/
63theorem riemann_antisymmetric_last_two (g : MetricTensor) (x : Fin 4 → ℝ) (ρ σ μ ν : Fin 4) :
64 riemann_tensor g x (fun _ => ρ) (fun i => if i.val = 0 then σ else if i.val = 1 then μ else ν) =
65 -riemann_tensor g x (fun _ => ρ) (fun i => if i.val = 0 then σ else if i.val = 1 then ν else μ) := by
66 -- The Riemann tensor definition: ∂μ Γ^ρ_νσ - ∂ν Γ^ρ_μσ + Γ^ρ_μλ Γ^λ_νσ - Γ^ρ_νλ Γ^λ_μσ
67 -- Swapping μ ↔ ν gives: ∂ν Γ^ρ_μσ - ∂μ Γ^ρ_νσ + Γ^ρ_νλ Γ^λ_μσ - Γ^ρ_μλ Γ^λ_νσ
68 -- Which is exactly the negation of the original
69 unfold riemann_tensor
70 -- Simplify the index functions - the pattern is:
71 -- LHS: low 0 = σ, low 1 = μ, low 2 = ν
72 -- RHS: low 0 = σ, low 1 = ν, low 2 = μ
73 -- The Riemann structure: ∂_{low 1} Γ_{low 2, low 0} - ∂_{low 2} Γ_{low 1, low 0} + quadratic terms
74 -- Swapping low 1 ↔ low 2 negates the expression
75 simp only [Fin.val_zero, Fin.val_one, Fin.val_two,
76 show (0 : ℕ) ≠ 1 from by decide,
77 show (1 : ℕ) ≠ 0 from by decide,
78 show (2 : ℕ) ≠ 0 from by decide, show (2 : ℕ) ≠ 1 from by decide,
79 if_true, if_false]
80 ring
81