pith. machine review for the scientific record. sign in
theorem proved tactic proof high

dAlembert_contDiff_top

show as:
view Lean formalization →

Continuous solutions to the d'Alembert equation H(t+u) + H(t-u) = 2 H(t) H(u) with H(0)=1 are infinitely differentiable. Researchers in functional equations and Recognition Science cost algebra cite this to remove any smoothness hypothesis from the Aczél classification. The proof first obtains C^∞ regularity by bootstrap from continuity, derives the ODE H'' = c H, then classifies solutions by the sign of c = H''(0) and invokes uniqueness for the resulting differential equations.

claimLet $H : ℝ → ℝ$ be continuous with $H(0) = 1$ and satisfy $H(t+u) + H(t-u) = 2 H(t) H(u)$ for all real $t,u$. Then $H$ is infinitely differentiable.

background

In the cost algebra, H is the shifted cost function defined by H(x) = J(x) + 1, where J satisfies the Recognition Composition Law; this substitution converts the RCL into the additive d'Alembert equation H(t+u) + H(t-u) = 2 H(t) H(u). The module proves that every continuous solution with H(0)=1 is C^∞, recovering the three classical cases: the constant 1, cosh(λ t), and cos(λ t). Upstream results supply the initial smoothness bootstrap (dAlembert_contDiff_smooth) and the ODE derivation (dAlembert_to_ODE_general), which states that H''(t) = H''(0) · H(t) once H is C².

proof idea

The proof invokes dAlembert_contDiff_smooth to obtain ContDiff ℝ smooth H, extracts a C² version, and applies dAlembert_to_ODE_general to reach the ODE with constant c = H''(0). It then branches on the sign of c. For c > 0 a rescaled function g satisfies g'' = g and is identified with cosh by ode_cosh_uniqueness_contdiff. For c < 0 the rescaled equation becomes g'' = -g and is identified with cos by ode_cos_uniqueness. The remaining case c = 0 yields the constant solution 1, which is smooth.

why it matters in Recognition Science

This declaration supplies the final step that turns the Aczél classification into an unconditional theorem, feeding directly into h_aczel_classification_proved which asserts H_AczelClassification without axioms. It closes the last foundation gap in the IndisputableMonolith codebase and aligns with the cost-algebra origin of H from J. The result matches the 1966 Aczél reference cited in the module and supports the smoothness presupposed by the phi-ladder and mass formulas in the Recognition framework.

scope and limits

Lean usage

theorem aczel_smooth (H : ℝ → ℝ) (h_one : H 0 = 1) (h_cont : Continuous H) (h_dAl : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u) : ContDiff ℝ ⊤ H := dAlembert_contDiff_top H h_one h_cont h_dAl

formal statement (Lean)

 353private theorem dAlembert_contDiff_top (H : ℝ → ℝ)
 354    (h_one : H 0 = 1) (h_cont : Continuous H)
 355    (h_dAl : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u) :
 356    ContDiff ℝ ⊤ H := by

proof body

