Angle defect of a symplectic period cocycle

Proved

BirkhoffGlobalSection.variational_cocycle_angle_defect_symplectic

by Sneed · Sep 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

dynamical-systemssymplectic-geometry

For a symplectic period cocycle, the shifted ambient increment agrees with the base increment up to one turn.

Let $Y(t)$ be the identity-normalized variational flow along a trajectory, satisfying the cocycle identity $Y(t+T) = Y(t)Y(T)$ , and assume each $Y(t)$ is symplectic. Let $\alpha$ be a continuous ambient rotation angle, so that $\det(Y(t)_{\mathbb C}) = \rho(t)(\cos\alpha(t) + i\sin\alpha(t))$ with $\rho > 0$ . Then

\alpha(a+T)-\alpha(a) \le \alpha(T)-\alpha(0)+2\pi \qquad\text{for every }a.

The cocycle identity makes the shifted variational flow conjugate to the base flow, so the two determinant paths differ only by the branch choice. This is the analytic core of shift stability with the ODE infrastructure factored out as hypotheses.

Formalization Note Symplecticity is stated as preservation of $\omega(u,v) = u \cdot Jv$ with the quaternionic matrix $J$ (TangentialHessian.qI). This is the explicit-symplecticity variant of BirkhoffGlobalSection.variational_cocycle_angle_defect; the periodicity hypothesis is retained for the intended application although only the cocycle identity is used.

Preamble

import Definitions.Def_BirkhoffGlobalSection_AmbientRotation

Formal statement

namespace BirkhoffGlobalSection

theorem variational_cocycle_angle_defect_symplectic
    (F : Phase → ℝ) (x : ℝ → Phase) (T : ℝ)
    (hper : ∀ t : ℝ, x (t + T) = x t)
    (Y : ℝ → (Phase →L[ℝ] Phase))
    (hY : IsHamiltonianVariationalSolution F x Y)
    (hcocycle : ∀ t : ℝ, Y (t + T) = (Y t).comp (Y T))
    (hsymp : ∀ t : ℝ, ∀ u v : Phase,
      (Y t) u ⬝ᵥ TangentialHessian.qI.mulVec ((Y t) v) =
        u ⬝ᵥ TangentialHessian.qI.mulVec v)
    (α : ℝ → ℝ) (hα : IsAmbientRotationAngle Y α) :
    ∀ a : ℝ, α (a + T) - α a ≤ α T - α 0 + 2 * Real.pi := by sorry

end BirkhoffGlobalSection

Source

Joung-van Koert, Section 2.3, https://arxiv.org/html/2407.19159v3; Gutt, Generalized Conley-Zehnder index, https://arxiv.org/pdf/1307.7239, Corollary 12. Explicit-symplecticity variant of BirkhoffGlobalSection.variational_cocycle_angle_defect.

View graph