Cost Agrees On Exp Of Bounds

Agreement on a line

The declaration agrees_on_exp_of_bounds concerns a bridge between a narrow check and a full identity. The check runs along the exponential curve, the set of numbers of the form e^t for real t. The identity is the recognition cost function J(x) = (x + 1/x)/2 − 1, the framework's measure of how costly it is to recognize a ratio x. The declaration proves that if a function F agrees with J on every point of that exponential curve, then F equals J everywhere on the positive real line. The exponential curve is a one-dimensional slice; the conclusion covers the entire positive half-line.

The proof rests on two facts. First, J itself, when fed an exponential input, becomes the hyperbolic cosine minus one: J(e^t) = cosh(t) − 1. This identity is proved in the machine-checked library as Jcost_exp_cosh. Second, the hyperbolic cosine is even, so the exponential curve covers each positive number twice, once through t and once through −t. The agreement on the curve therefore pins down J at every positive real number. The declaration's name reflects this: agreement on the exponential curve, extended by bounds, yields the full identity.

What the declaration does not claim is that agreement on any curve suffices. The exponential curve is special because it is the image of a group homomorphism from the additive reals to the multiplicative positive reals. A generic curve, say the parabola y = x², carries no such structure, and agreement there would not force the identity. The declaration also does not claim that the recognition cost function is the only function with this extension property; it claims only that J has it, and that any function agreeing with J on the curve must be J itself.

In the framework's own account, this declaration is a lemma in the proof that the cost function is unique. The uniqueness theorem, T5_cost_uniqueness_on_pos, uses this extension to show that any function satisfying the framework's five axioms must equal J everywhere. The declaration is therefore a bridge: it turns a check along one line into a statement about all positive ratios. A reader who wants to see the bridge in action can look at the proof of T5, where the extension is the decisive step.

def AgreesOnExp (F : ℝ → ℝ) : Prop := ∀ t : ℝ, F (Real.exp t) = Jcost (Real.exp t)

/-- J in terms of cosh: J(exp(t)) = cosh(t) - 1 -/
lemma Jcost_exp_cosh (t : ℝ) : Jcost (Real.exp t) = Real.cosh t - 1 :=
  Jlog_as_cosh t

theorem T5_cost_uniqueness_on_pos {F : ℝ → ℝ} [JensenSketch F] :
  ∀ {x : ℝ}, 0 < x → F x = Jcost x :=
by
  intro x hx
  have hAgree : AgreesOnExp F := by
    intro t
    exact le_antisymm (JensenSketch.axis_upper (F:=F) t) (JensenSketch.axis_lower (F:=F) t)
  exact (agree_on_exp_extends (F:=F) hAgree) hx

What this page does not claim

Agreement on any curve, such as a parabola, forces the identity. The recognition cost function is the only function with this extension property. The declaration itself proves the uniqueness of the cost function; it is a lemma toward that theorem.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cost.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: