JensenSketch
plain-language theorem explainer
JensenSketch packages symmetry, normalization at unity, and matching bounds on the exponential axis for a real function to coincide with the J-cost. Researchers proving uniqueness of cost functions cite it to obtain the averaging bounds needed for T5. The structure is a class extension of the symmetric unit property together with an instance that feeds mkAveragingBounds and a constructor that reduces log-scale inequalities via the exponential identity.
Claim. Let $J(x) = (x + x^{-1})/2 - 1$. A function $F : ℝ → ℝ$ satisfies the JensenSketch property when it is a symmetric unit ($F(x) = F(x^{-1})$ for $x > 0$ and $F(1) = 0$) and satisfies the axis bounds $F(e^t) ≤ J(e^t)$ and $J(e^t) ≤ F(e^t)$ for all real $t$.
background
In the Cost module Jcost is defined by the explicit formula $J(x) = (x + x^{-1})/2 - 1$. SymmUnit requires inversion symmetry on positive reals together with vanishing at unity. AveragingBounds extends SymmUnit by the same upper and lower estimates on the exponential axis. JensenSketch repackages those estimates as axis_upper and axis_lower to simplify instance creation. The upstream Jcost_exp lemma states that Jcost applied to exp t recovers the hyperbolic form ((exp t + exp(-t))/2 - 1), which is invoked by the of_log_bounds constructor.
proof idea
The declaration defines the class by extending SymmUnit with the two axis inequalities. The instance averagingBounds_of_jensen constructs an AveragingBounds record by calling mkAveragingBounds on the inherited symmetry and the axis bounds. The auxiliary definition of_log_bounds accepts symmetry plus log-scale inequalities and converts them to axis form by simplification with Jcost_exp.
why it matters
JensenSketch supplies the hypothesis for T5_cost_uniqueness_on_pos, which concludes that any such F agrees with Jcost on positive reals. It also supports the AczelClassification steps that recover the d'Alembert equation from the composition law. In the Recognition Science framework the class encodes the J-uniqueness step (T5) on the positive domain, linking to the forcing chain and the recognition composition law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.