AczelSecondDerivativeIdentity
plain-language theorem explainer
The declaration defines the second-derivative identity extracted from a smooth Aczél equation on the log-cost function G. Analysts of continuous route-independence combiners in the generalized d'Alembert setting cite it when isolating the relation between G''(t) and G''(0) via an auxiliary function ψ. It is introduced directly as a named Prop that encodes the condition without further derivation.
Claim. For a function $G : ℝ → ℝ$, the second-derivative identity holds if there exists a function $ψ : ℝ → ℝ$ such that $2 G''(t) = ψ(G(t)) · G''(0)$ for all real $t$.
background
The GeneralizedDAlembert module relaxes the polynomial-degree-≤2 restriction on the route-independence combiner P to continuity alone, invoking the Aczél–Kannappan classification of continuous solutions to the d'Alembert equation. The log-cost is reparametrized via G(t) = F(exp t) from the upstream Cost.FunctionalEquation.G definition. The identity isolates the second-derivative extraction, with ψ understood as morally ∂₂P(u,0) per the module doc-comment.
proof idea
This is a definition that directly states the extracted identity ∃ ψ, ∀ t, 2 * deriv (deriv G) t = ψ (G t) * deriv (deriv G) 0. No lemmas or tactics are applied; the body is the complete content of the definition.
why it matters
It supplies the named analysis input 2a (ContinuousCombinerSecondDerivativeInput) that feeds ContinuousCombinerPsiAffineCompletion and the quartic counterexample theorem. The definition supports the module goal of embedding the Aczél–Kannappan classification to replace the polynomial hypothesis with continuity in the Law-of-Logic pipeline. It touches the open question whether the quartic-log obstruction persists under weaker smoothness assumptions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.