The Schrödinger flow is a Kähler symplectomorphism

Category: 3-Local (The Schrödinger flow is a Kähler symplectomorphism).

This ties the pointwise Kähler form (Mathlib/Analysis/InnerProductSpace/KahlerForm.lean) to the Schrödinger pillar (schrodingerUnitary, LF4/ProjectedDynamics.lean): the deterministic quantum evolution exp(-itH) preserves the Fubini–Study Kähler structure — the metric g = re⟪·,·⟫ and the fundamental form ω = im⟪·,·⟫. So Schrödinger evolution is a symplectic isometry (a symplectomorphism) of the projective phase space — the Kibble / Ashtekar–Schilling picture of quantum mechanics as classical Hamiltonian mechanics on the Kähler manifold ℂℙ^{N-1}, at the pointwise/linear level.

The mechanism is elementary: exp(-itH) is unitary (schrodingerUnitary, expNegITH_unitary_group), so it preserves the Hermitian inner product (inner_toEuclideanLin_unitary), hence its real and imaginary parts g and ω.

Why this matters (and its honest scope)

This is the first rung of the geometric-QM statement "Schrödinger evolution is Hamiltonian flow on the Fubini–Study phase space" — the dynamics-preserves-the-form half. It connects, in one theorem, the Kähler form, the Schrödinger flow, and the geometric (Kibble/Ashtekar–Schilling) formulation. It is the form-level companion to the geometric phase / action (Aharonov–Anandan), whose primitive is the symplectic potential of ω.

It does NOT derive the flow FROM the form (the Hamiltonian-vector-field statement X_H = ω⁻¹dH, KG-2) — that needs the symplectic-gradient / manifold-differential API Mathlib lacks and stays blocked. This module proves the invariance (a symmetry of ω), not the generation. It is at the Hilbert-vector level; the descent to the ray-level FS form rides on the tangent-space J-invariance (Kahler.tangent_complexStructure_invariant).

noncomputable def CSD.LF4.schrodingerVectorFlow {N : ℕ} {H : Matrix (Fin N) (Fin N) ℂ} (hH : H.IsHermitian) (t : ℝ) (v : EuclideanSpace ℂ (Fin N)) : EuclideanSpace ℂ (Fin N)

The Schrödinger flow on the state vector. exp(-itH) acting on ψ ∈ ℂ^N, i.e. the deterministic unitary evolution schrodingerUnitary hH t applied as a linear map.

Equations

• CSD.LF4.schrodingerVectorFlow hH t v = (Matrix.toEuclideanLin ↑(CSD.LF4.schrodingerUnitary hH t)) v

theorem CSD.LF4.schrodingerVectorFlow_preserves_metric {N : ℕ} {H : Matrix (Fin N) (Fin N) ℂ} (hH : H.IsHermitian) (t : ℝ) (u v : EuclideanSpace ℂ (Fin N)) : Kahler.metric (schrodingerVectorFlow hH t u) (schrodingerVectorFlow hH t v) = Kahler.metric u v

Schrödinger evolution preserves the metric g. g (U_t u) (U_t v) = g u v for U_t = exp(-itH) — the flow is a g-isometry (it preserves the Fubini–Study Riemannian metric).

theorem CSD.LF4.schrodingerVectorFlow_preserves_fundamentalForm {N : ℕ} {H : Matrix (Fin N) (Fin N) ℂ} (hH : H.IsHermitian) (t : ℝ) (u v : EuclideanSpace ℂ (Fin N)) : Kahler.fundamentalForm (schrodingerVectorFlow hH t u) (schrodingerVectorFlow hH t v) = Kahler.fundamentalForm u v

Schrödinger evolution preserves the fundamental form ω. ω (U_t u) (U_t v) = ω u v for U_t = exp(-itH) — the flow is a symplectomorphism (it preserves the Fubini–Study symplectic form).

theorem CSD.LF4.schrodinger_flow_kahler_symplectomorphism {N : ℕ} {H : Matrix (Fin N) (Fin N) ℂ} (hH : H.IsHermitian) (t : ℝ) (u v : EuclideanSpace ℂ (Fin N)) : Kahler.metric (schrodingerVectorFlow hH t u) (schrodingerVectorFlow hH t v) = Kahler.metric u v ∧ Kahler.fundamentalForm (schrodingerVectorFlow hH t u) (schrodingerVectorFlow hH t v) = Kahler.fundamentalForm u v

Schrödinger evolution is a Kähler symplectomorphism. The deterministic flow exp(-itH) preserves BOTH the Fubini–Study metric g and the symplectic form ω: g (U_t u)(U_t v) = g u v and ω (U_t u)(U_t v) = ω u v. So quantum evolution is a symplectic isometry of the Kähler geometry of ℂℙ^{N-1} — the Kibble / Ashtekar–Schilling geometric picture (QM as Hamiltonian mechanics on the Fubini–Study phase space), at the pointwise/linear level. Ties the Kähler form to the Schrödinger pillar; the converse (flow generated BY the form, X_H = ω⁻¹dH, KG-2) needs the manifold symplectic-gradient API Mathlib lacks and stays blocked.