Existence and Stability of Hopf Solitons in the Faddeev-Niemi Model

Abstract

We prove that the Faddeev-Niemi action E_FN[n] = ∫_(ℝ³)(κ₂|∇n|² + (κ₄)/(2)|F[n]|²) d³x on the energy space of finite-energy maps n:ℝ³→ S² admits a smooth, exponentially-localised, dynamically stable critical point in every non-trivial Hopf class H∈π₃(S²)∖{0}. The proof combines the direct method of the calculus of variations, Lions' concentration-compactness principle to prevent loss of topological charge at infinity, the Vakulenko-Kapitanski topological lower bound to guarantee coercivity, polyconvex lower-semicontinuity in the sense of Ball, and elliptic bootstrap regularity. The minimiser saturates the Vakulenko-Kapitanski inequality in scaling, and its Hessian is non-negative with kernel of dimension at least six, corresponding to translations and rotations. The full proof is formally verified in Lean 4 (Mathlib v4.29.0) across eight modules, ~2,500 lines, with zero `sorry` axioms (snapshot of 2026-04-25: 84 axioms, 35 theorems, 0 sorry, per Paper CXXIII §6) — to our knowledge the first formal verification of a soliton existence proof for a topologically constrained continuum field theory on ℝ³. The result improves the variational existence theorem of Lin and Yang [LY04] by establishing full smoothness, exponential decay, dynamical stability, and a machine-checked formalisation. The formalisation imports a finite catalogue of well-known mathematical results (polyconvex lower-semicontinuity à la Ball, Schauder bootstrap, Agmon decay, Persson's essential-spectrum bound, the Lin-Yang strict-subadditivity inequality) as Type-1 axioms, in the sense of Paper CXXIII.