Stable Residual Swap Curvature Bound

Abstract

Stable swap curvature is linear-quadratic in residual local factors.

Definition 1.1 (Stable residual swap curvature).

Lean statement: D5/S3/Observer/AgencyHolonomy/StableResidualSwapCurvatureBound.stableResidualSwapCurvature

Formalization. D5/S3/Observer/AgencyHolonomy/StableResidualSwapCurvatureBound.stableResidualSwapCurvature (✓ std3).

Source. Repository-derived.

Commentary.

Write the two scalar local factors as one plus their residuals and their stable-channel memory injections as residual times channel. This definition is the adjacent-swap defect of those two lifted updates.

Theorem 1.2 (Residual factors control stable swap curvature).

$$\begin{array}{c}\forall K:NormedField,a,r_p,r_q,v_p,v_q:K,\\ (\Vert v_p\Vert \le 1\wedge \Vert v_q\Vert \le 1)\Rightarrow \\ C_{st}(a,r_p,r_q,v_p,v_q)=(a-1)\cdot (r_p\cdot v_p-r_q\cdot v_q)+r_p\cdot r_q\cdot (v_q-v_p)\wedge \\ \Vert C_{st}(a,r_p,r_q,v_p,v_q)\Vert \le \Vert (a-1)\Vert \cdot (\Vert r_p\Vert +\Vert r_q\Vert )+2\cdot \Vert r_p\Vert \cdot \Vert r_q\Vert \wedge \\ (\forall \epsilon :\mathbb{R},(0\le \epsilon \wedge \Vert r_p\Vert \le \epsilon \wedge \Vert r_q\Vert \le \epsilon )\Rightarrow \Vert C_{st}(a,r_p,r_q,v_p,v_q)\Vert \le 2\cdot \Vert (a-1)\Vert \cdot \epsilon +2\cdot {\epsilon }^2).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/AgencyHolonomy/StableResidualSwapCurvatureBound.stable_residual_swap_curvature_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

Over any normed field, assume the two channel coordinates have norm at most one. Expanding the adjacent-swap defect gives one term linear in the residuals and one bilinear correction.

The triangle inequality and multiplicativity of the field norm bound the linear term by the sum of the two residual norms and the channel difference by two.

If both residual norms are bounded by a common nonnegative envelope, the defect is at most two times the stable gap times that envelope, plus twice its square. No decay of the envelope is assumed here.

References

• Truth anchor: D5/S3/Observer/AgencyHolonomy/StableResidualSwapCurvatureBound.stableResidualSwapCurvature
• Truth anchor: D5/S3/Observer/AgencyHolonomy/StableResidualSwapCurvatureBound.stable_residual_swap_curvature_bound