Jcost_exact
plain-language theorem explainer
Jcost_exact supplies the closed-form expression for the J-cost of a small deviation ε from unity, namely ε²/(2(1+ε)). Equivalence-principle derivations in Recognition Science cite it to quantify the difference between the quadratic approximation and the exact cost. The definition is a direct algebraic transcription of the series expansion remainder for J(1+ε).
Claim. The exact J-cost for a deviation ε is given by $frac{ε^{2}}{2(1+ε)}$.
background
In the Recognition Science framework the single cost function is J(x) = ½(x + x^{-1}) - 1. For a body whose ledger state deviates from balance by a small factor ε, so that x = 1 + ε, the exact cost is obtained by direct substitution. Module G-003 uses this expression to compare inertial and gravitational mass functionals, both of which are built from the same J. Upstream results on circle-phase lifting supply bounds that justify the small-ε regime in which this expansion is applied.
proof idea
The definition is obtained by substituting x = 1 + ε into the closed-form expression for J and simplifying the resulting rational function.
why it matters
This definition is invoked by ep_relative_error to compute the O(ε⁴) relative discrepancy between the quadratic approximation and the exact J-cost. Because both inertial and gravitational masses are extracted from the identical J function (T5 uniqueness), the relative error is the same for both, thereby enforcing the equivalence principle. The parent result ep_relative_error appears in the formalization of G-003.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.