Berry's rotating field as an instance of Kato's adiabatic theorem

Category: 3-Local (QM-validity). BACKLOG #165 (out of #88): #56's rigid rotation as an instance of the general theorem — a regression and an honest comparison, nothing more.

BerryAdiabatic.lean solves the spin-½ in a rotating field exactly and reads off the phase with an explicit O(ω) error. The general theorem (#158–#164) must specialise to it. Here it does:

• ★ fieldHam_mul_self, fieldHam_trace, fieldHam_eigenvalues_sq, card_eigenvalues_eq_one — H(t)² = (B/2)² · 1 and tr H(t) = 0, so the eigenvalues of H(t) are exactly ±B/2, one each (the general facts Matrix.IsHermitian.eigenvalues_sq_eq_of_mul_self, Fintype.card_subtype_eq_one_of_two are stated separately);
• ★★ conePath — H(t) = (B/2) n(t)·σ is a GappedPath with branch B/2 and gap B; contDiff_fieldHam (every order), conePath_mult_eq_one (nondegenerate), conePath_hex, conePath_proj_one_eq (closed for ω = 2π);
• ★★ conePath_isPhysPropagator — the exact propagator V(Ts) is the physical propagator at speed T of the path fieldHam θ (ωT) B;
• ★ coneSection_* — BP-2's cone curve is a C¹ unit section of the eigenline (GappedPath.proj_toEuclideanCLM_apply_of_eq), closed for ω = 2π;
• ★★★ exists_norm_state_sub_phase_le — the general phase theorem, specialised: there is C such that for every ω > 0 (with Ω ≠ 0), after one turn T = 2π/ω, ‖ψ(T) − e^{i(−(B/2)T − π(1 − cos θ))} ψ₀‖ ≤ C ω / (2π) — the same dynamical and geometric phases as #56's ★★★ norm_inner_state_sub_exp_le;
• exists_norm_inner_state_sub_exp_le — the overlap form, directly comparable with #56;
• berry_bound_eq_kato_form, berry_bound_le_kato_form — the honest comparison: #56's explicit error πω/(2(B − ω)) + (ω/(B − ω))² is π²/((B − ω) T) + 4π²/((B − ω)² T²) in the general theorem's variable T, and for ω ≤ B/2 it is at most (2π(π + 2)/B) · ω/(2π) — so in this model the general theorem's constant can be taken C = 2π(π + 2)/g for the overlap, with g = B the gap. The general formula of AdiabaticConstant.lean (#166), 8M₁/g² + 4M₂/g² + 80M₁²/g³, gives for this path (by hand: ‖Ḣ‖ = πB sin θ, ‖Ḧ‖ = 2π²B sin θ, not computed in Lean) about 894/B at θ = π/2 — larger, as it must be.

Honest scope

• The general constant C exists by compactness (#162) and is not computed; what is compared is the shape of the bound and the phases, which agree exactly, plus the explicit constant that #56's exact solution supplies for this one model.
• Ω ≠ 0 (rabiFreq θ ω B ≠ 0) is the hypothesis under which #56's propagator is proved to solve the Schrödinger equation; it holds for 0 < ω < B.
• The path parameter is s = t/T; the general theorem's [0, 1] is one turn of the field.

References: M. V. Berry, Proc. R. Soc. A 392 (1984) 45, §5; T. Kato, J. Phys. Soc. Japan 5 (1950); AdiabaticPhase.lean (#164), AdiabaticBornFock.lean (#163), AdiabaticComparison.lean (#162), BerryAdiabatic.lean (#56), BerryPhase.lean (BP-2); specs/berry-phase-scoping.md BP-5; specs/BACKLOG.md #165, #88, #56.

Two general facts

theorem Matrix.IsHermitian.eigenvalues_sq_eq_of_mul_self {N : ℕ} {A : Matrix (Fin N) (Fin N) ℂ} (hA : A.IsHermitian) {r : ℝ} (hsq : A * A = ↑(r ^ 2) • 1) (j : Fin N) : hA.eigenvalues j ^ 2 = r ^ 2

The eigenvalues of a Hermitian matrix with A² = r² · 1 satisfy μ² = r².

theorem Fintype.card_subtype_eq_one_of_two {f : Fin 2 → ℝ} {r : ℝ} (hr : r ≠ 0) (hsq : ∀ (j : Fin 2), f j ^ 2 = r ^ 2) (hsum : f 0 + f 1 = 0) : card { j : Fin 2 // f j = r } = 1

A real function on Fin 2 with values in {r, −r}, r ≠ 0, summing to zero takes the value r exactly once.

theorem norm_inner_sub_le_norm_sub_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {x : E} (hx : ‖x‖ = 1) (v : E) (c : ℂ) : ‖inner ℂ x v - c‖ ≤ ‖v - c • x‖

|⟪x, v⟫ − c| ≤ ‖v − c x‖ for a unit vector x.

The spectrum of H(t)

theorem CSD.Empirical.QM.BerryKato.fieldHam_mul_self (θ ω B t : ℝ) : BerryAdiabatic.fieldHam θ ω B t * BerryAdiabatic.fieldHam θ ω B t = ↑((B / 2) ^ 2) • 1

H(t)² = (B/2)² · 1.

theorem CSD.Empirical.QM.BerryKato.fieldHam_trace (θ ω B t : ℝ) : (BerryAdiabatic.fieldHam θ ω B t).trace = 0

theorem CSD.Empirical.QM.BerryKato.fieldHam_eigenvalues_sq (θ ω B t : ℝ) (j : Fin 2) : ⋯.eigenvalues j ^ 2 = (B / 2) ^ 2

Every eigenvalue of H(t) has μ² = (B/2)².

theorem CSD.Empirical.QM.BerryKato.fieldHam_eigenvalues_sum (θ ω B t : ℝ) : ⋯.eigenvalues 0 + ⋯.eigenvalues 1 = 0

theorem CSD.Empirical.QM.BerryKato.card_eigenvalues_eq_one (θ ω : ℝ) {B : ℝ} (hB : 0 < B) (t : ℝ) : Fintype.card { j : Fin 2 // ⋯.eigenvalues j = B / 2 } = 1

★ B/2 is a simple eigenvalue of H(t).

Smoothness and periodicity of the path

theorem CSD.Empirical.QM.BerryKato.fieldHam_eq (θ ω B : ℝ) : BerryAdiabatic.fieldHam θ ω B = fun (t : ℝ) => ↑(1 / 2) • (Real.cos (ω * t) • QuantumInfo.SU2.pauliAxis (B * Real.sin θ) 0 0 + Real.sin (ω * t) • QuantumInfo.SU2.pauliAxis 0 (B * Real.sin θ) 0 + QuantumInfo.SU2.pauliAxis 0 0 (B * Real.cos θ))

H(t) as cos ωt · M₁ + sin ωt · M₂ + M₃ with constant matrices.

theorem CSD.Empirical.QM.BerryKato.contDiff_fieldHam (θ ω B : ℝ) (n : WithTop ℕ∞) : ContDiff ℝ n (BerryAdiabatic.fieldHam θ ω B)

The path is smooth to every order.

theorem CSD.Empirical.QM.BerryKato.fieldHam_rescale (θ ω B T s : ℝ) : BerryAdiabatic.fieldHam θ ω B (T * s) = BerryAdiabatic.fieldHam θ (ω * T) B s

Rescaling the parameter: H_ω(T s) = H_{ωT}(s).

theorem CSD.Empirical.QM.BerryKato.fieldHam_one_eq_zero (θ B : ℝ) : BerryAdiabatic.fieldHam θ (2 * Real.pi) B 1 = BerryAdiabatic.fieldHam θ (2 * Real.pi) B 0

For ω = 2π the path closes after one unit of parameter.

The gapped path

noncomputable def CSD.Empirical.QM.BerryKato.conePath (θ ω : ℝ) {B : ℝ} (hB : 0 < B) : Matrix.GappedPath 2

★★ The rotating field is a gapped path: branch B/2, gap B.

Equations

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

theorem CSD.Empirical.QM.BerryKato.conePath_H (θ ω : ℝ) {B : ℝ} (hB : 0 < B) : (conePath θ ω hB).H = BerryAdiabatic.fieldHam θ ω B

theorem CSD.Empirical.QM.BerryKato.conePath_lam (θ ω : ℝ) {B : ℝ} (hB : 0 < B) (s : ℝ) : (conePath θ ω hB).lam s = B / 2

theorem CSD.Empirical.QM.BerryKato.conePath_hex (θ ω : ℝ) {B : ℝ} (hB : 0 < B) (s : ℝ) : ∃ (j : Fin 2), ⋯.eigenvalues j = (conePath θ ω hB).lam s

The branch is an eigenvalue at every parameter.

theorem CSD.Empirical.QM.BerryKato.conePath_mult_eq_one (θ ω : ℝ) {B : ℝ} (hB : 0 < B) : (conePath θ ω hB).mult 0 = 1

★ The branch is nondegenerate.

theorem CSD.Empirical.QM.BerryKato.conePath_proj_one_eq (θ : ℝ) {B : ℝ} (hB : 0 < B) : (conePath θ (2 * Real.pi) hB).proj 1 = (conePath θ (2 * Real.pi) hB).proj 0

For ω = 2π the eigenprojectors close up: P 1 = P 0.

The exact propagator is the physical propagator

theorem CSD.Empirical.QM.BerryKato.conePath_isPhysPropagator (θ : ℝ) {ω B T : ℝ} (hB : 0 < B) (hΩ : BerryAdiabatic.rabiFreq θ ω B ≠ 0) : (conePath θ (ω * T) hB).IsPhysPropagator T fun (s : ℝ) => BerryAdiabatic.prop θ ω B (T * s)

★★ V(Ts) is the physical propagator at speed T of the path fieldHam θ (ωT) B.

The cone curve is a section of the eigenline

theorem CSD.Empirical.QM.BerryKato.toEuclideanCLM_fieldHam_coneCurve (θ ω B s : ℝ) : (Matrix.toEuclideanCLM (BerryAdiabatic.fieldHam θ ω B s)) (BerryPhase.coneCurve θ (ω * s)) = ↑(B / 2) • BerryPhase.coneCurve θ (ω * s)

H(s) ψ(s) = (B/2) ψ(s) for the cone curve, in toEuclideanCLM form.

theorem CSD.Empirical.QM.BerryKato.coneSection_contDiff (θ ω : ℝ) : ContDiff ℝ 1 fun (s : ℝ) => BerryPhase.coneCurve θ (ω * s)

theorem CSD.Empirical.QM.BerryKato.coneSection_norm (θ ω s : ℝ) : ‖BerryPhase.coneCurve θ (ω * s)‖ = 1

theorem CSD.Empirical.QM.BerryKato.coneSection_proj (θ ω : ℝ) {B : ℝ} (hB : 0 < B) (s : ℝ) : (Matrix.toEuclideanCLM ((conePath θ ω hB).proj s)) (BerryPhase.coneCurve θ (ω * s)) = BerryPhase.coneCurve θ (ω * s)

★ The cone curve lies in the eigenline of the path at every parameter.

theorem CSD.Empirical.QM.BerryKato.coneSection_cyclic (θ : ℝ) : BerryPhase.coneCurve θ (2 * Real.pi * 1) = Complex.exp (↑0 * Complex.I) • BerryPhase.coneCurve θ (2 * Real.pi * 0)

For ω = 2π the section closes with total phase 0.

theorem CSD.Empirical.QM.BerryKato.coneSection_geometricPhase (θ : ℝ) : GeometricPhase.geometricPhase (fun (s : ℝ) => BerryPhase.coneCurve θ (2 * Real.pi * s)) 1 0 = -Real.pi * (1 - Real.cos θ)

The geometric phase of the section over one unit of parameter is Berry's −π(1 − cos θ).

The general theorem, specialised

theorem CSD.Empirical.QM.BerryKato.conePath_dynPhase (θ ω : ℝ) {B : ℝ} (hB : 0 < B) (T : ℝ) : (conePath θ ω hB).dynPhase T 1 = Complex.exp (-Complex.I * ↑T * ↑(B / 2))

The dynamical phase of the path over one unit of parameter at speed T: e^{−iT·B/2}.

theorem CSD.Empirical.QM.BerryKato.exists_norm_state_sub_phase_le (θ : ℝ) {B : ℝ} (hB : 0 < B) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (ω : ℝ), 0 < ω → BerryAdiabatic.rabiFreq θ ω B ≠ 0 → ‖BerryAdiabatic.state θ ω B (2 * Real.pi / ω) - Complex.exp (↑(-(B / 2) * (2 * Real.pi / ω) - Real.pi * (1 - Real.cos θ)) * Complex.I) • BerryAdiabatic.spinUp θ‖ ≤ C * ω / (2 * Real.pi)

★★★ Kato's phase theorem specialised to Berry's rotating field. There is a constant C such that for every ω > 0 with Ω ≠ 0, after one turn T = 2π/ω,

‖ψ(T) − e^{i(−(B/2)T − π(1 − cos θ))} ψ₀‖ ≤ C ω / (2π):

the same dynamical phase −(B/2)T and geometric phase −π(1 − cos θ) as #56's exact norm_inner_state_sub_exp_le, with the general theorem's O(1/T) = O(ω) error.

theorem CSD.Empirical.QM.BerryKato.exists_norm_inner_state_sub_exp_le (θ : ℝ) {B : ℝ} (hB : 0 < B) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (ω : ℝ), 0 < ω → BerryAdiabatic.rabiFreq θ ω B ≠ 0 → ‖inner ℂ (BerryAdiabatic.spinUp θ) (BerryAdiabatic.state θ ω B (2 * Real.pi / ω)) - Complex.exp (↑(-(B / 2) * (2 * Real.pi / ω) - Real.pi * (1 - Real.cos θ)) * Complex.I)‖ ≤ C * ω / (2 * Real.pi)

★★ The overlap form, directly comparable with #56's norm_inner_state_sub_exp_le: |⟪ψ₀, ψ(T)⟫ − e^{i(−(B/2)T − π(1 − cos θ))}| ≤ C ω / (2π).

The honest comparison of constants

theorem CSD.Empirical.QM.BerryKato.berry_bound_eq_kato_form {ω B T : ℝ} (hω : 0 < ω) (hωB : ω < B) (hT : ω * T = 2 * Real.pi) : Real.pi * ω / (2 * (B - ω)) + (ω / (B - ω)) ^ 2 = Real.pi ^ 2 / ((B - ω) * T) + 4 * Real.pi ^ 2 / ((B - ω) ^ 2 * T ^ 2)

#56's explicit error in the general theorem's variable T = 2π/ω: πω/(2(B − ω)) + (ω/(B − ω))² = π²/((B − ω) T) + 4π²/((B − ω)² T²) — a 1/T term with constant π²/(B − ω) and a 1/T² remainder.

theorem CSD.Empirical.QM.BerryKato.berry_bound_le_kato_form {ω B : ℝ} (hω : 0 < ω) (hωB : ω ≤ B / 2) : Real.pi * ω / (2 * (B - ω)) + (ω / (B - ω)) ^ 2 ≤ 2 * Real.pi * (Real.pi + 2) / B * ω / (2 * Real.pi)

For ω ≤ B/2, #56's error is at most (2π(π + 2)/B) · ω/(2π): in this model the general theorem's constant can be taken to be 2π(π + 2)/g, g = B the gap.