Berry's adiabatic theorem for a spin-½ in a rotating field

Category: 3-Local (QM-validity). BACKLOG #56, brick BP-5 of specs/berry-phase-scoping.md.

A spin-½ in a magnetic field of fixed magnitude B whose direction sweeps the cone of half-angle θ at angular velocity ω, H(t) = (1/2) B n(t)·σ, n(t) = (sin θ cos ωt, sin θ sin ωt, cos θ), is the model Berry solves in §5 of his 1984 paper. Everything here is exact, with the adiabatic limit appearing as an explicit bound in ω, never as an unproved approximation.

The four statements

• ★★★ hasDerivAt_prop — the time-dependent Schrödinger equation is solved exactly: V(t) = R_z(ωt) R_k(Ωt) satisfies V′ = −i H(t) V, V 0 = 1, V t unitary, where Ω = √((B sin θ)² + (B cos θ − ω)²) is the Rabi frequency and k the unit axis of the rotating-frame Hamiltonian K = H(0) − (ω/2)σ₃. ★★ hasDerivAt_state is the same equation for the state ψ(t) = V(t) ψ₀.
• ★★ fieldHam_mulVec_coneCurve — the instantaneous eigenvector of H(t) with eigenvalue B/2 is exactly the cone curve (cos θ/2, e^{iωt} sin θ/2) of BP-2, so the ray loop whose geometric phase BerryPhase.lean computed is the loop this Hamiltonian traces.
• ★★★ norm_inner_coneCurve_state_sq — adiabatic following, exactly: the probability of still being in the instantaneous eigenstate is 1 − (ω sin θ/Ω)² sin²(Ωt/2), hence ★★★ one_sub_le_norm_inner_coneCurve_state_sq bounds the loss by (ω/(B − ω))² for all time.
• ★★★ norm_inner_state_sub_exp_le — the phase at the end of one turn T = 2π/ω is the dynamical phase −(B/2)T plus the geometric phase −π(1 − cos θ) of BP-2, with an error ≤ πω/(2(B − ω)) + (ω/(B − ω))², i.e. O(ω). ★ geometricPhase_cone_loop identifies that second summand as GeometricPhase.geometricPhase of the loop over [0, T], so the statement is Berry's, not a coincidence of numbers.

How it is proved

The rotating-frame reduction of CsdLean4/Mathlib/QuantumInfo/RotatingFrame.lean: because H(t) = R_z(ωt) H(0) R_z(ωt)ᴴ (★ drive_conj_initHam, the Bloch rotation axisRot_z_conj), the propagator is the drive times the evolution generated by the constant K = H(0) − (ω/2)σ₃ (★ initHam_sub_driveGen), and both factors are axis–angle rotations whose derivative is hasDerivAt_axisRot. No matrix exponential, no Dyson series, no perturbation theory.

The overlap is then algebra: R_z(ωt) is unitary, so it drops out of the inner product (inner_toEuclideanCLM_unitary) and the whole time dependence sits in the Rabi factor, whose diagonal matrix element is cos(Ωt/2) − i (k·n₀) sin(Ωt/2) (★★ inner_spinUp_rabiProp). The two error bounds come from one exact identity, ★ one_sub_cosDelta_sq: 1 − (k·n₀)² = (ω sin θ/Ω)².

Honest scope

