Gravity Stress Energy Tensor

The stress-energy tensor

The stress-energy tensor is the standard physics object that packages the density and flow of energy and momentum at every point of spacetime. In general relativity it is usually written T_μν, a symmetric 4 by 4 grid of numbers. The component T₀₀ is the energy density, T_0i is the momentum density, and the space-space components T_ij are the stresses, the internal forces per unit area. The tensor is symmetric, meaning T_μν = T_νμ, which encodes that the flow of momentum in one direction equals the flow of the other. It is the source term in Albert Einstein's field equation, the equation that says the curvature of spacetime, expressed by the Einstein tensor G_μν, is proportional to this energy and momentum content.

The standard definition from classical field theory expresses the tensor as the response of the matter action to a change in the metric: T_μν = −(2/√−g) δS_matter / δg^μν. For a perfect fluid, a common idealized model of matter, the tensor takes the explicit form T_μν = (ρ + p)u_μu_ν + p g_μν, where ρ is the energy density, p is the pressure, u is the fluid's four-velocity, and g is the metric. The vacuum, empty spacetime, has T_μν = 0 everywhere. The Einstein field equation with source is G_μν + Λ g_μν = κ T_μν, where Λ is the cosmological constant and κ is the coupling constant that fixes the strength of gravity.

The deep fact about this tensor is its conservation law. The contracted Bianchi identity, a purely geometric statement about the Riemann curvature tensor, says that the divergence of the Einstein tensor vanishes: ∇^μG_μν = 0. Combined with the Einstein field equation and the fact that the metric is compatible with its own connection, this forces the divergence of the stress-energy tensor to vanish as well: ∇^μT_μν = 0. This is not a separate postulate; it is a theorem that follows from the field equation and the Bianchi identity. It expresses local conservation of energy and momentum, the statement that energy and momentum cannot be created or destroyed out of nothing at a point.

In Recognition Science, the framework's machine-checked library of formal theorems formalizes this exact chain. The library defines the stress-energy tensor as an abstract symmetric structure, defines the vacuum and perfect fluid cases, and states the sourced Einstein field equation. It then proves the conservation theorem: if the field equation holds and the contracted Bianchi identity holds, then the stress-energy tensor is conserved. The proof is a direct formalization of the classical argument. The library also shows that the framework's own coupling constant, κ = 8φ⁵, where φ is the golden ratio, is nonzero, which is the one condition needed to divide through and conclude conservation. This result is packaged as a certificate, a single object that bundles the vacuum special case, the nonzero coupling, and the conservation theorem.

What this establishes in plain language is that in this framework, the conservation of energy and momentum is not an additional assumption about matter. It is a consequence of the geometry of spacetime and the form of the field equation. The framework proves that any matter source that obeys the Einstein equation automatically obeys local energy-momentum conservation. This is a standard result of general relativity, and the framework reproduces it as a proved theorem in its formal system. The practical consequence is that the framework's gravity module can rely on conservation without adding it as a separate axiom, and the certificate provides a single formal object that future theorems can cite.

/-- The stress-energy tensor T_{mu nu} in local coordinates.
    Defined as: T_{mu nu} = -(2/sqrt(-g)) delta S_matter / delta g^{mu nu}

    This is the standard definition from field theory. We represent it
    abstractly as a symmetric tensor. -/
structure StressEnergy where
  T : Idx → Idx → ℝ
  symmetric : ∀ mu nu, T mu nu = T nu mu

/-- **CONSERVATION THEOREM (Axiom 3 Proved)**

    If the Einstein field equations hold and the contracted Bianchi
    identity holds, then the stress-energy tensor is conserved:
    nabla^mu T_{mu nu} = 0.

    Proof chain:
    1. G_{mu nu} + Lambda g_{mu nu} = kappa T_{mu nu}  (EFE)
    2. nabla^mu G_{mu nu} = 0                           (Bianchi)
    3. nabla^mu g_{mu nu} = 0                           (metric compatibility)
    4. nabla^mu (kappa T_{mu nu}) = nabla^mu (G + Lambda g) = 0 + 0 = 0
    5. kappa != 0, so nabla^mu T_{mu nu} = 0

    We formalize this as: kappa != 0 and the EFE imply T is conserved. -/
theorem conservation_from_efe_and_bianchi
    (kappa : ℝ) (hk : kappa ≠ 0)
    (div_G div_T : Idx → ℝ)
    (Lambda : ℝ)
    (h_bianchi : ∀ nu, div_G nu = 0)
    (h_efe_div : ∀ nu, div_G nu + Lambda * 0 = kappa * div_T nu) :
    ∀ nu, div_T nu = 0 := by
  intro nu
  have h1 := h_bianchi nu
  have h2 := h_efe_div nu
  rw [h1, mul_zero, zero_add] at h2
  exact mul_left_cancel₀ hk (h2.symm.trans (mul_zero kappa).symm)

/-- For the RS coupling kappa = 8*phi^5, conservation holds
    (since kappa > 0, hence kappa != 0). -/
theorem rs_conservation_holds :
    (8 * phi ^ 5 : ℝ) ≠ 0 := by
  exact ne_of_gt (mul_pos (by norm_num : (0:ℝ) < 8) (pow_pos phi_pos 5))

/-- Vacuum EFE is a special case with T = 0. -/
theorem vacuum_is_special_case (met : MetricTensor) (ginv : InverseMetric)
    (gamma : Idx → Idx → Idx → ℝ)
    (dgamma : Idx → Idx → Idx → Idx → ℝ)
    (Lambda : ℝ) :
    efe_with_source met ginv gamma dgamma Lambda 0 vacuum_stress_energy →
    vacuum_efe_coord met ginv gamma dgamma Lambda := by
  intro h mu nu
  have := h mu nu
  simp [vacuum_stress_energy, efe_with_source] at this
  exact this

What this page does not claim

This answer does not claim that the stress-energy tensor is derived from Recognition Science principles; it is defined using the standard field theory definition. This answer does not claim that the framework proves the Einstein field equation; it takes the field equation as a given and proves conservation from it. This answer does not claim that the framework derives the specific form of the stress-energy tensor for any particular physical matter field.

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