The Hamiltonian vector field on a Hermitian space: X_H = ω⁻¹ dH, linear level

Category: 1-Mathlib (CSD-free upstream candidate).

This is BACKLOG A4's formalisable fragment. A4 is the manifold identification X_𝓗 = ω⁻¹d𝓗 — the arrow from a scalar observable to the flow that generates measurement dynamics. Mathlib has no symplectic-form or Poisson API on manifolds (verified again 2026-08-06: Analysis/Calculus/DifferentialForm/ now delivers the exterior derivative on normed spaces — flat space — with manifold forms explicitly TODO upstream). What IS formalisable today is the identification on the flat Hermitian model E, where the Fubini–Study form's pointwise value is Kahler.fundamentalForm (KahlerForm.lean) and a single global chart covers everything:

• hamiltonianVectorFieldOf w = -(J w) — the ω-dual of the covector g w ·. The name is earned by the theorem, not asserted: fundamentalForm_hamiltonianVectorFieldOf proves ω (X w) v = g w v for every v, which is exactly the defining equation ι_X ω = dH once w is the g-representative (gradient) of dH.
• ★ hamiltonian_duality — X_H = ω⁻¹dH for an arbitrary observable: if dH at x is g-represented by w, then ω (hamiltonianVectorFieldOf w) · = dH ·.
• quadraticEnergy A x = ½ g x (A x) — the quantum energy observable ½⟨x, Ax⟩ of a symmetric operator, with hasFDerivAt_quadraticEnergy/fderiv_quadraticEnergy computing its differential: dH_A(x) = g (A x) ·.
• ★★ quadraticEnergy_hamiltonian_duality — the two combined: the Hamiltonian vector field of the quantum energy is -(i • A x) — the Schrödinger vector field. This is the Kibble/Ashtekar–Schilling statement "Schrödinger evolution is Hamiltonian flow for the Fubini–Study symplectic structure" at the linear level, as a theorem.

Honest scope

The manifold statement — ω as a closed 2-form on ℂℙ^{N-1} (or the product arena), X_𝓗 as a vector field on the quotient, the flow generated through charts — remains the §2a boundary: Mathlib's differential forms stop at normed spaces today. This module is to A4 what ChartBracket.lean is to A3: the honest fragment on a model where every object is total and explicit, with the transport to the arena manifold carried as prose. Nothing here claims dω = 0 (on flat space it is the closedness of a constant form and is now formalisable via extDeriv — recorded, not landed) or the global quotient statement.

References

specs/BACKLOG.md A4, A3 (ChartBracket.lean — the Darboux-chart Poisson fragment this complements); KahlerForm.lean (fundamentalForm, metric, complexStructure — the pointwise Kähler triple this consumes); SigmaLayer/SchrodingerKahlerInvariance.lean (KG-2's invariance half: the flow preserves ω; this module is the generation half's linear fragment: the flow is generated by ω); specs/reconstruction-status.md §2a.

def Kahler.hamiltonianVectorFieldOf {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (w : E) : E

The Hamiltonian vector field of a gradient representative: the ω-dual -(J w) of the covector g w ·. fundamentalForm_hamiltonianVectorFieldOf is the defining equation ι_X ω = g w ·; feed it the gradient of an observable (hamiltonian_duality) and it reads ι_X ω = dH — the identification X_H = ω⁻¹ dH with no inverse ever formed.

Equations

• Kahler.hamiltonianVectorFieldOf w = -Kahler.complexStructure w

theorem Kahler.fundamentalForm_hamiltonianVectorFieldOf {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (w v : E) : fundamentalForm (hamiltonianVectorFieldOf w) v = metric w v

The ω-duality: ω (X w) v = g w v. In Kähler-triple terms, ω(-Jw, ·) = g(w, ·) — the algebraic core of X_H = ω⁻¹ dH.

theorem Kahler.hamiltonian_duality {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (H : E → ℝ) {x w : E} (hw : HasFDerivAt H (Complex.reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ ((innerSL ℂ) w)) x) (v : E) : fundamentalForm (hamiltonianVectorFieldOf w) v = (fderiv ℝ H x) v

★ X_H = ω⁻¹ dH, linear level, arbitrary observable. If the differential of H : E → ℝ at x is g-represented by w (i.e. dH x v = re ⟪w, v⟫ — w is the gradient), then the fundamental form pairs the Hamiltonian vector field against any direction to give exactly the differential: ι_{X_H} ω = dH.

The quantum energy observable and its differential

noncomputable def Kahler.quadraticEnergy {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (x : E) : ℝ

The quadratic (quantum) energy of an operator: H_A(x) = ½ g x (A x) = ½ re⟪x, Ax⟫ — the expectation value of A in the state x, the observable whose Hamiltonian flow is Schrödinger evolution.

Equations

• Kahler.quadraticEnergy A x = 1 / 2 * Kahler.metric x (A x)

theorem Kahler.hasFDerivAt_quadraticEnergy {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (hA : ∀ (u v : E), inner ℂ (A u) v = inner ℂ u (A v)) (x : E) : HasFDerivAt (quadraticEnergy A) (Complex.reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ ((innerSL ℂ) (A x))) x

The differential of the quadratic energy of a symmetric operator: dH_A(x) = g (A x) · — the gradient of the energy is A x.

theorem Kahler.fderiv_quadraticEnergy {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (hA : ∀ (u v : E), inner ℂ (A u) v = inner ℂ u (A v)) (x : E) : fderiv ℝ (quadraticEnergy A) x = Complex.reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ ((innerSL ℂ) (A x))

theorem Kahler.quadraticEnergy_hamiltonian_duality {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (hA : ∀ (u v : E), inner ℂ (A u) v = inner ℂ u (A v)) (x v : E) : fundamentalForm (hamiltonianVectorFieldOf (A x)) v = (fderiv ℝ (quadraticEnergy A) x) v

★★ The Schrödinger vector field is Hamiltonian: for a symmetric operator A, the ω-dual of the quadratic energy's differential at x is hamiltonianVectorFieldOf (A x) = -(i • A x) — the generator of exp(-itA). X_{H_A} = ω⁻¹ dH_A, with everything explicit and no inverse formed: this is the Kibble/Ashtekar–Schilling "Schrödinger evolution is Hamiltonian flow" at the linear level.