single_source_ratio_unity
Any single-source mass theory has inertial mass equal to gravitational mass, so the ratio is one for nonzero gravitational mass. Recognition Science researchers cite this to derive the equivalence principle from cost uniqueness rather than an added postulate. The proof is a term-mode reduction that substitutes the equality from the prior equivalence result and cancels the denominator via the nonzero hypothesis.
claimFor any single-source mass theory $T$, any positive real $x$ with nonzero gravitational mass, the ratio of inertial mass to gravitational mass equals 1.
background
The module addresses G-003, the Recognition Science derivation of the equivalence principle. A single-source mass theory is a structure in which a single cost function determines both inertial mass (resistance to ledger state change) and gravitational mass (source of curvature), with both set equal to the cost for positive arguments. This encodes the claim that the unique J-cost function forces the masses to coincide.
proof idea
The term proof rewrites the inertial mass to equal the gravitational mass using the prior equivalence result for single-source theories, then applies the division identity on the nonzero hypothesis.
why it matters in Recognition Science
This fills the G-003 registry item by showing the mass ratio of one follows directly from the single cost function. It is applied by the follow-on result that obtains the ratio for the concrete J-cost theory. The declaration ties the equivalence principle to T5 uniqueness of J, confirming it is a tautology in the framework.
scope and limits
- Does not prove that all mass theories must be single-source.
- Does not apply when gravitational mass vanishes.
- Does not derive the explicit form of the cost function.
- Does not address relativistic or quantum corrections.
Lean usage
theorem rs_equivalence_ratio (x : ℝ) (hx : 0 < x) (hne : Jcost_mass_theory.gravitational_mass x ≠ 0) : Jcost_mass_theory.inertial_mass x / Jcost_mass_theory.gravitational_mass x = 1 := single_source_ratio_unity Jcost_mass_theory x hx hneformal statement (Lean)
68theorem single_source_ratio_unity (T : SingleSourceMassTheory)
69 (x : ℝ) (hx : 0 < x) (hne : T.gravitational_mass x ≠ 0) :
70 T.inertial_mass x / T.gravitational_mass x = 1 := by
proof body
Term-mode proof.
71 rw [single_source_equivalence T x hx, div_self hne]
72
73/-! ## J-Cost Is a Single-Source Theory -/
74
75noncomputable section
76
77/-- J-cost defines a canonical single-source mass theory. Both inertial
78 response and gravitational coupling derive from J(x) = ½(x + x⁻¹) − 1. -/