pith. sign in
theorem

ode_constant_case

proved
show as:
module
IndisputableMonolith.Foundation.AxiomDischargePlan
domain
Foundation
line
44 · github
papers citing
3 papers (below)

plain-language theorem explainer

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.

Claim. Let $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

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.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.

papers checked against this theorem (showing 3 of 3)