Cost Calibration Jlog Eq Cosh

The calibration identity

The declaration Jlog_eq_cosh establishes a clean identity: in log-coordinates, the recognition cost function Jlog equals cosh t minus 1. The hyperbolic cosine, familiar from the shape of a hanging chain, describes how the cost grows as the ratio of two compared quantities moves away from 1. The identity says that in these coordinates the cost is exactly cosh t - 1, no more and no less.

From this identity the framework derives a calibration fact: the second derivative of Jlog at zero equals 1. The second derivative measures curvature, so this says the cost function has unit curvature at the identity point where the two quantities are equal. This unit curvature is not an accident; it is the calibration axiom that fixes the scale of the cost uniquely. The framework's library proves this as a theorem, with the derivative calculations carried through step by step.

The identity also connects two ways of writing the cost. In ordinary coordinates the cost is written Jcost; in log-coordinates it becomes Jlog. The declaration Jcost_comp_exp_eq_Jlog shows these are the same function: evaluating Jcost at exp t gives exactly Jlog t. This bridge matters because it lets the framework move between the two coordinate systems freely, carrying the calibration fact along.

What the declaration does not claim is just as important. It does not say that the cost function is the only one satisfying the five conditions; that uniqueness is a separate theorem proved elsewhere. It does not claim anything about the value of the cost at any particular point, only its curvature at the identity. And it does not assert that the unit curvature is physically meaningful; it is a definitional choice within the framework, a calibration that sets the scale.

/-- Jlog equals cosh t - 1 -/
lemma Jlog_eq_cosh (t : ℝ) : Jlog t = Real.cosh t - 1 := Jlog_as_cosh t

/-- The calibration theorem: second derivative at zero equals 1 -/
theorem Jlog_second_deriv_at_zero : deriv (deriv Jlog) 0 = 1 := by
  rw [deriv2_Jlog]
  exact cosh_zero

/-- Identity: (Jcost ∘ exp) equals Jlog pointwise. -/
lemma Jcost_comp_exp_eq_Jlog : (fun t : ℝ => Jcost (Real.exp t)) = Jlog := rfl

What this page does not claim

The declaration does not prove that J is the unique cost function satisfying the five conditions. The declaration does not assign a physical meaning to the unit curvature; it is a definitional calibration. The declaration does not state the value of the cost at any point other than its curvature at the identity.

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/Calibration.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: