Gravity Stress Energy Tensor Conservation From Efe And Bianchi

The conservation theorem

In general relativity, the stress-energy tensor T_μν describes the density and flow of energy and momentum in matter and fields. Its covariant divergence, ∇^μT_μν, measures how much energy and momentum is locally created or destroyed. The conservation law ∇^μT_μν = 0 states that, in a small region, energy and momentum are neither created nor destroyed; they only move and change form. This is a key part of the theory, and it is not an independent postulate. It is a consequence of the Einstein field equations (EFE), G_μν + Λg_μν = κT_μν, together with a purely geometric identity.

The geometric identity is the contracted Bianchi identity, ∇^μG_μν = 0. It holds for any metric, independent of any field equation, because of the symmetries of the Riemann curvature tensor. Taking the divergence of both sides of the EFE, the left side vanishes by Bianchi, and the term involving the metric tensor vanishes by metric compatibility (∇^μg_μν = 0). This leaves κ∇^μT_μν = 0. Since the coupling constant κ is nonzero, the conservation law follows. This chain of reasoning is standard textbook material.

The machine-checked library of formal theorems in the Recognition Science framework formalizes this argument. Its declaration conservation_from_efe_and_bianchi proves the implication: if the EFE hold and the contracted Bianchi identity holds, then the stress-energy tensor is conserved. The proof is a direct algebraic manipulation: it substitutes the Bianchi identity into the divergence of the EFE and cancels the nonzero κ. The library also proves that the framework's own coupling constant, κ = 8φ⁵, is nonzero, so the conservation result applies to it.

What the declaration does not do is derive the EFE itself, nor does it prove the contracted Bianchi identity. Those are taken as inputs. The theorem is conditional: it shows that conservation follows from those two premises. It also does not prove that the stress-energy tensor defined by variation of a matter action is the correct physical one; that definition is a separate modeling choice. The formal statement works with abstract divergence functions, not with an explicit coordinate formula for the covariant derivative.

The value of this formalization is precision. It pins down exactly which premises are needed for a central result in general relativity, and it verifies that the logical chain has no hidden gaps. For the framework, it proves what it calls Axiom 3, the matter coupling axiom, in the sense that the conservation law is a consequence of the geometric and field equations. The reader can now see that the conservation of energy and momentum in general relativity rests on two clearly stated assumptions, and nothing more.

/-- **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 declaration does not prove the Einstein field equations or the contracted Bianchi identity; it takes them as premises. The declaration does not establish that the stress-energy tensor defined by variation of a matter action is the correct physical one. The declaration does not provide an explicit coordinate formula for the covariant divergence used in the proof.

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: