SingleSourceMassTheory

formal source

  48/-- A mass theory that derives both inertial and gravitational mass from
  49    a single cost function. The RS claim is that any physical mass theory
  50    must have this form (because J is the unique cost function). -/
  51structure SingleSourceMassTheory where
  52  cost : ℝ → ℝ
  53  inertial_mass : ℝ → ℝ
  54  gravitational_mass : ℝ → ℝ
  55  inertial_from_cost : ∀ x, 0 < x → inertial_mass x = cost x
  56  gravitational_from_cost : ∀ x, 0 < x → gravitational_mass x = cost x
  57
  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