Foundation Jcost Cosh Identity Jcost Exp Cosh Form

The cosh form of cost

The hyperbolic cosine, written cosh, is the average of an exponential and its reciprocal: cosh(y) = (e^y + e^−y)/2. It is the curve a hanging chain forms, and it appears throughout physics wherever a quantity is symmetric under reversal. The Recognition Science framework's cost function, which measures the price of a recognition event, takes exactly this shape when its input is written as an exponential. The theorem jcost_exp_cosh_form states that for any real number y, the cost J of e^y equals cosh(y) − 1.

This identity is not a new assumption. It follows from the definition of cost and the algebraic properties of the exponential function, and the proof is checked by a machine-checked library of formal theorems. The statement is one line: J(e^y) = (e^y + e^−y)/2 − 1. From this single form, four properties become visible. At y = 0, the cost is zero. The cost is symmetric: J(e^y) equals J(e^−y), so reversing the input changes nothing. The cost is never negative. And for any nonzero y, the cost is strictly positive. These are the properties that make cost a sensible measure of departure from the unit value.

In Recognition Science, the cost function is the object whose uniqueness is forced by five plain conditions, and this cosh form is the explicit expression that appears in the strong-field Regge action. The identity connects the abstract forcing theorem to a concrete analytic formula. It shows that the cost of a recognition event grows smoothly and symmetrically as the input moves away from 1, the point of zero cost. The form also makes the positivity proof transparent: since cosh(y) is always at least 1, subtracting 1 leaves a nonnegative remainder.

The theorem does not claim that the cost function was derived from the cosh form, nor that the cosh form explains why the cost function exists. It is a rewriting, not a new physical law. The identity also does not assert anything about the magnitude of the cost for any particular physical system; it is a statement about the function's shape. What the theorem establishes is that the cost function, already fixed by the forcing conditions, has a clean analytic presentation that makes its symmetry and positivity immediate.

/-- J(eʸ) = (eʸ + e⁻ʸ)/2 - 1. -/
theorem jcost_exp_cosh_form (y : ℝ) :
    Jcost (Real.exp y) = (Real.exp y + Real.exp (-y)) / 2 - 1 := by
  rw [Jcost_eq_sq (Real.exp_ne_zero y)]
  rw [Real.exp_neg]
  field_simp [Real.exp_ne_zero y]
  ring

/-- J(e⁰) = 0. -/
theorem jcost_exp_zero : Jcost (Real.exp 0) = 0 := by
  rw [jcost_exp_cosh_form]; simp

/-- J(eʸ) = J(e⁻ʸ). -/
theorem jcost_exp_symm (y : ℝ) :
    Jcost (Real.exp y) = Jcost (Real.exp (-y)) := by
  rw [jcost_exp_cosh_form, jcost_exp_cosh_form]
  rw [neg_neg]; ring

/-- J(eʸ) ≥ 0. -/
theorem jcost_exp_nonneg (y : ℝ) : 0 ≤ Jcost (Real.exp y) := by
  rw [jcost_exp_cosh_form]
  have := Real.add_one_le_exp y
  have := Real.add_one_le_exp (-y)
  nlinarith [Real.exp_pos y, Real.exp_pos (-y)]

/-- J(eʸ) > 0 for y ≠ 0. -/
theorem jcost_exp_pos {y : ℝ} (hy : y ≠ 0) : 0 < Jcost (Real.exp y) := by
  have hexp_ne_one : Real.exp y ≠ 1 := by
    intro h; exact hy (by rwa [Real.exp_eq_one_iff] at h)
  exact Jcost_pos_of_ne_one _ (Real.exp_pos y) hexp_ne_one

/-- J(eʸ) = (eʸ + e⁻ʸ)/2 - 1. -/
theorem jcost_exp_cosh_form (y : ℝ) :
    Jcost (Real.exp y) = (Real.exp y + Real.exp (-y)) / 2 - 1 := by
  rw [Jcost_eq_sq (Real.exp_ne_zero y)]
  rw [Real.exp_neg]
  field_simp [Real.exp_ne_zero y]
  ring

What this page does not claim

The cosh identity does not derive the cost function from scratch; it rewrites an already-defined function. The theorem does not assign a numerical value to the cost for any physical system. The identity does not imply that the cost function is the only function with these properties.

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/Foundation/JCostCoshIdentity.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: