Cost Jlog Jlog Strict Mono On Ici0

The monotonicity result

The declaration Jlog_strictMonoOn_Ici0 is a theorem in the framework's machine-checked library of formal theorems. It states that the log-form cost function Jlog, which measures the price of a recognition event as a function of the ratio between two quantities, is strictly increasing on the nonnegative real numbers. In plain language: as the input value grows from zero upward, the cost output never decreases and never stays flat; it always rises. The result is proved in the file IndisputableMonolith/Cost/Jlog.lean and rests on the classical fact that the hyperbolic cosine function is strictly increasing on that same interval.

The cost function itself is defined as Jlog(t) = (e^t + e^(-t))/2 - 1, which is the hyperbolic cosine minus one. At t = 0 the cost is exactly zero. For any positive t, the cost is positive and grows without bound. The theorem's content is that the mapping from t to cost is one-to-one on the nonnegative reals: no two distinct nonnegative inputs produce the same cost. This monotonicity is a structural property that the framework uses when it derives constants and scaling laws from the cost function's shape.

What the theorem does not claim is just as important. It does not say anything about negative inputs; the statement is explicitly restricted to t ≥ 0. It does not assert that the cost function is linear, bounded, or differentiable, though those properties may hold separately. It does not claim that the cost function is the unique function with this monotonicity property; many functions increase strictly on the nonnegative reals. The theorem only pins down the behavior of this particular cost function on this particular interval.

In the broader Recognition Science account, this monotonicity is one of the plain conditions that the forcing chain relies on. The framework models recognition events as entries in a discrete ledger, and the cost of each event is forced by the five axioms to take the form J(x) = (x + 1/x)/2 - 1. The log-form version Jlog(t) = cosh(t) - 1 is the same cost written in exponential coordinates. The strict increase on the nonnegative side means that moving further from the unity ratio, where cost is zero, always costs more, never less or the same. That monotonic behavior is what lets the framework treat the cost function as a reliable ordering device when it derives the golden ratio and the eight-tick cycle.

The practical consequence for a reader is simple: in the framework's own terms, the cost of a recognition event is a faithful measure of how far the event's ratio departs from one. The theorem guarantees that no two distinct nonnegative ratios share a cost, so the cost function can serve as a clean coordinate for the framework's derivations. This is a small but load-bearing result, and the honest statement of its scope is part of what makes the framework's claims trustworthy.

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

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

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

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 theorem does not say anything about negative inputs. The theorem does not claim the cost function is linear, bounded, or differentiable. The theorem does not assert that Jlog is the only function with this monotonicity property.

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: