localBackreaction

formal source

  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