Jcost_quadratic
plain-language theorem explainer
The quadratic approximation to the J-cost near balance is defined as ε²/2. Researchers deriving inertial-gravitational mass equality from a single cost function cite this when linearizing the restoring force for small deviations. It is introduced by direct definition matching the second-order Taylor term of J(1 + ε).
Claim. The quadratic approximation to the cost function for small deviations ε from unity is given by $ε²/2$.
background
The Recognition Science cost function is J(x) = ½(x + x⁻¹) − 1, the unique solution to the Recognition Composition Law. Upstream, the cost of any recognition event is this J-cost, and for a multiplicative recognizer it is obtained by applying the derived comparator to positive ratios. In the G-003 module setting both inertial mass (resistance to ledger change) and gravitational mass (source of curvature via J-cost density) are extracted from functionals of the identical J, so equality is forced by T5 uniqueness rather than imposed.
proof idea
Direct definition encoding the known second-order Taylor expansion of J around 1. No lemmas or tactics are invoked; the body simply writes the quadratic term.
why it matters
It supplies the explicit small-ε form used by the downstream ep_relative_error to quantify O(ε⁴) corrections while showing that inertial and gravitational masses remain identical because both employ the same J_full. The definition therefore closes the G-003 registry item: equivalence is a tautology once a single cost function is adopted. It sits inside the T5–T8 forcing chain and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.