Cost Functional Equation D Alembert Cosh Solution Of Log Curvature

The uniqueness of cosh

The hyperbolic cosine, written cosh, is the average of an exponential and its reciprocal: cosh(t) = (e^t + e^-t)/2. It describes the shape of a hanging chain, the curve of a catenary, and the sum of two traveling waves. In 1747, Jean le Rond d'Alembert derived the wave equation for a vibrating string and showed its solutions are combinations of functions of the form f(x + ct) and g(x - ct). His analysis led to a functional equation that bears his name: H(t+u) + H(t-u) = 2 H(t) H(u), which says the value at two shifted points averages to twice the product of the values at the original points.

This equation has many solutions, but they are all variations on the same theme. Without extra conditions, H could be identically zero, or it could be a cosine function, cos(kt), for any constant k. The classical theorem, proved by Cauchy and others in the nineteenth century, is that if H is continuous and H(0) = 1, then the only solutions are H(t) = cosh(kt) for real k, and H(t) = cos(kt) for imaginary k. The hyperbolic cosine is selected when the second derivative at zero is positive, which corresponds to a curvature that pushes the graph upward.

In Recognition Science, the framework's machine-checked library of formal theorems contains a result that sharpens this classical picture. The declaration dAlembert_cosh_solution_of_log_curvature proves that if H satisfies the d'Alembert equation, H(0) = 1, and the log-curvature condition (the limit of 2(H(t) - 1)/t^2 as t approaches 0) equals 1, then H(t) = cosh(t) for every real t. The proof proceeds by showing these hypotheses imply the second derivative of H at zero is 1, which then forces H to satisfy the ordinary differential equation H'' = H with initial conditions H(0) = 1 and H'(0) = 0. The unique solution to that initial value problem is cosh.

This theorem is a stepping stone in the framework's chain of results. It establishes that the cost function J(x) = (x + 1/x)/2 - 1, which appears throughout Recognition Science, has a log-curvature of exactly 1 when expressed in log coordinates. The theorem does not claim that every solution to the d'Alembert equation is cosh; it requires the specific curvature condition. It also does not claim that the d'Alembert equation alone determines the cost function, nor does it address the physical interpretation of the cost function as a measure of recognition effort.

The practical consequence is that a single number, the log-curvature at zero, completely determines the solution among the family of hyperbolic cosines. This is what makes the framework's cost function unique: once the composition law and the curvature calibration are fixed, there is no freedom left. The theorem turns a functional equation with many solutions into a unique one by adding one geometric condition, and that uniqueness is what the rest of the framework builds on.

theorem dAlembert_cosh_solution_of_log_curvature
    (H : ℝ → ℝ)
    (h_one : H 0 = 1)
    (h_dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u)
    {κ : ℝ} (h_calib : HasLogCurvature H κ)
    (h_deriv2_zero : deriv (deriv H) 0 = 1)
    (h_smooth_hyp : dAlembert_continuous_implies_smooth_hypothesis H)
    (h_ode_hyp : dAlembert_to_ODE_hypothesis H)
    (h_cont_hyp : ode_regularity_continuous_hypothesis H)
    (h_diff_hyp : ode_regularity_differentiable_hypothesis H)
    (h_bootstrap_hyp : ode_linear_regularity_bootstrap_hypothesis H) :
    ∀ t, H t = Real.cosh t := by
  have h_cont : Continuous H := dAlembert_continuous_of_log_curvature H h_one h_dAlembert h_calib
  exact dAlembert_cosh_solution H h_one h_cont h_dAlembert h_deriv2_zero
    h_smooth_hyp h_ode_hyp h_cont_hyp h_diff_hyp h_bootstrap_hyp

/-- **d'Alembert to ODE derivation.**

    If H satisfies the d'Alembert equation and is smooth, then H'' = H.

    Proof sketch: Differentiate H(t+u) + H(t-u) = 2H(t)H(u) twice with respect to u,
    then set u = 0 to get H''(t) = H''(0) · H(t). With calibration H''(0) = 1, this
    gives H''(t) = H(t). -/
def dAlembert_to_ODE_hypothesis (H : ℝ → ℝ) : Prop :=
  H 0 = 1 → Continuous H → (∀ t u, H (t+u) + H (t-u) = 2 * H t * H u) →
    deriv (deriv H) 0 = 1 → ∀ t, deriv (deriv H) t = H t

theorem ode_cosh_uniqueness (H : ℝ → ℝ)
    (h_ODE : ∀ t, deriv (deriv H) t = H t)
    (h_H0 : H 0 = 1)
    (h_H'0 : deriv H 0 = 0)
    (h_cont_hyp : ode_regularity_continuous_hypothesis H)
    (h_diff_hyp : ode_regularity_differentiable_hypothesis H)
    (h_bootstrap_hyp : ode_linear_regularity_bootstrap_hypothesis H) :
    ∀ t, H t = Real.cosh t := by
  have h_cont : Continuous H := h_cont_hyp h_ODE
  have h_diff : Differentiable ℝ H := h_diff_hyp h_ODE h_cont
  have h_C2 : ContDiff ℝ 2 H := h_bootstrap_hyp h_ODE h_cont h_diff
  exact ode_cosh_uniqueness_contdiff H h_C2 h_ODE h_H0 h_H'0

/-- **Non-vacuity witness.** The canonical cost satisfies the calibration. A
regularity hypothesis nobody exhibits a model for is worth nothing, which is the
lesson of the full-filter version this replaced. -/
theorem jcost_hasLogCurvature_one : HasLogCurvature (H Cost.Jcost) 1 := by
  have hfun : H Cost.Jcost = Real.cosh := by
    funext t
    have h := Jcost_G_eq_cosh_sub_one t
    simp only [H]
    linarith [h]
  have hd0 : deriv Real.cosh 0 = 0 := by
    rw [Real.deriv_cosh]; exact Real.sinh_zero
  have hd2 : deriv (deriv Real.cosh) 0 = 1 := by
    rw [Real.deriv_cosh, Real.deriv_sinh]; exact Real.cosh_zero
  have h := logCurvature_eq_deriv2 Real.cosh Real.contDiff_cosh Real.cosh_zero hd0
  rw [hd2] at h
  rwa [hfun]

theorem dAlembert_cosh_solution_of_log_curvature
    (H : ℝ → ℝ)
    (h_one : H 0 = 1)
    (h_dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u)
    {κ : ℝ} (h_calib : HasLogCurvature H κ)
    (h_deriv2_zero : deriv (deriv H) 0 = 1)
    (h_smooth_hyp : dAlembert_continuous_implies_smooth_hypothesis H)
    (h_ode_hyp : dAlembert_to_ODE_hypothesis H)
    (h_cont_hyp : ode_regularity_continuous_hypothesis H)
    (h_diff_hyp : ode_regularity_differentiable_hypothesis H)
    (h_bootstrap_hyp : ode_linear_regularity_bootstrap_hypothesis H) :
    ∀ t, H t = Real.cosh t := by
  have h_cont : Continuous H := dAlembert_continuous_of_log_curvature H h_one h_dAlembert h_calib
  exact dAlembert_cosh_solution H h_one h_cont h_dAlembert h_deriv2_zero
    h_smooth_hyp h_ode_hyp h_cont_hyp h_diff_hyp h_bootstrap_hyp

What this page does not claim

The d'Alembert equation alone, without the curvature condition, does not force the solution to be cosh. The theorem does not establish that the cost function J is the only possible cost function in the framework. The theorem does not provide a physical interpretation of the cost function or its curvature.

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