ode_constant_case
A twice continuously differentiable real function H with H(0)=1, H'(0)=0 and H'' identically zero must be the constant function 1. This uniqueness result is invoked in the case analysis that discharges the Aczél–Kannappan functional equation for d'Alembert solutions. The argument first shows the first derivative is constant via the zero second derivative, then forces it to vanish at zero and concludes constancy of H.
claimLet $H : ℝ → ℝ$ be twice continuously differentiable. If $H(0) = 1$, $H'(0) = 0$ and $H''(x) = 0$ for all $x ∈ ℝ$, then $H(x) = 1$ for all $x$.
background
The AxiomDischargePlan module reduces the classical axiom aczel_kannappan_continuous_dAlembert to prior theorems by splitting on the sign of the second derivative at zero. The shifted cost H(x) = J(x) + 1 converts the Recognition Composition Law into the d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y). The constant case corresponds to the subcase H'' ≡ 0, which must be shown to force the trivial solution H ≡ 1 under the given initial conditions.
proof idea
The term proof first extracts differentiability of H and of deriv H from the ContDiff hypothesis. It applies is_const_of_deriv_eq_zero to deriv H using the hypothesis that its derivative vanishes identically, yielding that deriv H is constant. Specializing at zero with the initial condition forces deriv H ≡ 0. A second application of the same lemma to H itself shows H is constant, after which the value H(0) = 1 finishes the claim.
why it matters in Recognition Science
This result supplies the constant-case branch inside aczel_kannappan_via_cases, which together with cosh_rescaling_lemma completes the discharge of the Aczél–Kannappan axiom. It isolates the trivial fixed point of the J-cost functional equation and aligns with the T5 uniqueness step in the forcing chain. The lemma ensures no other smooth solutions exist when the second derivative vanishes, closing one of the three analytic cases required for the full classification.
scope and limits
- Does not apply without the C² smoothness hypothesis.
- Does not cover cases where the second derivative is nonzero anywhere.
- Does not extend to discontinuous or non-real-valued functions.
- Does not supply quantitative bounds or convergence rates.
formal statement (Lean)
44theorem ode_constant_case
45 (H : ℝ → ℝ) (h_smooth : ContDiff ℝ 2 H)
46 (h_one : H 0 = 1) (h_deriv0 : deriv H 0 = 0)
47 (h_d2_zero : ∀ x, deriv (deriv H) x = 0) :
48 ∀ x, H x = 1 := by
proof body
Term-mode proof.
49 -- Step 1: H is differentiable.
50 have hDiffH : Differentiable ℝ H :=
51 h_smooth.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
52 -- Step 2: deriv H is differentiable.
53 have hC2 : ContDiff ℝ 2 H := h_smooth
54 have hC2eq : (2 : WithTop ℕ∞) = 1 + 1 := rfl
55 rw [hC2eq] at hC2
56 rw [contDiff_succ_iff_deriv] at hC2
57 have hC1_dH : ContDiff ℝ 1 (deriv H) := hC2.2.2
58 have hDiff_dH : Differentiable ℝ (deriv H) :=
59 hC1_dH.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
60 -- Step 3: deriv H is globally constant (its derivative is everywhere 0).
61 have h_dH_const : ∀ x y, deriv H x = deriv H y :=
62 is_const_of_deriv_eq_zero hDiff_dH h_d2_zero
63 -- Step 4: deriv H is identically 0.
64 have h_dH_zero : ∀ x, deriv H x = 0 := fun x => by
65 rw [h_dH_const x 0, h_deriv0]
66 -- Step 5: H is globally constant.
67 have h_H_const : ∀ x y, H x = H y :=
68 is_const_of_deriv_eq_zero hDiffH h_dH_zero
69 -- Step 6: H ≡ H 0 = 1.
70 intro x
71 rw [h_H_const x 0, h_one]
72
73/-- **Zero uniqueness for `f'' = -f`**: if `f(0)=0` and `f'(0)=0`,
74then `f ≡ 0`. Proof by conservation of the energy
75`E(t) = f(t)^2 + f'(t)^2`. -/