ep_exact_all_orders
plain-language theorem explainer
Any mass theory deriving both inertial and gravitational mass from the single unique cost function J must equate them for all positive ratios. This theorem asserts exact equality holds in SingleSourceMassTheory, so the Eötvös parameter is zero at every order. A physicist testing composition dependence would cite it to obtain the RS prediction of eta exactly zero. The proof is a direct one-line application of the single-source equivalence lemma.
Claim. Let $T$ be a single-source mass theory. For every $x > 0$, the inertial mass equals the gravitational mass: $m_mathrm{inertial}(x) = m_mathrm{gravitational}(x)$.
background
Module G-003 formalizes the RS derivation that inertial mass equals gravitational mass. SingleSourceMassTheory is the structure requiring a single cost function together with the two axioms inertial_from_cost and gravitational_from_cost, each stating that the respective mass equals the cost for every positive ratio. The module document states that both masses are functionals of the same J, so they cannot differ. Upstream single_source_equivalence already records the same identity by rewriting those two axioms.
proof idea
This is a one-line wrapper that applies the single_source_equivalence lemma to the supplied theory T and positive ratio x.
why it matters
The declaration completes G-003 by establishing exact equality inside any single-source theory. It thereby supplies the formal content of the RS claim that the equivalence principle is a tautology once J is unique (T5). The result predicts the Eötvös parameter eta equals zero with no composition-dependent corrections possible. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.