stability_calibrated
When the curvature parameter equals 1 under standard Recognition Science calibration, the d'Alembert stability bound reduces to |H(t) - cosh t| ≤ δ_error(ε, B, K, h) ⋅ (cosh |t| - 1) for |t| ≤ T - h. Researchers modeling the shifted cost functional would cite this result to obtain explicit approximation control once the general estimate is specialized. The proof is a one-line wrapper that applies the general StabilityEstimate and simplifies under the curvature assumption.
claimLet $H : ℝ → ℝ$ be $C^3$ and even with $H(0) = 1$ and $H''(0) = 1$. Let $ε, B, K$ be the uniform bounds on the defect, $|H|$, and $|H'''|$ over $[-T, T]$. Then for any $h$ with $0 < h ≤ T$ and all $t$ with $|t| ≤ T - h$, $|H(t) - cosh t| ≤ δ_error(ε, B, K, h) ⋅ (cosh |t| - 1)$.
background
The module formalizes stability estimates for near-solutions of the d'Alembert equation $H(t+u) + H(t-u) = 2 H(t) H(u)$. The defect $Δ_H(t,u)$ measures deviation from this identity. StabilityHypotheses packages the standing assumptions: $H$ is $C^3$ on $[-T,T]$, even, normalized by $H(0)=1$, and has positive curvature $a = H''(0)$. StabilityBounds collects the uniform defect bound $ε$, the function bound $B$, and the third-derivative bound $K$. The general StabilityEstimate then asserts closeness of $H$ to $cosh(√a t)$ with error proportional to $(cosh(√a |t|) - 1)$. Upstream, the shifted cost $H(x) = J(x) + 1$ converts the Recognition Composition Law into the d'Alembert equation.
proof idea
The proof introduces $t$ under the hypothesis $|t| ≤ T - h$, invokes the general stability estimate at the given curvature, and simplifies the resulting expression by substituting the assumption that curvature equals 1 together with the identities $√1 = 1$ and division by one.
why it matters in Recognition Science
This declaration specializes the general d'Alembert stability theorem to the curvature value 1 that appears in the Recognition Science calibration of the cost functional. It supplies the concrete error bound required when transferring stability from the functional equation to the $J$-cost via the shift $H = J + 1$. The parent development is the cost stability corollary in the paper on uniqueness of the canonical reciprocal cost. It closes the step between the abstract estimate and the cosh approximation used in the forcing chain from T5 (J-uniqueness) onward.
scope and limits
- Does not establish existence of solutions, only quantitative closeness given a defect bound.
- Does not extend the bound beyond the interval |t| ≤ T - h.
- Does not remove the C³ smoothness assumption on H.
- Does not supply bounds when curvature differs from 1.
formal statement (Lean)
301theorem stability_calibrated
302 (H : ℝ → ℝ) (T : ℝ) (hyp : StabilityHypotheses H T)
303 (h_a1 : hyp.curvature = 1)
304 (bounds : StabilityBounds H T)
305 (h_stab : StabilityEstimate H T hyp.curvature bounds)
306 (h : ℝ) (hh_pos : 0 < h) (hh_le : h ≤ T) :
307 ∀ t : ℝ, |t| ≤ T - h →
308 |H t - Real.cosh t| ≤ δ_error bounds.ε bounds.B bounds.K h * (Real.cosh |t| - 1) := by
proof body
Term-mode proof.
309 intro t ht
310 have h_main := h_stab h hh_pos hh_le t ht
311 simp only [h_a1, Real.sqrt_one, one_mul, div_one] at h_main
312 exact h_main
313
314/-- When a = 1, the cost stability simplifies to |F(x) - J(x)| ≤ δ · J(x). -/