IndisputableMonolith.Relativity.ILG.PPNDerive

   1import Mathlib
   2import IndisputableMonolith.Relativity.ILG.PPN
   3
   4namespace IndisputableMonolith
   5namespace Relativity
   6namespace ILG
   7
   8/-- Toy “extraction formulas” for PPN parameters.
   9
  10We intentionally keep these *local* to the ILG layer (rather than importing the full
  11PostNewtonian stack) to avoid creating heavy dependency edges from `Relativity.lean`.
  12The point of this file is to eliminate the previous `Prop := True` stub
  13with a small, honest certificate.
  14-/
  15noncomputable def gamma_extraction_formula (α C_lag : ℝ) : ℝ :=
  16  1 + (1/10 : ℝ) * (α * C_lag)
  17
  18noncomputable def beta_extraction_formula (α C_lag : ℝ) : ℝ :=
  19  1 + (1/20 : ℝ) * (α * C_lag)
  20
  21/-- Model-level “certificate”: the ILG linearised PPN functions match the toy extraction
  22formulas after identifying parameter order. -/
  23def PPNDerivationHolds : Prop :=
  24  ∀ α C_lag : ℝ,
  25    (gamma_extraction_formula α C_lag = PPN.gamma_lin C_lag α) ∧
  26    (beta_extraction_formula α C_lag = PPN.beta_lin C_lag α)
  27
  28theorem ppn_derivation_holds : PPNDerivationHolds := by
  29  intro α C_lag
  30  constructor
  31  · -- γ: coefficients match and multiplication commutes
  32    simp [gamma_extraction_formula, PPN.gamma_lin, mul_comm, mul_left_comm, mul_assoc]
  33  · -- β: coefficients match and multiplication commutes
  34    simp [beta_extraction_formula, PPN.beta_lin, mul_comm, mul_left_comm, mul_assoc]
  35
  36end ILG
  37end Relativity
  38end IndisputableMonolith
  39