zero_defect_implies_cosh
plain-language theorem explainer
If H satisfies the stability hypotheses and the d'Alembert defect vanishes uniformly on [-T,T]^2, then H coincides exactly with cosh of sqrt(curvature) times t on that interval. Researchers deriving cost stability corollaries or uniqueness results for the shifted cost function cite this base case. The argument is a direct one-line application of the ZeroDefectImpliesCoshHypothesis to the zero bound.
Claim. Let $H : ℝ → ℝ$ and $T > 0$. Suppose $H$ is $C^3$, even, normalized by $H(0)=1$, with positive curvature $a = H''(0)$. If the d'Alembert defect satisfies $|Δ_H(t,u)| ≤ 0$ for all $|t|,|u| ≤ T$, then $H(t) = cosh(√a · t)$ for all $|t| ≤ T$.
background
The module develops quantitative stability for near-solutions of the d'Alembert equation $H(t+u) + H(t-u) = 2 H(t) H(u)$. The defect is defined as $Δ_H(t,u) := H(t+u) + H(t-u) - 2 H(t) H(u)$. StabilityHypotheses bundles $C^3$ smoothness on [-T,T], evenness, normalization $H(0)=1$, and positive curvature $a = H''(0)$. UniformDefectBound requires the defect to be at most ε uniformly on the square [-T,T]^2. Upstream, the shifted cost $H(x) = J(x) + 1 = ½(x + x^{-1})$ converts the Recognition Composition Law into the exact d'Alembert identity.
proof idea
The proof is a one-line wrapper that applies the ZeroDefectImpliesCoshHypothesis directly to the supplied zero defect bound.
why it matters
This result supplies the exact cosh solution when defect vanishes and is invoked by the downstream calibrated corollary zero_defect_calibrated_implies_cosh that fixes curvature to 1. It closes the base case in the stability estimates for the cost functional, linking the d'Alembert identity (derived from the Recognition Composition Law) to the uniqueness of the cosh form. The module cites the development in Washburn & Zlatanović on uniqueness of the canonical reciprocal cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.