dalembert_deriv_ode
The lemma shows that any C² function obeying the d'Alembert equation f(x+y) + f(x-y) = 2 f(x) f(y) satisfies the ODE f''(x) = f''(0) f(x). Analysts reducing functional equations to linear ODEs or working in Recognition Science's derivation of hyperbolic solutions cite this step. The proof differentiates both sides twice with respect to y at y=0, computes the resulting HasDerivAt expressions separately, and equates them.
claimIf $f : ℝ → ℝ$ is twice continuously differentiable and satisfies $f(x + y) + f(x - y) = 2 f(x) f(y)$ for all real $x, y$, then $f''(x) = f''(0) · f(x)$ for all $x$.
background
The d'Alembert equation appears in Recognition Science as the addition formula satisfied by the J-cost function after composition of automorphisms. ContDiff ℝ 2 f encodes that f possesses a continuous second derivative everywhere. The lemma resides in the Relativity.Calculus.FunctionalEquationDeriv module and supplies the differential reduction used throughout the DAlembert submodules.
proof idea
Fix x and introduce g(y) := f(x+y) + f(x-y) together with h(y) := 2 f(x) f(y). The assumption forces g = h pointwise. Separate HasDerivAt calculations establish that the first derivative of g at 0 vanishes while its second derivative at 0 equals 2 f''(x); the corresponding second derivative of h at 0 equals 2 f(x) f''(0). Equating the two second derivatives at 0 and rearranging produces the ODE.
why it matters in Recognition Science
This reduction is invoked directly by dAlembert_classification and dAlembert_with_unit_calibration to conclude that calibrated solutions equal cosh, and by entangling_forces_hyperbolic_ode to obtain the G'' = G + 1 equation. In the framework it supports T5 J-uniqueness, where J(x) = cosh(log x) - 1, and the passage from the Recognition Composition Law to the eight-tick octave and D = 3. No open scaffolding remains at this node.
scope and limits
- Does not prove existence or uniqueness of solutions to the functional equation.
- Does not apply when f is only once differentiable.
- Does not fix the numerical value of f''(0) from other axioms.
- Does not extend the statement to complex or higher-dimensional domains.
formal statement (Lean)
9theorem dalembert_deriv_ode (f : ℝ → ℝ) (hf : ContDiff ℝ 2 f)
10 (hDA : ∀ x y, f (x + y) + f (x - y) = 2 * f x * f y) :
11 ∀ x, deriv (deriv f) x = deriv (deriv f) 0 * f x := by
proof body
Tactic-mode proof.
12 intro x
13 -- Differentiate w.r.t y twice at y=0
14 let g := fun y => f (x + y) + f (x - y)
15 let h := fun y => 2 * f x * f y
16 have hgh : g = h := by funext y; exact hDA x y
17
18 -- 1. Show that deriv g 0 = 0
19 have h_deriv_g : HasDerivAt g 0 0 := by
20 -- g'(y) = f'(x+y) - f'(x-y)
21 have h1 : HasDerivAt (fun y => f (x + y)) (deriv f x) 0 := by
22 have hd : HasDerivAt f (deriv f x) x := hf.differentiable (by decide) |>.differentiableAt.hasDerivAt
23 exact hd.comp 0 (hasDerivAt_id 0 |>.const_add x)
24 have h2 : HasDerivAt (fun y => f (x - y)) (- deriv f x) 0 := by
25 have hd : HasDerivAt f (deriv f x) x := hf.differentiable (by decide) |>.differentiableAt.hasDerivAt
26 have hsub : HasDerivAt (fun y => x - y) (-1) 0 := by
27 apply HasDerivAt.sub (hasDerivAt_const 0 x) (hasDerivAt_id 0)
28 exact hd.comp 0 hsub
29 convert h1.add h2 using 1; ring
30
31 -- 2. Show that HasDerivAt (deriv g) (2 * f''(x)) 0
32 -- We need to compute the derivative of y => deriv f (x+y) - deriv f (x-y)
33 have h_deriv_fun : ∀ y, deriv g y = deriv f (x + y) - deriv f (x - y) := by
34 intro y
35 have h1 : HasDerivAt (fun s => f (x + s)) (deriv f (x + y)) y := by
36 have hd : HasDerivAt f (deriv f (x + y)) (x + y) := hf.differentiable (by decide) |>.differentiableAt.hasDerivAt
37 exact hd.comp y (hasDerivAt_id y |>.const_add x)
38 have h2 : HasDerivAt (fun s => f (x - s)) (- deriv f (x - y)) y := by
39 have hd : HasDerivAt f (deriv f (x - y)) (x - y) := hf.differentiable (by decide) |>.differentiableAt.hasDerivAt
40 have hsub : HasDerivAt (fun s => x - s) (-1) y := by
41 apply HasDerivAt.sub (hasDerivAt_const y x) (hasDerivAt_id y)
42 exact hd.comp y hsub
43 exact (h1.add h2).deriv
44
45 have h_second_deriv_g : HasDerivAt (deriv g) (2 * deriv (deriv f) x) 0 := by
46 simp_rw [h_deriv_fun]
47 -- Differentiate y => deriv f (x+y) - deriv f (x-y)
48 have h1 : HasDerivAt (fun y => deriv f (x + y)) (deriv (deriv f) x) 0 := by
49 have hd : HasDerivAt (deriv f) (deriv (deriv f) x) x :=
50 hf.iterate_deriv 1 1 |>.differentiable (by decide) |>.differentiableAt.hasDerivAt
51 exact hd.comp 0 (hasDerivAt_id 0 |>.const_add x)
52 have h2 : HasDerivAt (fun y => deriv f (x - y)) (- deriv (deriv f) x) 0 := by
53 have hd : HasDerivAt (deriv f) (deriv (deriv f) x) x :=
54 hf.iterate_deriv 1 1 |>.differentiable (by decide) |>.differentiableAt.hasDerivAt
55 have hsub : HasDerivAt (fun y => x - y) (-1) 0 := by
56 apply HasDerivAt.sub (hasDerivAt_const 0 x) (hasDerivAt_id 0)
57 exact hd.comp 0 hsub
58 convert h1.sub h2 using 1; ring
59
60 -- 3. Show that HasDerivAt (deriv h) (2 * f(x) * f''(0)) 0
61 have h_second_deriv_h : HasDerivAt (deriv h) (2 * f x * deriv (deriv f) 0) 0 := by
62 unfold h
63 have h_deriv_fun : ∀ y, deriv h y = 2 * f x * deriv f y := by
64 intro y; rw [deriv_const_mul]; exact hf.differentiable (by decide) |>.differentiableAt
65 simp_rw [h_deriv_fun]
66 apply HasDerivAt.const_mul
67 exact hf.iterate_deriv 1 1 |>.differentiable (by decide) |>.differentiableAt.hasDerivAt
68
69 -- 4. Equate
70 have h_eq : deriv (deriv g) 0 = deriv (deriv h) 0 := by rw [hgh]
71 rw [h_second_deriv_g.deriv, h_second_deriv_h.deriv] at h_eq
72 linarith
73
74end Calculus
75end Relativity
76end IndisputableMonolith