Cost Cauchy Auxiliary Aczel Classification Conditional

The conditional classification

The d'Alembert equation, H(t+u) + H(t-u) = 2·H(t)·H(u), is a functional equation whose solutions are the hyperbolic cosine, the ordinary cosine, and constant functions. It appears in the study of functional equations, which are rules that describe a function in terms of its own values at different points. The equation is named after Jean le Rond d'Alembert, who studied it in 1747 while working on the vibrating string problem.

The classification of all continuous solutions is a classical result due to János Aczél. The standard strategy splits into two branches. If the solution H ever exceeds 1, one defines an auxiliary function φ(t) = H(t) + √(H(t)² - 1), which turns out to satisfy the multiplicative Cauchy equation φ(t+u) = φ(t)·φ(u). For continuous positive functions, this forces φ(t) = e^(λt), and hence H(t) = cosh(λt). If instead H(t) ≤ 1 everywhere, the solution is H(t) = cos(κt).

In Recognition Science, the framework's cost function J is linked to a d'Alembert solution H = 1 + J, which grows without bound, so only the cosh branch matters. The machine-checked library of formal theorems formalizes this branch. Its declaration aczel_classification_conditional proves that, given four hypotheses, the solution must be a hyperbolic cosine: H(t) = cosh(λt) for some real λ. The hypotheses are that H is continuous, H(0) = 1, H satisfies the d'Alembert equation, and H(t) ≥ 1 for all t.

Two of the four hypotheses are not yet proved as standalone theorems. The first, H_PhiMultiplicative, states that the auxiliary function φ is multiplicative; its proof is blocked by careful handling of square-root branches. The second, H_CauchyToExponential, is the standard textbook result that a continuous positive multiplicative function is an exponential; it requires either a Mathlib lemma or a custom proof via logarithms. The declaration is therefore conditional: it establishes the cosh conclusion only if those two bridge lemmas are granted.

What the declaration does not claim is just as important. It does not prove the full Aczél classification, because it omits the cosine branch. It does not prove that the bridge lemmas hold. And it does not by itself derive the framework's cost function J, which requires additional steps beyond this classification. The value of the declaration is that it isolates exactly which pieces remain open: the algebraic verification of multiplicativity and the exponential theorem for continuous Cauchy functions.

/-- The full Aczél classification, conditional on the two bridge lemmas. -/
theorem aczel_classification_conditional
    (H : ℝ → ℝ)
    (h_one : H 0 = 1)
    (h_cont : Continuous H)
    (h_dA : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u)
    (h_phi_mult : H_PhiMultiplicative H)
    (h_cauchy : H_CauchyToExponential)
    (h_ge_one : ∀ t, 1 ≤ H t) :
    ∃ lam : ℝ, ∀ t, H t = Real.cosh (lam * t) := by
  have h_phi_cont : Continuous (phi H) := by
    unfold phi
    exact h_cont.add ((h_cont.pow 2).sub continuous_const).sqrt
  have h_phi_pos : ∀ t, 0 < phi H t := fun t => phi_pos H t (h_ge_one t)
  have h_phi_zero : phi H 0 = 1 := phi_at_zero H h_one
  have h_phi_cauchy : ∀ t u, phi H (t + u) = phi H t * phi H u :=
    fun t u => h_phi_mult t u (h_ge_one t) (h_ge_one u)
  obtain ⟨lam_, hlam⟩ := h_cauchy (phi H) h_phi_cont h_phi_pos h_phi_zero h_phi_cauchy
  refine ⟨lam_, fun t => ?_⟩
  have h_phi_exp : phi H t = Real.exp (lam_ * t) := hlam t
  have h_phi_neg : phi H (-t) = Real.exp (-(lam_ * t)) := by
    rw [hlam (-t)]; ring_nf
  have h_H_from_phi := H_from_phi H t (h_ge_one t)
  rw [h_phi_exp] at h_H_from_phi
  rw [Real.cosh_eq]
  convert h_H_from_phi using 1
  rw [exp_neg]

What this page does not claim

The declaration does not prove the full Aczél classification, including the cosine branch. The declaration does not prove the bridge lemmas H_PhiMultiplicative or H_CauchyToExponential. The declaration does not by itself derive the framework's cost function J.

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