The phase: Berry's geometric phase survives the adiabatic limit #

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #164 (out of ~~#88~~; closes the loop ~~#56~~ opened — the general theorem behind Berry's model).

Along a gapped C² path Γ with a nondegenerate branch (mult = 1, so rank P = 1), the orbit s ↦ A s ψ₀ of the adiabatic intertwiner A (#160, A' = K A, K = [Ṗ, P]) is a unit section of the eigenline whose connection form vanishes — it is BP-1's horizontal lift (GeometricPhase.horizontalLift). Consequently, for a closed eigenvector loop ψ 1 = e^{iφ} ψ 0, A 1 ψ₀ = e^{iβ} ψ₀ with β = geometricPhase ψ 1 φ the geometric phase of the loop, and the physical propagator at speed T satisfies

U_T 1 ψ₀ = e^{−iT∫₀¹ lam} e^{iβ} ψ₀ + O(1/T):

dynamical phase times Berry's phase, with the error of #162.

The identification is a uniqueness-of-ODE step. For a C¹ unit section ψ of the eigenline (P ψ = ψ, ‖ψ‖ = 1), K ψ = (1 − P) ψ̇ (differentiate P ψ = ψ), and for a rank-one P, P ψ̇ = ⟪ψ, ψ̇⟫ ψ = i Im⟪ψ, ψ̇⟫ ψ (Re⟪ψ, ψ̇⟫ = 0 by unit norm), so K ψ = ψ̇ − i A ψ with A = Im⟪ψ, ψ̇⟫ the connection form. The horizontal lift e^{−i∫A} ψ therefore solves χ' = K χ, χ 0 = ψ 0, and so does A s ψ 0; the vector-level uniqueness for propagators (Heisenberg constancy of A† χ) identifies them.

Matrix.toEuclideanCLMᵣ, HasDerivWithinAt.toEuclideanCLM_apply, HasDerivAt.toEuclideanCLM_apply — the derivative of s ↦ M s (v s);
★ IsPropagator.conjTranspose_apply_eq, IsPropagator.eq_apply_init — vector-level uniqueness: every solution of v' = G v is U v 0 (anti-Hermitian G);
Matrix.toEuclideanCLM_apply_eq_inner_smul, eq_inner_smul_of_toEuclideanCLM_apply_eq — a rank-one Hermitian projector with P ψ = ψ, ‖ψ‖ = 1 is P v = ⟪ψ, v⟫ ψ;
inner_deriv_eq_im_mul_I — ⟪ψ, ψ̇⟫ = i Im⟪ψ, ψ̇⟫ along a unit curve;
exists_eq_exp_smul_of_norm_eq, GeometricPhase.horizontalLift_zero — small general facts;
GappedPath.rank_proj, rank_proj_eq_one, proj_one_eq_of_closed, exists_cyclic_of_proj_one_eq — rank P s = mult s; a closed path has P 1 = P 0; a unit section of a rank-one eigenline with P 1 = P 0 closes up to a phase;
★ GappedPath.K_apply_section, ★★ K_apply_unit_section — K ψ = (1 − P) ψ̇, and K ψ = ψ̇ − i A ψ for a nondegenerate branch;
★★ GappedPath.hasDerivAt_horizontalLift_K — the horizontal lift solves χ' = K χ;
★★★ GappedPath.IsIntertwiner.toEuclideanCLM_apply_eq_horizontalLift — the intertwiner's orbit is the horizontal lift: A s ψ₀ = horizontalLift ψ s on [0, 1] for every C¹ unit section ψ of the eigenline with ψ 0 = ψ₀;
★★ IsIntertwiner.toEuclideanCLM_apply_one_eq — A 1 ψ₀ = e^{iβ} ψ₀, β = geometricPhase ψ 1 φ; IsIntertwiner.exists_apply_one_eq — the holonomy exists (∃ β) without choosing a section;
★★ GappedPath.IsAdPropagator.toEuclideanCLM_apply_eq, exists_norm_sub_dynPhase_smul_le — U_A s ψ₀ = e^{−iT∫₀ˢ lam} A s ψ₀, and ‖U_T s ψ₀ − e^{−iT∫₀ˢ lam} A s ψ₀‖ ≤ (C/T)‖ψ₀‖ (the adiabatic approximation with the parallel-transported eigenvector, any multiplicity);
★★★ GappedPath.exists_norm_sub_phase_smul_le — the phase theorem: ‖U_T 1 ψ₀ − e^{−iT∫₀¹ lam} e^{iβ} ψ₀‖ ≤ C / T.

Honest scope #

The eigenvector section ψ is a C¹ map ℝ → EuclideanSpace ℂ (Fin N), unit everywhere and in the eigenline range (P t) for every real t (the path Γ is defined on all of ℝ); only [0, 1] is used for the propagators. Any two such sections differ by a rephasing, and GeometricPhase.geometricPhase_rephase says β does not depend on the choice.
Nondegeneracy is Γ.mult 0 = 1 (constant along the path, mult_eq); the closed-loop hypothesis is ψ 1 = e^{iφ} ψ 0, which for rank one is equivalent to P 1 = P 0 (exists_cyclic_of_proj_one_eq); H 1 = H 0 ∧ lam 1 = lam 0 gives it (proj_one_eq_of_closed).
C is #162's constant; the C² and eigenvalue hypotheses are #162's.

References: M. V. Berry, Proc. R. Soc. A 392 (1984) 45; B. Simon, PRL 51 (1983) 2167; T. Kato, J. Phys. Soc. Japan 5 (1950) §3; GeometricPhase.lean (BP-1, #10), AdiabaticBornFock.lean (#163), AdiabaticPropagators.lean (#161), AdiabaticIntertwiner.lean (#160); specs/berry-phase-scoping.md BP-1, BP-5; specs/BACKLOG.md #164, ~~#88~~, ~~#56~~.

The phase: Berry's geometric phase survives the adiabatic limit #

Honest scope #

The derivative of s ↦ M s (v s) #

Vector-level uniqueness for propagators #

Rank-one projectors #

Two small general facts #

Rank one and closed paths #

K on a unit section of the eigenline #

The intertwiner's orbit is the horizontal lift #

The phase theorem #

The derivative of `s ↦ M s (v s)` #

`K` on a unit section of the eigenline #