The geometric (Aharonov–Anandan) phase of a cyclic evolution

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

Glossary: https://glossary.constraintsurfacedynamics.com/geometric-phase/ Plain-language, CSD-role and formal statements of the geometric phase, with this module as the Lean anchor. Kept symmetric by scripts/check-glossary.sh.

A curve ψ : ℝ → E of unit vectors in a complex inner product space whose rays close, ψ T = e^{iφ} ψ 0, carries three phases: the total phase φ, the dynamical phase ∫₀ᵀ Im⟪ψ, ψ̇⟫ (for a Schrödinger evolution iψ̇ = Hψ, minus the time-integrated energy), and their difference, the geometric phase. A = Im⟪ψ, dψ⟫ is the connection form of the canonical U(1)-connection on the Hopf bundle S → ℙ(E), so the geometric phase is its holonomy — stated here without bundles, on the sphere:

• connectionForm ψ t = Im⟪ψ t, ψ̇ t⟫, dynamicalPhase ψ T, geometricPhase ψ T φ = φ − ∫₀ᵀ A, and rephase θ ψ = e^{iθ} ψ, the change of lift by a differentiable phase;
• connectionForm_rephase — A shifts by θ' under a rephasing (⟪ψ, ψ⟫ = 1 is all it uses);
• ★★ geometricPhase_rephase — gauge invariance: the geometric phase of e^{iθ} ψ (whose total phase is φ + θ T − θ 0) equals that of ψ, for every differentiable θ. The geometric phase is a function of the closed curve of rays alone;
• ★ connectionForm_horizontalLift, ★★ horizontalLift_cyclic — the geometric phase is the holonomy: the horizontal lift e^{−i∫₀ᵗ A} ψ has A = 0 along it and returns as e^{iβ} times its start, β the geometric phase;
• ★ connectionForm_of_schrodinger, inner_self_const_of_schrodinger, ★ geometricPhase_of_schrodinger — for ψ̇ = −iHψ with H self-adjoint the connection form is −⟪ψ, Hψ⟫, the energy is conserved, and β = φ + T ⟪ψ 0, H ψ 0⟫.

Honest scope

