module module high

`IndisputableMonolith.Gravity.EquivalencePrinciple`

This module defines a mass theory deriving both inertial and gravitational mass from the single J-cost function. It asserts that any physical mass theory must take this form due to J-uniqueness under the Recognition Composition Law. The module structures its content around single-source mass theories and equivalence ratios. Researchers deriving gravity from Recognition Science foundations would cite it when linking the equivalence principle to the forcing chain.

claimA mass theory in which inertial mass $m_i$ and gravitational mass $m_g$ are both obtained from the cost function $J(x) = (x + x^{-1})/2 - 1$, with the claim that every physical mass theory must adopt this form.

background

Recognition Science derives physics from the functional equation whose unique solution is the J-cost function. This module sits in the Gravity domain and imports the base time quantum τ₀ = 1 tick. It introduces SingleSourceMassTheory together with supporting lemmas on equivalence ratios and Jcost_mass_theory.

The local setting is that J satisfies the Recognition Composition Law, forcing inertial and gravitational masses to coincide when mass arises from a single source. The module therefore supplies the structural bridge between the uniqueness of J and the classical equivalence principle.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the mass-theory foundation required by the equivalence principle in Recognition Science. It feeds the Gravity domain by showing that J-uniqueness (T5) directly implies inertial-gravitational mass equality, thereby closing one step in the derivation of D = 3 and the Newtonian limit from the forcing chain.

scope and limits

Does not derive numerical mass spectra or particle masses.
Does not treat multi-source or composite mass theories.
Does not produce the gravitational constant G or curvature terms.
Does not address quantum corrections or field-theoretic extensions.

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