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

dAlembert_classification

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 137theorem dAlembert_classification (H : ℝ → ℝ)
 138    (h : IsDAlembertSolution H)
 139    (hCont : Continuous H)
 140    (hCalib : deriv (deriv H) 0 = 1)
 141    -- Regularity hypotheses (from Aczél theory)
 142    (hSmooth : dAlembert_continuous_implies_smooth_hypothesis H)
 143    (hODE : dAlembert_to_ODE_hypothesis H)
 144    (hODECont : ode_regularity_continuous_hypothesis H)
 145    (hODEDiff : ode_regularity_differentiable_hypothesis H)
 146    (hBoot : ode_linear_regularity_bootstrap_hypothesis H) :
 147    ∀ t, H t = cosh t :=

proof body

Term-mode proof.

 148  dAlembert_cosh_solution H h.1 hCont h.2 hCalib hSmooth hODE hODECont hODEDiff hBoot
 149
 150/-! ## The Inevitability Argument -/
 151
 152/-- **THEOREM (scoped): The compatibility constraints force a unique bilinear family.**
 153
 154If G : ℝ → ℝ satisfies:
 1551. G is even: G(-t) = G(t)
 1562. G(0) = 0
 1573. G(t+u) + G(t-u) = Φ(G(t), G(u)) for some polynomial Φ
 1584. G is continuous
 1595. G is non-constant
 160
 161Then Φ(a, b) = 2a + 2b + c·ab for some constant c (the forced bilinear family).
 162With a canonical normalization choice (c = 2), this is the shifted d'Alembert form. -/

used by (5)

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

depends on (25)

Lean names referenced from this declaration's body.