Gravity Stress Energy Tensor Vacuum Stress Energy

The zero tensor

The stress-energy tensor is the object in general relativity that describes how much energy, momentum, and stress occupy a region of spacetime. It is a rank-2 tensor, written T_μν, and its components answer concrete questions: T₀₀ is the energy density, T_0i is the momentum density, and T_ij are the stresses. In the standard field-theory definition, it is the variation of the matter action with respect to the metric, T_μν = −(2/√−g) δS_matter/δg^μν, and it is symmetric in its two indices.

The vacuum stress-energy tensor is the simplest possible case: it is identically zero. Every component, for every pair of indices, is set to 0. This is not a physical discovery but a definitional choice, a way to say that a region contains no matter or radiation. The framework's machine-checked library of formal theorems represents it as a structure with a function that returns 0 for all inputs and a proof of symmetry that holds by reflexivity. The definition is exactly what a textbook would write for empty space.

The zero tensor matters because it plugs into the Einstein field equations. With the source term set to zero, the equations reduce to the vacuum field equations, G_μν + Λg_μν = 0. The library proves this reduction as a theorem, vacuum_is_special_case, showing that the sourced equations with the zero tensor are equivalent to the vacuum form. This is the formal bridge between the general statement and the special case used for gravitational waves and black hole exteriors.

In Recognition Science, the declaration does more than define an object: it anchors a conservation law. The framework proves that if the Einstein field equations hold and the contracted Bianchi identity holds, then the stress-energy tensor is conserved, ∇^μT_μν = 0. The proof chain is short: the Bianchi identity kills the divergence of the Einstein tensor, metric compatibility kills the divergence of the metric, and the field equations then force the divergence of T to vanish, provided the coupling constant κ is nonzero. The library checks this for the framework's own coupling, κ = 8φ⁵, which is positive and therefore nonzero.

The declaration does not claim that empty space has no energy in any quantum sense. It does not address vacuum energy, zero-point fluctuations, or the cosmological constant problem, where quantum field theory suggests a large vacuum energy that observation does not confirm. It also does not claim that the conservation law is new physics; it is the standard result from general relativity, restated in the framework's notation. The zero tensor is a definition, and the conservation theorem is a formal consequence of the field equations, not an independent physical postulate.

/-- The vacuum (zero) stress-energy tensor. -/
def vacuum_stress_energy : StressEnergy where
  T := fun _ _ => 0
  symmetric := fun _ _ => rfl

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

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

What this page does not claim

The zero tensor does not represent a quantum vacuum with zero-point energy. The conservation law is not a new physical principle, only a formal consequence of the field equations. The declaration does not resolve the cosmological constant problem.

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: