rs_equivalence_principle
plain-language theorem explainer
rs_equivalence_principle shows that the J-cost single-source mass theory yields identical inertial and gravitational masses for any positive real parameter x. Researchers deriving the equivalence principle from a unique cost function cite this result. The proof is a direct one-line application of the general single-source equivalence lemma to the Jcost_mass_theory instance.
Claim. In the J-cost mass theory, where inertial mass and gravitational mass are both extracted as $J(x) = (x + x^{-1})/2 - 1$ for $x > 0$, the two masses coincide: $m_mathrm{inertial}(x) = m_mathrm{gravitational}(x)$.
background
The module formalizes G-003, the RS derivation of the equivalence principle. In RS, T5 establishes uniqueness of the cost function $J(x) = 1/2(x + x^{-1}) - 1$. Both inertial mass (resistance to ledger change, recovered as the quadratic coefficient $J''(1)$) and gravitational mass (source of curvature via J-cost density) are functionals of this single J. The Jcost_mass_theory definition sets inertial_mass x := J(x) and gravitational_mass x := J(x), with the extraction maps being the identity. Any SingleSourceMassTheory built from one cost function therefore forces the two masses to agree.
proof idea
The proof is a term-mode one-liner that applies the single_source_equivalence lemma directly to the Jcost_mass_theory instance and the hypothesis that x is positive.
why it matters
This theorem discharges G-003 by exhibiting the equivalence principle as an immediate consequence of T5 J-uniqueness: only one cost function exists, hence only one mass notion. It is invoked by the kappa_ne_zero result in ZeroParameterGravity to guarantee a nonzero Einstein coupling. The result anchors the framework claim that inertial-gravitational equality is a tautology rather than an empirical coincidence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.