SingleSourceMassTheory
plain-language theorem explainer
SingleSourceMassTheory encodes a mass theory in which a single cost function determines both inertial and gravitational mass for every positive ratio. Physicists deriving the equivalence principle from Recognition Science cost uniqueness cite this structure to formalize the single-source premise. The definition consists of three functions together with two axioms that force the two masses to equal the cost whenever the argument is positive.
Claim. A mass theory is single-source when it supplies a cost function $c : (0,∞) → ℝ$ such that the inertial mass $m_i(x)$ and gravitational mass $m_g(x)$ both satisfy $m_i(x) = c(x)$ and $m_g(x) = c(x)$ for all $x > 0$.
background
Recognition Science derives all masses from the unique cost function J(x) = ½(x + x⁻¹) − 1 fixed by T5. Inertial mass is the quadratic restoring coefficient for small ledger deviations from balance; gravitational mass is the integrated J-cost defect that sources curvature. Both quantities are therefore functionals of the same primitive J. The module G-003 formalizes this identity as the content of any SingleSourceMassTheory. Upstream cost definitions appear in ObserverForcing.cost (the J-cost of a recognition event) and MultiplicativeRecognizerL4.cost (the derived cost of a comparator on positive ratios).
proof idea
This is a structure definition with an empty proof body. It simply declares the three component functions and the two forcing axioms that identify inertial_mass and gravitational_mass with the supplied cost on the positive reals.
why it matters
The structure supplies the central hypothesis for G-003 and is invoked by single_source_equivalence and ep_exact_all_orders to conclude that the Eötvös parameter vanishes identically. It is also used to construct the concrete Jcost_mass_theory instance and to prove kappa_ne_zero in ZeroParameterGravity. The parent result is T5 J-uniqueness, which forces every physical mass theory to take this single-source form and thereby renders the equivalence principle a tautology rather than an independent postulate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.