IndisputableMonolith.ILG.ISWSign

   1import Mathlib
   2import IndisputableMonolith.ILG.Kernel
   3import IndisputableMonolith.ILG.GrowthODE
   4
   5namespace IndisputableMonolith
   6namespace ILG
   7
   8open Real
   9
  10/-!
  11# ISW Sign Proof
  12
  13This module formalizes the sign logic for the Integrated Sachs-Wolfe (ISW) driver
  14B(a,k). A positive driver B combined with a negative gravitational potential Phi
  15predicts a negative CMB-LSS cross-correlation at low multipoles.
  16
  17## References
  18- `Papers-tex/Gravity Set/Dark-Energy.tex`: "Because f > 1 and ∂lnw > 0 at late time,
  19  the bracket is positive while Phi < 0, yielding a negative CMB–galaxy correlation."
  20-/
  21
  22/-- The ISW driver B(a,k) = -1 + f + dlnw/dlna. -/
  23noncomputable def isw_driver (P : KernelParams) (k a : ℝ) : ℝ :=
  24  let f := f_growth_eds_ilg P k a
  25  let Xinv := a / (k * P.tau0)
  26  let dlnw := (P.alpha * P.C * Xinv ^ P.alpha) / (1 + P.C * Xinv ^ P.alpha)
  27  -1 + f + dlnw
  28
  29/-- Lemma: In ILG baseline, the growth rate f is greater than 1. -/
  30theorem f_growth_gt_one (P : KernelParams) (k a : ℝ) (ha : 0 < a) (hk : 0 < k)
  31    (halpha : 0 < P.alpha) (hC : 0 < P.C) :
  32    1 < f_growth_eds_ilg P k a := by
  33  set Xinv := a / (k * P.tau0)
  34  set B := growth_prefactor P.alpha P.C
  35  have hB : 0 < B := by
  36    unfold growth_prefactor
  37    apply div_pos
  38    · linarith
  39    · nlinarith
  40  have hXinv : 0 < Xinv := div_pos ha (mul_pos hk P.tau0_pos)
  41  have hXinv_pow : 0 < Xinv ^ P.alpha := rpow_pos_of_pos hXinv _
  42  unfold f_growth_eds_ilg
  43  -- f = (1 + B(1+alpha)X^alpha) / (1 + BX^alpha)
  44  -- 1 < (1 + BX^alpha + B*alpha*X^alpha) / (1 + BX^alpha)
  45  -- 1 < 1 + (B*alpha*X^alpha) / (1 + BX^alpha)
  46  field_simp
  47  apply lt_add_of_pos_right
  48  apply div_pos
  49  · repeat apply mul_pos <;> assumption
  50  · apply add_pos_of_pos_of_nonneg
  51    · exact one_pos
  52    · repeat apply mul_nonneg <;> (try exact le_of_lt hB) <;> (try exact le_of_lt hXinv_pow)
  53
  54/-- Lemma: In ILG baseline, the kernel log-derivative dlnw/dlna is positive. -/
  55theorem dlnw_pos (P : KernelParams) (k a : ℝ) (ha : 0 < a) (hk : 0 < k)
  56    (halpha : 0 < P.alpha) (hC : 0 < P.C) :
  57    0 < (P.alpha * P.C * (a / (k * P.tau0)) ^ P.alpha) / (1 + P.C * (a / (k * P.tau0)) ^ P.alpha) := by
  58  set Xinv := a / (k * P.tau0)
  59  have hXinv : 0 < Xinv := div_pos ha (mul_pos hk P.tau0_pos)
  60  have hXinv_pow : 0 < Xinv ^ P.alpha := rpow_pos_of_pos hXinv _
  61  apply div_pos
  62  · repeat apply mul_pos <;> assumption
  63  · apply add_pos_of_pos_of_nonneg
  64    · exact one_pos
  65    · repeat apply mul_nonneg <;> (try exact le_of_lt hC) <;> (try exact le_of_lt hXinv_pow)
  66
  67/-- Main Theorem (Target E): The ISW driver B(a,k) is strictly positive in ILG baseline. -/
  68theorem isw_driver_positive (P : KernelParams) (k a : ℝ) (ha : 0 < a) (hk : 0 < k)
  69    (halpha : 0 < P.alpha) (hC : 0 < P.C) :
  70    0 < isw_driver P k a := by
  71  unfold isw_driver
  72  have hf := f_growth_gt_one P k a ha hk halpha hC
  73  have hd := dlnw_pos P k a ha hk halpha hC
  74  linarith
  75
  76end ILG
  77end IndisputableMonolith
  78