equivalence_trivial_when_same
plain-language theorem explainer
Any nonzero real m satisfies m/m = 1. This identity is cited inside the Gravity.EquivalencePrinciple module to anchor the claim that inertial and gravitational masses coincide when both are extracted from the single J-cost function. The proof reduces immediately to the standard division property in the reals.
Claim. For every real number $m$ with $m ≠ 0$, $m/m = 1$.
background
The module formalizes G-003: the equivalence principle as a tautology once inertial mass (resistance to ledger change, given by J''(1)) and gravitational mass (source of T^00 curvature, given by integrated J-cost defect) are both computed from the same unique cost function J(x) = ½(x + x^{-1}) − 1. The RS derivation begins from T5 J-uniqueness and shows that any MassTheory extracting both masses from this J necessarily produces equal values. The trivial identity m/m = 1 supplies the algebraic step that converts identical J-cost inputs into a mass ratio of unity.
proof idea
One-line wrapper that applies the div_self lemma from Mathlib directly to the hypothesis m ≠ 0.
why it matters
It supplies the final algebraic closure for the ratio-unity step inside the G-003 derivation. The parent claim is that any single-source mass theory built on the unique J must satisfy inertial = gravitational mass; this identity is the concrete instance when the two sources are literally the same object. It touches the open question of whether the full structural equivalence (rs_equivalence_principle) follows without additional hypotheses on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.