module module high

`IndisputableMonolith.Gravity.EquivalencePrinciple`

The EquivalencePrinciple module defines a single-source mass theory deriving both inertial and gravitational mass from the same J-cost function. Foundational physicists cite it to obtain the equivalence principle as a consequence of J-uniqueness rather than an added postulate. The module organizes the argument through a chain of definitions and ratio lemmas that enforce unity whenever the underlying J-costs match.

claimA single-source mass theory derives inertial mass $m_i$ and gravitational mass $m_g$ from one cost function $J$, so that $m_i = f(J)$ and $m_g = g(J)$ for the same $J$, yielding the ratio $m_i/m_g = 1$.

background

The module belongs to the Gravity domain and imports Constants, whose sole documented content is the RS time quantum $\tau_0 = 1$ tick. Its local setting is the Recognition Science claim that J is the unique cost function, so every mass phenomenon must be expressed through it. The supplied doc-comment states the core thesis: any physical mass theory must take this single-source form because J is the unique cost function.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the rs_equivalence_principle and supporting ratio lemmas that realize the single-source claim inside the gravity section. It directly implements the doc-comment thesis that J-uniqueness forces equivalence of inertial and gravitational mass. No used_by edges are recorded, indicating it functions as a foundational block for later gravity results.

scope and limits

Does not derive numerical mass values from the phi-ladder.
Does not treat multi-source or composite systems.
Does not address corrections outside RS-native units.
Does not prove J-uniqueness; that is imported from Constants.

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