equivalence_ratio_unity
plain-language theorem explainer
The definition encodes that inertial and gravitational masses stand in ratio one whenever the masses coincide and gravitational mass is nonzero. Researchers deriving the equivalence principle from a single cost function cite this interface proposition. Its body directly states the universal ratio condition over the reals with no further reduction steps.
Claim. For all real numbers $m_i$ and $m_g$, if $m_g ≠ 0$ and $m_i = m_g$ then $m_i / m_g = 1$.
background
The module formalizes G-003 by showing both inertial and gravitational mass derive from the same J-cost function. Inertial mass is the quadratic response coefficient J''(1) near balance; gravitational mass is the integrated J-cost defect that sources curvature. The referenced Jcost_mass_theory sets both equal to (x + x^{-1})/2 - 1, so equality follows by construction once J is unique.
proof idea
This is a definition whose body is the stated universal quantification and implication. Downstream structural proofs invoke it directly and reduce the ratio via the equality hypothesis.
why it matters
The definition supplies the core proposition for the RS equivalence principle. It is applied by equivalence_implies_ratio_one and discharged by equivalence_ratio_unity_structural. It realizes the claim that a single cost function (T5 uniqueness) renders the equivalence principle a tautology rather than an extra assumption, advancing the gravity formalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.