module module high

`IndisputableMonolith.Gravity.EquivalencePrinciple`

This module defines a mass theory in Recognition Science that derives both inertial and gravitational mass from the single J-cost function. Researchers unifying gravity with the recognition framework cite it to ground the equivalence principle in J-uniqueness. The module organizes the argument through single-source definitions and ratio-unity conditions that follow from the forcing chain. It supplies the structural backbone for the claim that every physical mass theory must take this form.

claimA mass theory in which inertial mass $m_i$ and gravitational mass $m_g$ both arise from the same cost function $J(x) = (x + x^{-1})/2 - 1$, so that $m_i/m_g = 1$ whenever the sources coincide.

background

The module sits in the Gravity domain and imports the Constants module, which fixes the RS time quantum at τ₀ = 1 tick. It works from the J-cost function whose uniqueness is established upstream in the forcing chain. The supplied doc-comment states that any physical mass theory must have this form because J is the unique cost function. Sibling declarations introduce the single-source mass theory together with equivalence ratios that equal unity under identical sources.

proof idea

This is a definition module, no proofs. It collects the structural definitions for single-source mass theories, equivalence ratios, and unity conditions that implement the RS claim directly from J-uniqueness.

why it matters in Recognition Science

The module advances the RS claim, quoted in the doc-comment, that every physical mass theory must derive from the single J-cost. It supplies the foundation for downstream statements on equivalence ratios and single-source unity, linking to T5 J-uniqueness and the T0-T8 forcing chain. The parent structures include the single-source equivalence and ratio-unity results that close the argument for the equivalence principle.

scope and limits

Does not derive numerical mass spectra or specific rung values.
Does not treat multi-source or many-body gravitational systems.
Does not prove J-uniqueness, which is imported from the forcing chain.
Does not address quantum-field or curvature couplings beyond the mass definitions.

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