module module high

`IndisputableMonolith.Gravity.EquivalencePrinciple`

The Gravity.EquivalencePrinciple module defines a mass theory in which inertial and gravitational masses both derive from the single J-cost function. Foundational physicists cite it to ground the equivalence principle in Recognition Science. The module collects definitions and lemmas around single-source theories without internal proofs.

claimAny physical mass theory must derive both inertial mass $m_i$ and gravitational mass $m_g$ from the unique cost function $J$, yielding $m_i = m_g$.

background

The module imports Constants, which supplies the RS time quantum τ₀ = 1 tick. It introduces the single-source mass theory SingleSourceMassTheory together with supporting lemmas such as single_source_equivalence and rs_equivalence_principle. The local setting is Recognition Science, where J is the unique cost function satisfying the Recognition Composition Law, forcing all mass theories to take this form.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the single-source mass theory that realizes the RS claim that every physical mass theory must derive both masses from J. It anchors the equivalence principle inside the Gravity domain and feeds downstream gravity constructions that rely on inertial-gravitational equality.

scope and limits

Does not prove J-uniqueness (handled upstream).
Does not compute explicit mass values on the phi-ladder.
Does not treat multi-source or quantum corrections.
Does not derive numerical predictions beyond the structural claim.

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (20)

structure SingleSourceMassTheory L51
theorem single_source_equivalence L61
theorem single_source_ratio_unity L68
def Jcost_mass_theory L79
theorem rs_equivalence_principle L89
theorem rs_equivalence_ratio L94
def equivalence_ratio_unity L103
theorem ratio_one_when_equal L107
theorem equivalence_trivial_when_same L111
theorem equivalence_ratio_unity_structural L114
theorem equivalence_implies_ratio_one L118
def Jcost_full L154
def Jcost_quadratic L157
def Jcost_exact L160
def ep_relative_error L163
theorem ep_exact_all_orders L169
def eotvos_parameter L176
theorem rs_eotvos_zero L178
def microscope_bound L184
theorem rs_consistent_with_microscope L186