equivalence_implies_ratio_one
plain-language theorem explainer
The declaration shows that the equivalence ratio unity hypothesis forces the inertial-to-gravitational mass ratio to equal one exactly when the two masses are set equal. Researchers formalizing the equivalence principle from a single cost function would cite this to confirm exact mass equality in RS gravity. The proof is a direct term application of the defining hypothesis to the supplied masses and equality premise.
Claim. Assume the equivalence ratio unity condition. For real numbers $m_i$ and $m_g$ with $m_g ≠ 0$ and $m_i = m_g$, the ratio satisfies $m_i / m_g = 1$.
background
In Recognition Science the equivalence principle follows from a single cost function J(x) = ½(x + x⁻¹) − 1 whose uniqueness is fixed at T5. Inertial mass is recovered as the second derivative J''(1) = 1; gravitational mass is the integrated J-cost defect density. Both quantities are therefore functionals of the identical J, so their ratio is forced to unity for any body. Module G-003 registers this as the statement that any mass theory extracting both masses from the same J must produce equal values. The local formalization treats the principle as a tautology inside the single-cost framework rather than an independent postulate. Upstream results supply supporting structures such as ledger factorization and integration-gap lemmas that underwrite the J-cost definitions.
proof idea
The proof is a one-line term wrapper that applies the hypothesis equivalence_ratio_unity directly to the inertial mass, gravitational mass, non-zero guard, and equality assumption.
why it matters
The result completes the formalization of G-003 by confirming that the single-J framework yields exact mass equality without additional assumptions. It aligns with T5 J-uniqueness in the forcing chain and supports the prediction of zero EP violation to all orders. No downstream theorems yet consume it, but it anchors the exact (non-approximate) character of the RS equivalence principle against weak-field expansions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.