AgreesOnExp
plain-language theorem explainer
AgreesOnExp encodes the predicate requiring a real-valued function F to match Jcost exactly on the image of the exponential. Cost derivations in Recognition Science invoke this predicate when establishing agreement before lifting it to positive reals. The declaration is a direct predicate definition with no computational content or lemmas.
Claim. Let $J(x) := (x + x^{-1})/2 - 1$. A map $F : ℝ → ℝ$ satisfies the agreement predicate if $F(e^t) = J(e^t)$ for every real $t$.
background
The Cost module defines Jcost by the formula $J(x) = (x + x^{-1})/2 - 1$, which is the explicit form of the T5 J-uniqueness fixed point. AgreesOnExp is the predicate that F coincides with this Jcost precisely when the argument is exp(t) for arbitrary real t. The same predicate appears verbatim in the JcostCore submodule; the Cost version serves as the interface for downstream averaging classes. Upstream F aliases in AnchorPolicy and Pipelines are distinct gap functions and do not interact with this predicate.
proof idea
The declaration is a direct definition of the Prop. It introduces the universal quantifier over t and equates the two sides using the sibling Jcost definition; no lemmas or tactics are applied.
why it matters
This predicate is the base for extension results such as agree_on_exp_extends and F_eq_J_on_pos, which lift agreement to all positive reals, and for the classes AveragingAgree and AveragingDerivation. It anchors the cost side of T5 J-uniqueness in the unified forcing chain and supplies the interface used by averaging derivations that feed physical models.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.