Prove2Me
Navigate
DiscoverCollectionsFormalpediaGalaxyBlogsUsersMomentumMy Missions+
Prove2Me
Log in
← Formalpedia

Homotopy, loop and signature determine the Conley–Zehnder index

Proved
ConleyZehnder.czIndex_unique

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

conley-zehnder-indexmaslov-indexsymplectic-geometrysymplectic-group

Let μ\muμ assign an integer to each path and suppose that on SP(n)\mathrm{SP}(n)SP(n) it has the homotopy property (constant on connected components of SP(n)\mathrm{SP}(n)SP(n)), the loop property (μ(φψ)=μ(ψ)+2μ(φ)\mu(\varphi\psi)=\mu(\psi)+2\mu(\varphi)μ(φψ)=μ(ψ)+2μ(φ) for every symplectic loop φ\varphiφ at Id\mathrm{Id}Id) and the signature property (μ(t↦exp⁡(tJ0S))=12Sign(S)\mu(t\mapsto\exp(tJ_0S))=\tfrac12\mathrm{Sign}(S)μ(t↦exp(tJ0​S))=21​Sign(S) for symmetric nondegenerate SSS with all eigenvalues of absolute value <2π<2\pi<2π). Then

μ(ψ)=μCZ(ψ)for every ψ∈SP(n).\mu(\psi)=\mu_{CZ}(\psi)\qquad\text{for every }\psi\in\mathrm{SP}(n).μ(ψ)=μCZ​(ψ)for every ψ∈SP(n).
Preamble
import Definitions.Def_ConleyZehnder_Setting
Formal statement
namespace ConleyZehnder

/-- Gutt, Proposition 9: the homotopy, loop and signature properties characterize the
Conley–Zehnder index: every `μ : SP(n) → ℤ` with these properties equals `μ_CZ` on `SP(n)`. -/
theorem czIndex_unique {n : ℕ} (μ : C(unitInterval, Mat n) → ℤ) (hH : HomotopyAxiom μ)
    (hL : LoopAxiom μ) (hS : SignatureAxiom μ) (ψ : C(unitInterval, Mat n)) (hψ : ψ ∈ SP n) :
    μ ψ = czIndex ψ := 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 9, p. 7; 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 nnn (including n=0n=0n=0), Matn\mathrm{Mat}_nMatn​ denotes the real 2n×2n2n\times 2n2n×2n matrices whose rows and columns are indexed by two copies of {0,…,n−1}\{0,\dots,n-1\}{0,…,n−1}: a first ("qqq") block and a second ("ppp") block. Id\mathrm{Id}Id is the identity matrix. J0∈MatnJ_0\in\mathrm{Mat}_nJ0​∈Matn​ is the block matrix

J0=(0−IdId0).J_0=\begin{pmatrix}0&-\mathrm{Id}\\ \mathrm{Id}&0\end{pmatrix}.J0​=(0Id​−Id0​).

