zero_defect_calibrated_implies_cosh
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish the identification for nonzero defect bounds.
- Does not relax the $C^3$ smoothness or evenness requirements.
- Does not extend the equality outside the interval $[-T,T]$.
- Does not treat curvature values other than one.
formal statement (Lean)
355theorem zero_defect_calibrated_implies_cosh
356 (H : ℝ → ℝ) (T : ℝ) (hyp : StabilityHypotheses H T)
357 (h_a1 : hyp.curvature = 1)
358 (h_zero : UniformDefectBound H T 0)
359 (h_zero_hyp : ZeroDefectImpliesCoshHypothesis H T hyp) :
360 ∀ t : ℝ, |t| ≤ T → H t = Real.cosh t := by
proof body
Term-mode proof.
361 intro t ht
362 have h := zero_defect_implies_cosh H T hyp h_zero h_zero_hyp t ht
363 simp only [h_a1, Real.sqrt_one, one_mul] at h
364 exact h
365
366end Stability
367end DAlembert
368end Foundation
369end IndisputableMonolith