Gravity Equivalence Principle Ratio One When Equal

The ratio's scope

The declaration ratio_one_when_equal proves a fact about division: if two real numbers are equal and the second one is not zero, then their ratio is exactly 1. For any nonzero real number m, the statement m / m = 1 is a basic property of arithmetic. The theorem simply formalizes this in the framework's library, a machine-checked collection of formal theorems. It is a conditional statement: the equality of the two masses is assumed, and the nonzero condition is required because division by zero is undefined.

This result is the final step in a chain that attempts to derive the equivalence principle, the observation that inertial mass and gravitational mass are the same. The framework models both kinds of mass as outputs of the same underlying function, called the cost, a measure of the price of a change in a discrete record of events. Because both masses are defined to be that same function, a separate theorem proves they are equal for any positive input. The ratio_one_when_equal theorem then takes that proven equality and the nonzero condition to conclude the ratio is 1.

The theorem does not by itself say anything about physics. It contains no assumption about gravity, no model of a body, and no measurement. Its entire content is the arithmetic step from equality to a ratio of one. The physical weight of the equivalence principle in this framework comes from the earlier definition that both masses are the same function, not from this final division. The declaration is a small, correct, and necessary piece of bookkeeping.

What the framework claims beyond this theorem is a prediction: the equivalence principle holds exactly, with zero violation, because both masses derive from the single cost function. This prediction is falsifiable. A measured violation of the equivalence principle, an Eötvös parameter greater than zero, would require a modification of the single-cost-function framework. The ratio_one_when_equal theorem itself is not that prediction; it is the arithmetic that closes the proof once the physical equality has been established.

theorem equivalence_trivial_when_same :
    ∀ m : ℝ, m ≠ 0 → m / m = 1 := fun _ hm => div_self hm

theorem ratio_one_when_equal (m_i m_g : ℝ) (heq : m_i = m_g) (hg : m_g ≠ 0) :
    m_i / m_g = 1 := by
  rw [heq, div_self hg]

theorem ratio_one_when_equal (m_i m_g : ℝ) (heq : m_i = m_g) (hg : m_g ≠ 0) :
    m_i / m_g = 1 := by
  rw [heq, div_self hg]

What this page does not claim

The theorem does not prove that inertial mass equals gravitational mass. The theorem does not model any physical system or force. The theorem does not predict the result of any experiment.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/EquivalencePrinciple.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: