single_source_ratio_unity
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.