Gravity Stress Energy Tensor Vacuum Is Special Case

The vacuum as a special case

In general relativity, the stress-energy tensor (the mathematical object that encodes the density of energy, momentum, and stress in a region of spacetime) is the source of gravity. The Einstein field equations relate this tensor, written T, to the curvature of spacetime. The vacuum, meaning empty space with no matter or radiation, is not a special substance: it is the case where T is exactly zero. The field equations then lose their source term and become the vacuum field equations, which describe how spacetime curves in the absence of anything to curve it.

The machine-checked library of formal theorems in Recognition Science contains a declaration, vacuum_is_special_case, that proves this reduction. It shows that if the sourced field equations hold with the stress-energy tensor set to zero, then the vacuum field equations follow directly. The proof is a simple substitution: the zero tensor makes the right-hand side of the equation vanish, leaving only the geometric terms. This is a theorem, not a definition: the library proves that the vacuum case is a logical consequence of the general equations, not a separate postulate.

The same file also proves a conservation law. The contracted Bianchi identity, a purely geometric fact about the curvature tensor, together with the field equations, implies that the divergence of the stress-energy tensor is zero: ∇^μT_μν = 0. This is the formal statement that energy and momentum are locally conserved. The proof relies on the coupling constant κ being nonzero. For the framework's specific value, κ = 8φ⁵, the library proves this nonzero condition holds.

What the declaration does not claim is just as important. It does not say that the vacuum is physically empty in any absolute sense; quantum field theory suggests otherwise. It does not assert that the vacuum field equations have any particular solutions, such as the Schwarzschild metric. It does not claim that the stress-energy tensor is conserved in all circumstances; the proof requires the field equations and the Bianchi identity to hold. And it does not derive the Einstein field equations themselves from first principles; it takes them as given and proves a consequence.

In Recognition Science, this theorem is part of a larger effort to show that the framework's axioms are consistent with standard general relativity. The practical consequence is that the framework inherits the standard vacuum solutions, such as black holes and gravitational waves, without needing to add them as separate assumptions. The vacuum is not a separate chapter of physics; it is the zero case of a general equation.

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

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

What this page does not claim

The vacuum is physically empty in an absolute sense, as quantum field theory suggests otherwise. The vacuum field equations have any particular solutions, such as the Schwarzschild metric. The Einstein field equations are derived from first principles; they are taken as given.

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: