Cost Jlog

The log-form cost

In mathematics, a hyperbolic cosine, written cosh(t), describes the shape of a hanging chain or catenary: it is the average of the exponential function and its reciprocal, (e^t + e^(-t))/2. The cost function called jlog in Recognition Science is exactly that curve shifted down by one: jlog(t) = cosh(t) - 1. Equivalently, jlog(t) = (e^t + e^(-t))/2 - 1. At t = 0 the cost is zero; as t moves away from zero in either direction, the cost rises symmetrically and without bound.

The function gets its name from the logarithm. Recognition Science measures the cost of a recognition event on a logarithmic scale, so the underlying ratio x becomes t = ln(x). On that scale, the general cost formula J(x) = (x + 1/x)/2 - 1 turns into the exponential spelling above. The two forms are the same function seen in different coordinates: one in the original ratio, one in its logarithm. The log form is the one that makes the symmetry of the cost visible, since replacing t with -t leaves jlog unchanged.

In Recognition Science, the cost is the forced price of a recognition event, the amount a ledger must pay to register a change. The framework proves that any cost function satisfying five plain conditions must equal J(x) = (x + 1/x)/2 - 1. The jlog module supplies the working details of that function in its logarithmic form. It proves three facts. First, the exponential spelling is a theorem, not a separate definition: jlog(t) really is (e^t + e^(-t))/2 - 1. Second, the cost is strictly positive away from zero: jlog(t) > 0 exactly when t ≠ 0. Third, on the nonnegative numbers the cost is strictly increasing: if 0 ≤ a < b, then jlog(a) < jlog(b).

These three facts give the cost function its practical shape. The positivity result says that any nonzero recognition event carries a positive price, and the monotonicity result says that larger logarithmic deviations cost more. Together they mean the cost has a single minimum at zero and rises smoothly on both sides. That behavior is what lets the framework treat recognition as a forced expense: there is no free event, and the further an event strays from the identity ratio, the steeper the price.

The module also records a repair. An earlier version of the library tried to redefine jlog with the exponential formula while the main cost file already defined it with the ratio formula. Lean refused the duplicate name outright, and the correction, dated 2026-07-27, kept only one definition and promoted the exponential spelling to a theorem. The lesson is a practical one about how the library is built: each fact lives in exactly one place, and a theorem derived from the definition is preferred over a second definition of the same object.

/-- The exponential spelling of `Jlog`, which used to be a second definition of it. -/
@[simp] lemma Jlog_as_exp (t : ℝ) :
    Jlog t = ((Real.exp t + Real.exp (-t)) / 2) - 1 := by
  rw [Jlog_as_cosh, Real.cosh_eq]

@[simp] lemma Jlog_eq_cosh_sub_one (t : ℝ) : Jlog t = Real.cosh t - 1 := Jlog_as_cosh t

@[simp] lemma Jlog_pos_iff (t : ℝ) : 0 < Jlog t ↔ t ≠ 0 := by
  rw [Jlog_as_cosh]
  constructor
  · intro ht
    have : (1 : ℝ) < Real.cosh t := (sub_pos).1 ht
    exact (Real.one_lt_cosh (x := t)).1 this
  · intro hne
    have : (1 : ℝ) < Real.cosh t := (Real.one_lt_cosh (x := t)).2 hne
    exact (sub_pos).2 this

theorem Jlog_strictMonoOn_Ici0 : StrictMonoOn Jlog (Set.Ici (0 : ℝ)) := by
  intro x hx y hy hxy
  have hcosh : Real.cosh x < Real.cosh y :=
    Real.cosh_strictMonoOn hx hy hxy
  rw [Jlog_as_cosh, Jlog_as_cosh]
  exact sub_lt_sub_right hcosh 1

What this page does not claim

The module does not prove that jlog is the only possible cost function; that uniqueness belongs to the general cost theorem in Cost.lean. The module does not derive any physical constants or particle masses; it only establishes analytic properties of the log-form cost.

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