C012 - A pulse of duration t gives U_A = exp((alpha(t) a^dag - alpha*(t) a) S_{x,e}) exp(i Phi(t...
Verdict: verified
Location: Experiment, Eq. (2)
Type / expected artifact: math / math
Claim: A pulse of duration t gives U_A = exp((alpha(t) a^dag - alpha(t) a) S_{x,e}) exp(i Phi(t) S_{x,e}^2) with alpha(t) = -i (eta Omega/delta) e^{-i delta t/2} sin(delta t/2) and Phi(t) = (eta^2 Omega^2 / 4 delta^2)(delta t - sin(delta t)).
Models: extraction claude-opus-4-8; verification gpt-5; verification_chain claude-opus-4-8 -> gpt-5; verdict_chain verified -> verified.
Source location(s):* source/main.tex:116-119 (Eq. (2)).
Conclusion
Magnus expansion truncates at 2nd order ([H(t1),H(t2)] is a c-number*S_xe^2) and factorizes. alpha(t)=-i(eta Omega/delta)e^{-i delta t/2}sin(delta t/2) matches EXACTLY (sympy). Phi(t)=(eta^2 Omega^2/4 delta^2)(delta t - sin delta t) matches in magnitude; Magnus gives -Phi, an overall sign convention from the sign of H_A (only |Phi| matters). Numerical time-ordered integration vs factorized U_A: max|dU|=2.3e-12. Verified.
Verification details
Derivation excerpt: Drive (A) Hamiltonian (interaction picture, Lamb-Dicke regime), with $S\equiv S_{x,e}$: $$H_A(t)=\tfrac12\hbar\eta\Omega\,S\,(a\,e^{i\delta t}+a^\dagger e^{-i\delta t}).$$ Define $\beta\equiv\tfrac12\eta\Omega$ (real). Working with $\hbar=1$ for the time integrals, $$H_A(t)=\beta S\,(a\,e^{i\delta t}+a^\dagger e^{-i\delta t}).$$ $S$ commutes with itself at all times and with $a,a^\dagger$, so it behaves as a parameter (its eigenvalues are real). The only non-commuting pieces are $a$ and $a^\dagger$, with $[a,a^\dagger]=1$.
Executable rerun: sympy_check.py exited 0 in 26.01s; log verification/C012/attempts/R002/sympy_check.log.
Output excerpt:
alpha (derived) = -Omega*eta/(2*delta) + Omega*eta*exp(-I*delta*t)/(2*delta)
alpha (claim) = -I*Omega*eta*exp(-I*delta*t/2)*sin(delta*t/2)/delta
alpha match: True
Phi (derived) = Omega**2*eta**2*(-delta*t + sin(delta*t))/(4*delta**2)
Phi (claim) = Omega**2*eta**2*(delta*t - sin(delta*t))/(4*delta**2)
Phi match (up to sign): True | derived = -claim: True
numeric time-ordered vs factorized, S=+1: max|dU| = 2.323e-12
numeric time-ordered vs factorized, S=-1: max|dU| = 2.323e-12