Jcost_agrees_on_exp
plain-language theorem explainer
Jcost satisfies the AgreesOnExp predicate, which requires that the function evaluated at exp t equals Jcost at exp t for every real t. Researchers building averaging and Jensen-type structures for the Recognition Science cost function cite this result to equip Jcost with the necessary instances. The proof is a one-line tactic that introduces t and applies reflexivity to the identical sides.
Claim. The function $J(x) = (x + x^{-1})/2 - 1$ satisfies AgreesOnExp, i.e., for all real $t$, $J(e^t) = J(e^t)$.
background
Jcost is defined as Jcost(x) := (x + x^{-1})/2 - 1. AgreesOnExp F is the predicate requiring F(exp t) = Jcost(exp t) for all real t; it serves as the compatibility condition inside the AveragingAgree and AveragingDerivation classes. The local module supplies the core Jcost lemmas (Jcost_unit0, Jcost_symm) and the JensenSketch class that extends SymmUnit with axis bounds, all of which depend on this agreement property.
proof idea
The proof is a one-line wrapper: introduce the real parameter t, then apply reflexivity. No lemmas are invoked because both sides of the equality are syntactically identical.
why it matters
The declaration supplies the base agreement instance that lets Jcost inherit AveragingAgree, SymmUnit, AveragingDerivation, and JensenSketch. These structures feed the small-strain Taylor expansions used by Axiom A4 and align with the J-uniqueness step (T5) of the forcing chain, where J(x) is identified with cosh(log x) - 1. No open scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.