The curvature formula for the geometric phase

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #54, brick BP-3 of specs/berry-phase-scoping.md.

Let Ψ : ℝ × ℝ → E be a C² family of unit vectors on the rectangle [0, 1] × [0, T], thought of as a disc in polar form: the edge s = 0 is collapsed to a point (Ψ (0, t) = Ψ (0, 0)), the edge s = 1 is the loop ψ t = Ψ (1, t), and the edges t = 0, t = T are the same curve of rays, Ψ (s, T) = e^{iφ(s)} Ψ (s, 0) (the phase mismatch at the cut). Then the geometric phase of the loop is minus the integral of the curvature over the disc:

β = −∫₀¹ ∫₀ᵀ 2 Im⟪∂_sΨ, ∂_tΨ⟫ ds dt.

The connection form A = Im⟪Ψ, dΨ⟫ has the two components A_s = Im⟪Ψ, ∂_sΨ⟫, A_t = Im⟪Ψ, ∂_tΨ⟫, and its curvature dA(∂_s, ∂_t) = ∂_s A_t − ∂_t A_s is 2 Im⟪∂_sΨ, ∂_tΨ⟫ by the symmetry of second derivatives — the pullback of the Kähler form Im⟪·, ·⟫ of the Fubini–Study metric Re⟪·, ·⟫ (twice it, in that normalisation; on ℂℙ¹ it integrates to half the solid angle). Green's theorem on the rectangle (Mathlib's divergence theorem on ℝ × ℝ) turns the integral of dA into the circulation of A along the boundary: the loop contributes the dynamical phase, the collapsed edge nothing, and the cut contributes −(φ 1 − φ 0) = −φ, the total phase.

• connectionFormS, connectionFormT — the components of the connection form of a family; curvature Ψ p = 2 Im⟪∂_sΨ, ∂_tΨ⟫;
• fderiv_apply_one_zero, fderiv_apply_zero_one — the partial derivatives are the derivatives of the restricted curves, so the edge values of A_s, A_t are the connectionForm of the edge curves (connectionFormS_eq, connectionFormT_eq);
• hasFDerivAt_connectionFormS/T — the components are C¹ with explicit derivative (connectionFormS', connectionFormT', through fderivInnerCLM);
• ★ curvature_eq — the curvature is ∂_s A_t − ∂_t A_s (symmetric second derivatives);
• ★★ geometricPhase_eq_neg_integral_curvature — the curvature formula β = −∫∫ curvature.

Honest scope

⚠️ The disc is the rectangle in polar form: any C² map of the closed disc gives such a family (Ψ (s, t) = F (s cos t, s sin t)), so nothing is lost for C² discs, but the statement is not Stokes on a manifold. The identification of curvature with the pullback of the corpus's bundle-level Fubini–Study form (fsForm of ProjectiveSpaceFubiniStudyForm.lean) along the projection of Ψ to ℙ(E) is BACKLOG #65, done 2026-09-28: CsdLean4/Mathlib/Geometry/Manifold/Instances/ProjectiveSpaceGeometricPhase.lean proves curvature Ψ p = −(1/2) · ω_FS on the velocities of [Ψ] (★★★ fsForm_eq_neg_two_mul_curvature), hence β = (1/2) ∫∫ [Ψ]^* ω_FS.

References: M. V. Berry, Proc. R. Soc. A 392 (1984) 45, §3; B. Simon, PRL 51 (1983) 2167; Y. Aharonov, J. Anandan, PRL 58 (1987) 1593; specs/berry-phase-scoping.md BP-3; specs/BACKLOG.md #54; specs/future-work.md.

The connection form of a two-parameter family and its curvature

