IndisputableMonolith.Relativity.GRLimit.Observables

   1import Mathlib
   2import Mathlib.Data.Real.Basic
   3import Mathlib.Topology.Basic
   4import Mathlib.Analysis.SpecialFunctions.Log.Basic
   5import Mathlib.Analysis.SpecialFunctions.Exp
   6
   7/-!
   8# Observable Limits
   9
  10Proves that basic proxy observables (w, γ, β, c_T²) reduce to GR values as parameters → 0,
  11using only continuity arguments within mathlib.
  12-/
  13
  14namespace IndisputableMonolith
  15namespace Relativity
  16namespace GRLimit
  17
  18open Filter Topology
  19
  20noncomputable section
  21
  22/-- Weight function w in a weak-field proxy model.
  23We use an exponential representation to avoid rpow domain issues. -/
  24def weight_observable (α cLag : ℝ) (Tdyn tau0 : ℝ) : ℝ :=
  25  let A : ℝ := Tdyn / tau0
  26  1 + (α * cLag) * Real.exp (α * Real.log A)
  27
  28/-- Weight approaches 1 as (α,cLag) → (0,0), for any positive Tdyn,tau0. -/
  29 theorem weight_gr_limit (Tdyn tau0 : ℝ) (_h_Tdyn : 0 < Tdyn) (_h_tau0 : 0 < tau0) :
  30  Tendsto (fun params : ℝ × ℝ => weight_observable params.1 params.2 Tdyn tau0)
  31    (nhds (0, 0)) (nhds 1) := by
  32  have h_cont_mul : Continuous fun p : ℝ × ℝ => p.1 * p.2 :=
  33    continuous_fst.mul continuous_snd
  34  have A : ℝ := Tdyn / tau0
  35  have h_cont_g : Continuous fun p : ℝ × ℝ => Real.exp (p.1 * Real.log A) := by
  36    have : Continuous fun p : ℝ × ℝ => p.1 * Real.log A :=
  37      (continuous_fst.mul continuous_const)
  38    exact Real.continuous_exp.comp this
  39  have h_cont_weight : Continuous
  40      (fun p : ℝ × ℝ => 1 + (p.1 * p.2) * Real.exp (p.1 * Real.log A)) := by
  41    refine continuous_const.add ?_
  42    exact h_cont_mul.mul h_cont_g
  43  have h_tendsto := (h_cont_weight.tendsto (0, 0))
  44  have h_eval : (fun p : ℝ × ℝ => 1 + (p.1 * p.2) * Real.exp (p.1 * Real.log A)) (0, 0) = 1 := by
  45    simp
  46  simpa [weight_observable, h_eval] using h_tendsto
  47
  48/-- PPN parameter γ proxy: γ = 1 + 0.1 · |α·cLag|. -/
  49 def gamma_observable (α cLag : ℝ) : ℝ := 1 + (0.1 : ℝ) * |α * cLag|
  50
  51 theorem gamma_gr_limit :
  52  Tendsto (fun params : ℝ × ℝ => gamma_observable params.1 params.2)
  53    (nhds (0, 0)) (nhds 1) := by
  54  have h_cont_mul : Continuous fun p : ℝ × ℝ => p.1 * p.2 :=
  55    continuous_fst.mul continuous_snd
  56  have h_cont_abs : Continuous fun p : ℝ × ℝ => |p.1 * p.2| :=
  57    continuous_abs.comp h_cont_mul
  58  have h_cont : Continuous fun p : ℝ × ℝ => 1 + (0.1 : ℝ) * |p.1 * p.2| := by
  59    refine continuous_const.add ?_
  60    exact continuous_const.mul h_cont_abs
  61  have h := h_cont.tendsto (0, 0)
  62  have : (fun p : ℝ × ℝ => 1 + (0.1 : ℝ) * |p.1 * p.2|) (0, 0) = 1 := by simp
  63  simpa [gamma_observable, this]
  64
  65/-- PPN parameter β proxy: β = 1 + 0.05 · |α·cLag|. -/
  66 def beta_observable (α cLag : ℝ) : ℝ := 1 + (0.05 : ℝ) * |α * cLag|
  67
  68 theorem beta_gr_limit :
  69  Tendsto (fun params : ℝ × ℝ => beta_observable params.1 params.2)
  70    (nhds (0, 0)) (nhds 1) := by
  71  have h_cont_mul : Continuous fun p : ℝ × ℝ => p.1 * p.2 :=
  72    continuous_fst.mul continuous_snd
  73  have h_cont_abs : Continuous fun p : ℝ × ℝ => |p.1 * p.2| :=
  74    continuous_abs.comp h_cont_mul
  75  have h_cont : Continuous fun p : ℝ × ℝ => 1 + (0.05 : ℝ) * |p.1 * p.2| := by
  76    refine continuous_const.add ?_
  77    exact continuous_const.mul h_cont_abs
  78  have h := h_cont.tendsto (0, 0)
  79  have : (fun p : ℝ × ℝ => 1 + (0.05 : ℝ) * |p.1 * p.2|) (0, 0) = 1 := by simp
  80  simpa [beta_observable, this]
  81
  82/-- GW tensor speed proxy: c_T² = 1 + 0.01 · |α·cLag|. -/
  83 def c_T_squared_observable (α cLag : ℝ) : ℝ := 1 + (0.01 : ℝ) * |α * cLag|
  84
  85 theorem c_T_squared_gr_limit :
  86  Tendsto (fun params : ℝ × ℝ => c_T_squared_observable params.1 params.2)
  87    (nhds (0, 0)) (nhds 1) := by
  88  have h_cont_mul : Continuous fun p : ℝ × ℝ => p.1 * p.2 :=
  89    continuous_fst.mul continuous_snd
  90  have h_cont_abs : Continuous fun p : ℝ × ℝ => |p.1 * p.2| :=
  91    continuous_abs.comp h_cont_mul
  92  have h_cont : Continuous fun p : ℝ × ℝ => 1 + (0.01 : ℝ) * |p.1 * p.2| := by
  93    refine continuous_const.add ?_
  94    exact continuous_const.mul h_cont_abs
  95  have h := h_cont.tendsto (0, 0)
  96  have : (fun p : ℝ × ℝ => 1 + (0.01 : ℝ) * |p.1 * p.2|) (0, 0) = 1 := by simp
  97  simpa [c_T_squared_observable, this]
  98
  99/-- All four proxies approach GR values simultaneously. -/
 100 theorem observables_bundle_gr_limit (Tdyn tau0 : ℝ) (hT : 0 < Tdyn) (hτ : 0 < tau0) :
 101  Tendsto
 102    (fun params : ℝ × ℝ =>
 103      ( weight_observable params.1 params.2 Tdyn tau0
 104      , gamma_observable params.1 params.2
 105      , beta_observable params.1 params.2
 106      , c_T_squared_observable params.1 params.2 ))
 107    (nhds (0, 0)) (nhds (1, 1, 1, 1)) := by
 108  have h_w_cont : Continuous fun p : ℝ × ℝ => weight_observable p.1 p.2 Tdyn tau0 := by
 109    have A : ℝ := Tdyn / tau0
 110    have h_cont_mul : Continuous fun p : ℝ × ℝ => p.1 * p.2 :=
 111      continuous_fst.mul continuous_snd
 112    have h_cont_g : Continuous fun p : ℝ × ℝ => Real.exp (p.1 * Real.log A) := by
 113      have : Continuous fun p : ℝ × ℝ => p.1 * Real.log A :=
 114        (continuous_fst.mul continuous_const)
 115      exact Real.continuous_exp.comp this
 116    refine continuous_const.add ?_
 117    exact h_cont_mul.mul h_cont_g
 118  have h_g_cont : Continuous fun p : ℝ × ℝ => gamma_observable p.1 p.2 := by
 119    have h_cont_mul : Continuous fun p : ℝ × ℝ => p.1 * p.2 :=
 120      continuous_fst.mul continuous_snd
 121    have h_cont_abs : Continuous fun p : ℝ × ℝ => |p.1 * p.2| :=
 122      continuous_abs.comp h_cont_mul
 123    refine continuous_const.add ?_
 124    exact continuous_const.mul h_cont_abs
 125  have h_b_cont : Continuous fun p : ℝ × ℝ => beta_observable p.1 p.2 := by
 126    have h_cont_mul : Continuous fun p : ℝ × ℝ => p.1 * p.2 :=
 127      continuous_fst.mul continuous_snd
 128    have h_cont_abs : Continuous fun p : ℝ × ℝ => |p.1 * p.2| :=
 129      continuous_abs.comp h_cont_mul
 130    refine continuous_const.add ?_
 131    exact continuous_const.mul h_cont_abs
 132  have h_c_cont : Continuous fun p : ℝ × ℝ => c_T_squared_observable p.1 p.2 := by
 133    have h_cont_mul : Continuous fun p : ℝ × ℝ => p.1 * p.2 :=
 134      continuous_fst.mul continuous_snd
 135    have h_cont_abs : Continuous fun p : ℝ × ℝ => |p.1 * p.2| :=
 136      continuous_abs.comp h_cont_mul
 137    refine continuous_const.add ?_
 138    exact continuous_const.mul h_cont_abs
 139  have h_tuple_cont : Continuous
 140      (fun p : ℝ × ℝ =>
 141        ( weight_observable p.1 p.2 Tdyn tau0
 142        , gamma_observable p.1 p.2
 143        , beta_observable p.1 p.2
 144        , c_T_squared_observable p.1 p.2 )) := by
 145    simpa using
 146      (((h_w_cont.prod_mk h_g_cont).prod_mk h_b_cont).prod_mk h_c_cont)
 147  have h := h_tuple_cont.tendsto (0, 0)
 148  have :
 149      (fun p : ℝ × ℝ =>
 150        ( weight_observable p.1 p.2 Tdyn tau0
 151        , gamma_observable p.1 p.2
 152        , beta_observable p.1 p.2
 153        , c_T_squared_observable p.1 p.2 )) (0, 0) = (1, 1, 1, 1) := by
 154    simp [weight_observable]
 155  simpa [this] using h
 156
 157end
 158
 159end GRLimit
 160end Relativity
 161end IndisputableMonolith
 162