F_eq_J_on_pos
Any real-valued function F that agrees with the J-cost on the image of the exponential must equal the J-cost at every positive real. Researchers extending cost functions from exponential domains in Recognition Science cite this when deriving full-domain equalities. The proof is a one-line wrapper that invokes the extension theorem agree_on_exp_extends.
claimLet $F : ℝ → ℝ$ satisfy $F(e^t) = J(e^t)$ for all real $t$, where $J(y) = (y + y^{-1})/2 - 1$. Then $F(x) = J(x)$ for every $x > 0$.
background
The J-cost is the function $J(y) = (y + y^{-1})/2 - 1$, identical to cosh(log y) - 1 in the Recognition Science forcing chain. The predicate AgreesOnExp F requires that F(exp t) equals J(exp t) for every real t. This sits inside the Cost module, which develops cost functions compatible with the Recognition Composition Law.
proof idea
The proof is a one-line wrapper that applies the upstream theorem agree_on_exp_extends to the supplied agreement hypothesis, substituting x = exp(log x) and simplifying via exp_log.
why it matters in Recognition Science
This supplies the common extension step used by the downstream theorems F_eq_J_on_pos_of_averaging and F_eq_J_on_pos_of_derivation. It closes the passage from exponential agreement to the full positive domain, supporting the J-uniqueness step T5 in the forcing chain. The parent results apply it under averaging and symmetry-unit hypotheses.
scope and limits
- Does not establish equality for non-positive x.
- Does not construct any concrete F beyond the agreement hypothesis.
- Does not address complex-valued or vector-valued extensions.
- Does not prove uniqueness of F without the agreement condition.
Lean usage
example {F : ℝ → ℝ} (hAgree : AgreesOnExp F) : ∀ {x : ℝ}, 0 < x → F x = Jcost x := F_eq_J_on_pos hAgreeformal statement (Lean)
148theorem F_eq_J_on_pos {F : ℝ → ℝ}
149 (hAgree : AgreesOnExp F) :
150 ∀ {x : ℝ}, 0 < x → F x = Jcost x :=
proof body
One-line wrapper that applies agree_on_exp_extends.
151 agree_on_exp_extends (F:=F) hAgree
152