Jcost_one_plus_exact
plain-language theorem explainer
The exact algebraic identity equating the J-cost of a perturbed scale 1 + ε to the rational quadratic ε²/(2(1 + ε)). Weak-field gravity derivations cite it to replace recognition cost with a Hamiltonian-like kinetic term. The proof is a direct algebraic reduction that unfolds the definition and clears the resulting rational expression.
Claim. For real ε > -1, let J(x) = (x + x^{-1})/2 - 1. Then J(1 + ε) = ε² / (2(1 + ε)).
background
Jcost is the function J(x) = (x + x^{-1})/2 - 1 for x > 0, the unique cost functional forced by the Recognition Composition Law. The present theorem lives inside the EnergyProcessingBridge module, whose purpose is to equate energy distributions with processing gradients under the Recognition Science gravity model. No upstream lemmas are required; the identity follows immediately from the definition once the denominator is shown nonzero.
proof idea
Unfold the definition of Jcost. Establish 1 + ε > 0 by linarith to guarantee the reciprocal is defined. Apply field_simp to cancel the common denominator, then ring to confirm the numerator identity.
why it matters
This exact identity is invoked by energy_processing_bridge, Jcost_quadratic_ratio, cross_term_factored, Jcost_additive_leading, and superposition_justified. It supplies the precise bridge between J-cost and quadratic kinetic energy that the weak-field superposition principle and the energy-processing equivalence rest upon. In the larger framework it anchors the transition from the phi-ladder cost structure to classical Hamiltonian mechanics in the small-strain limit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.