Homotopy, loop and signature determine the Conley–Zehnder index
ProvedConleyZehnder.czIndex_uniqueLet assign an integer to each path and suppose that on it has the homotopy property (constant on connected components of ), the loop property ( for every symplectic loop at ) and the signature property ( for symmetric nondegenerate with all eigenvalues of absolute value ). Then
import Definitions.Def_ConleyZehnder_Setting
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
Read-back
What the Lean code literally says, in plain math · claude-opus-5-5
Throughout, for a natural number (including ), denotes the real matrices whose rows and columns are indexed by two copies of : a first ("") block and a second ("") block. is the identity matrix. is the block matrix
A matrix is called symplectic if . A path is a continuous map (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 . For all matrices are the empty matrix, whose determinant is .
is the set of paths such that is symplectic for every , , and .
is the set of symplectic with .
A symplectic loop is a path with symplectic for every and .
, and is the diagonal matrix whose -block diagonal is and whose -block diagonal is (the entry resp. sits at index ; all other diagonal entries are ). For , is the empty matrix.
For , let . Let be the upper-left (-row, -column) block of and its lower-left (-row, -column) block, and set
the determinant of the complex matrix (equal to when ). Then
with the convention that division by zero gives , so whenever .
For a function , a function is called an argument lift of if is continuous and for every . (No lift exists if for some , e.g. if takes the junk value ; continuity of is not separately assumed.)
For a path and an integer , " is a CZ value of " means: there exist a path with , for all , and or ; and argument lifts of and of with
(The lifts are of itself, not of ; the factor appears only in this equation. No condition is part of this notion.)
The index of a path is defined as: if some integer is a CZ value of , then is one such chosen by the axiom of choice (an unspecified one if several exist); if no CZ value exists, . It is defined for every path, not only those in .
For a path and an integer , " is a Maslov value of " means: there is an argument lift of with . The Maslov index is a choice-selected such if one exists (an unspecified one if several exist), and otherwise; it is defined for every path, not only loops.
For a real symmetric matrix (symmetric = Hermitian over ), let be its real eigenvalues listed with multiplicity. is the number of indices with minus the number with .
A function from paths in to satisfies the homotopy property if for every and every in the connected component of in (with the subspace topology inherited from the compact-open topology on paths), .
satisfies the loop property if for every symplectic loop and every ,
where and is the specific Maslov index defined above (not something derived from ).
satisfies the signature property if for every real symmetric with and all eigenvalues satisfying , and for every path with for all (matrix exponential, ), one has
Membership is not a hypothesis here. For the only such is the empty matrix (, ), so the property demands for the unique path.
Claim. Let and let be any function from all paths in to that has the homotopy, loop and signature properties. Then for every ,
(Nothing is asserted about paths outside .)
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.