IndisputableMonolith.Relativity.Cosmology.Buchert

   1import Mathlib
   2import IndisputableMonolith.Relativity.Cosmology.FRWMetric
   3
   4namespace IndisputableMonolith
   5namespace Relativity
   6namespace Cosmology
   7
   8/-!
   9# Buchert Backreaction Cancellation
  10
  11This module formalizes the algebraic cancellation of the Buchert kinematical
  12backreaction term Q_D for irrotational potential flow.
  13
  14## References
  15- `Papers-tex/Gravity Set/Dark-Energy.tex`: "The Buchert kinematical backreaction Q_D
  16  cancels mode–by–mode for potential flow even when f depends on k; thus ILG does
  17  not alter H(a) by averaging."
  18-/
  19
  20/-- Buchert's kinematical backreaction term Q_D (local/mode-by-mode version).
  21    Q_D = (2/3) * theta^2 - 2 * sigma^2.
  22    Note: The ⟨θ²⟩ - ⟨θ⟩² term reduces to theta^2 in the irrotational potential flow
  23    limit described in the paper. -/
  24def localBackreaction (θ σ2 : ℝ) : ℝ :=
  25  (2/3 : ℝ) * θ^2 - 2 * σ2
  26
  27/-- Theorem: For irrotational potential flow, the local backreaction vanishes.
  28    From the manuscript:
  29    - θ_pec = -H * f * δ
  30    - σ^2 = (1/3) * H^2 * f^2 * δ^2
  31-/
  32theorem buchert_cancellation (H f δ : ℝ) :
  33    let θ := -H * f * δ
  34    let σ2 := (1/3 : ℝ) * (H * f * δ)^2
  35    localBackreaction θ σ2 = 0 := by
  36  dsimp
  37  unfold localBackreaction
  38  field_simp
  39  ring
  40
  41/-- The "No Background Modification" result: because Q_D = 0, the background
  42    expansion (H) remains that of the chosen matter content. -/
  43def no_background_modification (H f δ : ℝ) : Prop :=
  44  localBackreaction (-H * f * δ) ((1/3 : ℝ) * (H * f * δ)^2) = 0
  45
  46theorem background_is_stable (H f δ : ℝ) : no_background_modification H f δ :=
  47  buchert_cancellation H f δ
  48
  49end Cosmology
  50end Relativity
  51end IndisputableMonolith
  52