JensenSketch
JensenSketch equips a symmetric unit function F with matching upper and lower bounds to the J-cost function along the positive exponential axis. Cost-model researchers cite it to derive averaging bounds and proceed to uniqueness results on the positive reals. The declaration supplies a one-line instance that builds AveragingBounds directly from the inherited symmetry and the two axis inequalities.
claimLet $J(x) := (x + x^{-1})/2 - 1$. A function $F : ℝ → ℝ$ satisfies JensenSketch if it obeys the symmetry condition $F(x) = F(x^{-1})$ for $x > 0$, the normalization $F(1) = 0$, and the axis bounds $F(e^t) = J(e^t)$ for all real $t$.
background
Jcost is the function $J(x) = (x + x^{-1})/2 - 1$. SymmUnit requires symmetry under inversion for positive arguments and vanishing at unity. AveragingBounds extends SymmUnit by adding the upper and lower inequalities that F(exp t) brackets Jcost(exp t). The local module Cost develops cost functions that satisfy the Recognition Composition Law and prepare the ground for T5 uniqueness. The lemma Jcost_exp rewrites Jcost on the exponential axis as the hyperbolic cosine expression minus one.
proof idea
The main content is the instance averagingBounds_of_jensen, a one-line wrapper that invokes mkAveragingBounds, passing the SymmUnit instance and the two axis projections. The auxiliary definition of_log_bounds converts logarithmic bounds into the exponential form by applying the simplification lemma Jcost_exp.
why it matters in Recognition Science
JensenSketch supplies the hypothesis for the uniqueness theorem T5_cost_uniqueness_on_pos, which concludes that any such F agrees with Jcost on the positive reals. It is also used in the Aczel classification and LogModel constructions. Within the framework this step closes the gap between the composition law and the explicit J-cost form required by the T5 J-uniqueness landmark.
scope and limits
- Does not establish agreement of F with Jcost away from the exponential axis.
- Does not assume or derive the full Recognition Composition Law.
- Does not address negative arguments or complex extensions.
- Does not provide numerical bounds or convergence rates.
formal statement (Lean)
88class JensenSketch (F : ℝ → ℝ) : Prop extends SymmUnit F where
89 axis_upper : ∀ t : ℝ, F (Real.exp t) ≤ Jcost (Real.exp t)
90 axis_lower : ∀ t : ℝ, Jcost (Real.exp t) ≤ F (Real.exp t)
91
92instance (priority := 95) averagingBounds_of_jensen {F : ℝ → ℝ} [JensenSketch F] :
proof body
Definition body.
93 AveragingBounds F :=
94 mkAveragingBounds F (symm := (inferInstance : SymmUnit F))
95 (upper := JensenSketch.axis_upper (F:=F))
96 (lower := JensenSketch.axis_lower (F:=F))
97
98noncomputable def JensenSketch.of_log_bounds (F : ℝ → ℝ)
99 (symm : SymmUnit F)
100 (upper_log : ∀ t : ℝ, F (Real.exp t) ≤ ((Real.exp t + Real.exp (-t)) / 2 - 1))
101 (lower_log : ∀ t : ℝ, ((Real.exp t + Real.exp (-t)) / 2 - 1) ≤ F (Real.exp t)) :
102 JensenSketch F :=
103{ toSymmUnit := symm
104, axis_upper := by intro t; simpa [Jcost_exp] using upper_log t
105, axis_lower := by intro t; simpa [Jcost_exp] using lower_log t }
106