F_eq_J_on_pos
plain-language theorem explainer
Any function F agreeing with Jcost on the image of the exponential extends to equality with Jcost on all positive reals. Researchers deriving cost functions in Recognition Science cite this when lifting exponential agreement to the full positive domain. The proof is a one-line wrapper that applies the extension theorem agree_on_exp_extends.
Claim. Let $F : ℝ → ℝ$ satisfy $F(e^t) = J(x)$ for all real $t$, where $J(x) = (x + x^{-1})/2 - 1$. Then $F(x) = J(x)$ for every $x > 0$.
background
In the Cost module, Jcost is the map $x ↦ (x + x^{-1})/2 - 1$, matching the J-uniqueness expression from the forcing chain. AgreesOnExp is the hypothesis that $F(e^t) = Jcost(e^t)$ holds for every real $t$. The upstream theorem agree_on_exp_extends lifts this pointwise agreement on the exponential image to all positive reals by substituting $x = e^{log x}$ and simplifying with the identity $e^{log x} = x$ for $x > 0$.
proof idea
The proof is a one-line wrapper that invokes agree_on_exp_extends on the supplied agreement hypothesis.
why it matters
This theorem is invoked by F_eq_J_on_pos_of_averaging and F_eq_J_on_pos_of_derivation to obtain equality under averaging and derivation agreement conditions. It supports identification of admissible cost functions with the J-cost in the Recognition Science framework, directly implementing the T5 J-uniqueness step of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.