noncomputable def GeometricPhase.connectionFormS {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (Ψ : ℝ × ℝ → E) (p : ℝ × ℝ) : ℝ

The s-component of the connection form of a family: A_s = Im⟪Ψ, ∂_sΨ⟫.

Equations

• GeometricPhase.connectionFormS Ψ p = (inner ℂ (Ψ p) ((fderiv ℝ Ψ p) (1, 0))).im

noncomputable def GeometricPhase.connectionFormT {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (Ψ : ℝ × ℝ → E) (p : ℝ × ℝ) : ℝ

The t-component of the connection form of a family: A_t = Im⟪Ψ, ∂_tΨ⟫.

Equations

• GeometricPhase.connectionFormT Ψ p = (inner ℂ (Ψ p) ((fderiv ℝ Ψ p) (0, 1))).im

noncomputable def GeometricPhase.curvature {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (Ψ : ℝ × ℝ → E) (p : ℝ × ℝ) : ℝ

The curvature dA(∂_s, ∂_t) = 2 Im⟪∂_sΨ, ∂_tΨ⟫ of the connection along a family.

Equations

• GeometricPhase.curvature Ψ p = 2 * (inner ℂ ((fderiv ℝ Ψ p) (1, 0)) ((fderiv ℝ Ψ p) (0, 1))).im

theorem GeometricPhase.fderiv_apply_one_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {Ψ : ℝ × ℝ → E} {s t : ℝ} (hΨ : DifferentiableAt ℝ Ψ (s, t)) : (fderiv ℝ Ψ (s, t)) (1, 0) = deriv (fun (s : ℝ) => Ψ (s, t)) s

The partial derivative in s is the derivative of the restricted curve.

theorem GeometricPhase.fderiv_apply_zero_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {Ψ : ℝ × ℝ → E} {s t : ℝ} (hΨ : DifferentiableAt ℝ Ψ (s, t)) : (fderiv ℝ Ψ (s, t)) (0, 1) = deriv (fun (t : ℝ) => Ψ (s, t)) t

The partial derivative in t is the derivative of the restricted curve.

theorem GeometricPhase.connectionFormS_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {Ψ : ℝ × ℝ → E} {s t : ℝ} (hΨ : DifferentiableAt ℝ Ψ (s, t)) : connectionFormS Ψ (s, t) = connectionForm (fun (s : ℝ) => Ψ (s, t)) s

theorem GeometricPhase.connectionFormT_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {Ψ : ℝ × ℝ → E} {s t : ℝ} (hΨ : DifferentiableAt ℝ Ψ (s, t)) : connectionFormT Ψ (s, t) = connectionForm (fun (t : ℝ) => Ψ (s, t)) t

The components are C¹

theorem GeometricPhase.hasFDerivAt_fderiv_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {Ψ : ℝ × ℝ → E} (hΨ : ContDiff ℝ 2 Ψ) (p v : ℝ × ℝ) : HasFDerivAt (fun (p : ℝ × ℝ) => (fderiv ℝ Ψ p) v) ((ContinuousLinearMap.apply ℝ E) v ∘SL fderiv ℝ (fderiv ℝ Ψ) p) p

The derivative of p ↦ ∂_vΨ(p) for a C² family: w ↦ D²Ψ(p)(w, v).

noncomputable def GeometricPhase.connectionFormS' {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (Ψ : ℝ × ℝ → E) (p : ℝ × ℝ) : ℝ × ℝ →L[ℝ] ℝ

The derivative of A_s.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def GeometricPhase.connectionFormT' {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (Ψ : ℝ × ℝ → E) (p : ℝ × ℝ) : ℝ × ℝ →L[ℝ] ℝ

The derivative of A_t.

Equations

• One or more equations did not get rendered due to their size.

theorem GeometricPhase.hasFDerivAt_connectionFormS {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {Ψ : ℝ × ℝ → E} (hΨ : ContDiff ℝ 2 Ψ) (p : ℝ × ℝ) : HasFDerivAt (connectionFormS Ψ) (connectionFormS' Ψ p) p

theorem GeometricPhase.hasFDerivAt_connectionFormT {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {Ψ : ℝ × ℝ → E} (hΨ : ContDiff ℝ 2 Ψ) (p : ℝ × ℝ) : HasFDerivAt (connectionFormT Ψ) (connectionFormT' Ψ p) p

theorem GeometricPhase.connectionFormS'_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {Ψ : ℝ × ℝ → E} (p w : ℝ × ℝ) : (connectionFormS' Ψ p) w = (inner ℂ (Ψ p) (((fderiv ℝ (fderiv ℝ Ψ) p) w) (1, 0)) + inner ℂ ((fderiv ℝ Ψ p) w) ((fderiv ℝ Ψ p) (1, 0))).im

theorem GeometricPhase.connectionFormT'_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {Ψ : ℝ × ℝ → E} (p w : ℝ × ℝ) : (connectionFormT' Ψ p) w = (inner ℂ (Ψ p) (((fderiv ℝ (fderiv ℝ Ψ) p) w) (0, 1)) + inner ℂ ((fderiv ℝ Ψ p) w) ((fderiv ℝ Ψ p) (0, 1))).im

theorem GeometricPhase.curvature_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {Ψ : ℝ × ℝ → E} (hΨ : ContDiff ℝ 2 Ψ) (p : ℝ × ℝ) : (connectionFormT' Ψ p) (1, 0) + (-connectionFormS' Ψ p) (0, 1) = curvature Ψ p

★ The curvature is ∂_s A_t − ∂_t A_s: the second-derivative terms cancel by symmetry.

The curvature formula

theorem GeometricPhase.contDiff_edgeS {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {Ψ : ℝ × ℝ → E} (hΨ : ContDiff ℝ 2 Ψ) (t : ℝ) : ContDiff ℝ 1 fun (s : ℝ) => Ψ (s, t)

The edge curve s ↦ Ψ (s, t) of a C² family is C¹.

theorem GeometricPhase.continuous_curvature {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {Ψ : ℝ × ℝ → E} (hΨ : ContDiff ℝ 2 Ψ) : Continuous (curvature Ψ)

theorem GeometricPhase.geometricPhase_eq_neg_integral_curvature {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {Ψ : ℝ × ℝ → E} (hΨ : ContDiff ℝ 2 Ψ) (hunit : ∀ (p : ℝ × ℝ), ‖Ψ p‖ = 1) {T : ℝ} {φ : ℝ → ℝ} (hφ : ContDiff ℝ 1 φ) (hφ0 : φ 0 = 0) (hleft : ∀ (t : ℝ), Ψ (0, t) = Ψ (0, 0)) (htop : ∀ (s : ℝ), Ψ (s, T) = Complex.exp (↑(φ s) * Complex.I) • Ψ (s, 0)) : geometricPhase (fun (t : ℝ) => Ψ (1, t)) T (φ 1) = -∫ (s : ℝ) in 0..1, ∫ (t : ℝ) in 0..T, curvature Ψ (s, t)

★★ The curvature formula for the geometric phase. For a C² family of unit vectors Ψ on [0, 1] × [0, T] — the disc in polar form: the edge s = 0 collapsed to a point, the edges t = 0 and t = T the same curve of rays up to the phase e^{iφ(s)}, φ 0 = 0 — the geometric phase of the loop t ↦ Ψ (1, t) (total phase φ 1) is minus the integral of the curvature 2 Im⟪∂_sΨ, ∂_tΨ⟫ over the disc.