The normalized complex determinant of a symplectic 2×2 matrix with positive trace has positive real part

Proved

ConleyZehnder.rhoHat_re_pos_of_trace_pos

by Mazecto · Nov 2, 2026 · Mathlib 0df444a (Lean v4.33.1)

conley-zehnder-indexsymplectic-geometry

Let $A\in\mathrm{Sp}(2)$ with $\operatorname{tr}A>0$ . Then $\operatorname{Re}\hat\rho(A)>0$ , where $\hat\rho(A)=\det_{\mathbb C}C_A/|\det_{\mathbb C}C_A|$ is the normalized complex determinant of the complex-linear part $C_A=\tfrac12(A-J_0AJ_0)$ .

This locates the argument of $\hat\rho$ for symplectic matrices with positive trace, for example along paths of positive hyperbolic matrices.

Formalization Note $A$ is ConleyZehnder.Mat 1 with ConleyZehnder.IsSymplectic A, and $\hat\rho$ is ConleyZehnder.rhoHat.

Preamble

import Definitions.Def_ConleyZehnder_Setting

Formal statement

namespace ConleyZehnder

/-- For a symplectic `2 × 2` matrix with positive trace, `ρ̂` has positive real part. -/
theorem rhoHat_re_pos_of_trace_pos (A : Mat 1) (hA : IsSymplectic A) (htr : 0 < A.trace) :
    0 < (rhoHat A).re := by
  sorry

end ConleyZehnder

Source

J. Gutt, Generalized Conley–Zehnder index, Ann. Fac. Sci. Toulouse Math. 23 (2014), arXiv:1307.7239, Section 2 (auxiliary lemma)

View graph