stability_calibrated
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.