ZeroDefectImpliesCoshHypothesis
plain-language theorem explainer
Zero defect on the d'Alembert equation forces H to coincide exactly with the scaled hyperbolic cosine whose curvature matches H''(0). Stability analysts in the Recognition Science program cite this interface when discharging the exact-solution case of the d'Alembert stability theorem. The declaration is a direct definition of the required implication, serving as a named placeholder until the proof is supplied.
Claim. Let $H : ℝ → ℝ$ and $T > 0$. Assume $H$ is $C^3$, even, satisfies $H(0) = 1$, and has positive curvature $a = H''(0)$. If the d'Alembert defect vanishes uniformly on $[-T,T]^2$, then $H(t) = cosh(√a · t)$ for all $|t| ≤ T$.
background
The d'Alembert functional equation is $H(t+u) + H(t-u) = 2 H(t) H(u)$. Its defect is $Δ_H(t,u) := H(t+u) + H(t-u) - 2 H(t) H(u)$. UniformDefectBound H T 0 asserts that this defect is identically zero on the square $[-T,T]^2$ (see the sibling definition at line 110). StabilityHypotheses packages the standing assumptions: $H$ is $C^3$ on $[-T,T]$, even, normalized by $H(0)=1$, and has positive second derivative $a$ at the origin (structure at line 114). This local setting arises from the Recognition Composition Law applied to the shifted cost $H = J + 1$, which converts the RCL into the exact d'Alembert identity (CostAlgebra.H and FunctionalEquation.H).
proof idea
The declaration is a definition whose body is the implication itself. It directly encodes UniformDefectBound H T 0 → ∀ t, |t|≤T → H t = cosh(√(hyp.curvature) t). No tactics or lemmas are applied inside the definition; it functions as a named hypothesis interface that downstream theorems discharge by exact application.
why it matters
The interface supplies the zero-defect case for the d'Alembert stability theorem (Module_DOC, Theorem 7.1). It is invoked verbatim by zero_defect_implies_cosh and zero_defect_calibrated_implies_cosh, which in turn feed the uniqueness results for the cost function J. In the broader chain this closes the exact-solution step that links to T5 (J-uniqueness via cosh(log x) - 1) and the eight-tick octave structure. It touches the open scaffolding task of proving the full stability theorem without extra hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.