AveragingBounds
AveragingBounds equips any function F with the symmetric unit axioms plus matching upper and lower inequalities against Jcost when both are evaluated on the exponential scale. Cost analysts in Recognition Science cite it to establish agreement between candidate functions and the J-cost that encodes T5 uniqueness. The declaration is a direct class extension that inherits SymmUnit and adds the two bound fields with no further proof obligations.
claimLet $J(x) = (x + x^{-1})/2 - 1$. A map $F : ℝ → ℝ$ satisfies AveragingBounds if it obeys the symmetric unit conditions ($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 function $J(x) = (x + x^{-1})/2 - 1$ that satisfies the Recognition Composition Law and is fixed by the self-similar point phi. SymmUnit is the class requiring inversion symmetry on the positive reals and vanishing at unity. The present class is introduced in the Cost module to capture those functions that coincide with Jcost after the change of variable $x = e^t$, which is the setting used to compare generating functionals arising in AnchorPolicy and Pipelines.
proof idea
This is a class definition that directly extends SymmUnit with the two field axioms upper and lower. No tactics or lemmas are applied; the structure is assembled by the mkAveragingBounds constructor or by the instance that lifts JensenSketch.
why it matters in Recognition Science
agrees_on_exp_of_bounds invokes the two bounds to obtain equality via antisymmetry, while F_eq_J_on_pos_alt and JensenSketch depend on the same interface. The class therefore supplies the precise link between arbitrary symmetric units and the J-cost that encodes T5 uniqueness, the phi fixed point, and the subsequent eight-tick octave and D = 3 steps in the forcing chain.
scope and limits
- Does not assert existence of any concrete F that meets the bounds.
- Does not constrain the behavior of F for non-positive arguments.
- Does not impose continuity, differentiability, or other regularity conditions.
- Does not derive the mass ladder or alpha-band values by itself.
formal statement (Lean)
57class AveragingBounds (F : ℝ → ℝ) : Prop extends SymmUnit F where
58 upper : ∀ t : ℝ, F (Real.exp t) ≤ Jcost (Real.exp t)
59 lower : ∀ t : ℝ, Jcost (Real.exp t) ≤ F (Real.exp t)
60