F_eq_J_on_pos_of_averaging
plain-language theorem explainer
Functions F satisfying the AveragingAgree property coincide with the J-cost function on all positive reals. Researchers modeling cost functions within the Recognition Science framework cite this to equate their generating maps with the explicit J expression. The proof is a one-line wrapper that instantiates F_eq_J_on_pos by projecting the agrees field from the supplied AveragingAgree instance.
Claim. Let $F : ℝ → ℝ$ satisfy the averaging agreement property. Then $F(x) = (x + x^{-1})/2 - 1$ for every $x > 0$.
background
Jcost is the explicit map $Jcost(x) := (x + x^{-1})/2 - 1$. AveragingAgree is the class requiring that F satisfies AgreesOnExp, the agreement condition on exponentials. The Cost module develops cost functions compatible with the Recognition Science forcing chain, and this theorem sits after the core identification result F_eq_J_on_pos, which itself reduces to agree_on_exp_extends.
proof idea
The proof is a one-line wrapper that applies F_eq_J_on_pos, supplying the hAgree argument directly from AveragingAgree.agrees (F:=F).
why it matters
This result closes the identification of any averaging-agreeing F with Jcost on positives, supporting J-uniqueness (T5) in the forcing chain. It enables substitution of the explicit Jcost into the F definitions appearing in AnchorPolicy (gap), Pipelines (log(1 + z/phi)), and TauStepDerivation, without requiring separate proofs for each instance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.