StabilityHypotheses
plain-language theorem explainer
StabilityHypotheses bundles the C³ regularity, evenness, normalization H(0)=1, positive second derivative at zero, and positive interval length T for functions satisfying the d'Alembert equation. Researchers applying quantitative stability bounds near cosh(√a t) or transferring estimates to the cost functional cite this bundle as the standard hypothesis set. The declaration is a plain structure definition with six fields that downstream theorems invoke directly.
Claim. For a map $H:ℝ→ℝ$ and $T>0$, the hypotheses require $H$ to be $C^3$ on $[-T,T]$, $H$ even, $H(0)=1$, $H''(0)=a$ for some $a>0$, and $T>0$.
background
The module formalizes stability estimates for near-solutions of the d'Alembert functional equation $H(t+u)+H(t-u)=2H(t)H(u)$. The defect is defined as $Δ_H(t,u):=H(t+u)+H(t-u)-2H(t)H(u)$. Upstream, the shifted cost $H(x)=J(x)+1$ from CostAlgebra converts the Recognition Composition Law into this d'Alembert identity, with $J$ the unique solution fixed by the forcing chain.
proof idea
The declaration is a structure definition that collects the six listed properties with no reduction steps or lemmas applied.
why it matters
This bundle serves as the entry point for the main stability theorem (dAlembert_stability, Theorem 7.1) and its corollaries on cost stability transfer and calibrated bounds. It supplies the local hypotheses needed to connect the d'Alembert equation to the Recognition Science cost functional via $F(x)=H(log x)-1$, supporting the uniqueness results for the canonical reciprocal cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.