`beta_extraction_formula`

definition

show as: view math explainer →

module: IndisputableMonolith.Relativity.ILG.PPNDerive
domain: Relativity
line: 18 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Relativity.ILG.PPNDerive on GitHub at line 18.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.