gamma_pot

formal source

   7namespace PPN
   8
   9/-- Potential-based PPN definitions (scaffold): use Φ, Ψ from ψ and params. -/
  10noncomputable def gamma_pot (ψ : RefreshField) (p : ILGParams) : ℝ := 1
  11noncomputable def beta_pot  (ψ : RefreshField) (p : ILGParams) : ℝ := 1
  12
  13/-- Minimal PPN scaffold: define γ, β to be 1 at leading order (GR limit). -/
  14noncomputable def gamma (_C_lag _α : ℝ) : ℝ := 1
  15noncomputable def beta  (_C_lag _α : ℝ) : ℝ := 1
  16
  17/-- PPN γ definition (for paper reference). -/
  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 * α)