mkAveragingBounds
plain-language theorem explainer
This definition packages a symmetry proof together with matching upper and lower inequalities against Jcost on the exponential scale into an AveragingBounds instance. Cost-function researchers cite it when they need to register a candidate F that obeys the required averaging relations before invoking Jensen sketches. The construction is a direct record builder that simply assigns the three supplied hypotheses to the class fields.
Claim. Let $F : ℝ → ℝ$. Assume $F$ satisfies $F(x) = F(x^{-1})$ for all $x > 0$ and $F(1) = 0$. Further assume that for every real $t$, $F(e^t) ≤ J(e^t)$ and $J(e^t) ≤ F(e^t)$, where $J(x) = (x + x^{-1})/2 - 1$. Then $F$ obeys the averaging bounds.
background
Jcost is the explicit map $J(x) = (x + x^{-1})/2 - 1$, the unique function satisfying the Recognition Composition Law at the T5 step of the forcing chain. SymmUnit is the class requiring inversion symmetry $F(x) = F(x^{-1})$ for $x > 0$ together with the normalization $F(1) = 0$. AveragingBounds extends SymmUnit by the two inequalities that compare $F(e^t)$ with $J(e^t)$ for all real $t$. The JcostCore module isolates these core algebraic properties before they are used in the parent Cost module or in downstream physics anchors such as the gap function $F(Z) = log(1 + Z/φ)/log(φ)$.
proof idea
One-line wrapper that applies the record constructor for AveragingBounds, directly assigning the supplied symm, upper, and lower fields.
why it matters
The constructor supplies the canonical way to inhabit AveragingBounds, which JensenSketch extends to obtain Jensen-type inequalities in the Cost module. It therefore sits at the interface between the algebraic J-cost properties and any later application to mass ladders or lepton-generation derivations. No open scaffolding questions are closed by this definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.