StabilityBounds
StabilityBounds packages the uniform bounds on defect ε, function magnitude B, and third derivative K that control the error for near-solutions of the d'Alembert equation on a symmetric interval. Analysts working on functional-equation stability or Recognition Science cost derivations cite the record when they invoke the quantitative transfer from H to J. The declaration is realized as a structure whose fields directly supply the hypotheses of the stability theorem together with the auxiliary error function δ(h).
claimLet $H:ℝ→ℝ$ and $T>0$. A structure StabilityBounds$(H,T)$ consists of constants $ε≥0$, $B>0$, $K≥0$ together with the assertions that $|Δ_H(t,u)|≤ε$ for all $|t|,|u|≤T$, $|H(t)|≤B$ for $|t|≤T$, and $|H'''(t)|≤K$ for $|t|≤T$, where $Δ_H(t,u):=H(t+u)+H(t-u)-2H(t)H(u)$.
background
The d'Alembert functional equation reads $H(t+u)+H(t-u)=2H(t)H(u)$. Its defect is defined by $Δ_H(t,u):=H(t+u)+H(t-u)-2H(t)H(u)$. In Recognition Science the shifted cost $H(x)=J(x)+1$ converts the Recognition Composition Law into this equation. UniformDefectBound $H$ $T$ $ε$ asserts that the defect remains bounded by $ε$ throughout the square $[-T,T]^2$. The module develops quantitative stability: when the defect is small and $H$ is $C^3$, $H$ stays close to the hyperbolic-cosine solution with explicit error controlled by the supplied bounds.
proof idea
The declaration is a structure that directly records the three independent bounds together with their sign conditions. The auxiliary function δ_error is defined by the explicit formula $ε/h^2+(1+B)Kh/3$. Its positivity lemma follows from a one-line calculation that applies div_pos to the first term and the positivity tactic to the second, then closes with linarith.
why it matters in Recognition Science
StabilityBounds supplies the concrete constants that appear in the hypotheses of dAlembert_stability and the cost-stability corollaries cost_stability_transfer and cost_stability_calibrated. It closes the quantitative step between the defect bound and the ODE approximation $|H''-aH|≤δ(h)$, which in turn feeds the transfer to the cost functional. Within the framework this realizes the stability half of the uniqueness argument for the canonical cost, linking back to J-uniqueness at T5 of the forcing chain.
scope and limits
- Does not derive the curvature parameter a.
- Does not prove the stability estimate itself.
- Does not assume any specific functional form for H beyond the three bounds.
- Does not extend the bounds outside the interval [-T,T].
- Does not connect to the phi-ladder or mass formula.
formal statement (Lean)
129structure StabilityBounds (H : ℝ → ℝ) (T : ℝ) where
130 /-- Uniform defect bound: |Δ_H(t,u)| ≤ ε for |t|,|u| ≤ T -/
131 ε : ℝ
132 ε_nonneg : 0 ≤ ε
133 defect_bound : UniformDefectBound H T ε
134 /-- Uniform bound on |H|: |H(t)| ≤ B for |t| ≤ T -/
135 B : ℝ
136 B_pos : 0 < B
137 H_bound : ∀ t : ℝ, |t| ≤ T → |H t| ≤ B
138 /-- Uniform bound on |H'''|: |H'''(t)| ≤ K for |t| ≤ T -/
139 K : ℝ
140 K_nonneg : 0 ≤ K
141 H'''_bound : ∀ t : ℝ, |t| ≤ T → |iteratedDeriv 3 H t| ≤ K
142
143/-! ## The δ(h) Error Function -/
144
145/-- The error bound function δ(h) from Theorem 7.1.
146
147For step size h > 0, the local error is controlled by:
148 δ(h) := ε/h² + (1+B)·K·h/3
proof body
Definition body.
149
150where:
151- ε is the defect bound
152- B is the H-bound
153- K is the H'''-bound -/
154noncomputable def δ_error (ε B K h : ℝ) : ℝ :=
155 ε / h^2 + (1 + B) * K * h / 3
156
157/-- δ(h) is positive when ε, K, h > 0 and B ≥ 0. -/
158lemma δ_error_pos (ε B K h : ℝ) (hε : 0 < ε) (hB : 0 ≤ B) (hK : 0 ≤ K) (hh : 0 < h) :
159 0 < δ_error ε B K h := by
160 unfold δ_error
161 have h1 : 0 < ε / h^2 := div_pos hε (pow_pos hh 2)
162 have h2 : 0 ≤ (1 + B) * K * h / 3 := by positivity
163 linarith
164
165/-- Optimal choice of h minimizes δ(h).
166
167Taking dδ/dh = 0 gives: -2ε/h³ + (1+B)K/3 = 0
168Solving: h³ = 6ε/((1+B)K), so h = (6ε/((1+B)K))^{1/3}
169
170This gives δ(h_opt) ~ O(ε^{1/3}) -/