Encyclopedia Foundation Foundation Axiom Discharge Plan Cosh Rescaling Lemma
ARTICLE 3 claims 3 theorems
Foundation Axiom Discharge Plan Cosh Rescaling Lemma
A lemma that turns any smooth solution of a classical functional equation into a hyperbolic cosine, by rescaling its time variable.
The rescaling lemma
The cosh_rescaling_lemma is a theorem about a classical functional equation, the d'Alembert equation, which relates a function's value at sums and differences of two numbers to its values at each number. The lemma states that if a continuous function H satisfies this equation, has H(0) = 1, and has a positive second derivative at zero, then H must equal the hyperbolic cosine of a scaled argument. In symbols, if H(x+y) + H(x-y) = 2H(x)H(y) for all real x and y, and H''(0) = α² > 0, then H(x) = cosh(αx) for every x.
The proof works by a change of variable. Define a new function G(t) = H(t/α). A direct computation using the chain rule shows that G satisfies the same d'Alembert equation, has G(0) = 1, and now has G''(0) = 1. At this point the framework's existing theorem, which already proves that a continuous d'Alembert solution with H''(0) = 1 is exactly the hyperbolic cosine, applies directly. The lemma therefore reduces the general positive case to the already-proved unit case.
In the broader Recognition Science program, this lemma is one piece of a plan to discharge a named classical input. The framework's library of formal theorems previously relied on an opaque axiom, the Aczél–Kannappan classification of continuous d'Alembert solutions. This lemma, together with three other proved theorems, replaces that axiom with a finite combination of explicit, machine-checked results. The constant case, the cosine case, and the cosh case are each now proved from first principles via ordinary differential equation uniqueness, with no unproved assumptions.
The lemma does not claim anything about the sign of the second derivative at zero. It requires α > 0, so it says nothing about the cosine case, where the second derivative is negative, nor about the constant case, where it is zero. It also does not assert that every d'Alembert solution is a hyperbolic cosine; that would be false, since cosine and constant solutions also exist. The lemma only covers the specific branch where the second derivative at zero is positive.
THEOREM cosh_rescaling_lemma · IndisputableMonolith/Foundation/AxiomDischargePlan.lean
/-- **Cosh-rescaling lemma (proved)**: an arbitrary positive scaling
factor on the time variable transforms a continuous d'Alembert
solution with `H''(0) = α² > 0` into one with second derivative `1`
at zero. The conclusion is handed off to `dAlembert_cosh_solution_aczel`
already in the framework. -/
theorem cosh_rescaling_lemma
[AczelSmoothnessPackage]
(H : ℝ → ℝ) (h_one : H 0 = 1) (h_cont : Continuous H)
(h_dAlembert : ∀ x y, H (x + y) + H (x - y) = 2 * H x * H y)
{α : ℝ} (hα : 0 < α)
(h_d2 : deriv (deriv H) 0 = α ^ 2) :
∀ x, H x = Real.cosh (α * x) := by
-- Smoothness of H from the AczelSmoothnessPackage instance.
have h_smooth_H : ContDiff ℝ ⊤ H :=
aczel_dAlembert_smooth H h_one h_cont h_dAlembert
-- Define the rescaled function H_α(t) := H(t / α).
set H_α : ℝ → ℝ := fun t => H (t / α) with hH_α_def
have hα_ne : (α : ℝ) ≠ 0 := ne_of_gt hα
-- (1) H_α(0) = 1.
have h_α_one : H_α 0 = 1 := by
show H (0 / α) = 1
rw [zero_div, h_one]
-- (2) H_α continuous.
have h_α_cont : Continuous H_α :=
h_cont.comp (continuous_id.div_const α)
-- (3) H_α satisfies the d'Alembert equation.
have h_α_dAlembert :
∀ x y, H_α (x + y) + H_α (x - y) = 2 * H_α x * H_α y := by
intro x y
show H ((x + y) / α) + H ((x - y) / α) = 2 * H (x / α) * H (y / α)
rw [add_div, sub_div]
exact h_dAlembert (x / α) (y / α)
-- (4) H_α''(0) = 1: chain rule on H_α(t) = H(t/α).
have h_α_d2 : deriv (deriv H_α) 0 = 1 := by
-- H_α = H ∘ (·/α), so by chain rule:
-- deriv H_α t = deriv H (t/α) / α
-- deriv (deriv H_α) t = deriv (deriv H) (t/α) / α²
-- At t = 0: H_α''(0) = H''(0) / α² = α²/α² = 1.
have h_diff_H : Differentiable ℝ H :=
h_smooth_H.differentiable (by decide : (⊤ : WithTop ℕ∞) ≠ 0)
have h_diff_H' : Differentiable ℝ (deriv H) := by
have h_succ : (⊤ : WithTop ℕ∞) = 1 + ⊤ := rfl
have hC2 : ContDiff ℝ (1 + ⊤) H := by rw [← h_succ]; exact h_smooth_H
have hC1d : ContDiff ℝ ⊤ (deriv H) := (contDiff_succ_iff_deriv.mp hC2).2.2
exact hC1d.differentiable (by decide : (⊤ : WithTop ℕ∞) ≠ 0)
have h_diff_phi : ∀ t, DifferentiableAt ℝ (fun x : ℝ => x / α) t :=
fun t => (differentiableAt_id).div_const α
-- First derivative of H_α.
have h_dHα : ∀ t, deriv H_α t = deriv H (t / α) / α := by
intro t
change deriv (fun s => H (s / α)) t = deriv H (t / α) / α
have hcomp : (fun s => H (s / α)) = H ∘ (fun s => s / α) := rfl
rw [hcomp, deriv_comp t (h_diff_H _) (h_diff_phi _)]
rw [show deriv (fun s : ℝ => s / α) t = 1 / α from by
rw [deriv_div_const]; simp]
ring
-- Second derivative of H_α.
have h_d2Hα : ∀ t, deriv (deriv H_α) t = deriv (deriv H) (t / α) / α ^ 2 := by
intro t
have h_eq : deriv H_α = fun t => deriv H (t / α) / α := by
funext t; exact h_dHα t
rw [h_eq]
change deriv (fun s => deriv H (s / α) / α) t = deriv (deriv H) (t / α) / α ^ 2
rw [deriv_div_const]
change deriv (fun s => deriv H (s / α)) t / α
= deriv (deriv H) (t / α) / α ^ 2
have hcomp : (fun s => deriv H (s / α)) = (deriv H) ∘ (fun s => s / α) := rfl
rw [hcomp, deriv_comp t (h_diff_H' _) (h_diff_phi _)]
rw [show deriv (fun s : ℝ => s / α) t = 1 / α from by
rw [deriv_div_const]; simp]
field_simp
rw [h_d2Hα 0, zero_div, h_d2]
field_simp
-- Apply the existing cosh classification.
have h_α_cosh : ∀ t, H_α t = Real.cosh t :=
dAlembert_cosh_solution_aczel H_α h_α_one h_α_cont h_α_dAlembert h_α_d2
-- Substitute t = α x to recover H.
intro x
have hkey : H (α * x / α) = Real.cosh (α * x) := h_α_cosh (α * x)
have h_cancel : α * x / α = x := by
field_simp
rw [h_cancel] at hkey
exact hkey
THEOREM cosh_rescaling_lemma · IndisputableMonolith/Foundation/AxiomDischargePlan.lean
/-- **Cosh-rescaling lemma (proved)**: an arbitrary positive scaling
factor on the time variable transforms a continuous d'Alembert
solution with `H''(0) = α² > 0` into one with second derivative `1`
at zero. The conclusion is handed off to `dAlembert_cosh_solution_aczel`
already in the framework. -/
theorem cosh_rescaling_lemma
[AczelSmoothnessPackage]
(H : ℝ → ℝ) (h_one : H 0 = 1) (h_cont : Continuous H)
(h_dAlembert : ∀ x y, H (x + y) + H (x - y) = 2 * H x * H y)
{α : ℝ} (hα : 0 < α)
(h_d2 : deriv (deriv H) 0 = α ^ 2) :
∀ x, H x = Real.cosh (α * x) := by
-- Smoothness of H from the AczelSmoothnessPackage instance.
have h_smooth_H : ContDiff ℝ ⊤ H :=
aczel_dAlembert_smooth H h_one h_cont h_dAlembert
-- Define the rescaled function H_α(t) := H(t / α).
set H_α : ℝ → ℝ := fun t => H (t / α) with hH_α_def
have hα_ne : (α : ℝ) ≠ 0 := ne_of_gt hα
-- (1) H_α(0) = 1.
have h_α_one : H_α 0 = 1 := by
show H (0 / α) = 1
rw [zero_div, h_one]
-- (2) H_α continuous.
have h_α_cont : Continuous H_α :=
h_cont.comp (continuous_id.div_const α)
-- (3) H_α satisfies the d'Alembert equation.
have h_α_dAlembert :
∀ x y, H_α (x + y) + H_α (x - y) = 2 * H_α x * H_α y := by
intro x y
show H ((x + y) / α) + H ((x - y) / α) = 2 * H (x / α) * H (y / α)
rw [add_div, sub_div]
exact h_dAlembert (x / α) (y / α)
-- (4) H_α''(0) = 1: chain rule on H_α(t) = H(t/α).
have h_α_d2 : deriv (deriv H_α) 0 = 1 := by
-- H_α = H ∘ (·/α), so by chain rule:
-- deriv H_α t = deriv H (t/α) / α
-- deriv (deriv H_α) t = deriv (deriv H) (t/α) / α²
-- At t = 0: H_α''(0) = H''(0) / α² = α²/α² = 1.
have h_diff_H : Differentiable ℝ H :=
h_smooth_H.differentiable (by decide : (⊤ : WithTop ℕ∞) ≠ 0)
have h_diff_H' : Differentiable ℝ (deriv H) := by
have h_succ : (⊤ : WithTop ℕ∞) = 1 + ⊤ := rfl
have hC2 : ContDiff ℝ (1 + ⊤) H := by rw [← h_succ]; exact h_smooth_H
have hC1d : ContDiff ℝ ⊤ (deriv H) := (contDiff_succ_iff_deriv.mp hC2).2.2
exact hC1d.differentiable (by decide : (⊤ : WithTop ℕ∞) ≠ 0)
have h_diff_phi : ∀ t, DifferentiableAt ℝ (fun x : ℝ => x / α) t :=
fun t => (differentiableAt_id).div_const α
-- First derivative of H_α.
have h_dHα : ∀ t, deriv H_α t = deriv H (t / α) / α := by
intro t
change deriv (fun s => H (s / α)) t = deriv H (t / α) / α
have hcomp : (fun s => H (s / α)) = H ∘ (fun s => s / α) := rfl
rw [hcomp, deriv_comp t (h_diff_H _) (h_diff_phi _)]
rw [show deriv (fun s : ℝ => s / α) t = 1 / α from by
rw [deriv_div_const]; simp]
ring
-- Second derivative of H_α.
have h_d2Hα : ∀ t, deriv (deriv H_α) t = deriv (deriv H) (t / α) / α ^ 2 := by
intro t
have h_eq : deriv H_α = fun t => deriv H (t / α) / α := by
funext t; exact h_dHα t
rw [h_eq]
change deriv (fun s => deriv H (s / α) / α) t = deriv (deriv H) (t / α) / α ^ 2
rw [deriv_div_const]
change deriv (fun s => deriv H (s / α)) t / α
= deriv (deriv H) (t / α) / α ^ 2
have hcomp : (fun s => deriv H (s / α)) = (deriv H) ∘ (fun s => s / α) := rfl
rw [hcomp, deriv_comp t (h_diff_H' _) (h_diff_phi _)]
rw [show deriv (fun s : ℝ => s / α) t = 1 / α from by
rw [deriv_div_const]; simp]
field_simp
rw [h_d2Hα 0, zero_div, h_d2]
field_simp
-- Apply the existing cosh classification.
have h_α_cosh : ∀ t, H_α t = Real.cosh t :=
dAlembert_cosh_solution_aczel H_α h_α_one h_α_cont h_α_dAlembert h_α_d2
-- Substitute t = α x to recover H.
intro x
have hkey : H (α * x / α) = Real.cosh (α * x) := h_α_cosh (α * x)
have h_cancel : α * x / α = x := by
field_simp
rw [h_cancel] at hkey
exact hkey
THEOREM aczel_kannappan_via_cases · IndisputableMonolith/Foundation/AxiomDischargePlan.lean
/-- **Aczél–Kannappan via the explicit reduction**: the discharge
puts the three cases together. We retain the conclusion's form to
match the original axiom. -/
theorem aczel_kannappan_via_cases
[AczelSmoothnessPackage]
(H : ℝ → ℝ) (h_cont : Continuous H) (h_one : H 0 = 1)
(h_dAlembert : ∀ x y, H (x + y) + H (x - y) = 2 * H x * H y)
(h_smooth : ContDiff ℝ ⊤ H) (h_deriv0 : deriv H 0 = 0)
(h_classification : (deriv (deriv H) 0 = 0)
∨ (∃ α : ℝ, 0 < α ∧ deriv (deriv H) 0 = α ^ 2)
∨ (∃ β : ℝ, 0 < β ∧ deriv (deriv H) 0 = -β ^ 2)) :
(∀ x, H x = 1) ∨
(∃ α : ℝ, ∀ x, H x = Real.cosh (α * x)) ∨
(∃ β : ℝ, ∀ x, H x = Real.cos (β * x)) := by
have h_smooth2 : ContDiff ℝ 2 H := h_smooth.of_le le_top
rcases h_classification with h0 | ⟨α, hα, hα2⟩ | ⟨β, hβ, hβ2⟩
· left
intro x
exact ode_constant_case H h_smooth2 h_one h_deriv0
(by
intro y
have hb := dAlembert_to_ODE_general H h_smooth h_dAlembert y
rw [h0] at hb; simpa using hb) x
· right; left
refine ⟨α, ?_⟩
intro x
exact cosh_rescaling_lemma H h_one h_cont h_dAlembert hα hα2 x
· right; right
refine ⟨β, ?_⟩
intro x
have h_bridge : ∀ y, deriv (deriv H) y = -β ^ 2 * H y := by
intro y
have hb := dAlembert_to_ODE_general H h_smooth h_dAlembert y
rw [hb, hβ2]
exact ode_cosine_case H h_smooth2 h_one h_deriv0 hβ h_bridge x
What this page does not claim
The lemma does not cover the cosine case, where the second derivative at zero is negative. The lemma does not assert that every d'Alembert solution is a hyperbolic cosine. The lemma does not claim anything about solutions that are not continuous or not twice differentiable.
Verify this page
Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:
$ lake env lean IndisputableMonolith/Foundation/AxiomDischargePlan.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)
A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.
Derived articles
This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:
- How does the framework's proof of the unit case, dAlembert_cosh_solution_aczel, establish that a continuous solution with H''(0) = 1 is exactly cosh?
- What is the full statement of the Aczél–Kannappan classification that this discharge plan replaces?
- How does the general ODE bridge dAlembert_to_ODE_general relate the second derivative at zero to the function's values everywhere?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM cosh_rescaling_lemma · IndisputableMonolith/Foundation/AxiomDischargePlan.lean
/-- **Cosh-rescaling lemma (proved)**: an arbitrary positive scaling factor on the time variable transforms a continuous d'Alembert solution with `H''(0) = α² > 0` into one with second derivative `1` at zero. The conclusion is handed off to `dAlembert_cosh_solution_aczel` already in the framework. -/ theorem cosh_rescaling_lemma [AczelSmoothnessPackage] (H : ℝ → ℝ) (h_one : H 0 = 1) (h_cont : Continuous H) (h_dAlembert : ∀ x y, H (x + y) + H (x - y) = 2 * H x * H y) {α : ℝ} (hα : 0 < α) (h_d2 : deriv (deriv H) 0 = α ^ 2) : ∀ x, H x = Real.cosh (α * x) := by -- Smoothness of H from the AczelSmoothnessPackage instance. have h_smooth_H : ContDiff ℝ ⊤ H := aczel_dAlembert_smooth H h_one h_cont h_dAlembert -- Define the rescaled function H_α(t) := H(t / α). set H_α : ℝ → ℝ := fun t => H (t / α) with hH_α_def have hα_ne : (α : ℝ) ≠ 0 := ne_of_gt hα -- (1) H_α(0) = 1. have h_α_one : H_α 0 = 1 := by show H (0 / α) = 1 rw [zero_div, h_one] -- (2) H_α continuous. have h_α_cont : Continuous H_α := h_cont.comp (continuous_id.div_const α) -- (3) H_α satisfies the d'Alembert equation. have h_α_dAlembert : ∀ x y, H_α (x + y) + H_α (x - y) = 2 * H_α x * H_α y := by intro x y show H ((x + y) / α) + H ((x - y) / α) = 2 * H (x / α) * H (y / α) rw [add_div, sub_div] exact h_dAlembert (x / α) (y / α) -- (4) H_α''(0) = 1: chain rule on H_α(t) = H(t/α). have h_α_d2 : deriv (deriv H_α) 0 = 1 := by -- H_α = H ∘ (·/α), so by chain rule: -- deriv H_α t = deriv H (t/α) / α -- deriv (deriv H_α) t = deriv (deriv H) (t/α) / α² -- At t = 0: H_α''(0) = H''(0) / α² = α²/α² = 1. have h_diff_H : Differentiable ℝ H := h_smooth_H.differentiable (by decide : (⊤ : WithTop ℕ∞) ≠ 0) have h_diff_H' : Differentiable ℝ (deriv H) := by have h_succ : (⊤ : WithTop ℕ∞) = 1 + ⊤ := rfl have hC2 : ContDiff ℝ (1 + ⊤) H := by rw [← h_succ]; exact h_smooth_H have hC1d : ContDiff ℝ ⊤ (deriv H) := (contDiff_succ_iff_deriv.mp hC2).2.2 exact hC1d.differentiable (by decide : (⊤ : WithTop ℕ∞) ≠ 0) have h_diff_phi : ∀ t, DifferentiableAt ℝ (fun x : ℝ => x / α) t := fun t => (differentiableAt_id).div_const α -- First derivative of H_α. have h_dHα : ∀ t, deriv H_α t = deriv H (t / α) / α := by intro t change deriv (fun s => H (s / α)) t = deriv H (t / α) / α have hcomp : (fun s => H (s / α)) = H ∘ (fun s => s / α) := rfl rw [hcomp, deriv_comp t (h_diff_H _) (h_diff_phi _)] rw [show deriv (fun s : ℝ => s / α) t = 1 / α from by rw [deriv_div_const]; simp] ring -- Second derivative of H_α. have h_d2Hα : ∀ t, deriv (deriv H_α) t = deriv (deriv H) (t / α) / α ^ 2 := by intro t have h_eq : deriv H_α = fun t => deriv H (t / α) / α := by funext t; exact h_dHα t rw [h_eq] change deriv (fun s => deriv H (s / α) / α) t = deriv (deriv H) (t / α) / α ^ 2 rw [deriv_div_const] change deriv (fun s => deriv H (s / α)) t / α = deriv (deriv H) (t / α) / α ^ 2 have hcomp : (fun s => deriv H (s / α)) = (deriv H) ∘ (fun s => s / α) := rfl rw [hcomp, deriv_comp t (h_diff_H' _) (h_diff_phi _)] rw [show deriv (fun s : ℝ => s / α) t = 1 / α from by rw [deriv_div_const]; simp] field_simp rw [h_d2Hα 0, zero_div, h_d2] field_simp -- Apply the existing cosh classification. have h_α_cosh : ∀ t, H_α t = Real.cosh t := dAlembert_cosh_solution_aczel H_α h_α_one h_α_cont h_α_dAlembert h_α_d2 -- Substitute t = α x to recover H. intro x have hkey : H (α * x / α) = Real.cosh (α * x) := h_α_cosh (α * x) have h_cancel : α * x / α = x := by field_simp rw [h_cancel] at hkey exact hkeyThe lemma states that if a continuous function H satisfies the d'Alembert equation, has H(0) = 1, and has a positive second derivative at zero, then H must equal the hyperbolic cosine of a scaled argument. cosh_rescaling_lemma · IndisputableMonolith/Foundation/AxiomDischargePlan.leanTHEOREM cosh_rescaling_lemma · IndisputableMonolith/Foundation/AxiomDischargePlan.lean
/-- **Cosh-rescaling lemma (proved)**: an arbitrary positive scaling factor on the time variable transforms a continuous d'Alembert solution with `H''(0) = α² > 0` into one with second derivative `1` at zero. The conclusion is handed off to `dAlembert_cosh_solution_aczel` already in the framework. -/ theorem cosh_rescaling_lemma [AczelSmoothnessPackage] (H : ℝ → ℝ) (h_one : H 0 = 1) (h_cont : Continuous H) (h_dAlembert : ∀ x y, H (x + y) + H (x - y) = 2 * H x * H y) {α : ℝ} (hα : 0 < α) (h_d2 : deriv (deriv H) 0 = α ^ 2) : ∀ x, H x = Real.cosh (α * x) := by -- Smoothness of H from the AczelSmoothnessPackage instance. have h_smooth_H : ContDiff ℝ ⊤ H := aczel_dAlembert_smooth H h_one h_cont h_dAlembert -- Define the rescaled function H_α(t) := H(t / α). set H_α : ℝ → ℝ := fun t => H (t / α) with hH_α_def have hα_ne : (α : ℝ) ≠ 0 := ne_of_gt hα -- (1) H_α(0) = 1. have h_α_one : H_α 0 = 1 := by show H (0 / α) = 1 rw [zero_div, h_one] -- (2) H_α continuous. have h_α_cont : Continuous H_α := h_cont.comp (continuous_id.div_const α) -- (3) H_α satisfies the d'Alembert equation. have h_α_dAlembert : ∀ x y, H_α (x + y) + H_α (x - y) = 2 * H_α x * H_α y := by intro x y show H ((x + y) / α) + H ((x - y) / α) = 2 * H (x / α) * H (y / α) rw [add_div, sub_div] exact h_dAlembert (x / α) (y / α) -- (4) H_α''(0) = 1: chain rule on H_α(t) = H(t/α). have h_α_d2 : deriv (deriv H_α) 0 = 1 := by -- H_α = H ∘ (·/α), so by chain rule: -- deriv H_α t = deriv H (t/α) / α -- deriv (deriv H_α) t = deriv (deriv H) (t/α) / α² -- At t = 0: H_α''(0) = H''(0) / α² = α²/α² = 1. have h_diff_H : Differentiable ℝ H := h_smooth_H.differentiable (by decide : (⊤ : WithTop ℕ∞) ≠ 0) have h_diff_H' : Differentiable ℝ (deriv H) := by have h_succ : (⊤ : WithTop ℕ∞) = 1 + ⊤ := rfl have hC2 : ContDiff ℝ (1 + ⊤) H := by rw [← h_succ]; exact h_smooth_H have hC1d : ContDiff ℝ ⊤ (deriv H) := (contDiff_succ_iff_deriv.mp hC2).2.2 exact hC1d.differentiable (by decide : (⊤ : WithTop ℕ∞) ≠ 0) have h_diff_phi : ∀ t, DifferentiableAt ℝ (fun x : ℝ => x / α) t := fun t => (differentiableAt_id).div_const α -- First derivative of H_α. have h_dHα : ∀ t, deriv H_α t = deriv H (t / α) / α := by intro t change deriv (fun s => H (s / α)) t = deriv H (t / α) / α have hcomp : (fun s => H (s / α)) = H ∘ (fun s => s / α) := rfl rw [hcomp, deriv_comp t (h_diff_H _) (h_diff_phi _)] rw [show deriv (fun s : ℝ => s / α) t = 1 / α from by rw [deriv_div_const]; simp] ring -- Second derivative of H_α. have h_d2Hα : ∀ t, deriv (deriv H_α) t = deriv (deriv H) (t / α) / α ^ 2 := by intro t have h_eq : deriv H_α = fun t => deriv H (t / α) / α := by funext t; exact h_dHα t rw [h_eq] change deriv (fun s => deriv H (s / α) / α) t = deriv (deriv H) (t / α) / α ^ 2 rw [deriv_div_const] change deriv (fun s => deriv H (s / α)) t / α = deriv (deriv H) (t / α) / α ^ 2 have hcomp : (fun s => deriv H (s / α)) = (deriv H) ∘ (fun s => s / α) := rfl rw [hcomp, deriv_comp t (h_diff_H' _) (h_diff_phi _)] rw [show deriv (fun s : ℝ => s / α) t = 1 / α from by rw [deriv_div_const]; simp] field_simp rw [h_d2Hα 0, zero_div, h_d2] field_simp -- Apply the existing cosh classification. have h_α_cosh : ∀ t, H_α t = Real.cosh t := dAlembert_cosh_solution_aczel H_α h_α_one h_α_cont h_α_dAlembert h_α_d2 -- Substitute t = α x to recover H. intro x have hkey : H (α * x / α) = Real.cosh (α * x) := h_α_cosh (α * x) have h_cancel : α * x / α = x := by field_simp rw [h_cancel] at hkey exact hkeyThe proof works by a change of variable, reducing the general positive case to the already-proved unit case. cosh_rescaling_lemma · IndisputableMonolith/Foundation/AxiomDischargePlan.leanTHEOREM aczel_kannappan_via_cases · IndisputableMonolith/Foundation/AxiomDischargePlan.lean
/-- **Aczél–Kannappan via the explicit reduction**: the discharge puts the three cases together. We retain the conclusion's form to match the original axiom. -/ theorem aczel_kannappan_via_cases [AczelSmoothnessPackage] (H : ℝ → ℝ) (h_cont : Continuous H) (h_one : H 0 = 1) (h_dAlembert : ∀ x y, H (x + y) + H (x - y) = 2 * H x * H y) (h_smooth : ContDiff ℝ ⊤ H) (h_deriv0 : deriv H 0 = 0) (h_classification : (deriv (deriv H) 0 = 0) ∨ (∃ α : ℝ, 0 < α ∧ deriv (deriv H) 0 = α ^ 2) ∨ (∃ β : ℝ, 0 < β ∧ deriv (deriv H) 0 = -β ^ 2)) : (∀ x, H x = 1) ∨ (∃ α : ℝ, ∀ x, H x = Real.cosh (α * x)) ∨ (∃ β : ℝ, ∀ x, H x = Real.cos (β * x)) := by have h_smooth2 : ContDiff ℝ 2 H := h_smooth.of_le le_top rcases h_classification with h0 | ⟨α, hα, hα2⟩ | ⟨β, hβ, hβ2⟩ · left intro x exact ode_constant_case H h_smooth2 h_one h_deriv0 (by intro y have hb := dAlembert_to_ODE_general H h_smooth h_dAlembert y rw [h0] at hb; simpa using hb) x · right; left refine ⟨α, ?_⟩ intro x exact cosh_rescaling_lemma H h_one h_cont h_dAlembert hα hα2 x · right; right refine ⟨β, ?_⟩ intro x have h_bridge : ∀ y, deriv (deriv H) y = -β ^ 2 * H y := by intro y have hb := dAlembert_to_ODE_general H h_smooth h_dAlembert y rw [hb, hβ2] exact ode_cosine_case H h_smooth2 h_one h_deriv0 hβ h_bridge xThis lemma, together with three other proved theorems, replaces that axiom with a finite combination of explicit, machine-checked results. aczel_kannappan_via_cases · IndisputableMonolith/Foundation/AxiomDischargePlan.lean