Prove2Me

The graph determinant is multiplicative on Sp(4)Sp(4) up to a factor in the slit plane

Proved
HryniewiczCriterion.graphBasis4_det_mul_ratio_mem_slitPlane

by Mazecto · Oct 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

hamiltonian-dynamicssymplectic-geometry

Let g1,g2g_1,g_2 be real 4×44\times4 matrices preserving the standard symplectic form ω0\omega_0, and let δ(g)=det⁡(graphBasis4 g)\delta(g)=\det(\texttt{graphBasis4}\ g) be the graph determinant. Then δ(g1)≠0\delta(g_1)\neq0, δ(g2)≠0\delta(g_2)\neq0, and

4 δ(g1g2)δ(g1) δ(g2)∈C∖(−∞,0].\frac{4\,\delta(g_1g_2)}{\delta(g_1)\,\delta(g_2)}\in\mathbb{C}\setminus(-\infty,0].

So δ\delta is multiplicative on the symplectic group up to a factor that never meets the negative real axis. Along continuous paths of symplectic matrices, the principal argument of this factor is therefore continuous. This is the quasimorphism property of the Maslov rotation function, and it lets one compare determinant angles of products of symplectic paths without a homotopy argument.

Preamble
import Definitions.Def_HryniewiczCriterion_GraphAngle

open HryniewiczCriterion
open scoped ContDiff
Formal statement
theorem HryniewiczCriterion.graphBasis4_det_mul_ratio_mem_slitPlane (g₁ g₂ : Matrix (Fin 4) (Fin 4) ℝ)
    (h₁ : ∀ u v : R4, omega0 (g₁.mulVec u) (g₁.mulVec v) = omega0 u v)
    (h₂ : ∀ u v : R4, omega0 (g₂.mulVec u) (g₂.mulVec v) = omega0 u v) :
    (graphBasis4 g₁).det ≠ 0 ∧ (graphBasis4 g₂).det ≠ 0 ∧
      4 * (graphBasis4 (g₁ * g₂)).det / ((graphBasis4 g₁).det * (graphBasis4 g₂).det) ∈
        Complex.slitPlane := by sorry
Source
Standard estimate behind the quasimorphism property of the Maslov rotation function on the symplectic group (cf. McDuff–Salamon, Introduction to Symplectic Topology, Section 2.2); stated and proved here in the coordinates of `graphBasis4`. Used for the determinant angle in Hofer–Wysocki–Zehnder, The dynamics on three-dimensional strictly convex energy surfaces, Ann. of Math. 148 (1998), https://doi.org/10.2307/120994, Theorem 3.4, pp. 219–222.

View graph