Paths of symplectic matrices, $\hat\rho$ , and the Conley–Zehnder and Maslov indices

Definition

ConleyZehnder_Setting

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

conley-zehnder-indexmaslov-indexsymplectic-geometrysymplectic-group

Objects for the Conley–Zehnder index of paths of symplectic matrices, following Gutt, §2.

Symplectic group. $\mathbb{R}^{2n}$ has coordinates $(q,p)$ and

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

$\mathrm{Sp}(2n)$ is the set of real $2n\times2n$ matrices with $AJ_0A^{\mathsf T}=J_0$ , and $\mathrm{Sp}^*(2n)=\{A\in\mathrm{Sp}(2n):\det(\mathrm{Id}-A)\neq0\}$ . 2. Paths. $\mathrm{SP}(n)$ is the set of continuous $\psi:[0,1]\to\mathrm{Sp}(2n)$ with $\psi(0)=\mathrm{Id}$ and $\psi(1)\in\mathrm{Sp}^*(2n)$ (Definition 4). A symplectic loop is a continuous $\varphi:[0,1]\to\mathrm{Sp}(2n)$ with $\varphi(0)=\varphi(1)=\mathrm{Id}$ . 3. Endpoints. $W^+=-\mathrm{Id}$ and $W^-=\mathrm{diag}(2,-1,\dots,-1,\tfrac12,-1,\dots,-1)$ . 4. Complex determinant. $C_A=\tfrac12(A-J_0AJ_0)=\begin{pmatrix}X&-Y\\Y&X\end{pmatrix}$ , $\det_{\mathbb C}C_A=\det(X+iY)$ , and $\hat\rho(A)=\det_{\mathbb C}C_A/|\det_{\mathbb C}C_A|$ (formula (9)). 5. Degree. A continuous $\theta:[0,1]\to\mathbb{R}$ is an argument of $f:[0,1]\to\mathbb{C}$ if $f(t)=e^{i\theta(t)}$ for all $t$ . An extension of $\psi\in\mathrm{SP}(n)$ is a path $\chi$ in $\mathrm{Sp}^*(2n)$ from $\psi(1)$ to $W^+$ or $W^-$ . The integer $k$ is a value of the index of $\psi$ if for some extension $\chi$ and arguments $\theta_1$ of $\hat\rho\circ\psi$ and $\theta_2$ of $\hat\rho\circ\chi$ ,

2\big((\theta_1(1)-\theta_1(0))+(\theta_2(1)-\theta_2(0))\big)=2\pi k,

i.e. $k=\deg(\hat\rho^2\circ\tilde\psi)$ for the concatenation $\tilde\psi$ of $\psi$ and $\chi$ . 6. Indices. $\mu_{CZ}(\psi)$ is such a value $k$ (Definition 7 in the form of Corollary 12), and the Maslov index $\mu(\varphi)$ of a loop is an integer $k$ with $\theta(1)-\theta(0)=2\pi k$ for an argument $\theta$ of $\hat\rho\circ\varphi$ . 7. Signature and block sum. $\mathrm{Sign}(S)$ is the number of positive minus the number of negative eigenvalues of a symmetric $S$ . $A'\diamond A''$ is the block embedding $\mathrm{Sp}(2n')\times\mathrm{Sp}(2n'')\to\mathrm{Sp}(2(n'+n''))$ , $(q',p')\oplus(q'',p'')\mapsto(q',q'',p',p'')$ . 8. The three characterizing properties for a map $\mu$ from paths to $\mathbb{Z}$ :

Homotopy: $\mu$ is constant on each connected component of $\mathrm{SP}(n)$ (compact-open topology).
Loop: $\mu(\varphi\psi)=\mu(\psi)+2\mu(\varphi)$ for every symplectic loop $\varphi$ and every $\psi\in\mathrm{SP}(n)$ .
Signature: $2\mu(t\mapsto\exp(tJ_0S))=\mathrm{Sign}(S)$ for every symmetric nondegenerate $S$ whose eigenvalues all have absolute value $<2\pi$ .

Formalization Note Matrices are indexed by Fin n ⊕ Fin n; $J_0$ is Matrix.J and $\mathrm{Sp}(2n)$ is Matrix.symplecticGroup. Paths are C(unitInterval, Mat n). czIndex and maslovIndex pick a value by choice and return $0$ if none exists; that the value exists and is unique is a separate theorem. Index maps are functions on all continuous paths, and the properties constrain them only on $\mathrm{SP}(n)$ .

Definition code

import Mathlib.LinearAlgebra.SymplecticGroup
import Mathlib.LinearAlgebra.Matrix.Block
import Mathlib.Analysis.Normed.Algebra.MatrixExponential
import Mathlib.Analysis.Matrix.Spectrum
import Mathlib.Analysis.SpecialFunctions.Complex.Circle
import Mathlib.Topology.Instances.Matrix
import Mathlib.Topology.ContinuousMap.Basic
import Mathlib.Topology.UnitInterval
import Mathlib.Topology.Connected.Basic
import Mathlib.Data.Real.Sign

/-!
# The Conley–Zehnder index of a path of symplectic matrices

Salamon–Zehnder (CPAM 45, 1992), §3; Salamon, *Lectures on Floer homology* (1999), §2.4;
in the form of Gutt, *Generalized Conley–Zehnder index*, Ann. Fac. Sci. Toulouse 23 (2014),
arXiv:1307.7239, §2: Definition 4 (`SP(n)`), Definition 7 with Corollary 12 (the index),
the Maslov index of a loop and the signature used in Proposition 8.

Conventions. `ℝ²ⁿ` is indexed by `Fin n ⊕ Fin n` (first block `q`, second block `p`).
`J₀ = [[0, -Id], [Id, 0]]` is Mathlib's `Matrix.J`. The symplectic group is Mathlib's
`Matrix.symplecticGroup`, `A J₀ Aᵀ = J₀`, which is the group `Sp(ℝ²ⁿ, Ω₀)`,
`Ω₀ = [[0, Id], [-Id, 0]] = -J₀`, of Gutt §2. Paths are continuous maps on `[0, 1]`.

The index is the degree of `ρ̂² ∘ ψ̃` (Gutt, Corollary 12, formula (8)), where `ψ̃` is `ψ`
followed by a path in `Sp*` ending at `W⁺` or `W⁻`, and `ρ̂(A)` is the normalized complex
determinant of the `ℂ`-linear part `½(A - J₀AJ₀)` (formula (9)). Under the identification
`(x, y) ↦ x + i y` of `ℝ²ⁿ` with `ℂⁿ`, `J₀` is multiplication by `i` and a real matrix
`[[X, -Y], [Y, X]]` is the complex matrix `X + i Y`.
-/

namespace ConleyZehnder

noncomputable section

open Matrix Classical

/-- Real `2n × 2n` matrices, indexed by `Fin n ⊕ Fin n`. -/
abbrev Mat (n : ℕ) := Matrix (Fin n ⊕ Fin n) (Fin n ⊕ Fin n) ℝ

/-- `J₀ = [[0, -Id], [Id, 0]]`. -/
abbrev J₀ (n : ℕ) : Mat n := Matrix.J (Fin n) ℝ

variable {n : ℕ}

/-- `A ∈ Sp(ℝ²ⁿ, Ω₀)`. -/
def IsSymplectic (A : Mat n) : Prop := A ∈ Matrix.symplecticGroup (Fin n) ℝ

/-- `Sp*(ℝ²ⁿ, Ω₀)`: symplectic matrices without eigenvalue `1`. -/
def SpStar (n : ℕ) : Set (Mat n) := {A | IsSymplectic A ∧ (1 - A).det ≠ 0}

/-- Gutt, Definition 4: `SP(n)`, the continuous paths `ψ : [0, 1] → Sp(ℝ²ⁿ, Ω₀)` with
`ψ(0) = Id` such that `1` is not an eigenvalue of `ψ(1)`. -/
def SP (n : ℕ) : Set C(unitInterval, Mat n) :=
  {ψ | (∀ t, IsSymplectic (ψ t)) ∧ ψ 0 = 1 ∧ (1 - ψ 1).det ≠ 0}

/-- A loop `φ : [0, 1] → Sp(ℝ²ⁿ, Ω₀)` with `φ(0) = φ(1) = Id`. -/
def IsSymplecticLoop (φ : C(unitInterval, Mat n)) : Prop :=
  (∀ t, IsSymplectic (φ t)) ∧ φ 0 = 1 ∧ φ 1 = 1

/-- `W⁺ = -Id`. -/
def Wplus (n : ℕ) : Mat n := -1

/-- `W⁻ = diag(2, -1, …, -1, 1/2, -1, …, -1)`. -/
def Wminus (n : ℕ) : Mat n :=
  Matrix.diagonal (Sum.elim (fun j : Fin n => if j.val = 0 then (2 : ℝ) else -1)
    (fun j : Fin n => if j.val = 0 then (1 / 2 : ℝ) else -1))

/-- The `ℂ`-linear part `C_A = ½(A - J₀ A J₀)` of `A`. -/
def complexLinearPart (A : Mat n) : Mat n := (1 / 2 : ℝ) • (A - J₀ n * A * J₀ n)

/-- `det_ℂ C_A`: writing `C_A = [[X, -Y], [Y, X]]`, the determinant of the complex
`n × n` matrix `X + i Y`. -/
def complexLinearDet (A : Mat n) : ℂ :=
  ((complexLinearPart A).toBlocks₁₁.map (fun x : ℝ => (x : ℂ)) +
    Complex.I • (complexLinearPart A).toBlocks₂₁.map (fun x : ℝ => (x : ℂ))).det

/-- Gutt (9): `ρ̂(A) = det_ℂ C_A / |det_ℂ C_A|`. -/
def rhoHat (A : Mat n) : ℂ := complexLinearDet A / (‖complexLinearDet A‖ : ℂ)

/-- `θ` is a continuous argument of `f : [0, 1] → S¹`: `f(t) = e^{i θ(t)}`. -/
def IsArgLift (f : unitInterval → ℂ) (θ : unitInterval → ℝ) : Prop :=
  Continuous θ ∧ ∀ t, f t = Complex.exp ((θ t : ℂ) * Complex.I)

/-- `χ` continues `ψ` as in Gutt §2: it starts at `ψ(1)`, stays in `Sp*`, and ends at
`W⁺` or `W⁻`. (The extension `ψ̃ : [0, 2] → Sp` is `ψ` followed by `χ`.) -/
def IsSpStarExtension (ψ χ : C(unitInterval, Mat n)) : Prop :=
  χ 0 = ψ 1 ∧ (∀ t, χ t ∈ SpStar n) ∧ (χ 1 = Wplus n ∨ χ 1 = Wminus n)

/-- `k = deg(ρ̂² ∘ ψ̃)` for some extension `ψ̃` of `ψ`: the total change of a continuous
argument of `ρ̂² ∘ ψ̃` along `ψ` followed by `χ` is `2π k`. -/
def IsCZValue (ψ : C(unitInterval, Mat n)) (k : ℤ) : Prop :=
  ∃ χ : C(unitInterval, Mat n), IsSpStarExtension ψ χ ∧
    ∃ θ₁ θ₂ : unitInterval → ℝ, IsArgLift (fun t => rhoHat (ψ t)) θ₁ ∧
      IsArgLift (fun t => rhoHat (χ t)) θ₂ ∧
      2 * ((θ₁ 1 - θ₁ 0) + (θ₂ 1 - θ₂ 0)) = 2 * Real.pi * k

/-- Gutt, Definition 7 / Corollary 12: the Conley–Zehnder index `μ_CZ(ψ) = deg(ρ̂² ∘ ψ̃)`. -/
def czIndex (ψ : C(unitInterval, Mat n)) : ℤ :=
  if h : ∃ k, IsCZValue ψ k then h.choose else 0

/-- `k = deg(ρ̂ ∘ φ)` for a loop `φ`. -/
def IsMaslovValue (φ : C(unitInterval, Mat n)) (k : ℤ) : Prop :=
  ∃ θ : unitInterval → ℝ, IsArgLift (fun t => rhoHat (φ t)) θ ∧ θ 1 - θ 0 = 2 * Real.pi * k

/-- The Maslov index `μ(φ) = deg(ρ̂ ∘ φ)` of a loop of symplectic matrices. -/
def maslovIndex (φ : C(unitInterval, Mat n)) : ℤ :=
  if h : ∃ k, IsMaslovValue φ k then h.choose else 0

/-- `Sign(S)`: the number of positive minus the number of negative eigenvalues of a
symmetric matrix, counted with multiplicity. -/
def signature (S : Mat n) (hS : S.IsHermitian) : ℤ :=
  ((Finset.univ.filter fun i => 0 < hS.eigenvalues i).card : ℤ) -
    ((Finset.univ.filter fun i => hS.eigenvalues i < 0).card : ℤ)

/-- The block-diagonal embedding `A' ⋄ A''` of `Sp(ℝ²ⁿ') × Sp(ℝ²ⁿ'')` into
`Sp(ℝ^{2(n'+n'')})`, `(q', p') ⊕ (q'', p'') ↦ (q', q'', p', p'')`. -/
def diamond {n' n'' : ℕ} (A : Mat n') (B : Mat n'') : Mat (n' + n'') :=
  Matrix.reindex
    ((Equiv.sumSumSumComm (Fin n') (Fin n') (Fin n'') (Fin n'')).trans
      (Equiv.sumCongr finSumFinEquiv finSumFinEquiv))
    ((Equiv.sumSumSumComm (Fin n') (Fin n') (Fin n'') (Fin n'')).trans
      (Equiv.sumCongr finSumFinEquiv finSumFinEquiv))
    (Matrix.fromBlocks A 0 0 B)

/-- (Homotopy) `μ` is constant on the connected components of `SP(n)`, a subspace of
`C([0, 1], ℝ^{2n×2n})` with the compact-open topology. -/
def HomotopyAxiom (μ : C(unitInterval, Mat n) → ℤ) : Prop :=
  ∀ ψ ∈ SP n, ∀ ψ' ∈ connectedComponentIn (SP n) ψ, μ ψ' = μ ψ

/-- (Loop) `μ(φψ) = μ(ψ) + 2 μ(φ)` for every loop `φ` at `Id` and every `ψ ∈ SP(n)`. -/
def LoopAxiom (μ : C(unitInterval, Mat n) → ℤ) : Prop :=
  ∀ φ, IsSymplecticLoop φ → ∀ ψ ∈ SP n, μ (φ * ψ) = μ ψ + 2 * maslovIndex φ

/-- (Signature) If `S = Sᵀ` is nondegenerate with all eigenvalues of absolute value
`< 2π` and `ψ(t) = exp(J₀ S t)`, then `μ(ψ) = ½ Sign(S)`. -/
def SignatureAxiom (μ : C(unitInterval, Mat n) → ℤ) : Prop :=
  ∀ (S : Mat n) (hS : S.IsHermitian), S.det ≠ 0 →
    (∀ i, |hS.eigenvalues i| < 2 * Real.pi) →
    ∀ ψ : C(unitInterval, Mat n), (∀ t, ψ t = NormedSpace.exp ((t : ℝ) • (J₀ n * S))) →
      2 * μ ψ = signature S hS

end

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), Section 2, pp. 5-9: Definition 4, Definition 7, Propositions 8-9, Corollary 12, formula (9); 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

Definition module (all definitions in one namespace, every $n\in\mathbb N$ allowed, including $n=0$ ).

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$ .

Symplectic. $A$ is symplectic iff $AJ_0A^{\mathsf T}=J_0$ .

$\mathrm{Sp}^*$ . $\mathrm{Sp}^*(n)$ is the set of symplectic $A\in\mathrm{Mat}_n$ with $\det(\mathrm{Id}-A)\neq 0$ .

$\mathrm{SP}(n)$ . $\mathrm{SP}(n)$ is the set of paths $\psi$ such that $\psi(t)$ is symplectic for every $t\in[0,1]$ , $\psi(0)=\mathrm{Id}$ , and $\det(\mathrm{Id}-\psi(1))\neq 0$ .

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

$W^\pm$ . $W^+=-\mathrm{Id}$ , and $W^-$ is the diagonal matrix whose $q$ -block diagonal is $(2,-1,\dots,-1)$ and whose $p$ -block diagonal is $(\tfrac12,-1,\dots,-1)$ (the entry $2$ resp. $\tfrac12$ sits at index $0$ ; all other diagonal entries are $-1$ ). For $n=0$ , $W^+=W^-$ is the empty matrix.

Complex-linear part, its determinant, and $\hat\rho$ . 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$ .

Argument lift. 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.)

Extension through $\mathrm{Sp}^*$ . For paths $\psi,\chi$ : $\chi$ is an extension of $\psi$ iff $\chi(0)=\psi(1)$ , $\chi(t)\in\mathrm{Sp}^*(n)$ for all $t$ , and $\chi(1)\in\{W^+,W^-\}$ .

CZ value. For a path $\psi$ and an integer $k$ , " $k$ is a CZ value of $\psi$ " means: there exist a path $\chi$ with $\chi(0)=\psi(1)$ , $\chi(t)\in\mathrm{Sp}^*(n)$ for all $t\in[0,1]$ , and $\chi(1)=W^+$ or $\chi(1)=W^-$ ; and argument lifts $\theta_1$ of $t\mapsto\hat\rho(\psi(t))$ and $\theta_2$ of $t\mapsto\hat\rho(\chi(t))$ with

2\big[(\theta_1(1)-\theta_1(0))+(\theta_2(1)-\theta_2(0))\big]=2\pi k.

(The lifts are of $\hat\rho$ itself, not of $\hat\rho^2$ ; the factor $2$ appears only in this equation. No condition $\psi\in\mathrm{SP}(n)$ is part of this notion.)

Conley–Zehnder index. The index $\mu_{CZ}(\psi)\in\mathbb Z$ of a path $\psi$ is defined as: if some integer $k$ is a CZ value of $\psi$ , then $\mu_{CZ}(\psi)$ is one such $k$ chosen by the axiom of choice (an unspecified one if several exist); if no CZ value exists, $\mu_{CZ}(\psi)=0$ . It is defined for every path, not only those in $\mathrm{SP}(n)$ .

Maslov value and Maslov index. For a path $\varphi$ and an integer $k$ , " $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$ . The Maslov index $\mu(\varphi)$ is a choice-selected such $k$ if one exists (an unspecified one if several exist), and $0$ otherwise; it is defined for every path, not only loops.

Signature. For a real symmetric matrix $S\in\mathrm{Mat}_n$ (symmetric = Hermitian over $\mathbb R$ ), let $\lambda_1,\dots,\lambda_{2n}$ be its real eigenvalues listed with multiplicity. $\mathrm{Sign}(S)$ is the number of indices $i$ with $\lambda_i>0$ minus the number with $\lambda_i<0$ . (The eigenvalue list is the one supplied by the spectral theorem for the given symmetry proof; the counts do not depend on that choice.)

Block sum $\diamond$ . For $A\in\mathrm{Mat}_{n'}$ and $B\in\mathrm{Mat}_{n''}$ , $A\diamond B\in\mathrm{Mat}_{n'+n''}$ is the matrix obtained from the block-diagonal matrix $\begin{pmatrix}A&0\\0&B\end{pmatrix}$ (indexed by $(q',p')$ then $(q'',p'')$ ) by relabeling indices so that the new $q$ -block is $(q'_0,\dots,q'_{n'-1},q''_0,\dots,q''_{n''-1})$ and the new $p$ -block is $(p'_0,\dots,p'_{n'-1},p''_0,\dots,p''_{n''-1})$ . Concretely, for $s,s'\in\{q,p\}$ : the $(s_k,s'_{l})$ entry of $A\diamond B$ is $A_{s_k,s'_l}$ if $k,l<n'$ , is $B_{s_{k-n'},s'_{l-n'}}$ if $k,l\ge n'$ , and is $0$ otherwise.

Homotopy property. A function $\mu$ from paths in $\mathrm{Mat}_n$ to $\mathbb Z$ satisfies the homotopy property if for every $\psi\in\mathrm{SP}(n)$ and every $\psi'$ in the connected component of $\psi$ in $\mathrm{SP}(n)$ (with the subspace topology inherited from the compact-open topology on paths), $\mu(\psi')=\mu(\psi)$ .

Loop property. $\mu$ satisfies the loop property if for every symplectic loop $\varphi$ and every $\psi\in\mathrm{SP}(n)$ ,

\mu(\varphi\psi)=\mu(\psi)+2\,\mu_{\mathrm{Maslov}}(\varphi),

where $(\varphi\psi)(t)=\varphi(t)\psi(t)$ and $\mu_{\mathrm{Maslov}}$ is the specific Maslov index defined above (not something derived from $\mu$ ).

Signature property. $\mu$ satisfies the signature property if for every real symmetric $S\in\mathrm{Mat}_n$ with $\det S\neq 0$ and all eigenvalues satisfying $|\lambda_i|<2\pi$ , and for every path $\psi$ with $\psi(t)=\exp(t\,J_0S)$ for all $t\in[0,1]$ (matrix exponential, $\exp(M)=\sum_{m\ge0}M^m/m!$ ), one has

2\,\mu(\psi)=\mathrm{Sign}(S).

Membership $\psi\in\mathrm{SP}(n)$ is not a hypothesis here. For $n=0$ the only such $S$ is the empty matrix ( $\det=1$ , $\mathrm{Sign}=0$ ), so the property demands $\mu(\psi)=0$ for the unique path.

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

Paths of symplectic matrices, ρ^\hat\rhoρ^​, and the Conley–Zehnder and Maslov indices

Paths of symplectic matrices, $\hat\rho$ , and the Conley–Zehnder and Maslov indices