pith. machine review for the scientific record. sign in
theorem

dAlembert_cosh_solution_aczel

proved
show as:
module
IndisputableMonolith.Cost.FunctionalEquation
domain
Cost
line
1053 · github
papers citing
23 papers (below)

plain-language theorem explainer

Continuous solutions of d'Alembert's functional equation with H(0)=1 and H''(0)=1 coincide with the hyperbolic cosine. Recognition Science researchers cite this to establish the explicit form of the shifted cost under the composition law. The argument first invokes Aczél smoothness to reach infinite differentiability, derives the ODE H''=H, and concludes via ODE uniqueness.

Claim. Let $H:ℝ→ℝ$ be continuous and satisfy $H(t+u)+H(t-u)=2H(t)H(u)$ for all real $t,u$, with $H(0)=1$ and $H''(0)=1$. Then $H(t)=cosh(t)$ for all real $t$.

background

In Recognition Science the shifted cost is $H(x)=J(x)+1$, where $J$ satisfies the Recognition Composition Law. Under this change of variable the RCL becomes d'Alembert's equation $H(t+u)+H(t-u)=2H(t)H(u)$. The module supplies supporting lemmas for the T5 uniqueness argument. The AczelSmoothnessPackage states that every continuous solution with $H(0)=1$ is $C^∞$. Upstream, dAlembert_to_ODE_theorem shows that the functional equation plus $H''(0)=1$ forces the ODE $H''=H$ everywhere.

proof idea

The term proof first applies aczel_dAlembert_smooth to obtain ContDiff ℝ ⊤ H, then uses dAlembert_even to establish evenness and even_deriv_at_zero to obtain H'(0)=0. It invokes dAlembert_to_ODE_theorem to derive the ODE H''=H, reduces to ContDiff ℝ 2 H, and finishes by applying ode_cosh_uniqueness_contdiff.

why it matters

This supplies the cosh identification required by washburn_uniqueness_aczel, which proves that the J-cost is the unique reciprocal cost obeying the composition law, normalization, calibration, and continuity. It fills the explicit-solution step in the T5 J-uniqueness forcing chain. The result also supports the downstream discharge lemmas aczel_kannappan_via_cases and cosh_rescaling_lemma in the AxiomDischargePlan.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.

papers checked against this theorem (showing 23 of 23)