single_source_ratio_unity

formal source

  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
  92
  93/-- The RS equivalence ratio is 1 for all bodies with nonzero mass. -/
  94theorem rs_equivalence_ratio (x : ℝ) (hx : 0 < x)
  95    (hne : Jcost_mass_theory.gravitational_mass x ≠ 0) :
  96    Jcost_mass_theory.inertial_mass x / Jcost_mass_theory.gravitational_mass x = 1 :=
  97  single_source_ratio_unity Jcost_mass_theory x hx hne
  98