SatisfiesDAlembert
plain-language theorem explainer
A real-valued function H satisfies d'Alembert structure when H(0) equals 1 and H(t+u) + H(t-u) equals 2 H(t) H(u) for all real t and u. Recognition Science workers cite this definition to certify that cost-derived lifts obey the hyperbolic addition law before invoking classification or forcing results. The declaration is a direct encoding of the classical functional equation with normalization, serving as the interface for downstream theorems without any proof steps.
Claim. A function $H:ℝ→ℝ$ satisfies d'Alembert's equation when $H(0)=1$ and $H(t+u)+H(t-u)=2H(t)H(u)$ for all real $t,u$.
background
The Fourth Gate formalizes the d'Alembert functional equation as a cross-check on cost functions in the Recognition Science chain. Upstream CostAlgebra defines the shifted cost H(x) = J(x) + 1, where J is the recognition cost; under this H the Recognition Composition Law reduces exactly to the d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y). The module notes that Gate 3 (curvature) already forces the cosh solution in the Option A formulation, so Gate 4 is derived rather than independent; the classical result that continuous solutions are cosh(λt) supplies the historical anchor.
proof idea
The declaration is a direct definition that encodes the two clauses: normalization H(0)=1 together with the addition law. No lemmas or tactics are invoked; it functions as a pure interface predicate for theorems such as cosh_satisfies_dAlembert and dAlembert_classification.
why it matters
This definition supplies the predicate used by dAlembert_classification, dAlembert_forces_Gcosh, and dAlembert_with_unit_calibration to recover G = cosh - 1 from calibration. It closes the link from J-uniqueness (T5) and the self-similar fixed point (T6) to the eight-tick octave, and is invoked by Jcost_has_dAlembert_structure to certify cost functions arising from multiplicative recognizers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.