ratio_one_when_equal
When inertial and gravitational masses are set equal with nonzero denominator, their ratio equals one. Researchers formalizing the Recognition Science equivalence principle cite this identity as the terminal algebraic step. The proof is a one-line rewrite that substitutes the equality hypothesis and applies the division-self lemma for nonzero reals.
claimLet $m_i, m_g : ℝ$ with $m_i = m_g$ and $m_g ≠ 0$. Then $m_i / m_g = 1$.
background
The module G-003 derives the equivalence principle from the single cost function J(x) = ½(x + x⁻¹) − 1 whose uniqueness is fixed at T5. Inertial mass arises as the quadratic coefficient of J near balance while gravitational mass is the integrated J-cost defect; both therefore coincide by construction. The present theorem supplies the elementary identity needed once the two masses are already asserted equal.
proof idea
One-line wrapper that rewrites the goal by the hypothesis m_i = m_g and then invokes div_self on the nonzero m_g.
why it matters in Recognition Science
The result is the final step inside equivalence_ratio_unity_structural, which itself proves the full equivalence_ratio_unity statement of G-003. It therefore closes the algebraic part of the Recognition Science argument that a unique J forces inertial and gravitational masses to be identical, consistent with the T5 uniqueness and the single-source mass theory developed in the same module.
scope and limits
- Does not prove that inertial and gravitational masses are equal in general.
- Does not apply when m_g = 0.
- Does not derive the explicit mass expressions from J.
- Operates only on real numbers.
Lean usage
exact ratio_one_when_equal m_i m_g heq hgformal statement (Lean)
107theorem ratio_one_when_equal (m_i m_g : ℝ) (heq : m_i = m_g) (hg : m_g ≠ 0) :
108 m_i / m_g = 1 := by
proof body
One-line wrapper that applies rw.
109 rw [heq, div_self hg]
110