The rotating frame: a time-dependent Schrödinger equation solved exactly

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

A Hamiltonian that is rigidly rotated by a one-parameter unitary group, H(t) = e^{−itG} H₀ e^{itG}, has an exactly solvable time-dependent Schrödinger equation: its propagator is V(t) = e^{−itG} · e^{−it(H₀ − G)}, the drive times the evolution generated by the constant rotating-frame Hamiltonian K = H₀ − G. ★★ hasDerivAt_rotProp proves V′(t) = −i H(t) V(t) (with V 0 = 1 and V t unitary), and ★ hasDerivAt_rotState transports it to a state V(t) ψ₀ of ℂᴺ.

The reduction is one line of algebra once it is stated in the right form: ★★ hasDerivAt_mul_of_gen asks only that u be generated by G on the right, that e be generated by K = H₀ − G on the left, and that u t be unitary — then u t (−iG) e t + u t (−iK) e t = u t (−iH₀) e t = −i H(t) · u t e t. Both instances in the corpus are four-line applications: the matrix exponential here, and the axis–angle rotations of spin-½ in CsdLean4/Empirical/QM/BerryAdiabatic.lean (BACKLOG #56, the adiabatic theorem for a spin in a rotating field), which never mention exp at all.

The second half of the file is the spin-½ calculus that application needs: the Hermitian Pauli combination pauliAxis a b c = a σ₁ + b σ₂ + c σ₃ with ★ pauliAxis_mul_self ((n·σ)² = ‖n‖² · 1), the rotations of SU2Rotation.lean written in terms of it (axisRot_eq), their derivative in the angle (★ hasDerivAt_axisRot, d/dt R_n(Ωt) = (−i(Ω/2) n·σ) R_n(Ωt), with no matrix exponential and no entrywise differentiation — the path is a scalar combination of two constant matrices) and the Bloch rotation ★ axisRot_z_conj: conjugating n·σ by a z-rotation turns n about z by the angle. That last identity is what makes a rotating field a rigid rotation of a fixed Hamiltonian.

Main declarations

• ★★ hasDerivAt_mul_of_gen — the rotating-frame reduction, hypothesis form;
• schrodingerUnitary_hasDerivAt_left — the left-generated twin of Matrix.schrodingerUnitary_hasDerivAt;
• rotHam, rotProp, rotHam_isHermitian, rotProp_zero, rotProp_mem_unitaryGroup;
• ★★ hasDerivAt_rotProp — V′ = −i H(t) V for V(t) = e^{−itG} e^{−it(H₀−G)};
• ★ hasDerivAt_rotState — the same equation for the state V(t) ψ₀ on ℂᴺ;
• inner_toEuclideanCLM_left and ★ inner_toEuclideanCLM_unitary — a matrix crosses an inner product as its conjugate transpose, and a unitary preserves it;
• pauliAxis, pauliAxis_isHermitian, su2_eq, pauliAxis_eq_smul_su2, su2_scalar, su2_mul_self_imaginary, pauliAxis_smul, smul_pauliAxis, pauliAxis_add, pauliAxis_sub, ★ pauliAxis_mul_self (with pauliAxis_mul_self_of_unit);
• axisRot_eq, su2_conjTranspose, axisRot_conjTranspose, axisRot_mul_conjTranspose, axisRot_two_pi, commute_smul_pauliAxis_axisRot;
• ★ smul_pauliAxis_mul_axisRot, ★ hasDerivAt_axisRot and ★ hasDerivAt_axisRot_right (the generator on either side), ★ su2_z_conj and ★ axisRot_z_conj.

Honest scope

⚠️ The drive is a rigid rotation: H(t) is the conjugation orbit of a single H₀ under a one-parameter group, so the eigenvalues never move. Nothing here treats a general time-dependent H(t), for which there is no closed form, nor the adiabatic theorem of Kato–Born–Fock in its general form (an arbitrary gapped path of Hamiltonians, error O(1/T)): that is BACKLOG #88, and it is not claimed anywhere in this corpus.

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

The reduction

theorem QuantumInfo.RotatingFrame.hasDerivAt_mul_of_gen {N : ℕ} {G H₀ : Matrix (Fin N) (Fin N) ℂ} {u e : ℝ → Matrix (Fin N) (Fin N) ℂ} {t : ℝ} (hu : HasDerivAt u (u t * -Complex.I • G) t) (he : HasDerivAt e (-Complex.I • (H₀ - G) * e t) t) (hU : (u t).conjTranspose * u t = 1) : HasDerivAt (fun (τ : ℝ) => u τ * e τ) (-Complex.I • (u t * H₀ * (u t).conjTranspose * (u t * e t))) t

★★ The rotating-frame reduction. If u is a matrix path generated by G on the right (u′ = u · (−iG)), e a path generated by K = H₀ − G on the left (e′ = (−iK) · e) and u t is unitary, then the product u e solves the time-dependent Schrödinger equation of the rigidly rotated Hamiltonian H(t) = u t · H₀ · (u t)ᴴ: (u e)′(t) = −i H(t) · (u t · e t).

Nothing is assumed about how u and e are built; the two instances in the corpus are the matrix exponential (hasDerivAt_rotProp) and the axis–angle rotations of spin-½.

theorem QuantumInfo.RotatingFrame.schrodingerUnitary_hasDerivAt_left {N : ℕ} (H : Matrix (Fin N) (Fin N) ℂ) (hH : H.IsHermitian) (t : ℝ) : HasDerivAt (fun (τ : ℝ) => ↑(Matrix.schrodingerUnitary hH τ)) (-Complex.I • H * ↑(Matrix.schrodingerUnitary hH t)) t

The left-generated twin of Matrix.schrodingerUnitary_hasDerivAt: the family U t = e^{−itH} also has derivative (−iH) · U t, since a matrix exponential commutes with its own generator.

The exponential instance

noncomputable def QuantumInfo.RotatingFrame.rotHam {N : ℕ} {G : Matrix (Fin N) (Fin N) ℂ} (hG : G.IsHermitian) (H₀ : Matrix (Fin N) (Fin N) ℂ) (t : ℝ) : Matrix (Fin N) (Fin N) ℂ

The rigidly rotated Hamiltonian H(t) = e^{−itG} H₀ e^{itG}.

Equations

• QuantumInfo.RotatingFrame.rotHam hG H₀ t = ↑(Matrix.schrodingerUnitary hG t) * H₀ * (↑(Matrix.schrodingerUnitary hG t)).conjTranspose

noncomputable def QuantumInfo.RotatingFrame.rotProp {N : ℕ} {G : Matrix (Fin N) (Fin N) ℂ} (hG : G.IsHermitian) {H₀ : Matrix (Fin N) (Fin N) ℂ} (hH : H₀.IsHermitian) (t : ℝ) : Matrix (Fin N) (Fin N) ℂ

The rotating-frame propagator V(t) = e^{−itG} · e^{−it(H₀ − G)}.

Equations

• QuantumInfo.RotatingFrame.rotProp hG hH t = ↑(Matrix.schrodingerUnitary hG t) * ↑(Matrix.schrodingerUnitary ⋯ t)

theorem QuantumInfo.RotatingFrame.rotHam_zero {N : ℕ} {G : Matrix (Fin N) (Fin N) ℂ} (hG : G.IsHermitian) (H₀ : Matrix (Fin N) (Fin N) ℂ) : rotHam hG H₀ 0 = H₀

theorem QuantumInfo.RotatingFrame.rotHam_isHermitian {N : ℕ} {G : Matrix (Fin N) (Fin N) ℂ} (hG : G.IsHermitian) {H₀ : Matrix (Fin N) (Fin N) ℂ} (hH : H₀.IsHermitian) (t : ℝ) : (rotHam hG H₀ t).IsHermitian

theorem QuantumInfo.RotatingFrame.rotProp_zero {N : ℕ} {G : Matrix (Fin N) (Fin N) ℂ} (hG : G.IsHermitian) {H₀ : Matrix (Fin N) (Fin N) ℂ} (hH : H₀.IsHermitian) : rotProp hG hH 0 = 1

theorem QuantumInfo.RotatingFrame.rotProp_mem_unitaryGroup {N : ℕ} {G : Matrix (Fin N) (Fin N) ℂ} (hG : G.IsHermitian) {H₀ : Matrix (Fin N) (Fin N) ℂ} (hH : H₀.IsHermitian) (t : ℝ) : rotProp hG hH t ∈ Matrix.unitaryGroup (Fin N) ℂ

theorem QuantumInfo.RotatingFrame.hasDerivAt_rotProp {N : ℕ} {G : Matrix (Fin N) (Fin N) ℂ} (hG : G.IsHermitian) {H₀ : Matrix (Fin N) (Fin N) ℂ} (hH : H₀.IsHermitian) (t : ℝ) : HasDerivAt (rotProp hG hH) (-Complex.I • (rotHam hG H₀ t * rotProp hG hH t)) t

★★ The rigidly rotated Hamiltonian has an exact propagator. For Hermitian G and H₀, the path V(t) = e^{−itG} e^{−it(H₀−G)} solves the time-dependent Schrödinger equation V′(t) = −i H(t) V(t) of H(t) = e^{−itG} H₀ e^{itG}, with V 0 = 1 (rotProp_zero) and V t unitary (rotProp_mem_unitaryGroup).

theorem QuantumInfo.RotatingFrame.hasDerivAt_rotState {N : ℕ} {G : Matrix (Fin N) (Fin N) ℂ} (hG : G.IsHermitian) {H₀ : Matrix (Fin N) (Fin N) ℂ} (hH : H₀.IsHermitian) (ψ₀ : EuclideanSpace ℂ (Fin N)) (t : ℝ) : HasDerivAt (fun (τ : ℝ) => (Matrix.toEuclideanCLM (rotProp hG hH τ)) ψ₀) (-Complex.I • (Matrix.toEuclideanCLM (rotHam hG H₀ t)) ((Matrix.toEuclideanCLM (rotProp hG hH t)) ψ₀)) t

★ The state form. The path ψ(t) = V(t) ψ₀ of ℂᴺ solves ψ′(t) = −i H(t) ψ(t).

Inner products on ℂᴺ

The two facts the state-level analysis needs: a matrix moves across an inner product as its conjugate transpose, and a unitary preserves the inner product.

theorem QuantumInfo.RotatingFrame.inner_toEuclideanCLM_left {N : ℕ} (A : Matrix (Fin N) (Fin N) ℂ) (x y : EuclideanSpace ℂ (Fin N)) : inner ℂ ((Matrix.toEuclideanCLM A) x) y = inner ℂ x ((Matrix.toEuclideanCLM A.conjTranspose) y)

theorem QuantumInfo.RotatingFrame.inner_toEuclideanCLM_unitary {N : ℕ} {U : Matrix (Fin N) (Fin N) ℂ} (hU : U.conjTranspose * U = 1) (x y : EuclideanSpace ℂ (Fin N)) : inner ℂ ((Matrix.toEuclideanCLM U) x) ((Matrix.toEuclideanCLM U) y) = inner ℂ x y

★ A unitary preserves the inner product of ℂᴺ.

The spin-½ calculus

The 2 × 2 layer the rotating-field application consumes: the Hermitian Pauli combination, the rotations of SU2Rotation.lean in terms of it, and their derivative in the angle.

def QuantumInfo.SU2.pauliAxis (a b c : ℝ) : Matrix (Fin 2) (Fin 2) ℂ

The Hermitian Pauli combination pauliAxis a b c = a σ₁ + b σ₂ + c σ₃. Its square is (a² + b² + c²) · 1 (★ pauliAxis_mul_self), so for a unit vector it is an involution with eigenvalues ±1, and (B/2) · pauliAxis is the Hamiltonian of a spin-½ in the field B·(a, b, c).

Equations

• QuantumInfo.SU2.pauliAxis a b c = !![↑c, ↑a - Complex.I * ↑b; ↑a + Complex.I * ↑b, -↑c]

theorem QuantumInfo.SU2.pauliAxis_isHermitian (a b c : ℝ) : (pauliAxis a b c).IsHermitian

theorem QuantumInfo.SU2.su2_eq (w x y z : ℝ) : su2 w x y z = ↑w • 1 - Complex.I • pauliAxis x y z

su2 w x y z = w·1 − i(x σ₁ + y σ₂ + z σ₃), in terms of pauliAxis.

theorem QuantumInfo.SU2.pauliAxis_eq_smul_su2 (a b c : ℝ) : pauliAxis a b c = Complex.I • su2 0 a b c

pauliAxis is i times a purely imaginary quaternion: this is how it inherits the quaternion product su2_mul.

theorem QuantumInfo.SU2.su2_scalar (w : ℝ) : su2 w 0 0 0 = ↑w • 1

A real quaternion is a scalar matrix.

theorem QuantumInfo.SU2.su2_mul_self_imaginary (a b c : ℝ) : su2 0 a b c * su2 0 a b c = su2 (-(a ^ 2 + b ^ 2 + c ^ 2)) 0 0 0

The square of a purely imaginary quaternion is the real scalar −‖·‖².

theorem QuantumInfo.SU2.pauliAxis_smul (s a b c : ℝ) : pauliAxis (a * s) (b * s) (c * s) = ↑s • pauliAxis a b c

pauliAxis is linear in the vector.

theorem QuantumInfo.SU2.pauliAxis_mul_self (a b c : ℝ) : pauliAxis a b c * pauliAxis a b c = ↑(a ^ 2 + b ^ 2 + c ^ 2) • 1

★ (n·σ)² = ‖n‖² · 1.

theorem QuantumInfo.SU2.pauliAxis_mul_self_of_unit {a b c : ℝ} (hu : a ^ 2 + b ^ 2 + c ^ 2 = 1) : pauliAxis a b c * pauliAxis a b c = 1

theorem QuantumInfo.SU2.axisRot_eq (a b c θ : ℝ) : axisRot a b c θ = ↑(Real.cos (θ / 2)) • 1 - (Complex.I * ↑(Real.sin (θ / 2))) • pauliAxis a b c

The axis rotation in terms of pauliAxis: R_n(θ) = cos(θ/2)·1 − i sin(θ/2) n·σ. Both matrices on the right are constant in θ, which is what makes the derivative elementary.

theorem QuantumInfo.SU2.su2_conjTranspose (w x y z : ℝ) : (su2 w x y z).conjTranspose = su2 w (-x) (-y) (-z)

theorem QuantumInfo.SU2.axisRot_conjTranspose (a b c θ : ℝ) : (axisRot a b c θ).conjTranspose = axisRot a b c (-θ)

theorem QuantumInfo.SU2.axisRot_mul_conjTranspose {a b c : ℝ} (hu : a ^ 2 + b ^ 2 + c ^ 2 = 1) (θ : ℝ) : axisRot a b c θ * (axisRot a b c θ).conjTranspose = 1

theorem QuantumInfo.SU2.axisRot_two_pi (a b c : ℝ) : axisRot a b c (2 * Real.pi) = -1

A 2π rotation is −1: the sign that turns the phase accumulated around a closed loop into the geometric phase.

theorem QuantumInfo.SU2.smul_pauliAxis_mul_axisRot {a b c : ℝ} (hu : a ^ 2 + b ^ 2 + c ^ 2 = 1) (Ω θ : ℝ) : (-Complex.I * ↑(Ω / 2)) • pauliAxis a b c * axisRot a b c θ = ↑(-(Ω / 2) * Real.sin (θ / 2)) • 1 - (Complex.I * ↑(Ω / 2 * Real.cos (θ / 2))) • pauliAxis a b c

★ The algebraic heart of the derivative: (−i(Ω/2) n·σ) · R_n(θ) in cos/sin form, for a unit axis.

theorem QuantumInfo.SU2.hasDerivAt_axisRot {a b c : ℝ} (hu : a ^ 2 + b ^ 2 + c ^ 2 = 1) (Ω t : ℝ) : HasDerivAt (fun (τ : ℝ) => axisRot a b c (Ω * τ)) ((-Complex.I * ↑(Ω / 2)) • pauliAxis a b c * axisRot a b c (Ω * t)) t

★ The derivative of an axis rotation. d/dt R_n(Ωt) = (−i(Ω/2) n·σ) · R_n(Ωt): the rotation about a unit axis is the Schrödinger evolution generated by the constant Hamiltonian (Ω/2) n·σ. No matrix exponential and no entrywise differentiation is involved — R_n(Ωt) is a scalar combination of the two constant matrices 1 and n·σ.

theorem QuantumInfo.SU2.su2_z_conj (a b c φ : ℝ) : axisRot 0 0 1 φ * su2 0 a b c * (axisRot 0 0 1 φ).conjTranspose = su2 0 (a * Real.cos φ - b * Real.sin φ) (a * Real.sin φ + b * Real.cos φ) c

★ The Bloch rotation, quaternion form.

theorem QuantumInfo.SU2.axisRot_z_conj (a b c φ : ℝ) : axisRot 0 0 1 φ * pauliAxis a b c * (axisRot 0 0 1 φ).conjTranspose = pauliAxis (a * Real.cos φ - b * Real.sin φ) (a * Real.sin φ + b * Real.cos φ) c

★ The Bloch rotation. Conjugating n·σ by the z-rotation R_z(φ) turns n about the z-axis by φ. This is the SU(2) → SO(3) homomorphism on one axis, and it is what lets a rotating field be written as a rigid rotation of a fixed Hamiltonian.

theorem QuantumInfo.SU2.pauliAxis_add (a b c a' b' c' : ℝ) : pauliAxis a b c + pauliAxis a' b' c' = pauliAxis (a + a') (b + b') (c + c')

theorem QuantumInfo.SU2.pauliAxis_sub (a b c a' b' c' : ℝ) : pauliAxis a b c - pauliAxis a' b' c' = pauliAxis (a - a') (b - b') (c - c')

theorem QuantumInfo.SU2.smul_pauliAxis (s a b c : ℝ) : ↑s • pauliAxis a b c = pauliAxis (s * a) (s * b) (s * c)

pauliAxis_smul with the scalar on the left.

theorem QuantumInfo.SU2.commute_smul_pauliAxis_axisRot (z : ℂ) (a b c θ : ℝ) : z • pauliAxis a b c * axisRot a b c θ = axisRot a b c θ * z • pauliAxis a b c

n·σ commutes with every rotation about n.

theorem QuantumInfo.SU2.hasDerivAt_axisRot_right {a b c : ℝ} (hu : a ^ 2 + b ^ 2 + c ^ 2 = 1) (Ω t : ℝ) : HasDerivAt (fun (τ : ℝ) => axisRot a b c (Ω * τ)) (axisRot a b c (Ω * t) * (-Complex.I * ↑(Ω / 2)) • pauliAxis a b c) t

★ hasDerivAt_axisRot with the generator on the right, the form the rotating-frame reduction takes for the drive.