Jcost_mass_theory
plain-language theorem explainer
The definition supplies the canonical single-source mass theory in which both inertial and gravitational mass equal the J-cost J(x) = (x + x^{-1})/2 - 1. Researchers deriving the equivalence principle from Recognition Science cite this as the concrete model forced by T5 uniqueness. The construction directly populates the SingleSourceMassTheory structure with the shared cost expression and discharges the two mass-equality fields by reflexivity.
Claim. Let $J(x) := (x + x^{-1})/2 - 1$. The single-source mass theory is the structure whose cost function is $J$, whose inertial mass map is $J$, whose gravitational mass map is $J$, and whose two extraction axioms hold identically for every positive real $x$.
background
A SingleSourceMassTheory is a structure requiring a cost function together with inertial_mass and gravitational_mass maps, each required to equal the cost on positive reals. In the G-003 module this structure encodes the claim that inertial response (resistance to ledger change) and gravitational coupling (source of curvature) must coincide once both are derived from the same cost. The local setting is the RS derivation that a unique cost function J forces the equivalence principle to be a tautology rather than an independent postulate. Upstream, the J expression itself is obtained as the derived cost of a multiplicative recognizer and as the cost assigned to recognition events.
proof idea
The definition is a direct structure instantiation: cost, inertial_mass and gravitational_mass are all set to the J expression, after which the two from_cost fields are supplied as constant functions returning reflexivity.
why it matters
This definition is the concrete model consumed by rs_equivalence_principle (which states inertial_mass x = gravitational_mass x) and rs_equivalence_ratio (which states the ratio equals 1). It realizes the G-003 registry item by exhibiting the single J-cost as a mass theory, thereby closing the step from T5 J-uniqueness to the observed equality of inertial and gravitational mass. The construction touches the open question of whether every physical mass theory must be single-source.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.