The Maslov index $\deg(\hat\rho\circ\varphi)$ of a symplectic loop is well defined

Proved

ConleyZehnder.maslovValue_existsUnique

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

conley-zehnder-indexmaslov-indexsymplectic-geometrysymplectic-group

Let $\varphi:[0,1]\to\mathrm{Sp}(2n)$ be continuous with $\varphi(0)=\varphi(1)=\mathrm{Id}$ . There is exactly one integer $k$ such that some continuous argument $\theta$ of $\hat\rho\circ\varphi$ satisfies

\theta(1)-\theta(0)=2\pi k .

This integer is the Maslov index $\mu(\varphi)$ appearing in the loop property.

Preamble

import Definitions.Def_ConleyZehnder_Setting

Formal statement

namespace ConleyZehnder

/-- The Maslov index of a loop is well defined: every loop `φ` of symplectic
matrices at `Id` has a unique degree `deg(ρ̂ ∘ φ)`. -/
theorem maslovValue_existsUnique {n : ℕ} (φ : C(unitInterval, Mat n))
    (hφ : IsSymplecticLoop φ) : ∃! k : ℤ, IsMaslovValue φ k := by sorry

end ConleyZehnder

Source

Gutt, Generalized Conley-Zehnder index, Ann. Fac. Sci. Toulouse Math. 23 (2014) 907-932, https://doi.org/10.5802/afst.1430 (arXiv:1307.7239), Proposition 8 (5), p. 7 (Maslov index of a loop); Salamon, Lectures on Floer homology, IAS/Park City Math. Ser. 7 (1999) 143-229, https://doi.org/10.1090/pcms/007/05

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Throughout, for a natural number $n$ (including $n=0$ ), $\mathrm{Mat}_n$ denotes the real $2n\times 2n$ matrices whose rows and columns are indexed by two copies of $\{0,\dots,n-1\}$ : a first (" $q$ ") block and a second (" $p$ ") block. $\mathrm{Id}$ is the identity matrix. $J_0\in\mathrm{Mat}_n$ is the block matrix

J_0=\begin{pmatrix}0&-\mathrm{Id}\\ \mathrm{Id}&0\end{pmatrix}.

A matrix $A$ is called symplectic if $A\,J_0\,A^{\mathsf T}=J_0$ . A path is a continuous map $[0,1]\to\mathrm{Mat}_n$ (with the usual Euclidean topology on matrix entries); the set of paths carries the compact-open topology (equivalently the topology of uniform convergence). Products, inverses and transposes of paths below are always taken pointwise in $t$ . For $n=0$ all matrices are the empty $0\times 0$ matrix, whose determinant is $1$ .

A symplectic loop is a path $\varphi$ with $\varphi(t)$ symplectic for every $t$ and $\varphi(0)=\varphi(1)=\mathrm{Id}$ .

For $A\in\mathrm{Mat}_n$ , let $C_A=\tfrac12\,(A-J_0AJ_0)$ . Let $X$ be the upper-left ( $q$ -row, $q$ -column) $n\times n$ block of $C_A$ and $Y$ its lower-left ( $p$ -row, $q$ -column) block, and set

d(A)=\det{}_{\mathbb C}\,(X+iY)\in\mathbb C,

the determinant of the complex $n\times n$ matrix $X+iY$ (equal to $1$ when $n=0$ ). Then

\hat\rho(A)=\frac{d(A)}{|d(A)|}\in\mathbb C,

with the convention that division by zero gives $0$ , so $\hat\rho(A)=0$ whenever $d(A)=0$ .

For a function $f:[0,1]\to\mathbb C$ , a function $\theta:[0,1]\to\mathbb R$ is called an argument lift of $f$ if $\theta$ is continuous and $f(t)=e^{i\theta(t)}$ for every $t\in[0,1]$ . (No lift exists if $|f(t)|\neq 1$ for some $t$ , e.g. if $\hat\rho$ takes the junk value $0$ ; continuity of $f$ is not separately assumed.)

For a path $\varphi$ and $k\in\mathbb Z$ , " $k$ is a Maslov value of $\varphi$ " means there is an argument lift $\theta$ of $t\mapsto\hat\rho(\varphi(t))$ with $\theta(1)-\theta(0)=2\pi k$ .

Claim. For every $n\in\mathbb N$ and every symplectic loop $\varphi$ in $\mathrm{Mat}_n$ , there is exactly one integer $k$ that is a Maslov value of $\varphi$ (existence of a lift with $\theta(1)-\theta(0)\in2\pi\mathbb Z$ , and uniqueness of that integer across all lifts).

Human review

Endorsed by Shuze Chen · Oct 9, 2026
Confirmed by the moderator at approval.
Endorsed by Mazecto · Oct 9, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

The Maslov index deg⁡(ρ^∘φ)\deg(\hat\rho\circ\varphi)deg(ρ^​∘φ) of a symplectic loop is well defined

The Maslov index $\deg(\hat\rho\circ\varphi)$ of a symplectic loop is well defined