dAlembert_to_ODE_hypothesis
The d'Alembert to ODE hypothesis packages the conditions under which a continuous real function H with H(0)=1, H''(0)=1 and satisfying the addition formula H(t+u)+H(t-u)=2 H(t) H(u) for all real t,u must obey the differential equation H''=H everywhere. Researchers proving T5 uniqueness of the cost algebra cite this packaging when they reduce the Recognition Composition Law to its ODE form. The declaration is a direct definition that bundles the four antecedents into a single Prop for use in downstream uniqueness and classification arguments.
claimLet $H : ℝ → ℝ$. The hypothesis asserts that if $H(0)=1$, $H$ is continuous, $H(t+u)+H(t-u)=2 H(t) H(u)$ holds for all real $t,u$, and the second derivative satisfies $H''(0)=1$, then $H''(t)=H(t)$ for every real $t$.
background
The Cost.FunctionalEquation module supplies helper lemmas for the T5 cost uniqueness proof. The shifted cost is introduced by the sibling definition H(t) := G(t) + 1, where G is the reparametrized cost function. Upstream, the CostAlgebra module defines the same H(x) = J(x) + 1 = ½(x + x^{-1}), under which the Recognition Composition Law reduces exactly to the d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y).
proof idea
This is a definition that directly encodes the implication from the d'Alembert functional equation plus continuity and the calibration H''(0)=1 to the ODE H''=H. No tactics or lemmas are applied inside the body; the declaration simply names the four-antecedent Prop for reuse.
why it matters in Recognition Science
It supplies the ODE hypothesis required by the canonical cost algebra uniqueness theorem cost_algebra_unique, which establishes that any CostAlgebraData obeying the axioms and the calibration J''(1)=1 must coincide with the J function of T5. The declaration is also invoked by the AczelRegularityKernel structure and by the cosh solution theorems that verify the hypothesis for the explicit cosh case.
scope and limits
- Does not prove that any concrete H satisfies the d'Alembert equation.
- Does not establish existence or uniqueness of solutions to the ODE.
- Does not supply higher regularity than the second derivative.
- Does not extend to complex-valued or non-continuous functions.
Lean usage
theorem downstream_use (H : ℝ → ℝ) (h0 : H 0 = 1) (hcont : Continuous H) (hdA : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u) (hderiv : deriv (deriv H) 0 = 1) : ∀ t, deriv (deriv H) t = H t := (dAlembert_to_ODE_hypothesis H) h0 hcont hdA hderivformal statement (Lean)
535def dAlembert_to_ODE_hypothesis (H : ℝ → ℝ) : Prop :=
proof body
Definition body.
536 H 0 = 1 → Continuous H → (∀ t u, H (t+u) + H (t-u) = 2 * H t * H u) →
537 deriv (deriv H) 0 = 1 → ∀ t, deriv (deriv H) t = H t
538
539/-- cosh satisfies the d'Alembert smoothness hypothesis. -/
used by (14)
-
cost_algebra_unique -
aczel_kernel_ode -
AczelRegularityKernel -
dAlembert_to_ODE_hypothesis_of_contDiff -
cosh_dAlembert_to_ODE -
dAlembert_cosh_solution -
dAlembert_cosh_solution_of_log_curvature -
washburn_uniqueness -
T5_uniqueness_complete -
UniqueCostAxioms -
unique_cost_on_pos_from_rcl -
uniqueness_specification -
dAlembert_classification -
ZeroCompositionLaw