AveragingBounds
plain-language theorem explainer
AveragingBounds packages the requirement that a map F from reals to reals extends the symmetric-unit axioms and matches the J-cost function from both sides when restricted to the positive reals via the exponential map. Workers on cost-function uniqueness in Recognition Science cite it when they need to pass from bounding inequalities to pointwise agreement on positives. The declaration is a direct class definition extending SymmUnit with the two inequalities and carries no separate proof obligations.
Claim. A function $F : ℝ → ℝ$ satisfies AveragingBounds when it obeys the symmetric-unit conditions $F(x) = F(x^{-1})$ for all $x > 0$ and $F(1) = 0$, together with the two inequalities $F(e^t) ≤ J(e^t)$ and $J(e^t) ≤ F(e^t)$ for every real $t$, where $J(x) := (x + x^{-1})/2 - 1$.
background
Jcost is the explicit map $J(x) := (x + x^{-1})/2 - 1$, which is the unique function satisfying the Recognition Composition Law and the J-uniqueness fixed-point condition from the T0–T8 forcing chain. SymmUnit is the auxiliary class requiring inversion symmetry on positives and vanishing at unity. The present declaration sits inside the Cost module that develops the interface between arbitrary cost maps and this canonical J-cost; it is duplicated in the JcostCore sub-module and is referenced by the AnchorPolicy and Pipelines modules that supply concrete generating functionals.
proof idea
The declaration is a class definition that directly extends SymmUnit F and adjoins the two bounding inequalities on the exponential axis. No lemmas are invoked and no tactics are executed; it functions as a pure packaging of hypotheses for later use in agreement theorems.
why it matters
AveragingBounds supplies the hypothesis interface consumed by agrees_on_exp_of_bounds (which extracts equality on the exponential image) and by F_eq_J_on_pos_alt (which lifts the equality to all positive reals). It also underwrites the JensenSketch alternative axiomatization and the mkAveragingBounds constructor. In the broader framework it closes the step that forces cost functions to coincide with the J-uniqueness expression (T5), thereby supporting the phi-ladder mass formulas and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.