Jcost_quadratic_ratio
plain-language theorem explainer
For small positive ε the J-cost of the perturbed state 1+ε is bounded above by ε²/2. Workers deriving emergent gravity from recognition costs cite the bound to control quadratic energy densities in the processing field. The proof is a one-line term reduction that substitutes the closed-form identity for Jcost(1+ε) and applies a standard non-negative division inequality.
Claim. For real ε satisfying -1 < ε and ε > 0, if J(x) := ½(x + x⁻¹) - 1 denotes the J-cost, then J(1 + ε) ≤ ε²/2.
background
J-cost is the function J(x) = (x + x⁻¹)/2 - 1 for x > 0; it is the unique cost functional forced by the Recognition Composition Law. In the EnergyProcessingBridge module energy is identified with J-cost density, which is the processing potential that sources gravity via the identity T⁰⁰ = J-cost density. Upstream results supply the exact identity Jcost(1 + ε) = ε²/(2(1 + ε)) together with non-negativity of recognition-event costs.
proof idea
The proof is a direct term-mode reduction. It rewrites Jcost(1 + ε) via the exact identity Jcost_one_plus_exact, then applies div_le_div_of_nonneg_left using non-negativity of ε² and positivity of the denominators.
why it matters
The bound supplies the quadratic control required for the energy-to-processing-field map that bridges to gravity. It supports the sibling theorems EnergyProcessingEquivalence and energy_distribution_creates_gravity_modifier. Within the Recognition framework it furnishes the small-perturbation estimate needed for the T0 forcing chain in which J-cost generates the spatial defect that sources gravity, consistent with the eight-tick octave and D = 3 emergence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.