Jcost_full
plain-language theorem explainer
The declaration defines the full J-cost function J(x) = (x + x^{-1})/2 - 1 on the reals. Equivalence-principle derivations in Recognition Science cite it as the single source for both inertial mass (quadratic term near x=1) and gravitational mass (J-cost density). It is supplied by a direct one-line definition matching the T5 uniqueness formula.
Claim. The full J-cost function is defined by $J(x) := (x + x^{-1})/2 - 1$ for $x$ real.
background
Module Gravity.EquivalencePrinciple formalizes G-003: the RS derivation that inertial mass equals gravitational mass because both are extracted from one cost function. Inertial mass arises as the quadratic coefficient J''(1) for small deviations x=1+ε, while gravitational mass is the integrated J-cost defect sourcing the Einstein tensor. The supplied definition gives the explicit form required by T5 uniqueness: J(x) = ½(x + x^{-1}) - 1.
proof idea
Direct definition that implements the T5 formula without reduction or approximation.
why it matters
This definition supplies the unique J required by the module's equivalence theorems, making inertial-gravitational equality a tautology rather than an extra assumption. It realizes the T5 step of the forcing chain and feeds the single-source mass theory results listed as siblings. No open scaffolding is closed here; the definition is foundational for all downstream mass-ratio statements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.