single_source_equivalence
plain-language theorem explainer
Any single-source mass theory equates inertial and gravitational mass for positive arguments via their shared cost function. Researchers deriving the equivalence principle from cost uniqueness would reference this. The term-mode proof rewrites both masses to the common cost using the structure axioms.
Claim. Let $T$ be a single-source mass theory. Then for all real $x > 0$, the inertial mass of $x$ under $T$ equals the gravitational mass of $x$ under $T$.
background
SingleSourceMassTheory is the structure requiring a shared cost function together with inertial_mass and gravitational_mass that both equal the cost for positive arguments. The module formalizes G-003 by showing that the equivalence principle follows because both masses derive from the unique J-cost function $J(x) = ½(x + x^{-1}) - 1$ (T5 uniqueness). Upstream results on phi-forcing and ledger factorization supply the uniqueness of this cost.
proof idea
One-line term proof that rewrites inertial_mass x and gravitational_mass x to the shared cost via the two from_cost fields of SingleSourceMassTheory.
why it matters
This theorem is the direct statement of the equivalence principle in single-source theories. It is invoked by rs_equivalence_principle to obtain the RS version and by ep_exact_all_orders to show corrections cannot split the masses. It realizes the G-003 registry item and rests on T5 J-uniqueness from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.