A matrix AAA is called symplectic if A J0 AT=J0A\,J_0\,A^{\mathsf T}=J_0AJ0​AT=J0​. A path is a continuous map [0,1]→Matn[0,1]\to\mathrm{Mat}_n[0,1]→Matn​ (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 ttt. For n=0n=0n=0 all matrices are the empty 0×00\times 00×0 matrix, whose determinant is 111.

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

Sp∗(n)\mathrm{Sp}^*(n)Sp∗(n) is the set of symplectic A∈MatnA\in\mathrm{Mat}_nA∈Matn​ with det⁡(Id−A)≠0\det(\mathrm{Id}-A)\neq 0det(Id−A)=0.

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

W+=−IdW^+=-\mathrm{Id}W+=−Id, and W−W^-W− is the diagonal matrix whose qqq-block diagonal is (2,−1,…,−1)(2,-1,\dots,-1)(2,−1,…,−1) and whose ppp-block diagonal is (12,−1,…,−1)(\tfrac12,-1,\dots,-1)(21​,−1,…,−1) (the entry 222 resp. 12\tfrac1221​ sits at index 000; all other diagonal entries are −1-1−1). For n=0n=0n=0, W+=W−W^+=W^-W+=W− is the empty matrix.

For A∈MatnA\in\mathrm{Mat}_nA∈Matn​, let CA=12 (A−J0AJ0)C_A=\tfrac12\,(A-J_0AJ_0)CA​=21​(A−J0​AJ0​). Let XXX be the upper-left (qqq-row, qqq-column) n×nn\times nn×n block of CAC_ACA​ and YYY its lower-left (ppp-row, qqq-column) block, and set

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

the determinant of the complex n×nn\times nn×n matrix X+iYX+iYX+iY (equal to 111 when n=0n=0n=0). Then

ρ^(A)=d(A)∣d(A)∣∈C,\hat\rho(A)=\frac{d(A)}{|d(A)|}\in\mathbb C,ρ^​(A)=∣d(A)∣d(A)​∈C,

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

For a function f:[0,1]→Cf:[0,1]\to\mathbb Cf:[0,1]→C, a function θ:[0,1]→R\theta:[0,1]\to\mathbb Rθ:[0,1]→R is called an argument lift of fff if θ\thetaθ is continuous and f(t)=eiθ(t)f(t)=e^{i\theta(t)}f(t)=eiθ(t) for every t∈[0,1]t\in[0,1]t∈[0,1]. (No lift exists if ∣f(t)∣≠1|f(t)|\neq 1∣f(t)∣=1 for some ttt, e.g. if ρ^\hat\rhoρ^​ takes the junk value 000; continuity of fff is not separately assumed.)

For a path ψ\psiψ and an integer kkk, "kkk is a CZ value of ψ\psiψ" means: there exist a path χ\chiχ with χ(0)=ψ(1)\chi(0)=\psi(1)χ(0)=ψ(1), χ(t)∈Sp∗(n)\chi(t)\in\mathrm{Sp}^*(n)χ(t)∈Sp∗(n) for all t∈[0,1]t\in[0,1]t∈[0,1], and χ(1)=W+\chi(1)=W^+χ(1)=W+ or χ(1)=W−\chi(1)=W^-χ(1)=W−; and argument lifts θ1\theta_1θ1​ of t↦ρ^(ψ(t))t\mapsto\hat\rho(\psi(t))t↦ρ^​(ψ(t)) and θ2\theta_2θ2​ of t↦ρ^(χ(t))t\mapsto\hat\rho(\chi(t))t↦ρ^​(χ(t)) with

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

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

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

For a path φ\varphiφ and an integer kkk, "kkk is a Maslov value of φ\varphiφ" means: there is an argument lift θ\thetaθ of t↦ρ^(φ(t))t\mapsto\hat\rho(\varphi(t))t↦ρ^​(φ(t)) with θ(1)−θ(0)=2πk\theta(1)-\theta(0)=2\pi kθ(1)−θ(0)=2πk. The Maslov index μ(φ)\mu(\varphi)μ(φ) is a choice-selected such kkk if one exists (an unspecified one if several exist), and 000 otherwise; it is defined for every path, not only loops.

For a real symmetric matrix S∈MatnS\in\mathrm{Mat}_nS∈Matn​ (symmetric = Hermitian over R\mathbb RR), let λ1,…,λ2n\lambda_1,\dots,\lambda_{2n}λ1​,…,λ2n​ be its real eigenvalues listed with multiplicity. Sign(S)\mathrm{Sign}(S)Sign(S) is the number of indices iii with λi>0\lambda_i>0λi​>0 minus the number with λi<0\lambda_i<0λi​<0.

A function μ\muμ from paths in Matn\mathrm{Mat}_nMatn​ to Z\mathbb ZZ satisfies the homotopy property if for every ψ∈SP(n)\psi\in\mathrm{SP}(n)ψ∈SP(n) and every ψ′\psi'ψ′ in the connected component of ψ\psiψ in SP(n)\mathrm{SP}(n)SP(n) (with the subspace topology inherited from the compact-open topology on paths), μ(ψ′)=μ(ψ)\mu(\psi')=\mu(\psi)μ(ψ′)=μ(ψ).

μ\muμ satisfies the loop property if for every symplectic loop φ\varphiφ and every ψ∈SP(n)\psi\in\mathrm{SP}(n)ψ∈SP(n),

μ(φψ)=μ(ψ)+2 μMaslov(φ),\mu(\varphi\psi)=\mu(\psi)+2\,\mu_{\mathrm{Maslov}}(\varphi),μ(φψ)=μ(ψ)+2μMaslov​(φ),

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

μ\muμ satisfies the signature property if for every real symmetric S∈MatnS\in\mathrm{Mat}_nS∈Matn​ with det⁡S≠0\det S\neq 0detS=0 and all eigenvalues satisfying ∣λi∣<2π|\lambda_i|<2\pi∣λi​∣<2π, and for every path ψ\psiψ with ψ(t)=exp⁡(t J0S)\psi(t)=\exp(t\,J_0S)ψ(t)=exp(tJ0​S) for all t∈[0,1]t\in[0,1]t∈[0,1] (matrix exponential, exp⁡(M)=∑m≥0Mm/m!\exp(M)=\sum_{m\ge0}M^m/m!exp(M)=∑m≥0​Mm/m!), one has

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

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

Claim. Let n∈Nn\in\mathbb Nn∈N and let μ\muμ be any function from all paths in Matn\mathrm{Mat}_nMatn​ to Z\mathbb ZZ that has the homotopy, loop and signature properties. Then for every ψ∈SP(n)\psi\in\mathrm{SP}(n)ψ∈SP(n),

μ(ψ)=μCZ(ψ).\mu(\psi)=\mu_{CZ}(\psi).μ(ψ)=μCZ​(ψ).

(Nothing is asserted about paths outside SP(n)\mathrm{SP}(n)SP(n).)

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

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paperProve2Me Team
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me