rs_equivalence_ratio
plain-language theorem explainer
The declaration shows that inertial and gravitational masses coincide exactly in the J-cost theory, so their ratio is identically one for any positive x with nonzero gravitational mass. Researchers deriving the equivalence principle from a single cost function would cite this as the concrete instance of the general single-source result. The proof is a direct one-line instantiation of single_source_ratio_unity on the Jcost_mass_theory definition.
Claim. In the J-cost mass theory, where both inertial mass and gravitational mass are given by the same function $J(x) = (x + x^{-1})/2 - 1$, the ratio of inertial mass to gravitational mass equals 1 for every $x > 0$ with nonzero gravitational mass.
background
The module formalizes G-003, the RS derivation of the equivalence principle. It starts from the single cost function $J(x) = (x + x^{-1})/2 - 1$ fixed by T5 uniqueness. Both inertial mass (resistance to ledger change, extracted from the quadratic term near $x=1$) and gravitational mass (source of curvature via J-cost density) are computed from this identical J, so they cannot differ. Jcost_mass_theory is the canonical SingleSourceMassTheory that sets cost, inertial_mass, and gravitational_mass all equal to this J, with the two from_cost fields being reflexivity.
proof idea
The proof is the term single_source_ratio_unity Jcost_mass_theory x hx hne. This directly instantiates the upstream theorem single_source_ratio_unity, which states that any SingleSourceMassTheory yields inertial_mass x / gravitational_mass x = 1 under the given positivity and nonzeroness hypotheses, then substitutes the Jcost_mass_theory instance.
why it matters
The result completes the formalization of G-003 by exhibiting the tautological equality that follows from a single cost function. It rests on T5 J-uniqueness and the single_source_ratio_unity lemma, confirming that equivalence is forced rather than postulated. The theorem sits inside the Gravity module and supplies the concrete case needed for any downstream derivation that invokes the RS equivalence principle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.