⚠️ No bundle, no parallel transport as an object: the holonomy statement is the horizontal-lift theorem on the sphere. The curvature formula β = −∫∫ dA is GeometricPhaseCurvature.lean (BP-3); the Aharonov–Bohm flux is BP-4: CsdLean4/Mathlib/QuantumInfo/AharonovBohmRing.lean and CsdLean4/Empirical/QM/AharonovBohm.lean (BACKLOG #55). Berry's adiabatic setting is BP-5: CsdLean4/Mathlib/QuantumInfo/RotatingFrame.lean solves a rigidly rotated Hamiltonian exactly and CsdLean4/Empirical/QM/BerryAdiabatic.lean reads the phase off it (BACKLOG #56); the general Kato–Born–Fock theorem is CsdLean4/Mathlib/Analysis/Matrix/AdiabaticComparison.lean (#162), and CsdLean4/Mathlib/Analysis/Matrix/AdiabaticPhase.lean (#164) identifies the orbit of Kato's intertwiner with horizontalLift, so β here is the phase that survives the adiabatic limit.

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

The connection form, the phases, and rephasing

noncomputable def GeometricPhase.connectionForm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (ψ : ℝ → E) (t : ℝ) : ℝ

The canonical connection form along a curve: A(t) = Im ⟪ψ t, ψ̇ t⟫.

Equations

• GeometricPhase.connectionForm ψ t = (inner ℂ (ψ t) (deriv ψ t)).im

noncomputable def GeometricPhase.dynamicalPhase {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (ψ : ℝ → E) (T : ℝ) : ℝ

The dynamical phase over [0, T]: ∫₀ᵀ Im ⟪ψ, ψ̇⟫.

Equations

• GeometricPhase.dynamicalPhase ψ T = ∫ (t : ℝ) in 0..T, GeometricPhase.connectionForm ψ t

noncomputable def GeometricPhase.geometricPhase {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (ψ : ℝ → E) (T φ : ℝ) : ℝ

The geometric phase of a cyclic evolution with total phase φ: φ − ∫₀ᵀ Im ⟪ψ, ψ̇⟫.

Equations

• GeometricPhase.geometricPhase ψ T φ = φ - GeometricPhase.dynamicalPhase ψ T

noncomputable def GeometricPhase.rephase {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (θ : ℝ → ℝ) (ψ : ℝ → E) (t : ℝ) : E

The rephased lift e^{iθ(t)} ψ(t).

Equations

• GeometricPhase.rephase θ ψ t = Complex.exp (↑(θ t) * Complex.I) • ψ t

theorem GeometricPhase.hasDerivAt_cexp_ofReal_mul_I {θ : ℝ → ℝ} {θ' t : ℝ} (hθ : HasDerivAt θ θ' t) : HasDerivAt (fun (s : ℝ) => Complex.exp (↑(θ s) * Complex.I)) (Complex.exp (↑(θ t) * Complex.I) * (↑θ' * Complex.I)) t

theorem GeometricPhase.hasDerivAt_rephase {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {θ : ℝ → ℝ} {ψ : ℝ → E} {θ' t : ℝ} {ψ' : E} (hθ : HasDerivAt θ θ' t) (hψ : HasDerivAt ψ ψ' t) : HasDerivAt (rephase θ ψ) (Complex.exp (↑(θ t) * Complex.I) • ψ' + (Complex.exp (↑(θ t) * Complex.I) * (↑θ' * Complex.I)) • ψ t) t

theorem GeometricPhase.conj_cexp_mul_self (x : ℝ) : (starRingEnd ℂ) (Complex.exp (↑x * Complex.I)) * Complex.exp (↑x * Complex.I) = 1

theorem GeometricPhase.inner_self_eq_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {ψ : ℝ → E} {t : ℝ} (hunit : ‖ψ t‖ = 1) : inner ℂ (ψ t) (ψ t) = 1

theorem GeometricPhase.connectionForm_rephase {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {θ : ℝ → ℝ} {ψ : ℝ → E} {t : ℝ} (hθ : DifferentiableAt ℝ θ t) (hψ : DifferentiableAt ℝ ψ t) (hunit : ‖ψ t‖ = 1) : connectionForm (rephase θ ψ) t = connectionForm ψ t + deriv θ t

The connection form shifts by θ' under the rephasing e^{iθ}.

theorem GeometricPhase.rephase_cyclic {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {θ : ℝ → ℝ} {ψ : ℝ → E} {T φ : ℝ} (hcyc : ψ T = Complex.exp (↑φ * Complex.I) • ψ 0) : rephase θ ψ T = Complex.exp (↑(φ + (θ T - θ 0)) * Complex.I) • rephase θ ψ 0

The rephased curve is cyclic with total phase φ + θ T − θ 0.

Gauge invariance

theorem GeometricPhase.continuous_connectionForm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {ψ : ℝ → E} (hψ : ContDiff ℝ 1 ψ) : Continuous (connectionForm ψ)

theorem GeometricPhase.dynamicalPhase_rephase {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {ψ : ℝ → E} {θ : ℝ → ℝ} (hθ : ContDiff ℝ 1 θ) (hψ : ContDiff ℝ 1 ψ) (hunit : ∀ (t : ℝ), ‖ψ t‖ = 1) (T : ℝ) : dynamicalPhase (rephase θ ψ) T = dynamicalPhase ψ T + (θ T - θ 0)

theorem GeometricPhase.geometricPhase_rephase {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {ψ : ℝ → E} {θ : ℝ → ℝ} (hθ : ContDiff ℝ 1 θ) (hψ : ContDiff ℝ 1 ψ) (hunit : ∀ (t : ℝ), ‖ψ t‖ = 1) (T φ : ℝ) : geometricPhase (rephase θ ψ) T (φ + (θ T - θ 0)) = geometricPhase ψ T φ

★★ Gauge invariance of the geometric phase. Rephasing the lift by any differentiable θ changes the total phase to φ + θ T − θ 0 and the dynamical phase by the same amount: the geometric phase depends on the closed curve of rays alone.

The horizontal lift: the geometric phase is the holonomy

noncomputable def GeometricPhase.horizontalLift {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (ψ : ℝ → E) : ℝ → E

The horizontal (parallel) lift e^{−i ∫₀ᵗ A} ψ.

Equations

• GeometricPhase.horizontalLift ψ = GeometricPhase.rephase (fun (t : ℝ) => -GeometricPhase.dynamicalPhase ψ t) ψ

theorem GeometricPhase.hasDerivAt_dynamicalPhase {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {ψ : ℝ → E} (hψ : ContDiff ℝ 1 ψ) (t : ℝ) : HasDerivAt (dynamicalPhase ψ) (connectionForm ψ t) t

theorem GeometricPhase.contDiff_neg_dynamicalPhase {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {ψ : ℝ → E} (hψ : ContDiff ℝ 1 ψ) : ContDiff ℝ 1 fun (t : ℝ) => -dynamicalPhase ψ t

theorem GeometricPhase.connectionForm_horizontalLift {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {ψ : ℝ → E} (hψ : ContDiff ℝ 1 ψ) (hunit : ∀ (t : ℝ), ‖ψ t‖ = 1) (t : ℝ) : connectionForm (horizontalLift ψ) t = 0

★ The horizontal lift is horizontal: its connection form vanishes.

theorem GeometricPhase.horizontalLift_cyclic {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {ψ : ℝ → E} {T φ : ℝ} (hcyc : ψ T = Complex.exp (↑φ * Complex.I) • ψ 0) : horizontalLift ψ T = Complex.exp (↑(geometricPhase ψ T φ) * Complex.I) • horizontalLift ψ 0

★★ The geometric phase is the holonomy: the horizontal lift of a cyclic evolution returns as e^{iβ} times its start, β the geometric phase.

Schrödinger evolutions: the dynamical phase is minus the energy

theorem GeometricPhase.connectionForm_of_schrodinger {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {ψ : ℝ → E} {H : E →L[ℂ] E} {t : ℝ} (hψ : HasDerivAt ψ (-Complex.I • H (ψ t)) t) : connectionForm ψ t = -(inner ℂ (ψ t) (H (ψ t))).re

For ψ̇ = −iHψ, the connection form is −⟪ψ, Hψ⟫ (real for self-adjoint H).

theorem GeometricPhase.inner_self_const_of_schrodinger {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {ψ : ℝ → E} {H : E →L[ℂ] E} (hH : ∀ (x y : E), inner ℂ (H x) y = inner ℂ x (H y)) (hψ : ∀ (t : ℝ), HasDerivAt ψ (-Complex.I • H (ψ t)) t) (s t : ℝ) : inner ℂ (ψ s) (H (ψ s)) = inner ℂ (ψ t) (H (ψ t))

The energy ⟪ψ, Hψ⟫ is conserved along a Schrödinger evolution with self-adjoint H.

theorem GeometricPhase.geometricPhase_of_schrodinger {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {ψ : ℝ → E} {H : E →L[ℂ] E} (hH : ∀ (x y : E), inner ℂ (H x) y = inner ℂ x (H y)) (hψ : ∀ (t : ℝ), HasDerivAt ψ (-Complex.I • H (ψ t)) t) (T φ : ℝ) : geometricPhase ψ T φ = φ + T * (inner ℂ (ψ 0) (H (ψ 0))).re

★ The geometric phase of a Schrödinger evolution: β = φ + T ⟪ψ 0, H ψ 0⟫ — the total phase plus the time-integrated energy.