Foundation Jcost Cosh Identity Jcost Exp Nonneg

The nonnegative cost

The declaration jcost_exp_nonneg establishes a simple inequality: for any real number y, the value of the cost function J at the exponential of y is greater than or equal to zero. In plain terms, the cost of a recognition event, a discrete record of a change, is never negative. The proof in the framework's machine-checked library of formal theorems shows this directly from the definition of J, with no additional assumptions. The result is part of a family of statements about the exponential form of the cost function, which is written as J(e^y) = (e^y + e^-y)/2 - 1.

This exponential form is the hyperbolic cosine minus one, a curve that opens upward and touches zero at y = 0. The inequality J(e^y) ≥ 0 is the statement that this curve never dips below the horizontal axis. The same library also proves companion facts: J(e^0) = 0, meaning the cost is zero when the input is 1, and J(e^y) = J(e^-y), meaning the cost is symmetric under replacing y with -y. A stronger version, jcost_exp_pos, shows that the cost is strictly positive whenever y is not zero. Together these statements certify that the cost function has a unique minimum at the point of no change, and that it grows as the input moves away from that point in either direction.

The inequality itself is a consequence of the general definition of J, which for any positive x is J(x) = (x + 1/x)/2 - 1. The proof of jcost_exp_nonneg uses the standard fact that 1 + y ≤ e^y for all real y, applied to both y and -y, and then combines the two inequalities. This is a direct, elementary argument; it does not rely on any special property of the exponential function beyond its basic growth bound. The theorem is part of a certificate structure that packages the cosh form, the zero at zero, the symmetry, and the nonnegativity into a single object, confirming that the exponential form satisfies the expected properties of the cost function.

In the wider framework, this nonnegativity result is a small but load-bearing piece. The cost function J is the unique function satisfying five plain conditions, and this theorem confirms that the exponential form inherits the fundamental property that costs cannot be negative. It does not, however, claim that the exponential form is the only form of J, nor does it say anything about how this form relates to the golden ratio or the forcing chain. The theorem is a local fact about the cost function's behavior on positive reals, not a statement about the origin of the cost function or its role in the broader theory.

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

The theorem does not claim that the exponential form is the only form of J. The theorem does not establish any connection between the cost function and the fine-structure constant. The theorem does not prove that the cost function is derived from the golden ratio.

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: