Cost Geometric Root Jcost Eq Cosh Log Sub One

The cost identity

The declaration jcost_eq_cosh_log_sub_one proves an exact identity for the cost function J that Recognition Science uses to price a recognition event. For any positive real number x, the theorem states that J(x) equals cosh(log x) minus 1. In plainer terms, the cost of recognizing a change whose scale is x is the hyperbolic cosine of the natural logarithm of x, with one subtracted. The hyperbolic cosine, written cosh, is the average of an exponential and its reciprocal, so the identity says the cost grows like half of x plus half of 1/x, minus 1. A second, equivalent form in the same module writes the cost as (x-1)²/(2x), which makes the symmetry plain: swapping x for 1/x leaves the cost unchanged.

The identity is not a numerical approximation. It is a theorem in a machine-checked library of formal theorems, meaning a computer program verified every step of the proof from the definitions. The library's kernel checks the argument and accepts it as valid, with no hidden assumptions beyond the standard axioms of the ambient type theory. The theorem is tagged THEOREM in the framework's own accounting, the strongest tag available. It derives from a more general functional equation for J, and it holds for every positive real input, not just for a convenient range of values.

What the identity does not claim is just as important. It does not, by itself, say anything about the golden ratio, about the number of spatial dimensions, or about any physical constant. Those results live elsewhere in the framework's library and depend on additional hypotheses. The identity is a single, isolated fact about the cost function's shape. It also does not assert that the cost function is the only possible one; that uniqueness claim is a separate theorem with its own proof. The identity merely states what J is, given the framework's definition of cost.

In Recognition Science, the cost function J is the price of recording a distinction in a ledger, a discrete record of events. The identity's value is that it gives a concrete, computable form to that price. It turns an abstract definition into a formula that can be evaluated, differentiated, and compared against other structures. The fact that the cost is symmetric under inversion, for instance, falls directly out of the formula. That symmetry is a structural property of the cost, not an assumption, and it is the kind of consequence the identity makes visible.

The identity also feeds into a larger argument about refinement. A separate theorem in the same module shows that splitting a fixed distinction into arbitrarily many micro-steps drives the total cost to zero. That result, combined with the identity's exact form, is what forces a ledger to have a minimum tick size. The identity alone does not force the tick; it is the subdivision theorem that does that. But the identity is the foundation on which that theorem rests, because it gives the precise cost of a single micro-step.

/-- In the additive coordinate `x = e^t`, `J = cosh t - 1` exactly.
This is the banked theorem restated through `log`. -/
theorem jcost_eq_cosh_log_sub_one {x : ℝ} (hx : 0 < x) :
    Jcost x = Real.cosh (Real.log x) - 1 := by
  have h := FunctionalEquation.Jcost_G_eq_cosh_sub_one (Real.log x)
  simpa [FunctionalEquation.G, Real.exp_log hx] using h

/-- The chordal form: `J(x) = (x-1)^2/(2x)`. On the upper half-plane this is
`cosh d(i, ix) - 1` with `d` the hyperbolic distance, via
`cosh d(z,w) - 1 = |z-w|^2/(2 Im z Im w)`. The geometric reading is the
docstring; the arithmetic content is this identity. -/
theorem jcost_eq_chordal {x : ℝ} (hx : 0 < x) :
    Jcost x = (x - 1) ^ 2 / (2 * x) := by
  unfold Jcost
  field_simp [hx.ne']
  ring

/-- In the additive coordinate `x = e^t`, `J = cosh t - 1` exactly.
This is the banked theorem restated through `log`. -/
theorem jcost_eq_cosh_log_sub_one {x : ℝ} (hx : 0 < x) :
    Jcost x = Real.cosh (Real.log x) - 1 := by
  have h := FunctionalEquation.Jcost_G_eq_cosh_sub_one (Real.log x)
  simpa [FunctionalEquation.G, Real.exp_log hx] using h

/-- **Subdivision trivializes.** The total cost of `n` equal micro-steps
spanning a fixed distinction of log-size `ε` tends to zero:
`n · J(e^{ε/n}) → 0`. A continuum (infinitely refinable) ledger prices every
finite chain arbitrarily low. -/
theorem jcost_subdivision_trivializes (ε : ℝ) :
    Filter.Tendsto (fun n : ℕ => (n : ℝ) * Jcost (Real.exp (ε / n)))
      Filter.atTop (nhds 0) := by
  have hC : Filter.Tendsto (fun n : ℕ => ε ^ 2 * Real.cosh ε / (2 * (n : ℝ)))
      Filter.atTop (nhds 0) := by
    have h := tendsto_const_div_atTop_nhds_zero_nat (ε ^ 2 * Real.cosh ε / 2)
    exact h.congr (fun n => by rw [div_div])
  exact squeeze_zero (subdivision_cost_nonneg ε) (subdivision_cost_bound ε) hC

What this page does not claim

The identity does not by itself force the golden ratio or any physical constant. The identity does not prove that the cost function is the only possible one. The identity does not establish a minimum tick size without the subdivision 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/GeometricRoot.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: