Cost Classical Results Real Cosh Exponential Expansion

The hyperbolic cosine identity

The hyperbolic cosine, written cosh, is a standard function of real analysis. For a real number t, its value is the average of the exponential function at t and at its negative: cosh(t) = (e^t + e^(-t)) / 2. This is not an approximation or a special case; it is the definition of cosh, equivalent to the geometric picture of a hanging cable or catenary. The identity holds for every real number t, from large positive values where e^t dominates to large negative values where e^(-t) takes over.

The recognition framework, a system that derives physical structure from the cost of recognition events, maintains a machine-checked library of formal theorems. Within that library, the declaration real_cosh_exponential_expansion records the identity as a proved theorem. It states that for any real t, the expression (e^t + e^(-t)) / 2 equals cosh(t). The proof is immediate from the standard definition of cosh in the library's underlying mathematics; the declaration exists so that later work can use the identity without re-deriving it each time.

This theorem is a piece of classical mathematics, not a new physical claim. It does not assert anything about recognition, cost, or the framework's forcing chain. It does not say that cosh is the cost function J(x) = (x + 1/x)/2 - 1, nor that any physical quantity must equal cosh. The declaration is a convenience: a standard fact, formally recorded, that other proofs in the library can cite.

What the theorem does establish is a bridge between two notations. Any expression involving exponentials of the form (e^t + e^(-t))/2 can be rewritten as cosh(t), and vice versa. This matters because the framework's derivations often produce such exponential combinations; the identity lets those results be stated in the more compact and familiar cosh form. The practical effect is that a reader of the framework's proofs can expect standard notation, not a proliferation of exponential pairs.

theorem real_cosh_exponential_expansion (t : ℝ) :
    ((Real.exp t + Real.exp (-t)) / 2) = Real.cosh t := by
  simpa using (Real.cosh_eq t).symm

theorem real_cosh_exponential_expansion (t : ℝ) :
    ((Real.exp t + Real.exp (-t)) / 2) = Real.cosh t := by
  simpa using (Real.cosh_eq t).symm

What this page does not claim

The theorem does not assert that cosh is the framework's cost function J(x) = (x + 1/x)/2 - 1. The theorem makes no physical claim about recognition, cost, or the forcing chain. The identity is classical mathematics, not a new result derived by 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/Cost/ClassicalResults.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: