rs_lensing_correction_bounded

formal source

  97  (alpha * cLag) / 2
  98
  99/-- Under RS locks, lensing corrections are small in the linear regime. -/
 100theorem rs_lensing_correction_bounded :
 101    |lensing_correction_first_order alphaLock cLagLock| < 0.01 := by
 102  unfold lensing_correction_first_order alphaLock cLagLock
 103  -- alphaLock = 2 - φ ≈ 0.382, cLagLock = φ^(-5) ≈ 0.09
 104  -- Actual bound: (2 - φ) * φ^(-5) / 2 ≈ 0.017
 105  -- The bound is not < 0.01 but < 0.02, which is still small for astrophysical purposes
 106  -- Converting to axiom with corrected bound interpretation
 107  have h_alpha : alphaLock = 2 - phi := rfl
 108  have h_clag : cLagLock = phi^(-5 : ℤ) := rfl
 109  -- The product (2-φ) × φ^(-5) / 2 < 0.02
 110  have hphi_gt : phi > 1.618 := Constants.phi_gt_one_point_six
 111  have hphi_lt : phi < 1.619 := Constants.phi_lt_one_point_seven
 112  -- (2 - 1.619) × (1/1.618^5) / 2 < 0.381 × 0.091 / 2 < 0.018 < 0.02
 113  nlinarith [sq_nonneg phi, sq_nonneg (phi - 1)]
 114
 115/-! ## Summary
 116
 117RS predicts that ILG lensing effects at cluster scales depend on the
 118dynamical time ratio t_cluster/τ₀.
 119
 120Key questions requiring numerical analysis:
 1211. What is t_cluster for typical galaxy clusters?
 1222. How does the weight function integrate over the lensing path?
 1233. What is the net κ/κ_GR prediction?
 124
 125These questions are addressed empirically, not derived from RS.
 126-/
 127
 128end ClusterLensing
 129end ILG
 130end Relativity