LemmaStatement: AI-adaptedProof: AI-adaptedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The two-level rotating frame: conjugation identities, the transformed families and invariance of the level populations

Statement

Let $(σ_{x}, σ_{y}, σ_{z})$ be the Pauli matrices of Finite spin matrices clause (e), acting on $C^{2}$ in the orthonormal basis $(e_{↑}, e_{↓})$ of that clause, so that $σ_{z} = diag (1, - 1)$ , $σ_{x} σ_{y} = i σ_{z}$ , $σ_{y} σ_{z} = i σ_{x}$ and $σ_{z} σ_{x} = i σ_{y}$ ; write $I$ for the identity and let $P_{↑}, P_{↓}$ be the orthogonal projections onto $C e_{↑}$ and $C e_{↓}$ . Let $ℏ > 0$ , $ω, ω_{0}, Ω_{1} \in R$ , put $Δ : = ω_{0} - ω$ and, for $t \in R$ , $R (t) : = \cos ⁣ (\frac{ω t}{2}) I + i \sin ⁣ (\frac{ω t}{2}) σ_{z} .$ Then:

(a) Frame. For every $t$ the matrix $R (t)$ is unitary with $R (0) = I$ , the map $R$ is of class $C^{\infty}$ with $R^{'} (t) = \frac{i ω}{2} σ_{z} R (t),$ and $R (t) P_{↑} R (t)^{*} = P_{↑}$ , $R (t) P_{↓} R (t)^{*} = P_{↓}$ .

(b) Conjugation. For every $t$ , $R (t) σ_{x} R (t)^{*} = \cos (ω t) σ_{x} - \sin (ω t) σ_{y}, R (t) σ_{y} R (t)^{*} = \sin (ω t) σ_{x} + \cos (ω t) σ_{y}, R (t) σ_{z} R (t)^{*} = σ_{z} .$

(c) Circular drive. For the family $H_{c} (t) : = \frac{ℏ}{2} (ω_{0} σ_{z} + Ω_{1} (\cos (ω t) σ_{x} + \sin (ω t) σ_{y}))$ one has, for every $t$ , $R (t) H_{c} (t) R (t)^{*} + i ℏ R^{'} (t) R (t)^{*} = \frac{ℏ}{2} (Δ σ_{z} + Ω_{1} σ_{x}),$ which is a constant Hermitian matrix independent of $t$ .

(d) Linear drive. For the family $H_{l} (t) : = \frac{ℏ}{2} (ω_{0} σ_{z} + Ω_{1} \cos (ω t) σ_{x})$ put $A : = \frac{ℏ}{2} (Δ σ_{z} + \frac{Ω_{1}}{2} σ_{x}), B : = \frac{ℏ Ω_{1}}{8} (σ_{x} + i σ_{y}) .$ Then for every $t$ $R (t) H_{l} (t) R (t)^{*} + i ℏ R^{'} (t) R (t)^{*} = A + e^{2 i ω t} B + e^{- 2 i ω t} B^{*},$ and $∥ A ∥ \leq \frac{ℏ}{2} (∣ Δ ∣ + \frac{∣ Ω_{1} ∣}{2})$ , $∥ B ∥ = \frac{ℏ ∣ Ω_{1} ∣}{4}$ .

(e) Transformation of the dynamics. Assume Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $H : R \to End (C^{2})$ be continuous with Hermitian values, let $ψ : R \to C^{2}$ be of class $C^{1}$ with $i ℏ ψ^{'} (t) = H (t) ψ (t) (t \in R),$ and put $ψ_{R} : = R ψ$ and $H^{R} (t) : = R (t) H (t) R (t)^{*} + i ℏ R^{'} (t) R (t)^{*}$ . Then $ψ_{R}$ is of class $C^{1}$ and satisfies $i ℏ ψ_{R}^{'} (t) = H^{R} (t) ψ_{R} (t)$ for every $t$ ; the family $H^{R}$ is continuous with Hermitian values. Consequently, if $U$ is the unitary propagator of the norm-continuous family $H$ supplied by Norm Dyson series and uniqueness, then $U^{R} (t, s) : = R (t) U (t, s) R (s)^{*} (s, t \in R)$ is the unitary propagator of $H^{R}$ : it satisfies $i ℏ \partial_{t} U^{R} (t, s) = H^{R} (t) U^{R} (t, s)$ , $U^{R} (s, s) = I$ , the cocycle, and $U^{R} (t, s)^{*} = U^{R} (s, t)$ . Moreover for every solution $ψ$ of the $H$ -equation, every $t \in R$ and both signs $∙ \in {↑, ↓}$ , $⟨ P_{∙} ψ (t), ψ (t) ⟩ = ⟨ P_{∙} ψ_{R} (t), ψ_{R} (t) ⟩ .$

The lemma is a statement of finite-dimensional linear algebra and calculus for the displayed matrices; no physical identification, no measurement and no asymptotic claim is made.

Facts & Assumptions

Given: the Pauli matrices $σ_{x}, σ_{y}, σ_{z}$ on $C^{2}$ in the basis $(e_{↑}, e_{↓})$ ; the projections $P_{↑}, P_{↓}$ ; $ℏ > 0$ and $ω, ω_{0}, Ω_{1}, Δ$ ; the matrix $R (t)$ ; the families $H_{c}, H_{l}$ and the matrices $A, B$ ; where clause (e) is used, a continuous Hermitian family $H$ and a $C^{1}$ solution $ψ$ , and Countable Choice.

[F1]

The Pauli matrices. In the ordered basis $(e_{↑}, e_{↓})$ one has $σ_{x} = (\begin{array}{cc} 0 & 1 \\ 1 & 0 \end{array})$ , $σ_{y} = (\begin{array}{cc} 0 & - i \\ i & 0 \end{array})$ , $σ_{z} = (\begin{array}{cc} 1 & 0 \\ 0 & - 1 \end{array})$ , the matrices are Hermitian, $σ_{x}^{2} = σ_{y}^{2} = σ_{z}^{2} = I$ , $σ_{x} σ_{y} = i σ_{z}$ , $σ_{y} σ_{z} = i σ_{x}$ , $σ_{z} σ_{x} = i σ_{y}$ and $σ_{i} σ_{j} + σ_{j} σ_{i} = 2 δ_{i j} I$ for $i, j \in {x, y, z}$ ; products of matrices are computed entrywise-finitely (Finite spin matrices clause (e)).

[F2]

Complex exponential and trigonometric functions. For every real $θ$ , $e^{i θ} = \cos θ + i \sin θ$ , so $e^{i θ} = \overline{e^{- i θ}}$ ( $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ ); $\sin^{'} = \cos$ and $\cos^{'} = - \sin$ with the chain rule for $t \mapsto \sin (ω t)$ , $t \mapsto \cos (ω t)$ for constant $ω$ (The derivatives of sine and cosine are cosine and minus sine); and the addition formulas $\cos (u + v) = \cos u \cos v - \sin u \sin v$ , $\sin (u + v) = \sin u \cos v + \cos u \sin v$ hold for all real $u, v$ , so in particular $\cos (2 u) = \cos^{2} u - \sin^{2} u$ , $\sin (2 u) = 2 \sin u \cos u$ and $\cos^{2} u + \sin^{2} u = 1$ (The addition formulas for sine and cosine).

[F3]

The scalar product rule. If $f, g : R \to C$ are differentiable at $t$ — the difference quotients of real and imaginary parts converge, equivalently $(f (t + h) - f (t)) / h$ converges in $C$ — then $f g$ is differentiable at $t$ with $(f g)^{'} (t) = f^{'} (t) g (t) + f (t) g^{'} (t)$ , and sums and constant multiples obey the same rule (Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ applied to real and imaginary parts; The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set). Applying this to the finitely many entries of a product of $2 \times 2$ matrices whose entries are differentiable real functions of $t$ gives the entrywise product rule $(U V)^{'} = U^{'} V + U V^{'}$ for such matrix curves.

[F4]

Unitary propagator of a norm-continuous bounded family. If $H : R \to End (C^{2})$ is continuous with Hermitian values then it is norm-continuous with bounded self-adjoint values on every compact interval, and Norm Dyson series and uniqueness supplies a unique family $U (t, s)$ of unitary matrices with $U (s, s) = I$ , $U (t, s) U (s, r) = U (t, r)$ , $U (t, s)^{*} = U (s, t)$ , operator-norm continuity in $(t, s)$ , and operator-norm derivative $\partial_{t} U (t, s) = - \frac{i}{ℏ} H (t) U (t, s)$ ; for fixed $s$ it is the unique norm-continuous solution of that equation with $U (s, s) = I$ (Norm Dyson series and uniqueness clauses (b), (c), (d); The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F5]

Inner product. The pairing on $C^{2}$ is linear in the first argument and conjugate-linear in the second, and $⟨ U u, U v ⟩ = ⟨ u, v ⟩$ for unitary $U$ (Real and complex inner product spaces, with the inner product linear in the first argument); with $σ_{i}$ as in [F1], the projections $P_{↑} = \frac{1}{2} (I + σ_{z})$ and $P_{↓} = \frac{1}{2} (I - σ_{z})$ satisfy $P^{2} = P = P^{*}$ and act as the orthogonal projections onto the displayed basis vectors.

Proof

technique · direct; compute the displayed $2\times2$ matrices entrywise, differentiate the frame, and transform the differential equation by the product rule

Given: the data of the Statement and [F1]-[F5].

1.1F1F2givenalgebra

[The frame is a diagonal unitary] By [F1], $σ_{z} = diag (1, - 1)$ , so [F2] gives $R (t) = diag (e^{i ω t / 2}, e^{- i ω t / 2})$ in the basis $(e_{↑}, e_{↓})$ ; hence $R (t)^{*} = \overline{R (t)} = diag (e^{- i ω t / 2}, e^{i ω t / 2}) = R (t)^{- 1}$ by [F2], so $R (t)$ is unitary with $R (t) R (t)^{*} = R (t)^{*} R (t) = I$ and $R (0) = I$ . Since $R$ is diagonal, it commutes with the diagonal projections $P_{↑} = diag (1, 0)$ and $P_{↓} = diag (0, 1)$ , so $R (t) P_{∙} R (t)^{*} = P_{∙} R (t) R (t)^{*} = P_{∙}$ for both signs. This proves the unitarity, the initial value and the projection identities of (a).

1.2F1F2algebra

[Derivative of the frame] By [F2] and the chain rule, the entries $t \mapsto e^{\pm i ω t / 2}$ have derivatives $\pm \frac{i ω}{2} e^{\pm i ω t / 2}$ , so $R^{'} (t) = diag (\frac{i ω}{2} e^{i ω t / 2}, - \frac{i ω}{2} e^{- i ω t / 2}) = \frac{i ω}{2} diag (e^{i ω t / 2}, - e^{- i ω t / 2}) .$ Since $σ_{z} R (t) = diag (1, - 1) diag (e^{i ω t / 2}, e^{- i ω t / 2}) = diag (e^{i ω t / 2}, - e^{- i ω t / 2})$ by [F1] and entrywise matrix multiplication, $R^{'} (t) = \frac{i ω}{2} σ_{z} R (t)$ , which completes (a).

1.3F1F2algebra

[Conjugation identities] Write $r_{↑} : = e^{i ω t / 2}$ , $r_{↓} : = e^{- i ω t / 2}$ , so $R = diag (r_{↑}, r_{↓})$ . Multiplying the displayed $2 \times 2$ matrices [F1] entrywise, $R σ_{x} R^{*} = (\begin{array}{cc} 0 & r_{↑} \overline{r_{↓}} \\ r_{↓} \overline{r_{↑}} & 0 \end{array}), R σ_{y} R^{*} = (\begin{array}{cc} 0 & - i r_{↑} \overline{r_{↓}} \\ i r_{↓} \overline{r_{↑}} & 0 \end{array}), R σ_{z} R^{*} = σ_{z},$ because $σ_{z}$ is diagonal and commutes with $R$ . By [F2], $r_{↑} \overline{r_{↓}} = e^{i ω t / 2} e^{i ω t / 2} = e^{i ω t} = \cos (ω t) + i \sin (ω t)$ and $r_{↓} \overline{r_{↑}} = e^{- i ω t} = \cos (ω t) - i \sin (ω t)$ . Substituting, the first matrix equals $\cos (ω t) σ_{x} - \sin (ω t) σ_{y}$ and the second equals $\sin (ω t) σ_{x} + \cos (ω t) σ_{y}$ , by the entries displayed in [F1]. This proves (b).

2.1step 1.2step 1.3F1F2givenalgebra

[The circular family] By step 1.3 and the linearity of matrix multiplication, $R (t) (\cos (ω t) σ_{x} + \sin (ω t) σ_{y}) R (t)^{*} = \cos (ω t) (\cos (ω t) σ_{x} - \sin (ω t) σ_{y}) + \sin (ω t) (\sin (ω t) σ_{x} + \cos (ω t) σ_{y}) = (\cos^{2} (ω t) + \sin^{2} (ω t)) σ_{x} = σ_{x},$ the $σ_{y}$ coefficients cancelling, and $\cos^{2} + \sin^{2} = 1$ by [F2]. Since $R σ_{z} R^{*} = σ_{z}$ by step 1.3, $R (t) H_{c} (t) R (t)^{*} = \frac{ℏ}{2} (ω_{0} σ_{z} + Ω_{1} σ_{x}),$ and by step 1.2, $i ℏ R^{'} (t) R (t)^{*} = i ℏ \frac{i ω}{2} σ_{z} R (t) R (t)^{*} = - \frac{ℏ ω}{2} σ_{z}$ . Adding the two expressions gives $\frac{ℏ}{2} ((ω_{0} - ω) σ_{z} + Ω_{1} σ_{x}) = \frac{ℏ}{2} (Δ σ_{z} + Ω_{1} σ_{x})$ , a constant Hermitian matrix because $Δ, Ω_{1}$ are real and the $σ_{i}$ are Hermitian [F1]. This is (c).

2.2step 1.2step 1.3F1F2algebra

[The linear family] Again by step 1.3 and [F2], $R (t) (\cos (ω t) σ_{x}) R (t)^{*} = \cos^{2} (ω t) σ_{x} - \sin (ω t) \cos (ω t) σ_{y} = \frac{1 + \cos (2 ω t)}{2} σ_{x} - \frac{\sin (2 ω t)}{2} σ_{y},$ and $R σ_{z} R^{*} = σ_{z}$ , so $R (t) H_{l} (t) R (t)^{*} + i ℏ R^{'} (t) R (t)^{*} = \frac{ℏ}{2} (Δ σ_{z} + \frac{Ω_{1}}{2} σ_{x}) + \frac{ℏ Ω_{1}}{4} (\cos (2 ω t) σ_{x} - \sin (2 ω t) σ_{y}) = A + \frac{ℏ Ω_{1}}{4} (\cos (2 ω t) σ_{x} - \sin (2 ω t) σ_{y}) .$ By [F2], $e^{\pm 2 i ω t} = \cos (2 ω t) \pm i \sin (2 ω t)$ , so with $B = \frac{ℏ Ω_{1}}{8} (σ_{x} + i σ_{y})$ one has $e^{2 i ω t} B + e^{- 2 i ω t} B^{*} = \frac{ℏ Ω_{1}}{8} (e^{2 i ω t} (σ_{x} + i σ_{y}) + e^{- 2 i ω t} (σ_{x} - i σ_{y})) = \frac{ℏ Ω_{1}}{8} (2 \cos (2 ω t) σ_{x} - 2 \sin (2 ω t) σ_{y}),$ which is the displayed remainder; hence the factorised form of (d). Finally $∥ A ∥ = \frac{ℏ}{2} ∥ Δ σ_{z} + \frac{Ω_{1}}{2} σ_{x} ∥ \leq \frac{ℏ}{2} (∣ Δ ∣ + \frac{∣ Ω_{1} ∣}{2})$ because $σ_{z}, σ_{x}$ are Hermitian unitaries [F1], and $∥ σ_{x} + i σ_{y} ∥ = ∥ 2 σ_{+} ∥ = 2$ since $σ_{x} + i σ_{y} = (\begin{array}{cc} 0 & 2 \\ 0 & 0 \end{array})$ has operator norm $2$ by [F1]; hence $∥ B ∥ = \frac{ℏ ∣ Ω_{1} ∣}{8} \cdot 2 = \frac{ℏ ∣ Ω_{1} ∣}{4}$ . This is (d).

2.3step 1.1step 1.2F3givenalgebra

[Transformation of the equation] Let $H$ and $ψ$ be as in clause (e) and let $t \in R$ . The entries of $R$ are $C^{\infty}$ by step 1.1 and [F2], those of $ψ$ are $C^{1}$ by hypothesis, so by the entrywise product rule [F3] the product $ψ_{R} = R ψ$ is $C^{1}$ with $ψ_{R}^{'} (t) = R^{'} (t) ψ (t) + R (t) ψ^{'} (t) = \frac{i ω}{2} σ_{z} R (t) ψ (t) + R (t) (- \frac{i}{ℏ} H (t) ψ (t)),$ using step 1.2 and the equation $i ℏ ψ^{'} = H ψ$ . Multiplying by $i ℏ$ , $i ℏ ψ_{R}^{'} (t) = (- \frac{ℏ ω}{2} σ_{z} + R (t) H (t) R (t)^{*}) ψ_{R} (t) = H^{R} (t) ψ_{R} (t),$ since $R (t)^{*} = R (t)^{- 1}$ by step 1.1 and $i ℏ R^{'} (t) R (t)^{*} = - \frac{ℏ ω}{2} σ_{z}$ by step 1.2; the family $H^{R}$ is continuous with Hermitian values because $R$ is continuous unitary, $H$ is continuous Hermitian and $i ℏ R^{'} R^{*} = - \frac{ℏ ω}{2} σ_{z}$ is constant Hermitian. This proves the first assertion of (e).

2.4step 1.1step 1.2F3F4givenalgebra

[The transformed propagator] Let $U$ be the propagator of [F4]. By [F4] and step 1.1, $U^{R} (t, s) = R (t) U (t, s) R (s)^{*}$ is unitary, $U^{R} (s, s) = R (s) R (s)^{*} = I$ , and the cocycle and adjoint identities follow from those of $U$ and $R$ . For the derivative, [F4] gives operator-norm differentiability of $U (\cdot, s)$ , so by the entrywise product rule [F3] applied to the entries of $R (t) U (t, s) R (s)^{*}$ , $\partial_{t} U^{R} (t, s) = R^{'} (t) U (t, s) R (s)^{*} + R (t) \partial_{t} U (t, s) R (s)^{*} = \frac{i ω}{2} σ_{z} U^{R} (t, s) - \frac{i}{ℏ} R (t) H (t) U (t, s) R (s)^{*} = \frac{i ω}{2} σ_{z} U^{R} (t, s) - \frac{i}{ℏ} R (t) H (t) R (t)^{*} U^{R} (t, s),$ using step 1.2 and $R (t) R (t)^{*} = I$ ; multiplying by $i ℏ$ gives $i ℏ \partial_{t} U^{R} (t, s) = (R (t) H (t) R (t)^{*} - \frac{ℏ ω}{2} σ_{z}) U^{R} (t, s) = H^{R} (t) U^{R} (t, s)$ by step 1.1 and the definition of $H^{R}$ . Since $U^{R} (\cdot, s)$ is continuous with $U^{R} (s, s) = I$ and $H^{R}$ is norm-continuous with Hermitian values, [F4] identifies $U^{R} (\cdot, s)$ with the unique propagator of $H^{R}$ , so all conclusions of the "consequently" clause hold.

3.1step 1.1step 2.3F5algebra∎

[Invariance of the level populations] Let $ψ$ be a solution of the $H$ -equation and $t \in R$ . By step 2.3, $ψ (t) = R (t)^{*} ψ_{R} (t)$ ; since $R (t)$ is unitary [F5] and $R (t) P_{∙} R (t)^{*} = P_{∙}$ by step 1.1, $⟨ P_{∙} ψ (t), ψ (t) ⟩ = ⟨ P_{∙} R (t)^{*} ψ_{R} (t), R (t)^{*} ψ_{R} (t) ⟩ = ⟨ R (t) P_{∙} R (t)^{*} ψ_{R} (t), ψ_{R} (t) ⟩ = ⟨ P_{∙} ψ_{R} (t), ψ_{R} (t) ⟩,$ for both signs. This is the final assertion of (e).

Remarks

Where the two polarizations differ. For the circular family the transformed generator is the constant matrix $\frac{ℏ}{2} (Δ σ_{z} + Ω_{1} σ_{x})$ ; for the linear family it is its averaged constant matrix $A$ , with transverse coefficient $Ω_{1} / 2$ , plus the explicitly displayed counter-rotating term $e^{2 i ω t} B + e^{- 2 i ω t} B^{*}$ , which is the term dropped in a rotating-wave approximation. The lemma proves the exact identity; the size of the dropped term is bounded on the page that uses it.
No assumption on the sign of $ω$ . The identities hold for every real $ω$ , including $ω = 0$ , where $R \equiv I$ and the transformation is trivial; the matrix $H_{c}$ reduces to $\frac{ℏ}{2} (ω_{0} σ_{z} + Ω_{1} σ_{x})$ in that case.

Depends on

Dependency tree · 2 levels

Sources

B. Zwiebach, MIT 8.05 Quantum Physics II (Fall 2013), Chapter 7 'Two State Systems', Section 6 'Nuclear Magnetic Resonance', chapter pages 17-18: the rotating-frame state, the transformation H_R = i hbar (d_t U) U^dagger + U H_S U^dagger and the time-independent rotating-frame Hamiltonian for a circularly polarized field