Finite Holonomy Energy

Abstract

Finite stable swap curvature aggregates into a faithful nonnegative energy.

Theorem 1.1 (Finite Stable Holonomy Energy Bound).

$$\begin{array}{c}\forall K:\mathrm{Type},\iota :\mathrm{Type},[\mathrm{NormedField}(K)],[\mathrm{Fintype}(\iota )],\\ a:K,r:\iota \to K,v:\iota \to K,\epsilon :\mathbb{R},\\ (0\le \epsilon \wedge (\forall p:\iota ,\Vert v(p)\Vert \le 1)\wedge (\forall p:\iota ,\Vert r(p)\Vert \le \epsilon ))\Rightarrow \\ \mathrm{let}E:=\mathrm{stableResidualHolonomyEnergy}(a,r,v),\\ (0\le E\wedge \\ E\le {\mathrm{card}}_{\mathbb{R}}(\iota {)}^2\times (2\times \Vert (a-1)\Vert \times \epsilon +2\times {\epsilon }^2{)}^2\wedge \\ (E=0⟺\forall p,q:\iota ,\mathrm{stableResidualSwapCurvature}(a,r(p),r(q),v(p),v(q))=0)\wedge \\ (\epsilon =0\Rightarrow E=0)).\end{array}$$

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

Source. Repository-derived.

Commentary.

For a finite carrier, assume every channel has norm at most one and every residual norm is bounded by a common nonnegative envelope. The stable residual holonomy energy is nonnegative and is at most the square of the carrier cardinality times the squared pairwise residual bound.

The energy is zero exactly when every ordered-pair stable residual swap curvature is zero, and a zero envelope forces zero energy. These claims concern only the finite unnormalized sum; they assert no residual decay, infinite-prime limit, or spectral-energy comparison.

References

• Truth anchor: D5/S3/Observer/AgencyHolonomy/FiniteHolonomyEnergy.finite_stable_holonomy_energy_bound
• Dependency: D5/S3/Observer/AgencyHolonomy/StableResidualSwapCurvatureBound