Foundation Jcost Cosh Identity Jcost Cosh Cert

The cosh identity

The J-cost function, the central object of Recognition Science, measures the cost of a recognition event. It is defined for any positive real number x by the formula J(x) = (x + 1/x)/2 - 1. The declaration JCostCoshCert establishes a key identity: when the input x is written as an exponential, e^y, the cost takes the form J(e^y) = (e^y + e^(-y))/2 - 1. This is the non-linear cosh form of J-cost, a result that appears in the strong-field Regge action.

This identity is not a new assumption; it is a proved theorem in the framework's machine-checked library of formal theorems. The library verifies four properties of this form. First, the cost is zero exactly at y = 0, meaning the cost of recognizing a value equal to itself is zero. Second, the cost is symmetric: J(e^y) = J(e^(-y)), so recognizing a value and its reciprocal carry the same cost. Third, the cost is always non-negative. Fourth, the cost is strictly positive whenever y is not zero, so any non-trivial recognition event carries a positive cost.

The declaration JCostCoshCert packages these four properties into a single structure, and a separate definition provides the certificate, a proof that the structure is inhabited. The certificate is checked with zero "sorry" and zero axioms, meaning it rests entirely on the framework's axioms. This is a formal, machine-verified result, not an empirical observation or a heuristic approximation.

In Recognition Science, this identity is more than a mathematical curiosity. It shows that the cost function, which is forced by five plain conditions, has a natural expression in terms of hyperbolic functions. This connection to the strong-field Regge action suggests a deep link between the framework's foundational cost and the structure of physical actions. The certificate makes this link precise and checkable.

What the declaration does not claim is equally important. It does not claim that the J-cost function is the only cost function satisfying these properties; that uniqueness is a separate theorem. It does not claim that the cosh form is valid for all real numbers x, only for positive x written as exponentials. And it does not claim that the strong-field Regge action is derived from J-cost; the appearance of the same form is noted, not proven.

/-- 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

noncomputable def jCostCoshCert : JCostCoshCert where
  cosh_form := jcost_exp_cosh_form
  zero_at_zero := jcost_exp_zero
  symmetric := jcost_exp_symm
  nonneg := jcost_exp_nonneg
  pos_off_zero := jcost_exp_pos

/-- 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

What this page does not claim

It does not claim that J-cost is the only cost function with these properties. It does not claim the cosh form is valid for all real numbers, only for positive x written as exponentials. It does not claim the strong-field Regge action is derived from J-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/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: