dAlembert_cosh_solution_aczel
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove existence of any solution.
- Does not classify solutions that fail continuity.
- Does not handle the case H''(0)≠1 without separate rescaling.
- Does not remove the AczelSmoothnessPackage hypothesis.
- Does not extend to non-real or higher-dimensional domains.
formal statement (Lean)
1053theorem dAlembert_cosh_solution_aczel
1054 [AczelSmoothnessPackage]
1055 (H : ℝ → ℝ)
1056 (h_one : H 0 = 1)
1057 (h_cont : Continuous H)
1058 (h_dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u)
1059 (h_d2_zero : deriv (deriv H) 0 = 1) :
1060 ∀ t, H t = Real.cosh t := by
proof body
Term-mode proof.
1061 have h_smooth : ContDiff ℝ ⊤ H := aczel_dAlembert_smooth H h_one h_cont h_dAlembert
1062 have hDiff : Differentiable ℝ H :=
1063 (h_smooth.of_le le_top : ContDiff ℝ 1 H).differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
1064 have h_even : Function.Even H := dAlembert_even H h_one h_dAlembert
1065 have h_H'0 : deriv H 0 = 0 := even_deriv_at_zero H h_even hDiff.differentiableAt
1066 have h_ode : ∀ t, deriv (deriv H) t = H t :=
1067 dAlembert_to_ODE_theorem H h_smooth h_dAlembert h_d2_zero
1068 have h_C2 : ContDiff ℝ 2 H := h_smooth.of_le le_top
1069 exact ode_cosh_uniqueness_contdiff H h_C2 h_ode h_one h_H'0
1070
1071/-- **Theorem (Washburn, clean form)**: The J-cost function is the unique
1072 reciprocal cost satisfying the RCL, normalization, calibration, and continuity.
1073
1074 This version uses the global Aczél axiom internally and requires NO regularity
1075 hypothesis parameters from the caller. -/