Gravity Ricci Tensor Sourced Efe Coord

Sourced field equations

Einstein's field equations are the heart of general relativity. They state, in coordinate form, that the geometry of spacetime, encoded in the Einstein tensor G, balances against the matter and energy content, encoded in the stress-energy tensor T. The equation reads G_μν + Λ g_μν = κ T_μν, where g is the metric tensor, Λ is the cosmological constant, and κ is the coupling constant that sets the strength of gravity. The left side describes curvature; the right side describes what causes it.

Albert Einstein published the vacuum form in 1915 and introduced the cosmological constant the following year to permit a static universe. The sourced form, with matter on the right, is the version used for stars, black holes, and cosmology. In a vacuum, where T vanishes, the equation reduces to G_μν + Λ g_μν = 0. The framework's library, a machine-checked collection of formal theorems, defines these objects from the Riemann tensor. The Ricci tensor R_μν is a contraction of the Riemann tensor, the scalar curvature R is its trace with the inverse metric, and the Einstein tensor combines them as G_μν = R_μν − (1/2)R g_μν.

In Recognition Science, the declaration sourced_efe_coord establishes the sourced field equation as a formal definition: a statement that for every pair of indices, the Einstein tensor plus the cosmological term equals the stress-energy term. It is a definition, not a proof that any particular metric solves the equation. The library proves that flat Minkowski spacetime satisfies the vacuum equation with Λ = 0, and that the Einstein tensor is symmetric when the Ricci tensor is, which holds for a torsion-free connection. These are structural facts about the formalism.

What the declaration does not claim is equally important. It does not assert that the equation holds for any physical spacetime, nor that any specific stress-energy tensor is correct. It does not derive the value of κ, the coupling constant, from first principles. It does not prove existence or uniqueness of solutions. The declaration is a precise statement of what the equation says, not a claim that nature obeys it in any particular case. The framework's contribution here is exactness of form, not physical content.

/-- The sourced Einstein field equation:
    G_{mu nu} + Lambda g_{mu nu} = kappa T_{mu nu} -/
def sourced_efe_coord (met : MetricTensor) (ginv : InverseMetric)
    (gamma : Idx → Idx → Idx → ℝ)
    (dgamma : Idx → Idx → Idx → Idx → ℝ)
    (Lambda kappa : ℝ)
    (T : Idx → Idx → ℝ) : Prop :=
  ∀ mu nu : Idx,
    einstein_tensor met ginv gamma dgamma mu nu + Lambda * met.g mu nu =
    kappa * T 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]

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

What this page does not claim

The declaration does not assert that any particular physical spacetime satisfies the sourced equation. The declaration does not derive the numerical value of the coupling constant κ. The declaration does not prove existence or uniqueness of solutions to the field equations.

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: