zero_defect_implies_cosh
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not supply error bounds when the defect is positive but small.
- Does not extend the equality beyond the interval [-T,T].
- Does not relax the C³ smoothness, evenness, or normalization assumptions.
- Does not apply if curvature is zero or negative.
formal statement (Lean)
347theorem zero_defect_implies_cosh
348 (H : ℝ → ℝ) (T : ℝ) (hyp : StabilityHypotheses H T)
349 (h_zero : UniformDefectBound H T 0)
350 (h_zero_hyp : ZeroDefectImpliesCoshHypothesis H T hyp) :
351 ∀ t : ℝ, |t| ≤ T → H t = Real.cosh (Real.sqrt hyp.curvature * t) := by
proof body
Term-mode proof.
352 exact h_zero_hyp h_zero
353
354/-- Zero defect + calibration a = 1 gives H = cosh exactly. -/