agree_on_exp_extends
plain-language theorem explainer
Any function F agreeing with Jcost on the image of the exponential must coincide with Jcost on all positive reals. Researchers deriving uniqueness of the cost function in Recognition Science cite this extension step. The proof substitutes x with exp(log x), invokes the agreement hypothesis, and cancels via the identity exp(log x) = x for x > 0.
Claim. If $F : ℝ → ℝ$ satisfies $F(ℝ.exp t) = Jcost(ℝ.exp t)$ for all real $t$, where $Jcost(x) := (x + x^{-1})/2 - 1$, then $F(x) = Jcost(x)$ for all $x > 0$.
background
The Cost module introduces Jcost(x) := (x + x^{-1})/2 - 1, the explicit form of the T5 J-uniqueness expression also written cosh(log x) - 1. AgreesOnExp F is the predicate ∀ t : ℝ, F(Real.exp t) = Jcost(Real.exp t). The local setting develops cost-function properties that feed the forcing chain from T0 through T5. Upstream, the definition of AgreesOnExp supplies the exact hypothesis used here; sibling results such as Jcost_symm and Jcost_nonneg establish basic algebraic properties of the same expression.
proof idea
Term-mode proof: introduce positive x, apply the AgreesOnExp hypothesis at log x to equate F and Jcost at exp(log x), then simplify the argument via Real.exp_log hx to obtain the desired equality at x.
why it matters
The result is invoked directly by F_eq_J_on_pos and thereby by T5_cost_uniqueness_on_pos. It supplies the missing extension from agreement on exponentials to agreement on positive reals, closing the step that realizes T5 J-uniqueness inside the Recognition Science forcing chain (T5 J-uniqueness, T6 phi fixed point). No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.