Explanation of Jcost_G_eq_cosh_sub_one

(1) What the declaration says in plain English

The theorem states that the J-cost function, re-expressed through the auxiliary reparametrization G, matches the expression cosh(t) − 1. In standard mathematical notation, if J(x) = (x + x⁻¹)/2 − 1 for x > 0, then G(J, t) ≔ J(eᵗ) equals cosh(t) − 1 exactly.

(2) Why it matters in Recognition Science

Recognition Science derives the unique reciprocal-symmetric cost J(x) = (x + x⁻¹)/2 − 1 from the Law of Logic (T5). This identity converts J into hyperbolic-cosine form in logarithmic coordinates, which satisfies the CoshAddIdentity and enables subsequent steps in the uniqueness argument for the cost function.

(3) How to read the formal statement

The Lean declaration is:

theorem Jcost_G_eq_cosh_sub_one (t : ℝ) : G Cost.Jcost t = Real.cosh t - 1

• (t : ℝ) introduces a real parameter.
• G Cost.Jcost t applies the definition G F t := F (Real.exp t) to the Jcost function.
• The right-hand side is the standard hyperbolic cosine minus one. The proof proceeds by unfolding the definitions of G and Jcost, rewriting the reciprocal exponential, and invoking the built-in identity Real.cosh_eq.

(4) Visible dependencies or certificates in the supplied source

The theorem lives in module IndisputableMonolith.Cost.FunctionalEquation. It directly uses the local definition

@[simp] noncomputable def G (F : ℝ → ℝ) (t : ℝ) : ℝ := F (Real.exp t)

and the imported Jcost. The short proof relies on simp only [G, Jcost] followed by rw [h1, Real.cosh_eq]. A closely related declaration in the same module is Jcost_cosh_add_identity, which establishes the corresponding addition identity CoshAddIdentity Cost.Jcost.

(5) What this declaration does not prove

The theorem only equates the two concrete expressions for the reparametrized cost. It does not establish uniqueness of Jcost among all reciprocal-symmetric functions, does not derive the forcing chain from the Law of Logic, and does not connect the cost to the golden-ratio constant φ or to any physical predictions. Those results lie outside the supplied module slice.