jcost_symmetric_pair
plain-language theorem explainer
The theorem proves that J-cost at symmetric points around its minimum sums to δ²/2 times (1/(1+δ) + 1/(1-δ)) for |δ|<1. Analysts deriving local stability and universal sensitivity in Recognition Science equilibria cite this algebraic identity when expanding quadratic costs for small deviations. The tactic proof substitutes the upstream quadratic-leading-order formula twice and applies ring to align the signed terms.
Claim. For real δ with 0 < 1-δ and 0 < 1+δ, the J-cost function satisfies $J(1+δ) + J(1-δ) = δ²/(2(1+δ)) + δ²/(2(1-δ))$, where $J(r) = (r-1)²/(2r)$ is the cost with minimum zero at r=1.
background
The module proves J-cost convexity on (0,∞) with unique minimum at r=1 where J(1)=0. The key identity is J(r)=(r-1)²/(2r), which yields non-negativity, the limit to zero at unity, and the leading quadratic term (r-1)²/2 near the minimum. This fixes the universal sensitivity coefficient at 1/2 for all Recognition Science equilibria.
proof idea
The tactic proof rewrites the first summand via the upstream lemma jcost_at_one_plus_delta applied to δ. It then invokes the same lemma on -δ (positivity by linarith), rewrites the argument 1+(-δ) to 1-δ by ring, squares the sign change, and substitutes to obtain the matching term for 1-δ. The final rewrite assembles both sides.
why it matters
This identity completes the local quadratic analysis near the J-cost minimum, directly supporting the C25 structural claim that the Hessian at r=1 supplies the universal sensitivity constant 1/2. It underpins equilibrium stability derivations across domains in the Recognition framework. No open questions remain; the result closes the algebraic verification of the quadratic approximation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.