Upsilon

formal source

  23
  24/-- The optical rescaling factor Upsilon(a).
  25    It gains an ILG enhancement at late times, modifying Ricci focusing. -/
  26noncomputable def Upsilon (P : ILG.KernelParams) (a : ℝ) : ℝ :=
  27  if a ≤ 0 then 1 else 1 + P.C * a ^ P.alpha
  28
  29/-- The modified Sachs focusing equation (Target G).
  30    For angular diameter distance D_A along an affine parameter λ:
  31    d²D_A/dλ² + (1/2) * Upsilon(a) * R_μν k^μ k^ν * D_A = 0
  32    where Ricci focusing is rescaled by Upsilon. -/
  33def SachsEquation_Extended (P : ILG.KernelParams) (z : ℝ) (DA_func : ℝ → ℝ) (ricci_focusing : ℝ) : Prop :=
  34  let a := 1 / (1 + z)
  35  -- Simplified ODE form in terms of z or λ
  36  ∀ z', deriv (deriv DA_func) z' + (Upsilon P a) * ricci_focusing * DA_func z' = 0
  37
  38/-- Angular diameter distance D_A under optical rescaling.
  39    Modeled as the background distance rescaled by the Upsilon factor. -/
  40noncomputable def DA_rescaled (z : ℝ) (bg_DA : ℝ) (P : ILG.KernelParams) : ℝ :=
  41  -- Scale factor a = 1 / (1 + z)
  42  bg_DA * (1 / sqrt (Upsilon P (1 / (1 + z))))
  43
  44/-- Luminosity distance D_L under optical rescaling.
  45    To preserve Etherington duality, it must scale identically to D_A. -/
  46noncomputable def DL_rescaled (z : ℝ) (bg_DL : ℝ) (P : ILG.KernelParams) : ℝ :=
  47  -- Etherington duality: D_L = (1 + z)^2 * D_A
  48  DA_rescaled z (bg_DL / (1 + z)^2) P * (1 + z)^2
  49
  50/-- Main Theorem (Target G): Etherington duality is preserved under optical rescaling.
  51    Regardless of the Upsilon rescaling, D_L = (1 + z)^2 * D_A remains satisfied. -/
  52theorem etherington_duality_preserved (z : ℝ) (bg_DA bg_DL : ℝ) (P : ILG.KernelParams)
  53    (h_bg_dual : bg_DL = (1 + z)^2 * bg_DA) :
  54    DL_rescaled z bg_DL P = (1 + z)^2 * DA_rescaled z bg_DA P := by
  55  unfold DL_rescaled
  56  rw [h_bg_dual]