dAlembert_first_deriv_of_contDiff
The declaration shows that any twice continuously differentiable solution Hf to the d'Alembert functional equation satisfies the differentiated identity Hf'(t+u) - Hf'(t-u) = 2 Hf(t) Hf'(u). Analysts reducing explicit regularity assumptions in the T5 step of Recognition Science cite this to reach the second-derivative relation at zero. The proof obtains differentiability from contDiffTwo_differentiable, builds HasDerivAt expressions for the shifted sum and the scaled product via the chain rule, then equates the derivatives after confirming the
claimLet $Hf : ℝ → ℝ$ satisfy $Hf(t + u) + Hf(t - u) = 2 Hf(t) Hf(u)$ for all real $t, u$, and suppose $Hf$ is twice continuously differentiable. Then $Hf'(t + u) - Hf'(t - u) = 2 Hf(t) Hf'(u)$ for all real $t, u$.
background
The ContDiffReduction module removes a central portion of the explicit T5 regularity seam. It shows that any ContDiff ℝ 2 solution to the d'Alembert equation satisfies the ODE H'' = H, after which the Recognition Composition Law plus normalization already force reciprocity. The upstream lemma contDiffTwo_differentiable states that ContDiff ℝ 2 Hf implies Differentiable ℝ Hf. The module doc states: 'A ContDiff ℝ 2 d'Alembert solution satisfies the ODE H'' = H.'
proof idea
The tactic proof first calls contDiffTwo_differentiable to obtain differentiability of Hf. It constructs HasDerivAt for v ↦ Hf(t + v) and v ↦ Hf(t - v) by composing the inner linear maps (constant plus id, constant minus id) with the differentiableAt map. These are added to produce the left-hand derivative. The right-hand side is differentiated as a constant times Hf. The original equation is rewritten as an equality of functions of v, its derivative at u is taken, and the two HasDerivAt expressions are substituted.
why it matters in Recognition Science
This theorem is the immediate predecessor of dAlembert_second_deriv_at_zero_of_contDiff, which differentiates again at u = 0 to obtain 2 H''(t) = 2 H(t) H''(0). It advances the T5 J-uniqueness claim by removing a regularity seam, allowing the phi-ladder and eight-tick octave (T7) to emerge from the ODE whose solutions are multiples of cosh. The module doc notes that on the ContDiff surface the canonical reciprocal cost follows from normalization, composition, and calibration alone.
scope and limits
- Does not prove existence or uniqueness of solutions to the d'Alembert equation.
- Does not apply when Hf is only once differentiable or merely continuous.
- Does not treat complex-valued or vector-valued functions.
- Does not derive the explicit closed form of Hf.
formal statement (Lean)
44theorem dAlembert_first_deriv_of_contDiff
45 (Hf : ℝ → ℝ)
46 (h_dAlembert : ∀ t u, Hf (t + u) + Hf (t - u) = 2 * Hf t * Hf u)
47 (h_diff : ContDiff ℝ 2 Hf) :
48 ∀ t u, deriv Hf (t + u) - deriv Hf (t - u) = 2 * Hf t * deriv Hf u := by
proof body
Tactic-mode proof.
49 intro t u
50 have h_diff1 : Differentiable ℝ Hf := contDiffTwo_differentiable h_diff
51 have h_plus :
52 HasDerivAt (fun v => Hf (t + v)) (deriv Hf (t + u)) u := by
53 have h_inner : HasDerivAt (fun v => t + v) 1 u := by
54 simpa using (hasDerivAt_const u t).add (hasDerivAt_id u)
55 simpa using (h_diff1.differentiableAt (x := t + u)).hasDerivAt.comp u h_inner
56 have h_minus :
57 HasDerivAt (fun v => Hf (t - v)) (-deriv Hf (t - u)) u := by
58 have h_inner : HasDerivAt (fun v => t - v) (-1) u := by
59 simpa using (hasDerivAt_const u t).sub (hasDerivAt_id u)
60 simpa using (h_diff1.differentiableAt (x := t - u)).hasDerivAt.comp u h_inner
61 have h_left :
62 HasDerivAt (fun v => Hf (t + v) + Hf (t - v))
63 (deriv Hf (t + u) - deriv Hf (t - u)) u := by
64 simpa using h_plus.add h_minus
65 have h_const : HasDerivAt (fun _ : ℝ => 2 * Hf t) 0 u :=
66 hasDerivAt_const u (2 * Hf t)
67 have h_right :
68 HasDerivAt (((fun _ : ℝ => 2 * Hf t) * Hf)) (2 * (Hf t * deriv Hf u)) u := by
69 simpa [mul_assoc] using h_const.mul ((h_diff1.differentiableAt (x := u)).hasDerivAt)
70 have h_eq :
71 (fun v => Hf (t + v) + Hf (t - v)) = ((fun _ : ℝ => 2 * Hf t) * Hf) := by
72 funext v
73 simpa [Pi.mul_apply, mul_assoc] using h_dAlembert t v
74 have h_deriv_eq := congrArg (fun f : ℝ → ℝ => deriv f u) h_eq
75 change deriv (fun v => Hf (t + v) + Hf (t - v)) u =
76 deriv (((fun _ : ℝ => 2 * Hf t) * Hf)) u at h_deriv_eq
77 rw [h_left.deriv, h_right.deriv] at h_deriv_eq
78 simpa [mul_assoc] using h_deriv_eq
79
80/-- Differentiate the first-derivative identity at `u = 0` to relate `H''(t)` to `H''(0)`. -/