JensenSketch
plain-language theorem explainer
JensenSketch defines a class of real functions F that extend SymmUnit and obey matching upper and lower bounds with Jcost along the exponential axis. Cost theorists and uniqueness proofs in Recognition Science cite this interface to force agreement with the hyperbolic form. The declaration is a direct class definition extending SymmUnit with two axis inequalities that together imply equality on positives.
Claim. Let $J(x) := (x + x^{-1})/2 - 1$. A function $F : ℝ → ℝ$ satisfies JensenSketch if it obeys the SymmUnit axioms ($F(x) = F(x^{-1})$ for $x > 0$ and $F(1) = 0$) together with $F(e^t) ≤ J(e^t)$ and $J(e^t) ≤ F(e^t)$ for every real $t$.
background
Jcost is the explicit map $Jcost(x) = (x + x^{-1})/2 - 1$, the candidate cost function arising from the Recognition Composition Law. SymmUnit is the base class requiring symmetry under inversion for positive arguments and normalization to zero at unity. The present class is declared inside JcostCore to localize the axis bounds used by downstream uniqueness arguments. It depends on the parallel JensenSketch declaration in the parent Cost module and on the F aliases supplied by AnchorPolicy and Pipelines.
proof idea
This is a class definition with an empty proof body. It simply packages the SymmUnit extension together with the two explicit inequalities axis_upper and axis_lower.
why it matters
The class supplies the hypothesis for T5_cost_uniqueness_on_pos, which concludes that any such F equals Jcost on positive reals. It is also referenced by LogModel, aczel_kernel_ode, and H_dAlembert_of_composition. Within the Recognition Science chain it supplies the bounding step that closes the T5 J-uniqueness argument, converting the composition law into the concrete cosh(log x) - 1 form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.