mkAveragingBounds
plain-language theorem explainer
This definition constructs an AveragingBounds instance for a real function F by packaging its symmetry and normalization properties together with explicit upper and lower bounds against the J-cost function. Researchers developing cost-function properties in the Recognition Science framework cite it when they need to instantiate the averaging condition for a concrete F. The construction is a direct structure assembly from the supplied hypotheses.
Claim. Let $F : ℝ → ℝ$. Assume $F$ satisfies symmetry $F(x) = F(x^{-1})$ for all $x > 0$ and normalization $F(1) = 0$. Assume further that $F(e^t) ≤ J(e^t)$ and $J(e^t) ≤ F(e^t)$ for all real $t$, where $J(x) := (x + x^{-1})/2 - 1$. Then $F$ satisfies the averaging bounds property.
background
The J-cost function is defined by $J(x) = (x + x^{-1})/2 - 1$, equivalently $cosh(log x) - 1$. SymmUnit requires a function to be invariant under $x ↦ x^{-1}$ for positive arguments and to vanish at unity. AveragingBounds extends SymmUnit by the two inequalities on the exponential scale; these inequalities are in fact equalities, forcing $F(e^t) = J(e^t)$ for every real $t$.
proof idea
The definition is a one-line wrapper that applies the structure constructor for AveragingBounds, supplying the symmetry proof to the toSymmUnit field and inserting the upper and lower bounds directly into the corresponding fields.
why it matters
The constructor feeds the JensenSketch class in the same module, which supplies an alternative axiomatization via axis bounds and derives an instance of AveragingBounds from it. It supports cost-function development that connects to J-uniqueness (T5) in the forcing chain and to the Recognition Composition Law. The definition closes a local scaffolding step by giving an explicit packaging of the bounds without further obligations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.