zero_defect_calibrated_implies_cosh
plain-language theorem explainer
When the d'Alembert defect vanishes uniformly and the curvature parameter equals one, H coincides exactly with cosh on [-T,T]. Researchers studying functional equations or the Recognition Science cost functional cite this specialization of the zero-defect case. The proof is a one-line wrapper that instantiates zero_defect_implies_cosh and simplifies the curvature factor via sqrt(1)=1.
Claim. Let $H:ℝ→ℝ$ and $T>0$. Suppose $H$ is $C^3$, even, normalized by $H(0)=1$, with curvature $H''(0)=1$. If the d'Alembert defect vanishes uniformly on $[-T,T]^2$, then $H(t)=cosh(t)$ for all $|t|≤T$.
background
The module develops stability estimates for near-solutions of the d'Alembert 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)$. StabilityHypotheses bundles the standing assumptions: $H$ is $C^3$ on $[-T,T]$, even, $H(0)=1$, and curvature $H''(0)=a>0$. UniformDefectBound states that $|Δ_H(t,u)|≤ε$ whenever $|t|,|u|≤T$. ZeroDefectImpliesCoshHypothesis encodes the implication from zero defect to the exact cosh form scaled by $sqrt(a)$. Upstream, the CostAlgebra definition $H(x)=J(x)+1$ converts the Recognition Composition Law into the d'Alembert identity.
proof idea
The proof is a one-line wrapper. It introduces $t$ under the bound $|t|≤T$, applies the general lemma zero_defect_implies_cosh to obtain equality with cosh of the scaled argument, then uses the hypothesis curvature=1 together with the simplifications sqrt(1)=1 and one_mul to reach cosh(t).
why it matters
This declaration supplies the exact unit-curvature identification required by the d'Alembert stability theory in the Recognition Science development. It specializes the general zero-defect implication to the canonical cosh solution that arises from the J-uniqueness step (T5) in the forcing chain, where $H(x)=(x+x^{-1})/2$ recovers cosh after logarithmic reparametrization. The result closes the calibrated case inside the stability estimates and supports transfer to the cost functional F.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.