Gravity Equivalence Principle Equivalence Implies Ratio One

The ratio and its limits

The equivalence principle is the physics observation that a body's resistance to being accelerated, its inertial mass, and its response to a gravitational field, its gravitational mass, are the same number. Experiments have tested this sameness with great care: the MICROSCOPE satellite measured the ratio to agree within one part in 10¹⁵. The principle is why a feather and a hammer fall together in vacuum. In classical physics it is an empirical fact, not a logical necessity.

Recognition Science (RS) is a framework that tries to derive physical laws from a single starting point: reality keeps a ledger, a discrete record of recognition events, and the cost of each recognition, measured by a function J(x) = (x + x⁻¹)/2 − 1, is forced by five plain conditions. A theorem in its machine-checked library of formal theorems proves that any cost function meeting those conditions must equal that J. From that unique function, the framework derives both inertial and gravitational mass as two functionals of the same J. Since both come from one source, they cannot differ.

Within this framework, the declaration equivalence_implies_ratio_one establishes a narrow logical point: if a mass theory extracts both masses from the same cost function, and if the gravitational mass is nonzero, then the ratio of inertial to gravitational mass is exactly 1. The proof is a short chain: the two masses are equal by construction, and dividing a nonzero number by itself gives 1. The declaration also states the same result for the specific J-cost function, where both masses are defined as J(x) itself. The theorem is exact, not an approximation: it holds for every positive ratio x, not only near x = 1. The framework's prediction is that the Eötvös parameter, a standard measure of equivalence violation, is exactly zero, which is consistent with the MICROSCOPE bound and is falsifiable by any measured nonzero value.

The declaration does not claim that the equivalence principle holds in the physical world. That is a separate, empirical question. The theorem only shows what follows if one accepts the framework's single-cost-function premise. It also does not claim that the ratio is 1 for a body with zero gravitational mass, since the theorem explicitly requires a nonzero denominator. And it does not, by itself, prove the uniqueness of the cost function J; that uniqueness is a prior theorem the declaration relies on. The ratio-one result is a consequence of a definitional choice, not a measurement of nature.

/-- The ratio of inertial to gravitational mass is exactly 1 in any
    single-source theory, for any body with nonzero mass. -/
theorem single_source_ratio_unity (T : SingleSourceMassTheory)
    (x : ℝ) (hx : 0 < x) (hne : T.gravitational_mass x ≠ 0) :
    T.inertial_mass x / T.gravitational_mass x = 1 := by
  rw [single_source_equivalence T x hx, div_self hne]

/-- The RS equivalence ratio is 1 for all bodies with nonzero mass. -/
theorem rs_equivalence_ratio (x : ℝ) (hx : 0 < x)
    (hne : Jcost_mass_theory.gravitational_mass x ≠ 0) :
    Jcost_mass_theory.inertial_mass x / Jcost_mass_theory.gravitational_mass x = 1 :=
  single_source_ratio_unity Jcost_mass_theory x hx hne

/-- For the EP, what matters is NOT the size of corrections, but whether
    they affect inertial and gravitational mass DIFFERENTLY.
    In SingleSourceMassTheory, they cannot differ: both use J_full. -/
theorem ep_exact_all_orders (T : SingleSourceMassTheory) (x : ℝ) (hx : 0 < x) :
    T.inertial_mass x = T.gravitational_mass x :=
  single_source_equivalence T x hx

theorem rs_eotvos_zero (a : ℝ) : eotvos_parameter a a = 0 := by
  unfold eotvos_parameter; simp

What this page does not claim

The theorem does not claim the equivalence principle holds in the physical world; that is an empirical matter. The theorem does not claim the ratio is 1 for a body with zero gravitational mass, since it requires a nonzero denominator. The declaration does not by itself prove the uniqueness of the cost function J; it relies on that as a prior theorem.

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: