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

dAlembert_cos_solution

show as:
view Lean formalization →

The d'Alembert functional equation with normalization H(0)=1, continuity, and second derivative at zero equal to -1 forces H to equal the cosine function on the reals. Recognition Science researchers cite this as the Angle T5 result that selects the oscillatory branch for angle coupling, parallel to the cosh solution in the cost sector. The proof derives the ODE H''=-H from the functional equation, establishes evenness and vanishing first derivative at zero via upstream lemmas, then applies the ODE uniqueness theorem.

claimLet $H:ℝ→ℝ$ be continuous with $H(0)=1$, satisfying the d'Alembert equation $H(t+u)+H(t-u)=2H(t)H(u)$ for all real $t,u$, and with $H''(0)=-1$, together with the regularity hypotheses that bootstrap to twice continuous differentiability. Then $H(t)=cos(t)$ for all real $t$.

background

In the Angle Functional Equation module the d'Alembert equation admits two solution branches under standard regularity: the cosh branch tied to the cost functional and the cos branch for angle coupling. Here H denotes the angle coupling map, satisfying axioms Aθ1 (d'Alembert), Aθ2 (continuity), Aθ3 (normalization H(0)=1), and Aθ4 (calibration H''(0)=-1). Upstream, the lemma dAlembert_even from Cost.FunctionalEquation shows that the functional equation forces H to be even. The companion result even_deriv_at_zero then yields deriv H 0 =0 once differentiability at zero is available. The key uniqueness statement ode_cos_uniqueness (appearing in both AczelProof and AczelTheorem) asserts that the unique solution to f''=-f with f(0)=1 and f'(0)=0 is the cosine.

proof idea

The tactic proof first invokes the hypothesis dAlembert_to_ODE_hypothesis_neg to obtain the ODE ∀t, deriv(deriv H)t = -H t. It then calls Cost.FunctionalEquation.dAlembert_even to establish that H is even. The smoothness hypothesis supplies differentiability at zero, after which even_deriv_at_zero gives deriv H 0 =0. The proof concludes by applying ode_cos_uniqueness with the ODE, the two initial conditions, and the remaining regularity hypotheses.

why it matters in Recognition Science

This theorem supplies the cosine uniqueness required by the downstream master result THEOREM_angle_coupling_rigidity, which packages axioms Aθ1–Aθ4 into the statement that any qualifying H equals cos. It completes the T5 step of the angle forcing chain, mirroring the cosh solution dAlembert_cosh_solution in the cost sector. The negative calibration H''(0)=-1 selects the oscillatory solution, in contrast to the positive curvature that yields the hyperbolic cosine for the shifted cost H(x)=J(x)+1.

scope and limits

Lean usage

exact dAlembert_cos_solution H hAxioms hReg

formal statement (Lean)

 275theorem dAlembert_cos_solution
 276    (H : ℝ → ℝ)
 277    (h_one : H 0 = 1)
 278    (h_cont : Continuous H)
 279    (h_dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u)
 280    (h_deriv2_zero : deriv (deriv H) 0 = -1)
 281    (h_smooth_hyp : dAlembert_continuous_implies_smooth_hypothesis_neg H)
 282    (h_ode_hyp : dAlembert_to_ODE_hypothesis_neg H)
 283    (h_cont_hyp : ode_regularity_continuous_hypothesis_neg H)
 284    (h_diff_hyp : ode_regularity_differentiable_hypothesis_neg H)
 285    (h_bootstrap_hyp : ode_linear_regularity_bootstrap_hypothesis_neg H) :
 286    ∀ t, H t = Real.cos t := by

proof body

Tactic-mode proof.

 287  -- d'Alembert + calibration → ODE H'' = -H
 288  have h_ode : ∀ t, deriv (deriv H) t = -H t := h_ode_hyp h_one h_cont h_dAlembert h_deriv2_zero
 289  -- d'Alembert → H is even
 290  have h_even : Function.Even H := Cost.FunctionalEquation.dAlembert_even H h_one h_dAlembert
 291  -- Even + differentiable → H'(0) = 0
 292  have h_deriv_zero : deriv H 0 = 0 := by
 293    have h_smooth := h_smooth_hyp h_one h_cont h_dAlembert
 294    have h_diff : DifferentiableAt ℝ H 0 := h_smooth.differentiable (by decide : (⊤ : WithTop ℕ∞) ≠ 0) |>.differentiableAt
 295    exact Cost.FunctionalEquation.even_deriv_at_zero H h_even h_diff
 296  -- Apply ODE uniqueness
 297  exact ode_cos_uniqueness H h_ode h_one h_deriv_zero h_cont_hyp h_diff_hyp h_bootstrap_hyp
 298
 299/-! ## Part 4: Master Theorem — Angle Coupling Rigidity (Aθ1–Aθ4)
 300
 301This packages the complete forcing chain for angle coupling.
 302-/
 303
 304/-- **Structure: Angle Coupling Axioms (Aθ1–Aθ4)**
 305
 306A function H : ℝ → ℝ is a valid angle coupling if it satisfies:
 307- Aθ1: d'Alembert functional equation
 308- Aθ2: Continuity (regularity)
 309- Aθ3: Normalization H(0) = 1
 310- Aθ4: Calibration H''(0) = -1 (selects cos branch)
 311-/

used by (1)

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

depends on (29)

Lean names referenced from this declaration's body.