SingleSourceMassTheory
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not specify the explicit functional form of the cost.
- Does not prove that J is the only admissible cost function.
- Does not treat zero or negative arguments.
- Does not incorporate composition-dependent corrections beyond cost equality.
formal statement (Lean)
51structure SingleSourceMassTheory where
52 cost : ℝ → ℝ
53 inertial_mass : ℝ → ℝ
54 gravitational_mass : ℝ → ℝ
55 inertial_from_cost : ∀ x, 0 < x → inertial_mass x = cost x
56 gravitational_from_cost : ∀ x, 0 < x → gravitational_mass x = cost x
57
58/-- In a single-source mass theory, inertial and gravitational mass are
59 identical for all positive-ratio states. This is the equivalence
60 principle derived from cost uniqueness. -/