Foundation Jcost Cosh Identity Jcost Exp Zero

The zero point of cost

The function J(x) = (x + 1/x)/2 - 1 measures the cost of a recognition event in the Recognition Science framework. A recognition event is a discrete record of a comparison between two quantities, and the cost is the forced price of making that comparison. The function has a unique zero: J(1) = 0. In plain terms, when the two quantities being compared are exactly equal, the cost of recognizing that equality is zero. This is the fixed point of the cost function, the one input where recognition is free.

The declaration jcost_exp_zero establishes this fact in a specific form. It states that J(e⁰) = 0, where e⁰ = 1. The proof is a direct consequence of the more general identity J(eʸ) = (eʸ + e⁻ʸ)/2 - 1, which rewrites the cost function using the exponential function. This identity is the hyperbolic cosine form of J-cost, and it appears in the strong-field Regge action within the framework. The theorem jcost_exp_zero is machine-checked in the framework's library of formal theorems, with no unproved assumptions.

The zero point is not just a numerical curiosity. It anchors the entire cost function. Because J is strictly positive for every input other than 1, the zero at 1 is the unique minimum. This means that in the framework, perfect agreement between compared quantities carries no cost, while any disagreement carries a positive cost. The symmetry J(eʸ) = J(e⁻ʸ) also follows from the cosh form, showing that the cost of recognizing a ratio y is the same as recognizing its reciprocal 1/y.

What the declaration does not claim is equally important. It does not say that recognition is always free, only that the cost is zero at the specific point where the input is 1. It does not claim that the cost function is derived from the exponential form; rather, the exponential form is a consequence of the more fundamental definition J(x) = (x + 1/x)/2 - 1. The theorem jcost_exp_zero is a lemma about a specific value, not a derivation of the cost function itself. The full derivation of J from five plain conditions is a separate, larger theorem in the framework.

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

/-- 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 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ʸ) = 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

What this page does not claim

The theorem does not claim that recognition is always free; it only establishes the zero at the specific input e⁰ = 1. The theorem does not derive the cost function itself; it is a consequence of the more fundamental definition J(x) = (x + 1/x)/2 - 1. The theorem does not establish the uniqueness of the cost function; that is a separate theorem in the framework.

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: