dAlembert_classification
The d'Alembert classification theorem states that any C² function H satisfying the d'Alembert functional equation with H(0)=1, H'(0)=0 and H''(0)=λ² must equal cosh(λt). Researchers verifying hyperbolic solutions in the Recognition Science cost algebra or functional-equation derivations would cite it. The proof splits on whether λ vanishes, reduces the nonzero case to the unit-calibration ODE uniqueness result via rescaling, and invokes the ODE uniqueness lemma for the scaled function.
claimLet $H : ℝ → ℝ$ be twice continuously differentiable. Suppose $H$ satisfies the d'Alembert equation $H(t+u) + H(t-u) = 2 H(t) H(u)$ for all real $t, u$, with $H(0) = 1$, $H'(0) = 0$, and $H''(0) = λ²$. Then $H(t) = cosh(λ t)$ for every real $t$.
background
SatisfiesDAlembert H encodes the d'Alembert structure: H(0)=1 together with the functional equation H(t+u) + H(t-u) = 2 H(t) H(u) for all t,u. This module presents the Fourth Gate as a derived cross-check on the curvature gate, where the normalized ODE G'' = G + 1 already selects the hyperbolic branch; the shifted lift H = G + 1 therefore satisfies d'Alembert automatically. Upstream, dalembert_deriv_ode supplies the relation H''(x) = H''(0) H(x), while ode_cosh_uniqueness_contdiff from Cost.FunctionalEquation establishes that the only C² solution to K'' = K with K(0)=1 and K'(0)=0 is cosh.
proof idea
The proof first obtains the second-order ODE H''(x) = λ² H(x) from dalembert_deriv_ode. It cases on λ = 0. When λ vanishes the ODE collapses to H'' = 0; combined with the initial conditions this forces H constant and equal to 1, matching cosh(0). For λ ≠ 0 the auxiliary K(s) := H(s/λ) is introduced; direct verification shows K satisfies K'' = K, K(0)=1, K'(0)=0 and C² regularity. The uniqueness lemma ode_cosh_uniqueness_contdiff then yields K(s) = cosh(s), which rescales to the claimed form for H.
why it matters in Recognition Science
This supplies the general-λ version of the d'Alembert classification that feeds the AczelProof and GeneralizedDAlembert modules. It closes the scaling argument noted in the module documentation, confirming that the λ=1 case proved separately in dAlembert_with_unit_calibration extends to arbitrary λ. Within the Recognition Science framework it corroborates the T5 J-uniqueness step that produces the hyperbolic cosine as the unique self-similar solution compatible with the Recognition Composition Law. The declaration is not required for the main forcing chain T0-T8, which uses only the unit-calibration instance.
scope and limits
- Does not classify solutions lacking C² regularity.
- Does not address the trigonometric cosine branch excluded by the sign of H''(0).
- Does not derive the functional equation from more primitive cost axioms.
- Does not treat complex-valued extensions.
formal statement (Lean)
172theorem dAlembert_classification :
173 ∀ H : ℝ → ℝ, ∀ lam : ℝ,
174 SatisfiesDAlembert H →
175 ContDiff ℝ 2 H →
176 deriv H 0 = 0 →
177 deriv (deriv H) 0 = lam ^ 2 →
178 ∀ t, H t = Real.cosh (lam * t) := by
proof body
Tactic-mode proof.
179 intro H lam hDA hSmooth hDeriv0 hCalib t
180 have h_ode : ∀ x, deriv (deriv H) x = deriv (deriv H) 0 * H x :=
181 dalembert_deriv_ode H hSmooth hDA.2
182 by_cases hlam : lam = 0
183 · -- λ = 0: H'' = 0, so H is constant; H(0)=1, H'(0)=0 ⇒ H = 1 = cosh(0)
184 subst hlam
185 have hode0 : ∀ x, deriv (deriv H) x = 0 := fun x => by
186 rw [h_ode x, hCalib, zero_pow two_ne_zero]; exact zero_mul (H x)
187 -- H''=0 ⇒ deriv H constant; deriv H 0 = 0 ⇒ deriv H = 0 ⇒ H constant; H 0 = 1 ⇒ H = 1
188 have hd_deriv : Differentiable ℝ (deriv H) := hSmooth.differentiable_deriv_two
189 have hH'0 : ∀ x, deriv H x = 0 := fun x => (is_const_of_deriv_eq_zero hd_deriv hode0 x 0).trans hDeriv0
190 have hH_const : ∀ x, H x = 1 := fun x => (is_const_of_deriv_eq_zero (hSmooth.differentiable (by decide)) hH'0 x 0).trans hDA.1
191 simp only [hH_const t, zero_mul, Real.cosh_zero]
192 · -- λ ≠ 0: K(s) = H(s/λ) satisfies K'' = K, K(0)=1, K'(0)=0, K''(0)=1; apply unit calibration.
193 let K := fun s => H (s / lam)
194 have hK0 : K 0 = 1 := by simp [K, hDA.1]
195 have hK_DA : SatisfiesDAlembert K := by
196 constructor; exact hK0
197 intro t u
198 simp only [K]
199 have ht : (t + u) / lam = t / lam + u / lam := by field_simp [hlam]
200 have ht' : (t - u) / lam = t / lam - u / lam := by field_simp [hlam]
201 rw [ht, ht']
202 exact hDA.2 (t / lam) (u / lam)
203 have hK_smooth : ContDiff ℝ 2 K :=
204 ContDiff.comp hSmooth ((contDiff_id.div_const lam).of_le le_top)
205 have hK'_0 : deriv K 0 = 0 := by
206 have K_eq : K = fun s => H ((1/lam) * s) := by ext s; simp [K]; congr 1; field_simp [hlam]
207 rw [K_eq, deriv_comp_mul_left (1/lam) H 0]
208 rw [show (1/lam) * 0 = 0 from by ring, hDeriv0]; simp
209 have hK''_0 : deriv (deriv K) 0 = 1 := by
210 have K_eq : K = fun s => H ((1/lam) * s) := by ext s; simp [K]; congr 1; field_simp [hlam]
211 have dK : deriv K = fun s => (1/lam) * deriv H (s/lam) := by
212 ext s
213 rw [K_eq, deriv_comp_mul_left (1/lam) H s, smul_eq_mul]
214 rw [show (1/lam) * s = s / lam from by field_simp [hlam]]
215 rw [dK, deriv_const_mul_field (1/lam)]
216 rw [show (fun s => deriv H (s/lam)) = fun s => (deriv H) ((1/lam) * s) from by ext s; congr 1; field_simp [hlam]]
217 rw [deriv_comp_mul_left (1/lam) (deriv H) 0, smul_eq_mul]
218 rw [show (1/lam) * 0 = 0 from by ring, h_ode 0, hCalib, hDA.1]
219 field_simp [hlam]
220 have hK_ode : ∀ s, deriv (deriv K) s = K s := by
221 intro s
222 have K_eq : K = fun z => H ((1/lam) * z) := by ext z; simp [K]; congr 1; field_simp [hlam]
223 have dK : deriv K = fun x => (1/lam) * deriv H (x/lam) := by
224 ext x
225 rw [K_eq, deriv_comp_mul_left (1/lam) H x, smul_eq_mul]
226 rw [show (1/lam) * x = x / lam from by field_simp [hlam]]
227 rw [dK, deriv_const_mul_field (1/lam)]
228 rw [show (fun x => deriv H (x/lam)) = fun x => (deriv H) ((1/lam) * x) from by ext x; congr 1; field_simp [hlam]]
229 rw [deriv_comp_mul_left (1/lam) (deriv H) s, smul_eq_mul]
230 rw [show (1/lam) * s = s / lam from by field_simp [hlam], h_ode (s/lam)]
231 simp only [K, hCalib]; field_simp [hlam]
232 have hK_eq_cosh : ∀ s, K s = Real.cosh s :=
233 Cost.FunctionalEquation.ode_cosh_uniqueness_contdiff K hK_smooth hK_ode hK0 hK'_0
234 have h_eq : K (lam * t) = H t := by simp [K]; field_simp [hlam]
235 rw [← h_eq, hK_eq_cosh (lam * t)]
236
237/-- **Corollary**: With calibration H''(0) = 1, we get H = cosh.
238 Proof: dalembert_deriv_ode gives H''(t) = H''(0)·H(t); substituting H''(0) = 1
239 gives H'' = H; ODE uniqueness (H(0)=1, H'(0)=0) then forces H = cosh. -/