Tactic-mode proof.

 357  have h_sm : ContDiff ℝ smooth H := dAlembert_contDiff_smooth H h_one h_cont h_dAl
 358  have h2 : ContDiff ℝ 2 H := by exact_mod_cast (contDiff_infty.mp h_sm) 2
 359  have hDiff : Differentiable ℝ H := h2.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
 360  have h_H'0 : deriv H 0 = 0 :=
 361    even_deriv_at_zero H (dAlembert_even H h_one h_dAl) hDiff.differentiableAt
 362  have h_ode := dAlembert_to_ODE_general H h_sm h_dAl
 363  set c := deriv (deriv H) 0
 364  have hDD : Differentiable ℝ (deriv H) := by
 365    rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h2
 366    exact (contDiff_succ_iff_deriv.mp h2).2.2.differentiable
 367      (by decide : (1 : WithTop ℕ∞) ≠ 0)
 368  by_cases hc_pos : 0 < c
 369  · -- Case c > 0: H = cosh(√c · t)
 370    have hsc_ne : Real.sqrt c ≠ 0 := ne_of_gt (Real.sqrt_pos.mpr hc_pos)
 371    let g : ℝ → ℝ := fun s => H (s / Real.sqrt c)
 372    have h_div : ∀ s, HasDerivAt (fun x => x / Real.sqrt c) (Real.sqrt c)⁻¹ s := fun s => by
 373      have := (hasDerivAt_id s).div_const (Real.sqrt c)
 374      simp only [id, one_div] at this; exact this
 375    have hg_d : ∀ s, HasDerivAt g (deriv H (s / Real.sqrt c) * (Real.sqrt c)⁻¹) s :=
 376      fun s => (hDiff _).hasDerivAt.comp s (h_div s)
 377    have hg_ode : ∀ t, deriv (deriv g) t = g t := by
 378      intro s
 379      have hg1 : deriv g = fun s => deriv H (s / Real.sqrt c) * (Real.sqrt c)⁻¹ :=
 380        funext fun s => (hg_d s).deriv
 381      have h_dd_g : HasDerivAt (deriv g)
 382          ((deriv (deriv H) (s / Real.sqrt c) * (Real.sqrt c)⁻¹) * (Real.sqrt c)⁻¹) s := by
 383        rw [hg1]
 384        exact ((hDD (s / Real.sqrt c)).hasDerivAt.comp s (h_div s)).mul_const _
 385      rw [h_dd_g.deriv, h_ode (s / Real.sqrt c)]
 386      simp only [g]
 387      rw [show c * H (s / Real.sqrt c) * (Real.sqrt c)⁻¹ * (Real.sqrt c)⁻¹ =
 388          H (s / Real.sqrt c) * (c * ((Real.sqrt c)⁻¹ * (Real.sqrt c)⁻¹)) from by ring,
 389          show (Real.sqrt c)⁻¹ * (Real.sqrt c)⁻¹ = (Real.sqrt c * Real.sqrt c)⁻¹ from
 390            (mul_inv_rev _ _).symm,
 391          Real.mul_self_sqrt (le_of_lt hc_pos),
 392          mul_inv_cancel₀ (ne_of_gt hc_pos), mul_one]
 393    have h_eq : ∀ t, H t = Real.cosh (Real.sqrt c * t) := fun t => by
 394      have := ode_cosh_uniqueness_contdiff g (h2.comp (contDiff_id.div_const _))
 395        hg_ode (by simp [g, h_one]) (by rw [(hg_d 0).deriv]; simp [h_H'0])
 396        (Real.sqrt c * t)
 397      simp only [g, mul_div_cancel_left₀ _ hsc_ne] at this; exact this
 398    rw [show H = fun t => Real.cosh (Real.sqrt c * t) from funext h_eq]
 399    exact Real.contDiff_cosh.comp (contDiff_const.mul contDiff_id)
 400  · by_cases hc_neg : c < 0
 401    · -- Case c < 0: H = cos(√|c| · t)
 402      set c' := -c
 403      have hsc_ne : Real.sqrt c' ≠ 0 := ne_of_gt (Real.sqrt_pos.mpr (neg_pos.mpr hc_neg))
 404      let g : ℝ → ℝ := fun s => H (s / Real.sqrt c')
 405      have h_div : ∀ s, HasDerivAt (fun x => x / Real.sqrt c') (Real.sqrt c')⁻¹ s :=
 406        fun s => by
 407        have := (hasDerivAt_id s).div_const (Real.sqrt c')
 408        simp only [id, one_div] at this; exact this
 409      have hg_d : ∀ s, HasDerivAt g (deriv H (s / Real.sqrt c') * (Real.sqrt c')⁻¹) s :=
 410        fun s => (hDiff _).hasDerivAt.comp s (h_div s)
 411      have hg_ode : ∀ t, deriv (deriv g) t = -(g t) := by
 412        intro s
 413        have hg1 : deriv g = fun s => deriv H (s / Real.sqrt c') * (Real.sqrt c')⁻¹ :=
 414          funext fun s => (hg_d s).deriv
 415        have h_dd_g : HasDerivAt (deriv g)
 416            ((deriv (deriv H) (s / Real.sqrt c') * (Real.sqrt c')⁻¹) * (Real.sqrt c')⁻¹) s := by
 417          rw [hg1]
 418          exact ((hDD (s / Real.sqrt c')).hasDerivAt.comp s (h_div s)).mul_const _
 419        rw [h_dd_g.deriv, h_ode (s / Real.sqrt c')]
 420        simp only [g, c']
 421        rw [show c * H (s / Real.sqrt (-c)) * (Real.sqrt (-c))⁻¹ * (Real.sqrt (-c))⁻¹ =
 422            H (s / Real.sqrt (-c)) * (c * ((Real.sqrt (-c))⁻¹ * (Real.sqrt (-c))⁻¹)) from
 423              by ring,
 424            show (Real.sqrt (-c))⁻¹ * (Real.sqrt (-c))⁻¹ = (Real.sqrt (-c) * Real.sqrt (-c))⁻¹
 425              from (mul_inv_rev _ _).symm,
 426            Real.mul_self_sqrt (le_of_lt (neg_pos.mpr hc_neg)),
 427            show c * (-c)⁻¹ = -(1 : ℝ) from by
 428              have hc_ne : c ≠ 0 := ne_of_lt hc_neg
 429              field_simp]
 430        ring
 431      have h_eq : ∀ t, H t = Real.cos (Real.sqrt c' * t) := fun t => by
 432        have := ode_cos_uniqueness g (h2.comp (contDiff_id.div_const _))
 433          hg_ode (by simp [g, h_one]) (by rw [(hg_d 0).deriv]; simp [h_H'0])
 434          (Real.sqrt c' * t)
 435        simp only [g, mul_div_cancel_left₀ _ hsc_ne] at this; exact this
 436      rw [show H = fun t => Real.cos (Real.sqrt c' * t) from funext h_eq]
 437-- ... 16 more lines elided ...

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (33)

Lean names referenced from this declaration's body.

… and 3 more