single_source_equivalence
In any single-source mass theory, inertial mass equals gravitational mass for every positive real x. Researchers deriving the equivalence principle from a unique cost function J would cite this lemma. The argument is a direct rewriting that invokes the two projection axioms of the theory structure.
claimFor any mass theory $T$ that derives both inertial and gravitational mass from a single cost function, and for any $x > 0$, the inertial mass at $x$ equals the gravitational mass at $x$.
background
Recognition Science derives the equivalence principle from the uniqueness of the cost function $J(x) = (x + x^{-1})/2 - 1$ (T5). Module G-003 formalizes this as the statement that any mass theory extracting both masses from the same $J$ must have them equal. A SingleSourceMassTheory is a structure consisting of a cost function together with inertial and gravitational mass maps, each required to equal the cost for positive arguments. This encodes the claim that physical mass theories are single-source because $J$ is unique. Upstream results include the structure of J-cost from PhiForcingDerived and ledger factorization, which establish that the cost is the sole source for both inertial resistance and gravitational coupling.
proof idea
The proof is a term-mode one-liner. It rewrites the inertial mass using the axiom that it equals the cost, then rewrites the gravitational mass using its corresponding axiom. Since both equal the cost, they are identical.
why it matters in Recognition Science
This theorem is the direct formalization of the equivalence principle in Recognition Science. It is invoked by rs_equivalence_principle to establish the result for the concrete J-cost theory and by ep_exact_all_orders to confirm exactness at all orders. It fills the G-003 registry item by showing that cost uniqueness (T5) forces inertial mass to equal gravitational mass, realizing the eight-tick octave and D=3 framework landmarks through the single J function.
scope and limits
- Does not apply to theories with multiple independent cost functions.
- Does not provide numerical mass values or spectra.
- Does not cover states with non-positive ratio x.
- Does not address quantum corrections or field-theoretic extensions.
formal statement (Lean)
61theorem single_source_equivalence (T : SingleSourceMassTheory)
62 (x : ℝ) (hx : 0 < x) :
63 T.inertial_mass x = T.gravitational_mass x := by
proof body
Term-mode proof.
64 rw [T.inertial_from_cost x hx, T.gravitational_from_cost x hx]
65
66/-- The ratio of inertial to gravitational mass is exactly 1 in any
67 single-source theory, for any body with nonzero mass. -/