Gravity Equivalence Principle Single Source Ratio Unity

The single-source ratio

The equivalence principle is the physics observation that a body's inertial mass, its resistance to being accelerated, and its gravitational mass, the charge that determines how strongly it feels gravity, are the same number. Experiments have tested this equality with extraordinary precision. The MICROSCOPE satellite mission, which compared the free-fall motion of different materials in orbit around Earth, found any difference between the two masses to be smaller than one part in 10¹⁵.

Recognition Science offers a reason why that ratio is exactly one rather than merely very close to it. The framework begins with a ledger, a discrete record of recognition events, and a single forced cost function J(x) = ½(x + x⁻¹) − 1 that measures the price of any state. In this account, both inertial and gravitational mass are read off from the same function J. A mass theory that extracts both quantities from one cost function is called single-source, and the structure definition in the framework's machine-checked library of formal theorems states this directly: for any positive ratio x, inertial_mass x equals cost x and gravitational_mass x equals cost x.

From that definition, the theorem single_source_ratio_unity follows in a few lines. If a body has nonzero gravitational mass, then dividing the inertial mass by the gravitational mass yields exactly 1. The proof is immediate once the two masses are known to be the same function, and the library records it as a formal theorem with no gaps. The framework's own cost function J provides a concrete instance: the theorem rs_equivalence_ratio applies it to show the ratio is 1 for all positive x, not just in the weak-field limit where J is approximately quadratic.

The framework states the claim as an exact equality to all orders, not an approximation. The full cost function J has higher-order terms beyond the quadratic approximation, but those corrections affect inertial and gravitational mass identically because both come from the same J. The predicted Eötvös parameter, a standard measure of equivalence-principle violation, is exactly zero. This is a falsifiable prediction: any measured nonzero value would require modifying the single-cost-function framework.

What the theorem does not claim is broader than it might appear. It does not assert that the framework has derived the specific numerical values of masses, nor that it has explained why the cost function takes its particular form. The theorem is conditional: if a mass theory is single-source, then the ratio is one. The framework argues that any physical mass theory must be single-source because J is unique, but that uniqueness is a separate theorem. The ratio result itself does not prove the equivalence principle in the physical world; it proves a structural fact about a class of formal theories.

/-- 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

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

/-- The MICROSCOPE experiment measures η < 10⁻¹⁵.
    RS predicts η = 0 exactly. This is consistent with experiment and
    makes the strongest possible prediction: any nonzero η falsifies RS. -/
def microscope_bound : ℝ := 1e-15

What this page does not claim

The theorem does not prove that any actual physical theory must be single-source. The theorem does not derive the numerical value of any mass. The theorem does not explain why the cost function J has its particular form.

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: