beta_def

formal source

  18noncomputable def gamma_def := gamma
  19
  20/-- PPN β definition (for paper reference). -/
  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]