AveragingBounds
plain-language theorem explainer
AveragingBounds is a class property on a real function F that extends symmetry under inversion and normalization at unity with the requirement that F and the J-cost function bound each other when evaluated on the positive reals via the exponential map. Cost theorists and Recognition Science researchers would cite this class to certify agreement between candidate functions and the canonical J-cost. The declaration is a direct class extension with no separate proof body.
Claim. Let $J(x) = (x + x^{-1})/2 - 1$. A function $F : ℝ → ℝ$ satisfies AveragingBounds if it obeys $F(x) = F(x^{-1})$ for all $x > 0$, $F(1) = 0$, and for every real $t$, $F(e^t) ≤ J(e^t) ≤ F(e^t)$.
background
The Jcost function is defined as Jcost(x) := (x + x^{-1})/2 - 1, which coincides with cosh(log x) - 1 and serves as the canonical cost measure. SymmUnit is the class requiring that F is invariant under taking reciprocals for positive arguments and vanishes at 1. This AveragingBounds class is declared in the JcostCore submodule of the Cost module, which focuses on properties of cost functions that average symmetrically. It builds on the basic SymmUnit class by adding the bounding conditions on the logarithmic scale.
proof idea
This is a class definition that directly extends the SymmUnit class by adjoining the two inequalities upper and lower. No tactics or lemmas are applied; it is the structural definition of the property.
why it matters
This declaration provides the interface for functions that agree with Jcost on the positive reals, which is used in downstream results such as agrees_on_exp_of_bounds to derive equality via antisymmetry of the bounds, and in F_eq_J_on_pos_alt to extend the agreement to all positive x. It supports the JensenSketch class and the construction mkAveragingBounds. In the broader framework, it anchors the uniqueness of the J-cost (T5) by providing a bounding property that forces agreement with the self-similar fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.