Gravity Full Efewith Dark Energy Flat Vacuum Stress Conserved

The conserved vacuum

In Einstein's general relativity, the stress-energy tensor describes the density and flow of energy and momentum in spacetime. The Bianchi identity, a geometric fact about the curvature of spacetime, implies that this tensor is covariantly conserved: its covariant derivative vanishes. This conservation is not an extra assumption; it is a necessary consequence of the field equations. A cosmological constant, often denoted Λ, represents a constant energy density of empty space, and it is incorporated into the field equations as an additional term proportional to the metric tensor.

The declaration flat_vacuum_stress_conserved, a theorem in the Recognition Science framework's machine-checked library, proves a specific instance of this conservation. It establishes that for a flat spacetime, the Minkowski metric, and a vacuum stress-energy tensor that is a constant multiple of that metric, the covariant derivative is identically zero. The proof relies on two key facts: the metric is covariantly constant (metric compatibility), and the covariant derivative is linear with respect to scalar multiplication. The theorem states that for any constant c, the covariant derivative of c times the metric is zero. This is the structural reason a cosmological constant is always consistent with the conservation law.

This result is part of a larger effort to integrate a dark energy term into the framework's Einstein field equations. The framework defines a specific positive cosmological constant, Λ_RS, and shows that the extended field equations recover the baseline when the Hubble parameter squared goes to zero. The vacuum equation of state is exactly w = -1, meaning the pressure is the negative of the energy density. The theorem flat_vacuum_stress_conserved provides the necessary consistency check for this term in a flat reference spacetime.

What the theorem does not claim is that the cosmological constant is conserved in a general, curved spacetime. The proof is specific to the flat Minkowski metric and a particular choice of connection. It does not establish the value of the cosmological constant, nor does it prove that dark energy exists. It only shows that a particular mathematical construction, a constant times the metric, is consistent with the conservation law in the flat case. The physical recognition-to-linking bridge that would connect this to a broader theory of quantum gravity remains an open target.

/-- **VACUUM TERM IS COVARIANTLY CONSERVED (flat reference, grounded).** Specialization of
`vacuum_stress_conserved` to the flat reference, using the proved
`minkowski_metric_compatible`. No metric compatibility is assumed; it is discharged. -/
theorem flat_vacuum_stress_conserved (c : ℝ) :
    ∀ lam mu nu : Connection.Idx,
      covDeriv02 (Connection.christoffel_from_metric Connection.minkowski_inverse (fun _ _ _ => 0))
        (fun a b => c * Connection.minkowski.g a b) (fun a b d => c * (fun _ _ _ => (0 : ℝ)) a b d)
        lam mu nu = 0 :=
  vacuum_stress_conserved c Connection.minkowski
    (Connection.christoffel_from_metric Connection.minkowski_inverse (fun _ _ _ => 0))
    (fun _ _ _ => 0) minkowski_metric_compatible

/-- The flat Minkowski metric is covariantly constant: `∇_λ g_μν = 0`. Both the ordinary
derivative (constant metric) and the Christoffel symbols (flat) vanish. -/
theorem minkowski_metric_compatible :
    Connection.metric_compatibility Connection.minkowski
      (Connection.christoffel_from_metric Connection.minkowski_inverse (fun _ _ _ => 0))
      (fun _ _ _ => 0) := by
  unfold Connection.metric_compatibility
  intro lam mu nu
  simp [Connection.flat_christoffel_vanish]

/-- Linearity of the (0,2) covariant derivative: scaling the tensor (and its ordinary
derivative) by a constant `c` scales the covariant derivative by `c`. -/
theorem covDeriv02_smul (ch : Connection.ChristoffelData)
    (Tg : Connection.Idx → Connection.Idx → ℝ)
    (dT : Connection.Idx → Connection.Idx → Connection.Idx → ℝ)
    (c : ℝ) (lam mu nu : Connection.Idx) :
    covDeriv02 ch (fun a b => c * Tg a b) (fun a b d => c * dT a b d) lam mu nu
      = c * covDeriv02 ch Tg dT lam mu nu := by
  have hs1 : ∑ rho : Connection.Idx, (ch.gamma rho lam mu * (c * Tg rho nu))
           = c * ∑ rho : Connection.Idx, (ch.gamma rho lam mu * Tg rho nu) := by
    rw [Finset.mul_sum]; apply Finset.sum_congr rfl; intro rho _; ring
  have hs2 : ∑ rho : Connection.Idx, (ch.gamma rho lam nu * (c * Tg mu rho))
           = c * ∑ rho : Connection.Idx, (ch.gamma rho lam nu * Tg mu rho) := by
    rw [Finset.mul_sum]; apply Finset.sum_congr rfl; intro rho _; ring
  simp only [covDeriv02]
  rw [hs1, hs2]; ring

/-- `Λ_RS` is positive for any positive Hubble scale (forced by `Ω_Λ > 0`). -/
theorem Lambda_RS_pos {H0sq : ℝ} (h : 0 < H0sq) : 0 < Lambda_RS H0sq := by
  unfold Lambda_RS
  exact mul_pos (mul_pos (by norm_num : (0 : ℝ) < 3) h) Omega_Lambda_RS_pos

/-- The Λ-extended data recovers the baseline `Λ = 0` data in the limit. -/
theorem recovers_baseline_lambda :
    (rs_efe_data_with_lambda 0).cosmological_constant
      = FullEFE.rs_efe_data.cosmological_constant := by
  show Lambda_RS 0 = 0
  exact Lambda_RS_zero

/-- **VACUUM EQUATION OF STATE IS `w = −1`.** The static vacuum fluid has `p/ρ = −1`. -/
theorem vacuum_eos (rho : ℝ) (h : rho ≠ 0) : vacuum_pressure rho / rho = -1 := by
  unfold vacuum_pressure
  rw [neg_div, div_self h]

What this page does not claim

The theorem does not prove conservation in a general curved spacetime. The theorem does not establish the existence or value of the cosmological constant. The theorem does not connect the flat spacetime result to a physical theory of quantum gravity.

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