⚠️ One model: a rigid rotation of a fixed H₀ for spin-½. The general adiabatic theorem (Born–Fock, Kato: an arbitrary gapped path H(R(t)), error O(1/T)) is not proved here; it is CsdLean4/Mathlib/Analysis/Matrix/AdiabaticComparison.lean and AdiabaticPhase.lean (#88 → #158–#164), and CsdLean4/Empirical/QM/BerryKatoInstance.lean (#165) shows this model is an instance of it. The bounds here are unconditional in t because this model's rotating frame is exact; the general theorem's constant is not.

References: M. V. Berry, Proc. R. Soc. A 392 (1984) 45, §5; I. I. Rabi, Phys. Rev. 51 (1937) 652; L. D. Landau, E. M. Lifshitz, Quantum Mechanics §39; specs/berry-phase-scoping.md; specs/qm-empirical-tests.md ER3; specs/BACKLOG.md #56.

The model

noncomputable def CSD.Empirical.QM.BerryAdiabatic.fieldHam (θ ω B t : ℝ) : Matrix (Fin 2) (Fin 2) ℂ

The Hamiltonian of a spin-½ in a field of magnitude B whose direction sweeps the cone of half-angle θ at angular velocity ω: H(t) = (1/2) B n(t)·σ with n(t) = (sin θ cos ωt, sin θ sin ωt, cos θ).

Equations

• CSD.Empirical.QM.BerryAdiabatic.fieldHam θ ω B t = ↑(1 / 2) • QuantumInfo.SU2.pauliAxis (B * Real.sin θ * Real.cos (ω * t)) (B * Real.sin θ * Real.sin (ω * t)) (B * Real.cos θ)

noncomputable def CSD.Empirical.QM.BerryAdiabatic.initHam (θ B : ℝ) : Matrix (Fin 2) (Fin 2) ℂ

The Hamiltonian at time zero.

Equations

• CSD.Empirical.QM.BerryAdiabatic.initHam θ B = ↑(1 / 2) • QuantumInfo.SU2.pauliAxis (B * Real.sin θ) 0 (B * Real.cos θ)

noncomputable def CSD.Empirical.QM.BerryAdiabatic.driveGen (ω : ℝ) : Matrix (Fin 2) (Fin 2) ℂ

The generator of the drive, G = (ω/2) σ₃.

Equations

• CSD.Empirical.QM.BerryAdiabatic.driveGen ω = ↑(1 / 2) • QuantumInfo.SU2.pauliAxis 0 0 ω

noncomputable def CSD.Empirical.QM.BerryAdiabatic.drive (ω t : ℝ) : Matrix (Fin 2) (Fin 2) ℂ

The drive U(t) = R_z(ωt) = e^{−i(ω/2)t σ₃}, which turns H(0) into H(t).

Equations

• CSD.Empirical.QM.BerryAdiabatic.drive ω t = QuantumInfo.SU2.axisRot 0 0 1 (ω * t)

noncomputable def CSD.Empirical.QM.BerryAdiabatic.rabiFreq (θ ω B : ℝ) : ℝ

The Rabi frequency Ω = √((B sin θ)² + (B cos θ − ω)²): twice the energy gap of the rotating-frame Hamiltonian K = H(0) − (ω/2)σ₃.

Equations

• CSD.Empirical.QM.BerryAdiabatic.rabiFreq θ ω B = √((B * Real.sin θ) ^ 2 + (B * Real.cos θ - ω) ^ 2)

noncomputable def CSD.Empirical.QM.BerryAdiabatic.rabiAxisX (θ ω B : ℝ) : ℝ

The x-component of the unit axis of K.

Equations

• CSD.Empirical.QM.BerryAdiabatic.rabiAxisX θ ω B = B * Real.sin θ / CSD.Empirical.QM.BerryAdiabatic.rabiFreq θ ω B

noncomputable def CSD.Empirical.QM.BerryAdiabatic.rabiAxisZ (θ ω B : ℝ) : ℝ

The z-component of the unit axis of K.

Equations

• CSD.Empirical.QM.BerryAdiabatic.rabiAxisZ θ ω B = (B * Real.cos θ - ω) / CSD.Empirical.QM.BerryAdiabatic.rabiFreq θ ω B

noncomputable def CSD.Empirical.QM.BerryAdiabatic.rabiProp (θ ω B t : ℝ) : Matrix (Fin 2) (Fin 2) ℂ

The rotating-frame evolution e^{−itK} = R_k(Ωt).

Equations

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

noncomputable def CSD.Empirical.QM.BerryAdiabatic.prop (θ ω B t : ℝ) : Matrix (Fin 2) (Fin 2) ℂ

The propagator of the driven spin: the drive times the rotating-frame evolution.

Equations

• CSD.Empirical.QM.BerryAdiabatic.prop θ ω B t = CSD.Empirical.QM.BerryAdiabatic.drive ω t * CSD.Empirical.QM.BerryAdiabatic.rabiProp θ ω B t

noncomputable def CSD.Empirical.QM.BerryAdiabatic.spinUp (θ : ℝ) : EuclideanSpace ℂ (Fin 2)

The initial state: spin-up along n(0), the +B/2 eigenvector of H(0).

Equations

• CSD.Empirical.QM.BerryAdiabatic.spinUp θ = !₂[↑(Real.cos (θ / 2)), ↑(Real.sin (θ / 2))]

noncomputable def CSD.Empirical.QM.BerryAdiabatic.state (θ ω B t : ℝ) : EuclideanSpace ℂ (Fin 2)

The state of the spin at time t, started in spinUp θ.

Equations

• CSD.Empirical.QM.BerryAdiabatic.state θ ω B t = (Matrix.toEuclideanCLM (CSD.Empirical.QM.BerryAdiabatic.prop θ ω B t)) (CSD.Empirical.QM.BerryAdiabatic.spinUp θ)

The Rabi frequency and its axis

theorem CSD.Empirical.QM.BerryAdiabatic.rabiFreq_sq (θ ω B : ℝ) : rabiFreq θ ω B ^ 2 = (B * Real.sin θ) ^ 2 + (B * Real.cos θ - ω) ^ 2

theorem CSD.Empirical.QM.BerryAdiabatic.sub_le_rabiFreq (θ : ℝ) {ω B : ℝ} (hω : 0 ≤ ω) (hB : 0 ≤ B) : B - ω ≤ rabiFreq θ ω B

The Rabi frequency is at least the detuning B − ω: the gap never closes below B − ω.

theorem CSD.Empirical.QM.BerryAdiabatic.rabiFreq_pos {θ ω B : ℝ} (hω : 0 < ω) (hωB : ω < B) : 0 < rabiFreq θ ω B

theorem CSD.Empirical.QM.BerryAdiabatic.rabiFreq_ne_zero {θ ω B : ℝ} (hω : 0 < ω) (hωB : ω < B) : rabiFreq θ ω B ≠ 0

theorem CSD.Empirical.QM.BerryAdiabatic.rabiAxis_unit {θ ω B : ℝ} (hΩ : rabiFreq θ ω B ≠ 0) : rabiAxisX θ ω B ^ 2 + 0 ^ 2 + rabiAxisZ θ ω B ^ 2 = 1

The axis of K is a unit vector.

theorem CSD.Empirical.QM.BerryAdiabatic.zero_zero_one_unit : 0 ^ 2 + 0 ^ 2 + 1 ^ 2 = 1

The rigid rotation

theorem CSD.Empirical.QM.BerryAdiabatic.isHermitian_smul_pauliAxis (s a b c : ℝ) : (↑s • QuantumInfo.SU2.pauliAxis a b c).IsHermitian

theorem CSD.Empirical.QM.BerryAdiabatic.initHam_isHermitian (θ B : ℝ) : (initHam θ B).IsHermitian

theorem CSD.Empirical.QM.BerryAdiabatic.driveGen_isHermitian (ω : ℝ) : (driveGen ω).IsHermitian

theorem CSD.Empirical.QM.BerryAdiabatic.fieldHam_isHermitian (θ ω B t : ℝ) : (fieldHam θ ω B t).IsHermitian

theorem CSD.Empirical.QM.BerryAdiabatic.fieldHam_zero (θ ω B : ℝ) : fieldHam θ ω B 0 = initHam θ B

theorem CSD.Empirical.QM.BerryAdiabatic.driveGen_eq (ω : ℝ) : driveGen ω = ↑(ω / 2) • QuantumInfo.SU2.pauliAxis 0 0 1

theorem CSD.Empirical.QM.BerryAdiabatic.drive_zero (ω : ℝ) : drive ω 0 = 1

theorem CSD.Empirical.QM.BerryAdiabatic.drive_conjTranspose_mul (ω t : ℝ) : (drive ω t).conjTranspose * drive ω t = 1

theorem CSD.Empirical.QM.BerryAdiabatic.drive_conj_initHam (θ ω B t : ℝ) : drive ω t * initHam θ B * (drive ω t).conjTranspose = fieldHam θ ω B t

★ The field Hamiltonian is a rigid rotation of H(0): H(t) = R_z(ωt) H(0) R_z(ωt)ᴴ, by the Bloch rotation axisRot_z_conj.

theorem CSD.Empirical.QM.BerryAdiabatic.initHam_sub_driveGen {θ ω B : ℝ} (hΩ : rabiFreq θ ω B ≠ 0) : initHam θ B - driveGen ω = ↑(rabiFreq θ ω B / 2) • QuantumInfo.SU2.pauliAxis (rabiAxisX θ ω B) 0 (rabiAxisZ θ ω B)

★ The rotating-frame Hamiltonian K = H(0) − (ω/2)σ₃ is (Ω/2) k·σ for the unit axis k = (B sin θ, 0, B cos θ − ω)/Ω.

The exact solution

theorem CSD.Empirical.QM.BerryAdiabatic.prop_zero (θ ω B : ℝ) : prop θ ω B 0 = 1

theorem CSD.Empirical.QM.BerryAdiabatic.rabiProp_conjTranspose_mul {θ ω B : ℝ} (hΩ : rabiFreq θ ω B ≠ 0) (t : ℝ) : (rabiProp θ ω B t).conjTranspose * rabiProp θ ω B t = 1

theorem CSD.Empirical.QM.BerryAdiabatic.prop_conjTranspose_mul {θ ω B : ℝ} (hΩ : rabiFreq θ ω B ≠ 0) (t : ℝ) : (prop θ ω B t).conjTranspose * prop θ ω B t = 1

theorem CSD.Empirical.QM.BerryAdiabatic.hasDerivAt_prop {θ ω B : ℝ} (hΩ : rabiFreq θ ω B ≠ 0) (t : ℝ) : HasDerivAt (prop θ ω B) (-Complex.I • (fieldHam θ ω B t * prop θ ω B t)) t

★★★ The time-dependent Schrödinger equation, solved exactly. For a spin-½ in a field of magnitude B precessing on the cone of half-angle θ at angular velocity ω, the propagator V(t) = R_z(ωt) · R_k(Ωt) satisfies V′(t) = −i H(t) V(t), with V 0 = 1 (prop_zero) and V t unitary (prop_conjTranspose_mul). No approximation and no time ordering: the drive is a rigid rotation, so the rotating-frame generator K is constant.

theorem CSD.Empirical.QM.BerryAdiabatic.hasDerivAt_state {θ ω B : ℝ} (hΩ : rabiFreq θ ω B ≠ 0) (t : ℝ) : HasDerivAt (state θ ω B) (-Complex.I • (Matrix.toEuclideanCLM (fieldHam θ ω B t)) (state θ ω B t)) t

★★ The state solves the Schrödinger equation.

The instantaneous eigenvector is BP-2's cone curve

theorem CSD.Empirical.QM.BerryAdiabatic.coneCurve_ofLp (θ φ : ℝ) : (BerryPhase.coneCurve θ φ).ofLp = ![↑(Real.cos (θ / 2)), Complex.exp (↑φ * Complex.I) * ↑(Real.sin (θ / 2))]

theorem CSD.Empirical.QM.BerryAdiabatic.coneCurve_zero_eq_spinUp (θ : ℝ) : BerryPhase.coneCurve θ 0 = spinUp θ

theorem CSD.Empirical.QM.BerryAdiabatic.exp_ofReal_mul_I_eq (x : ℝ) : Complex.exp (↑x * Complex.I) = ↑(Real.cos x) + Complex.I * ↑(Real.sin x)

e^{ix} = cos x + i sin x with real casts, the one bridge between the cos/sin form of axisRot and the exponential form of the cone curve.

theorem CSD.Empirical.QM.BerryAdiabatic.fieldHam_mulVec_coneCurve (θ ω B t : ℝ) : (fieldHam θ ω B t).mulVec (BerryPhase.coneCurve θ (ω * t)).ofLp = ↑(B / 2) • (BerryPhase.coneCurve θ (ω * t)).ofLp

★★ The cone curve of BP-2 is the instantaneous eigenvector of the rotating field, with eigenvalue B/2: H(t) (cos θ/2, e^{iωt} sin θ/2) = (B/2) (cos θ/2, e^{iωt} sin θ/2). The ray loop whose geometric phase BerryPhase.geometricPhase_coneCurve computed is therefore exactly the loop this Hamiltonian traces out.

The Rabi overlap

noncomputable def CSD.Empirical.QM.BerryAdiabatic.cosDelta (θ ω B : ℝ) : ℝ

cos δ = k·n(0) = (B − ω cos θ)/Ω, the cosine of the angle between the rotating-frame axis and the initial field direction. One exact identity, ★ one_sub_cosDelta_sq, controls the whole adiabatic error: 1 − cos²δ = (ω sin θ/Ω)².

Equations

• CSD.Empirical.QM.BerryAdiabatic.cosDelta θ ω B = (B - ω * Real.cos θ) / CSD.Empirical.QM.BerryAdiabatic.rabiFreq θ ω B

theorem CSD.Empirical.QM.BerryAdiabatic.rabiFreq_sq_sub (θ ω B : ℝ) : rabiFreq θ ω B ^ 2 - (B - ω * Real.cos θ) ^ 2 = (ω * Real.sin θ) ^ 2

theorem CSD.Empirical.QM.BerryAdiabatic.rabiAxis_dot (θ ω B : ℝ) : rabiAxisX θ ω B * Real.sin θ + rabiAxisZ θ ω B * Real.cos θ = cosDelta θ ω B

theorem CSD.Empirical.QM.BerryAdiabatic.one_sub_cosDelta_sq {θ ω B : ℝ} (hΩ : rabiFreq θ ω B ≠ 0) : 1 - cosDelta θ ω B ^ 2 = (ω * Real.sin θ / rabiFreq θ ω B) ^ 2

★ The one exact identity behind both adiabatic bounds.

theorem CSD.Empirical.QM.BerryAdiabatic.cosDelta_nonneg {θ ω B : ℝ} (hω : 0 < ω) (hωB : ω < B) : 0 ≤ cosDelta θ ω B

theorem CSD.Empirical.QM.BerryAdiabatic.cosDelta_le_one {θ ω B : ℝ} (hΩ : rabiFreq θ ω B ≠ 0) : cosDelta θ ω B ≤ 1

Inner products of two-component states

theorem CSD.Empirical.QM.BerryAdiabatic.toEuclideanCLM_apply_eq (M : Matrix (Fin 2) (Fin 2) ℂ) (x : EuclideanSpace ℂ (Fin 2)) : (Matrix.toEuclideanCLM M) x = WithLp.toLp 2 (M.mulVec x.ofLp)

theorem CSD.Empirical.QM.BerryAdiabatic.inner_toLp (x y : Fin 2 → ℂ) : inner ℂ (WithLp.toLp 2 x) (WithLp.toLp 2 y) = (starRingEnd ℂ) (x 0) * y 0 + (starRingEnd ℂ) (x 1) * y 1

theorem CSD.Empirical.QM.BerryAdiabatic.spinUp_ofLp (θ : ℝ) : (spinUp θ).ofLp = ![↑(Real.cos (θ / 2)), ↑(Real.sin (θ / 2))]

theorem CSD.Empirical.QM.BerryAdiabatic.inner_spinUp_toLp (θ : ℝ) (y : Fin 2 → ℂ) : inner ℂ (spinUp θ) (WithLp.toLp 2 y) = ↑(Real.cos (θ / 2)) * y 0 + ↑(Real.sin (θ / 2)) * y 1

The inner product against the (real) initial state, with the conjugation already taken.

theorem CSD.Empirical.QM.BerryAdiabatic.inner_spinUp_self (θ : ℝ) : inner ℂ (spinUp θ) (spinUp θ) = 1

theorem CSD.Empirical.QM.BerryAdiabatic.inner_spinUp_pauliAxis (θ a b c : ℝ) : inner ℂ (spinUp θ) ((Matrix.toEuclideanCLM (QuantumInfo.SU2.pauliAxis a b c)) (spinUp θ)) = ↑(a * Real.sin θ + c * Real.cos θ)

★ The Bloch expectation of n·σ in the state spin-up along n(0) is n·n(0); the σ₂-component drops out because the state is real.

theorem CSD.Empirical.QM.BerryAdiabatic.inner_spinUp_rabiProp (θ ω B t : ℝ) : inner ℂ (spinUp θ) ((Matrix.toEuclideanCLM (rabiProp θ ω B t)) (spinUp θ)) = ↑(Real.cos (rabiFreq θ ω B * t / 2)) - Complex.I * ↑(cosDelta θ ω B * Real.sin (rabiFreq θ ω B * t / 2))

★★ The Rabi overlap. The rotating-frame evolution has diagonal matrix element ⟪ψ₀, e^{−itK} ψ₀⟫ = cos(Ωt/2) − i cos δ sin(Ωt/2) in the initial eigenstate.

The state in the instantaneous eigenbasis

theorem CSD.Empirical.QM.BerryAdiabatic.drive_mulVec_spinUp (θ ω t : ℝ) : (drive ω t).mulVec (spinUp θ).ofLp = ![Complex.exp (↑(-(ω * t / 2)) * Complex.I) * ↑(Real.cos (θ / 2)), Complex.exp (↑(ω * t / 2) * Complex.I) * ↑(Real.sin (θ / 2))]

theorem CSD.Empirical.QM.BerryAdiabatic.exp_real_add (x y : ℝ) : Complex.exp (↑(x + y) * Complex.I) = Complex.exp (↑x * Complex.I) * Complex.exp (↑y * Complex.I)

theorem CSD.Empirical.QM.BerryAdiabatic.coneCurve_eq_smul_drive (θ ω t : ℝ) : BerryPhase.coneCurve θ (ω * t) = Complex.exp (↑(ω * t / 2) * Complex.I) • (Matrix.toEuclideanCLM (drive ω t)) (spinUp θ)

★ BP-2's cone curve is the drive applied to the initial eigenstate, up to the phase e^{iωt/2}: the two lifts of the same ray loop differ by a gauge, which is exactly what GeometricPhase.geometricPhase_rephase says the geometric phase does not see.

theorem CSD.Empirical.QM.BerryAdiabatic.inner_coneCurve_state (θ ω B t : ℝ) : inner ℂ (BerryPhase.coneCurve θ (ω * t)) (state θ ω B t) = (starRingEnd ℂ) (Complex.exp (↑(ω * t / 2) * Complex.I)) * inner ℂ (spinUp θ) ((Matrix.toEuclideanCLM (rabiProp θ ω B t)) (spinUp θ))

theorem CSD.Empirical.QM.BerryAdiabatic.norm_inner_coneCurve_state_sq {θ ω B : ℝ} (hΩ : rabiFreq θ ω B ≠ 0) (t : ℝ) : ‖inner ℂ (BerryPhase.coneCurve θ (ω * t)) (state θ ω B t)‖ ^ 2 = 1 - (ω * Real.sin θ / rabiFreq θ ω B) ^ 2 * Real.sin (rabiFreq θ ω B * t / 2) ^ 2

★★★ Adiabatic following, exactly. The probability of still being in the instantaneous eigenstate at time t is 1 − (ω sin θ/Ω)² sin²(Ωt/2): an exact Rabi formula, with no approximation anywhere.

theorem CSD.Empirical.QM.BerryAdiabatic.one_sub_le_norm_inner_coneCurve_state_sq {θ ω B : ℝ} (hω : 0 < ω) (hωB : ω < B) (t : ℝ) : 1 - (ω / (B - ω)) ^ 2 ≤ ‖inner ℂ (BerryPhase.coneCurve θ (ω * t)) (state θ ω B t)‖ ^ 2

★★★ The adiabatic theorem for this model: for 0 < ω < B the spin stays in the instantaneous eigenstate up to a probability (ω/(B − ω))², uniformly in time — the rotating frame is exact here, so no T-dependence is lost.

The phase after one turn

theorem CSD.Empirical.QM.BerryAdiabatic.geometricPhase_cone_loop (θ : ℝ) {ω T : ℝ} (hT : ω * T = 2 * Real.pi) : GeometricPhase.geometricPhase (fun (t : ℝ) => BerryPhase.coneCurve θ (ω * t)) T 0 = -Real.pi * (1 - Real.cos θ)

★ The geometric phase of the loop the field traces in one turn is BP-2's −π(1 − cos θ), in the repo's own GeometricPhase.geometricPhase: the reparametrisation t ↦ ωt does not change it.

theorem CSD.Empirical.QM.BerryAdiabatic.drive_period {ω T : ℝ} (hT : ω * T = 2 * Real.pi) : drive ω T = -1

theorem CSD.Empirical.QM.BerryAdiabatic.state_period {θ ω B T : ℝ} (hT : ω * T = 2 * Real.pi) : state θ ω B T = -(Matrix.toEuclideanCLM (rabiProp θ ω B T)) (spinUp θ)

theorem CSD.Empirical.QM.BerryAdiabatic.inner_spinUp_state_period {θ ω B T : ℝ} (hT : ω * T = 2 * Real.pi) : inner ℂ (spinUp θ) (state θ ω B T) = -(↑(Real.cos (rabiFreq θ ω B * T / 2)) - Complex.I * ↑(cosDelta θ ω B * Real.sin (rabiFreq θ ω B * T / 2)))

theorem CSD.Empirical.QM.BerryAdiabatic.norm_inner_state_sub_exp_le {θ ω B T : ℝ} (hω : 0 < ω) (hωB : ω < B) (hT : ω * T = 2 * Real.pi) : ‖inner ℂ (spinUp θ) (state θ ω B T) - Complex.exp (↑(-(B / 2) * T - Real.pi * (1 - Real.cos θ)) * Complex.I)‖ ≤ Real.pi * ω / (2 * (B - ω)) + (ω / (B - ω)) ^ 2

★★★ The phase at the end of one turn is dynamical plus geometric. For 0 < ω < B and ωT = 2π, the overlap of the final state with the initial eigenstate is e^{i(−(B/2)T − π(1 − cos θ))} up to an error πω/(2(B − ω)) + (ω/(B − ω))²: the dynamical phase −(B/2)T = −∫₀ᵀ E dt plus the geometric phase −π(1 − cos θ) of BP-2 (★ geometricPhase_cone_loop), with an O(ω) error that is explicit, not asymptotic.