IndisputableMonolith.Gravity.ILG

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4namespace Gravity
   5namespace ILG
   6
   7noncomputable section
   8open Real
   9
  10/-! Minimal extracted time-kernel basics with parametric interfaces. -/
  11
  12structure BridgeData where
  13  tau0 : ℝ
  14
  15structure BaryonCurves where
  16  vgas  : ℝ → ℝ
  17  vdisk : ℝ → ℝ
  18  vbul  : ℝ → ℝ
  19
  20/-! Configurable numeric regularization parameters. -/
  21structure Config where
  22  upsilonStar : ℝ
  23  eps_r : ℝ
  24  eps_v : ℝ
  25  eps_t : ℝ
  26  eps_a : ℝ
  27
  28@[simp] def defaultConfig : Config :=
  29  { upsilonStar := 1.0
  30  , eps_r := 1e-12
  31  , eps_v := 1e-12
  32  , eps_t := 0.01
  33  , eps_a := 1e-12 }
  34
  35structure ConfigProps (cfg : Config) : Prop where
  36  eps_t_nonneg : 0 ≤ cfg.eps_t
  37  eps_t_le_one : cfg.eps_t ≤ 1
  38
  39@[simp] lemma defaultConfig_props : ConfigProps defaultConfig := by
  40  refine ⟨?h0, ?h1⟩ <;> norm_num
  41
  42def vbarSq_with (cfg : Config) (C : BaryonCurves) (r : ℝ) : ℝ :=
  43  max 0 ((C.vgas r) ^ 2 + ((Real.sqrt cfg.upsilonStar) * (C.vdisk r)) ^ 2 + (C.vbul r) ^ 2)
  44
  45def vbar_with (cfg : Config) (C : BaryonCurves) (r : ℝ) : ℝ :=
  46  Real.sqrt (max cfg.eps_v (vbarSq_with cfg C r))
  47
  48def gbar_with (cfg : Config) (C : BaryonCurves) (r : ℝ) : ℝ :=
  49  (vbar_with cfg C r) ^ 2 / max cfg.eps_r r
  50
  51structure Params where
  52  alpha      : ℝ
  53  Clag       : ℝ
  54  A          : ℝ
  55  r0         : ℝ
  56  p          : ℝ
  57  hz_over_Rd : ℝ
  58
  59structure ParamProps (P : Params) : Prop where
  60  alpha_nonneg : 0 ≤ P.alpha
  61  Clag_nonneg  : 0 ≤ P.Clag
  62  Clag_le_one  : P.Clag ≤ 1
  63  A_nonneg     : 0 ≤ P.A
  64  r0_pos       : 0 < P.r0
  65  p_pos        : 0 < P.p
  66
  67def w_t_with (cfg : Config) (P : Params) (Tdyn τ0 : ℝ) : ℝ :=
  68  let t := max cfg.eps_t (Tdyn / τ0)
  69  1 + P.Clag * (Real.rpow t P.alpha - 1)
  70
  71@[simp] def w_t (P : Params) (Tdyn τ0 : ℝ) : ℝ := w_t_with defaultConfig P Tdyn τ0
  72
  73@[simp] def w_t_display (P : Params) (B : BridgeData) (Tdyn : ℝ) : ℝ :=
  74  w_t_with defaultConfig P Tdyn B.tau0
  75
  76lemma eps_t_le_one_default : defaultConfig.eps_t ≤ (1 : ℝ) := by
  77  norm_num
  78
  79/-- Reference identity under nonzero tick: w_t(τ0, τ0) = 1. -/
  80lemma w_t_ref_with (cfg : Config) (hcfg : ConfigProps cfg)
  81  (P : Params) (τ0 : ℝ) (hτ : τ0 ≠ 0) : w_t_with cfg P τ0 τ0 = 1 := by
  82  dsimp [w_t_with]
  83  have hdiv : τ0 / τ0 = (1 : ℝ) := by
  84    field_simp [hτ]
  85  have hmax : max cfg.eps_t (τ0 / τ0) = (1 : ℝ) := by
  86    simpa [hdiv, max_eq_right hcfg.eps_t_le_one]
  87  simp [hmax]
  88
  89lemma w_t_ref (P : Params) (τ0 : ℝ) (hτ : τ0 ≠ 0) : w_t P τ0 τ0 = 1 :=
  90  w_t_ref_with defaultConfig defaultConfig_props P τ0 hτ
  91
  92lemma w_t_rescale_with (cfg : Config) (P : Params) (c Tdyn τ0 : ℝ) (hc : 0 < c) :
  93  w_t_with cfg P (c * Tdyn) (c * τ0) = w_t_with cfg P Tdyn τ0 := by
  94  dsimp [w_t_with]
  95  have hc0 : (c : ℝ) ≠ 0 := ne_of_gt hc
  96  have : (c * Tdyn) / (c * τ0) = Tdyn / τ0 := by field_simp [hc0]
  97  simp [this]
  98
  99lemma w_t_rescale (P : Params) (c Tdyn τ0 : ℝ) (hc : 0 < c) :
 100  w_t P (c * Tdyn) (c * τ0) = w_t P Tdyn τ0 :=
 101  w_t_rescale_with defaultConfig P c Tdyn τ0 hc
 102
 103/-- Nonnegativity of time-kernel under ParamProps. -/
 104lemma w_t_nonneg_with (cfg : Config) (hcfg : ConfigProps cfg)
 105  (P : Params) (H : ParamProps P) (Tdyn τ0 : ℝ) :
 106  0 ≤ w_t_with cfg P Tdyn τ0 := by
 107  dsimp [w_t_with]
 108  set t := max cfg.eps_t (Tdyn / τ0) with ht
 109  have ht_nonneg : 0 ≤ t := by
 110    have hle : cfg.eps_t ≤ t := by
 111      simpa [ht] using le_max_left cfg.eps_t (Tdyn / τ0)
 112    exact le_trans hcfg.eps_t_nonneg hle
 113  have hrpow_nonneg : 0 ≤ Real.rpow t P.alpha := by
 114    simpa using Real.rpow_nonneg ht_nonneg P.alpha
 115  have h_rpow_minus_one : (-1 : ℝ) ≤ Real.rpow t P.alpha - 1 := by
 116    linarith
 117  have h_mul : (-P.Clag : ℝ) ≤ P.Clag * (Real.rpow t P.alpha - 1) := by
 118    have h := mul_le_mul_of_nonneg_left h_rpow_minus_one H.Clag_nonneg
 119    -- h : P.Clag * (-1) ≤ P.Clag * (Real.rpow t P.alpha - 1)
 120    simpa using h
 121  have h_base : 0 ≤ (1 : ℝ) - P.Clag := sub_nonneg.mpr H.Clag_le_one
 122  have h_lower : (1 : ℝ) - P.Clag ≤ 1 + P.Clag * (Real.rpow t P.alpha - 1) := by
 123    linarith
 124  exact le_trans h_base h_lower
 125
 126lemma w_t_nonneg (P : Params) (H : ParamProps P) (Tdyn τ0 : ℝ) :
 127    0 ≤ w_t P Tdyn τ0 := by
 128  -- For defaultConfig, eps_t = 0.01 > 0.
 129  -- Thus t = max(0.01, Tdyn/τ0) > 0.
 130  -- rpow t alpha is non-negative for t > 0.
 131  -- Result follows from Clag <= 1.
 132  unfold w_t
 133  exact w_t_nonneg_with defaultConfig defaultConfig_props P H Tdyn τ0
 134
 135/-- Time-kernel is at least 1 when alpha >= 0, Clag >= 0 and Tdyn >= tau0. -/
 136lemma w_t_ge_one (P : Params) (H : ParamProps P) (Tdyn τ0 : ℝ) (hτ : 0 < τ0) (hT : τ0 ≤ Tdyn) :
 137    1 ≤ w_t P Tdyn τ0 := by
 138  unfold w_t w_t_with
 139  let t := max defaultConfig.eps_t (Tdyn / τ0)
 140  have h_ratio : 1 ≤ Tdyn / τ0 := (one_le_div hτ).mpr hT
 141  have h_base : 1 ≤ t := le_max_of_le_right h_ratio
 142  -- Since base >= 1 and alpha >= 0, base^alpha >= 1
 143  have h_pow : 1 ≤ t ^ P.alpha := Real.one_le_rpow h_base H.alpha_nonneg
 144  have h_diff : 0 ≤ t ^ P.alpha - 1 := sub_nonneg.mpr h_pow
 145  have h_mul : 0 ≤ P.Clag * (t ^ P.alpha - 1) :=
 146    mul_nonneg H.Clag_nonneg h_diff
 147  -- Goal: 1 ≤ 1 + P.Clag * (t ^ P.alpha - 1)
 148  -- This follows from h_mul: 0 ≤ P.Clag * (t ^ P.alpha - 1)
 149  simp only [ge_iff_le, le_add_iff_nonneg_right]
 150  exact h_mul
 151
 152end
 153end ILG
 154end Gravity
 155end IndisputableMonolith
 156