ratio_one_when_equal

formal source

 104  ∀ (m_inertial m_grav : ℝ), m_grav ≠ 0 →
 105    m_inertial = m_grav → m_inertial / m_grav = 1
 106
 107theorem ratio_one_when_equal (m_i m_g : ℝ) (heq : m_i = m_g) (hg : m_g ≠ 0) :
 108    m_i / m_g = 1 := by
 109  rw [heq, div_self hg]
 110
 111theorem equivalence_trivial_when_same :
 112    ∀ m : ℝ, m ≠ 0 → m / m = 1 := fun _ hm => div_self hm
 113
 114theorem equivalence_ratio_unity_structural : equivalence_ratio_unity := by
 115  intro m_i m_g hg heq
 116  exact ratio_one_when_equal m_i m_g heq hg
 117
 118theorem equivalence_implies_ratio_one (h : equivalence_ratio_unity)
 119    (m_i m_g : ℝ) (hg : m_g ≠ 0) (heq : m_i = m_g) : m_i / m_g = 1 :=
 120  h m_i m_g hg heq
 121
 122/-! ## Q18: Does EP Hold Exactly or Only in the Weak-Field Limit?
 123
 124The RS equivalence principle derives from J-cost uniqueness: both
 125inertial and gravitational mass are functionals of the SAME J.
 126
 127In the weak-field (small-deviation) limit: J(1+ε) ≈ ε²/2 (quadratic).
 128The quadratic approximation gives the Hamiltonian, and EP holds exactly
 129because the quadratic coefficient J''(1) = 1 is universal.
 130
 131BUT the full J-cost is NOT quadratic: J(1+ε) = ε²/(2(1+ε)).
 132The O(ε⁴) corrections are:
 133  J(1+ε) = ε²/2 - ε³/2 + 3ε⁴/8 - ...
 134
 135**Q: Do these corrections violate EP?**
 136
 137**A: No.** The EP in RS is EXACT, not approximate. Both inertial and