gamma_bound

formal source

  21noncomputable def beta_def := beta
  22
  23/-- Solar‑System style bound (illustrative): |γ−1| ≤ 1/100000. -/
  24theorem gamma_bound (C_lag α : ℝ) :
  25  |gamma C_lag α - 1| ≤ (1/100000 : ℝ) := by
  26  -- LHS simplifies to 0; RHS is positive
  27  simpa [gamma] using (by norm_num : (0 : ℝ) ≤ (1/100000 : ℝ))
  28
  29/-- Solar‑System style bound (illustrative): |β−1| ≤ 1/100000. -/
  30theorem beta_bound (C_lag α : ℝ) :
  31  |beta C_lag α - 1| ≤ (1/100000 : ℝ) := by
  32  simpa [beta] using (by norm_num : (0 : ℝ) ≤ (1/100000 : ℝ))
  33
  34/-!
  35Linearised small-coupling PPN model (illustrative).
  36These definitions produce explicit bounds scaling with |C_lag·α|.
  37-/
  38
  39/-- Linearised γ with small scalar coupling. -/
  40noncomputable def gamma_lin (C_lag α : ℝ) : ℝ := 1 + (1/10 : ℝ) * (C_lag * α)
  41
  42/-- Linearised β with small scalar coupling. -/
  43noncomputable def beta_lin  (C_lag α : ℝ) : ℝ := 1 + (1/20 : ℝ) * (C_lag * α)
  44
  45/-- Bound: if |C_lag·α| ≤ κ then |γ−1| ≤ (1/10) κ. -/
  46theorem gamma_bound_small (C_lag α κ : ℝ)
  47  (h : |C_lag * α| ≤ κ) :
  48  |gamma_lin C_lag α - 1| ≤ (1/10 : ℝ) * κ := by
  49  unfold gamma_lin
  50  simp only [add_sub_cancel_left]
  51  rw [abs_mul]
  52  calc |1/10| * |C_lag * α| = (1/10) * |C_lag * α| := by norm_num
  53    _ ≤ (1/10) * κ := by exact mul_le_mul_of_nonneg_left h (by norm_num)
  54