IndisputableMonolith.Gravity.FullEFEWithDarkEnergy

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Gravity.FullEFE
   4import IndisputableMonolith.Gravity.Connection
   5import IndisputableMonolith.Cosmology.CosmologicalConstantDerivation
   6
   7/-!
   8# Full EFE With Dark Energy (QG integration of the forced vacuum term)
   9
  10## The blocker this module resolves
  11
  12`DarkEnergyStatus.blocker_efe_lambda_zero` records that the gravity-facing Einstein data
  13`Gravity.FullEFE.rs_efe_data` currently carries `cosmological_constant = 0`. Dark energy is
  14therefore not yet in the quantum-gravity / EFE master chain. This module puts a nonzero,
  15forced, covariantly-conserved vacuum term into that chain.
  16
  17## What is established here
  18
  191. **The vacuum term is forced positive.** `Λ_RS(H₀²) = 3 H₀² · Ω_Λ` with the RS-forced
  20   `Ω_Λ = 11/16 − α/π`. Since `Ω_Λ > 0` (proved) and `H₀² > 0`, `Λ_RS > 0`.
  212. **The Λ-extended EFE data recovers the baseline.** It keeps the derived coupling
  22   `κ = 8φ⁵` and dimension 4; only the cosmological-constant slot changes, and it collapses
  23   back to `0` in the `H₀² → 0` (equivalently zero-fraction) limit.
  243. **The vacuum equation of state is exactly `w = −1`.** Writing the vacuum term as a
  25   perfect fluid `T^vac_μν = −(Λ/κ) g_μν` gives density `ρ_vac = Λ/κ > 0` and pressure
  26   `p_vac = −ρ_vac`, i.e. `w = −1`. This is the static anchor the dynamic `δw(z)` kernel
  27   deviates from.
  284. **The vacuum term is covariantly conserved (Bianchi/U9), grounded, not assumed.** A
  29   constant times the metric has vanishing covariant derivative *because* the metric is
  30   covariantly constant (metric compatibility). We prove metric compatibility for the flat
  31   reference (`minkowski_metric_compatible`) and the linearity of the (0,2) covariant
  32   derivative (`covDeriv02_smul`), then conclude `∇(c·g) = 0` for any constant `c`, in
  33   particular `c = −Λ/κ`. This is the structural reason a cosmological constant is always
  34   consistent with `∇^μ G_μν = 0`.
  35
  36Status: THEOREM. Zero `sorry`, zero new `axiom`. The absolute scale enters only through the
  37input `H₀² > 0`; the dimensionless fraction `Ω_Λ` and every structural property are forced.
  38-/
  39
  40namespace IndisputableMonolith
  41namespace Gravity
  42namespace FullEFEWithDarkEnergy
  43
  44open Constants
  45
  46noncomputable section
  47
  48/-! ## §1. Covariant derivative of a (0,2) tensor and its linearity -/
  49
  50/-- The covariant derivative `∇_λ T_μν` of a (0,2) tensor with components `Tg`, given the
  51ordinary derivatives `dT` and the Christoffel symbols `ch`. The expression matches
  52`Connection.metric_compatibility` term-for-term, so metric compatibility is exactly the
  53statement `∀ λμν, covDeriv02 ch g dg λ μ ν = 0`. -/
  54def covDeriv02 (ch : Connection.ChristoffelData)
  55    (Tg : Connection.Idx → Connection.Idx → ℝ)
  56    (dT : Connection.Idx → Connection.Idx → Connection.Idx → ℝ)
  57    (lam mu nu : Connection.Idx) : ℝ :=
  58  dT lam mu nu
  59    - ∑ rho : Connection.Idx, (ch.gamma rho lam mu * Tg rho nu)
  60    - ∑ rho : Connection.Idx, (ch.gamma rho lam nu * Tg mu rho)
  61
  62/-- Linearity of the (0,2) covariant derivative: scaling the tensor (and its ordinary
  63derivative) by a constant `c` scales the covariant derivative by `c`. -/
  64theorem covDeriv02_smul (ch : Connection.ChristoffelData)
  65    (Tg : Connection.Idx → Connection.Idx → ℝ)
  66    (dT : Connection.Idx → Connection.Idx → Connection.Idx → ℝ)
  67    (c : ℝ) (lam mu nu : Connection.Idx) :
  68    covDeriv02 ch (fun a b => c * Tg a b) (fun a b d => c * dT a b d) lam mu nu
  69      = c * covDeriv02 ch Tg dT lam mu nu := by
  70  have hs1 : ∑ rho : Connection.Idx, (ch.gamma rho lam mu * (c * Tg rho nu))
  71           = c * ∑ rho : Connection.Idx, (ch.gamma rho lam mu * Tg rho nu) := by
  72    rw [Finset.mul_sum]; apply Finset.sum_congr rfl; intro rho _; ring
  73  have hs2 : ∑ rho : Connection.Idx, (ch.gamma rho lam nu * (c * Tg mu rho))
  74           = c * ∑ rho : Connection.Idx, (ch.gamma rho lam nu * Tg mu rho) := by
  75    rw [Finset.mul_sum]; apply Finset.sum_congr rfl; intro rho _; ring
  76  simp only [covDeriv02]
  77  rw [hs1, hs2]; ring
  78
  79/-! ## §2. Metric compatibility for the flat reference -/
  80
  81/-- The flat Minkowski metric is covariantly constant: `∇_λ g_μν = 0`. Both the ordinary
  82derivative (constant metric) and the Christoffel symbols (flat) vanish. -/
  83theorem minkowski_metric_compatible :
  84    Connection.metric_compatibility Connection.minkowski
  85      (Connection.christoffel_from_metric Connection.minkowski_inverse (fun _ _ _ => 0))
  86      (fun _ _ _ => 0) := by
  87  unfold Connection.metric_compatibility
  88  intro lam mu nu
  89  simp [Connection.flat_christoffel_vanish]
  90
  91/-! ## §3. Conservation of the static vacuum stress tensor (U9) -/
  92
  93/-- **VACUUM TERM IS COVARIANTLY CONSERVED (general).** For any metric-compatible setup,
  94the (0,2) tensor `c · g` (constant `c` times the metric) has vanishing covariant
  95derivative. With `c = −Λ/κ` this is the static vacuum stress tensor `T^vac = −(Λ/κ) g`, so
  96`∇_λ T^vac_μν = 0` for all indices, hence `∇^μ T^vac_μν = 0`. -/
  97theorem vacuum_stress_conserved (c : ℝ) (met : Connection.MetricTensor)
  98    (ch : Connection.ChristoffelData)
  99    (dg : Connection.Idx → Connection.Idx → Connection.Idx → ℝ)
 100    (hcompat : Connection.metric_compatibility met ch dg) :
 101    ∀ lam mu nu : Connection.Idx,
 102      covDeriv02 ch (fun a b => c * met.g a b) (fun a b d => c * dg a b d) lam mu nu = 0 := by
 103  intro lam mu nu
 104  rw [covDeriv02_smul]
 105  rw [show covDeriv02 ch met.g dg lam mu nu = (0 : ℝ) from hcompat lam mu nu]
 106  ring
 107
 108/-- **VACUUM TERM IS COVARIANTLY CONSERVED (flat reference, grounded).** Specialization of
 109`vacuum_stress_conserved` to the flat reference, using the proved
 110`minkowski_metric_compatible`. No metric compatibility is assumed; it is discharged. -/
 111theorem flat_vacuum_stress_conserved (c : ℝ) :
 112    ∀ lam mu nu : Connection.Idx,
 113      covDeriv02 (Connection.christoffel_from_metric Connection.minkowski_inverse (fun _ _ _ => 0))
 114        (fun a b => c * Connection.minkowski.g a b) (fun a b d => c * (fun _ _ _ => (0 : ℝ)) a b d)
 115        lam mu nu = 0 :=
 116  vacuum_stress_conserved c Connection.minkowski
 117    (Connection.christoffel_from_metric Connection.minkowski_inverse (fun _ _ _ => 0))
 118    (fun _ _ _ => 0) minkowski_metric_compatible
 119
 120/-! ## §4. The forced cosmological constant and vacuum fluid -/
 121
 122/-- The RS-forced dark-energy density fraction `Ω_Λ = 11/16 − α/π` is positive. -/
 123theorem Omega_Lambda_RS_pos :
 124    0 < Cosmology.CosmologicalConstantDerivation.Omega_Lambda_RS := by
 125  obtain ⟨hlo, _⟩ := Cosmology.CosmologicalConstantDerivation.Omega_Lambda_interval
 126  linarith
 127
 128/-- The RS cosmological constant at Hubble scale `H₀²`: `Λ_RS = 3 H₀² Ω_Λ`. -/
 129def Lambda_RS (H0sq : ℝ) : ℝ :=
 130  3 * H0sq * Cosmology.CosmologicalConstantDerivation.Omega_Lambda_RS
 131
 132/-- `Λ_RS` is positive for any positive Hubble scale (forced by `Ω_Λ > 0`). -/
 133theorem Lambda_RS_pos {H0sq : ℝ} (h : 0 < H0sq) : 0 < Lambda_RS H0sq := by
 134  unfold Lambda_RS
 135  exact mul_pos (mul_pos (by norm_num : (0 : ℝ) < 3) h) Omega_Lambda_RS_pos
 136
 137/-- `Λ_RS` collapses to `0` in the `H₀² → 0` limit (recovers the baseline `Λ = 0`). -/
 138theorem Lambda_RS_zero : Lambda_RS 0 = 0 := by unfold Lambda_RS; ring
 139
 140/-- The vacuum energy density read off from the cosmological term: `ρ_vac = Λ/κ`. -/
 141def rho_vac (lam kappa : ℝ) : ℝ := lam / kappa
 142
 143theorem rho_vac_pos {lam kappa : ℝ} (hl : 0 < lam) (hk : 0 < kappa) :
 144    0 < rho_vac lam kappa := div_pos hl hk
 145
 146/-- The vacuum pressure: `p_vac = −ρ_vac`. -/
 147def vacuum_pressure (rho : ℝ) : ℝ := -rho
 148
 149/-- **VACUUM EQUATION OF STATE IS `w = −1`.** The static vacuum fluid has `p/ρ = −1`. -/
 150theorem vacuum_eos (rho : ℝ) (h : rho ≠ 0) : vacuum_pressure rho / rho = -1 := by
 151  unfold vacuum_pressure
 152  rw [neg_div, div_self h]
 153
 154/-! ## §5. The Λ-extended EFE data -/
 155
 156/-- The full EFE data carrying the forced cosmological constant `Λ_RS(H₀²)`, with the same
 157derived coupling `κ = 8φ⁵` and dimension 4 as the baseline `rs_efe_data`. -/
 158def rs_efe_data_with_lambda (H0sq : ℝ) : FullEFE.FullEFEData where
 159  dimension := 4
 160  dim_eq := rfl
 161  kappa := FullEFE.rs_efe_data.kappa
 162  kappa_pos := FullEFE.rs_efe_data.kappa_pos
 163  cosmological_constant := Lambda_RS H0sq
 164
 165theorem lambda_efe_kappa (H0sq : ℝ) :
 166    (rs_efe_data_with_lambda H0sq).kappa = 8 * phi ^ 5 := FullEFE.rs_efe_kappa
 167
 168theorem lambda_efe_dimension (H0sq : ℝ) :
 169    (rs_efe_data_with_lambda H0sq).dimension = 4 := rfl
 170
 171theorem lambda_efe_lambda_pos {H0sq : ℝ} (h : 0 < H0sq) :
 172    0 < (rs_efe_data_with_lambda H0sq).cosmological_constant := Lambda_RS_pos h
 173
 174/-- The Λ-extended data recovers the baseline `Λ = 0` data in the limit. -/
 175theorem recovers_baseline_lambda :
 176    (rs_efe_data_with_lambda 0).cosmological_constant
 177      = FullEFE.rs_efe_data.cosmological_constant := by
 178  show Lambda_RS 0 = 0
 179  exact Lambda_RS_zero
 180
 181/-! ## §6. The master certificate -/
 182
 183/-- **DARK-ENERGY EFE CERTIFICATE.** The forced vacuum term is now in the EFE chain:
 184positive, of equation of state `w = −1`, covariantly conserved (grounded in flat metric
 185compatibility), preserving the derived `κ = 8φ⁵`, and recovering the `Λ = 0` baseline. -/
 186structure DarkEnergyEFECert where
 187  lambda_pos :
 188    ∀ {H0sq : ℝ}, 0 < H0sq → 0 < (rs_efe_data_with_lambda H0sq).cosmological_constant
 189  kappa_preserved : ∀ H0sq : ℝ, (rs_efe_data_with_lambda H0sq).kappa = 8 * phi ^ 5
 190  recovers_baseline :
 191    (rs_efe_data_with_lambda 0).cosmological_constant
 192      = FullEFE.rs_efe_data.cosmological_constant
 193  vacuum_eos_minus_one : ∀ rho : ℝ, rho ≠ 0 → vacuum_pressure rho / rho = -1
 194  vacuum_conserved :
 195    ∀ (c : ℝ) (lam mu nu : Connection.Idx),
 196      covDeriv02 (Connection.christoffel_from_metric Connection.minkowski_inverse
 197          (fun _ _ _ => 0))
 198        (fun a b => c * Connection.minkowski.g a b)
 199        (fun a b d => c * (fun _ _ _ => (0 : ℝ)) a b d) lam mu nu = 0
 200
 201/-- The dark-energy EFE certificate is inhabited: every claim is proved. -/
 202def darkEnergyEFECert : DarkEnergyEFECert where
 203  lambda_pos := fun h => lambda_efe_lambda_pos h
 204  kappa_preserved := lambda_efe_kappa
 205  recovers_baseline := recovers_baseline_lambda
 206  vacuum_eos_minus_one := vacuum_eos
 207  vacuum_conserved := flat_vacuum_stress_conserved
 208
 209end
 210
 211end FullEFEWithDarkEnergy
 212end Gravity
 213end IndisputableMonolith
 214