Gravity Equivalence Principle

The Single-Source Derivation

The gravity equivalence principle in Recognition Science is the statement that inertial mass and gravitational mass are the same quantity. The framework derives this from a single source: the unique cost function recognition cost J(x) = (x + x⁻¹)/2 − 1. Both masses are defined as functionals of this same J. Inertial mass is the resistance to ledger state change, measured by the quadratic coefficient of J near balance. Gravitational mass is the source of curvature, the integrated J-cost defect. Because both come from the same J, they cannot differ.

The module EquivalencePrinciple.lean formalizes this as a structure SingleSourceMassTheory: a theory that extracts both masses from one cost function. The theorem single_source_equivalence proves that in any such theory, inertial mass equals gravitational mass for all positive states. The theorem rs_equivalence_principle applies this to J-cost directly. The ratio of inertial to gravitational mass is exactly 1 for any nonzero mass, established in rs_equivalence_ratio.

The equality is exact, not a weak-field approximation. The full J-cost is not quadratic; it has higher-order corrections. But both masses are computed from the same full J, so the corrections affect both equally. The ratio holds for all x > 0, not just near x = 1. The theorem ep_exact_all_orders states this equality for every single-source theory at every order.

The framework makes a sharp empirical prediction: the Eötvös parameter η, which measures differences in acceleration between test bodies, is exactly zero. The theorem rs_eotvos_zero proves η = 0 for equal accelerations. This is consistent with the MICROSCOPE bound η < 10⁻¹⁵, established in rs_consistent_with_microscope. Any measured nonzero η would falsify the single-cost-function framework.

THEOREM single_source_equivalence · IndisputableMonolith/Gravity/EquivalencePrinciple.lean

THEOREM rs_equivalence_principle · IndisputableMonolith/Gravity/EquivalencePrinciple.lean

THEOREM rs_equivalence_ratio · IndisputableMonolith/Gravity/EquivalencePrinciple.lean

THEOREM ep_exact_all_orders · IndisputableMonolith/Gravity/EquivalencePrinciple.lean

THEOREM rs_eotvos_zero · IndisputableMonolith/Gravity/EquivalencePrinciple.lean

THEOREM rs_consistent_with_microscope · IndisputableMonolith/Gravity/EquivalencePrinciple.lean

What this page does not claim

This answer does not claim that the equivalence principle is an empirical observation; it is a derived theorem from cost uniqueness. This answer does not claim that the full J-cost is quadratic; the equality holds despite higher-order corrections. This answer does not claim that the physical bridge from J-cost to spacetime curvature is formalized; that remains open.

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: