single_source_equivalence

formal source

  58/-- In a single-source mass theory, inertial and gravitational mass are
  59    identical for all positive-ratio states. This is the equivalence
  60    principle derived from cost uniqueness. -/
  61theorem single_source_equivalence (T : SingleSourceMassTheory)
  62    (x : ℝ) (hx : 0 < x) :
  63    T.inertial_mass x = T.gravitational_mass x := by
  64  rw [T.inertial_from_cost x hx, T.gravitational_from_cost x hx]
  65
  66/-- The ratio of inertial to gravitational mass is exactly 1 in any
  67    single-source theory, for any body with nonzero mass. -/
  68theorem single_source_ratio_unity (T : SingleSourceMassTheory)
  69    (x : ℝ) (hx : 0 < x) (hne : T.gravitational_mass x ≠ 0) :
  70    T.inertial_mass x / T.gravitational_mass x = 1 := by
  71  rw [single_source_equivalence T x hx, div_self hne]
  72
  73/-! ## J-Cost Is a Single-Source Theory -/
  74
  75noncomputable section
  76
  77/-- J-cost defines a canonical single-source mass theory. Both inertial
  78    response and gravitational coupling derive from J(x) = ½(x + x⁻¹) − 1. -/
  79def Jcost_mass_theory : SingleSourceMassTheory where
  80  cost x := (x + x⁻¹) / 2 - 1
  81  inertial_mass x := (x + x⁻¹) / 2 - 1
  82  gravitational_mass x := (x + x⁻¹) / 2 - 1
  83  inertial_from_cost := fun _ _ => rfl
  84  gravitational_from_cost := fun _ _ => rfl
  85
  86/-- The RS equivalence principle: for J-cost, inertial = gravitational mass.
  87    This follows from T5 (J uniqueness): there is only one cost function,
  88    so there is only one notion of mass. -/
  89theorem rs_equivalence_principle (x : ℝ) (hx : 0 < x) :
  90    Jcost_mass_theory.inertial_mass x = Jcost_mass_theory.gravitational_mass x :=
  91  single_source_equivalence Jcost_mass_theory x hx