% Copyright (c) 2026 Ahmad Ali Parr and others. % SPDX-License-Identifier: LicenseRef-CPSC-ESCL-1.0 OR AGPL-3.0-only % % Build: latexmk -xelatex PAPER.tex (lualatex also works) \documentclass[11pt]{article} \usepackage[a4paper,margin=2.5cm]{geometry} \usepackage{amsmath,amsthm} \usepackage{unicode-math} \setmainfont{Latin Modern Roman} \setmathfont{Latin Modern Math} \setmonofont{DejaVu Sans Mono}[Scale=0.82] \usepackage{microtype} \usepackage{booktabs} \usepackage{array} \usepackage{float} \newcolumntype{L}[1]{>{\raggedright\arraybackslash}p{#1}} \setlength{\emergencystretch}{2em} \usepackage{enumitem} \usepackage{fancyvrb} \usepackage{xcolor} \usepackage[font=small,labelfont=bf]{caption} \usepackage[colorlinks=true,linkcolor=blue!50!black,citecolor=blue!50!black,urlcolor=blue!50!black]{hyperref} \newtheorem{theorem}{Theorem}[section] \newtheorem{proposition}[theorem]{Proposition} \newtheorem{lemma}[theorem]{Lemma} \newtheorem{corollary}[theorem]{Corollary} \theoremstyle{definition} \newtheorem{definition}[theorem]{Definition} \newcommand{\lean}[1]{\texttt{#1}} \newcommand{\leanref}[1]{\par\smallskip\noindent{\small\textit{Lean:} \lean{#1}}} \newcommand{\PiX}{\Pi_X} \newcommand{\Mag}{M} \newcommand{\sgn}{\operatorname{sgn}} \fvset{fontsize=\small,frame=single,framesep=2mm,rulecolor=\color{black!30}} \title{Conservation-Preserving Compilation for a 1+1D Lattice Shadow of $\phi^4$} \author{Ahmad Ali Parr} \date{10 October 2026} \begin{document} \maketitle \begin{abstract} \noindent We implement a compilation architecture for lattice scattering in which the symmetries of the target Hamiltonian constrain circuit synthesis rather than filter measured shots. The working model is the periodic transverse-field Ising chain, the qubit shadow of 1+1D $\phi^4$, not continuum $\phi^4$. Two facts fix the compiler. The quartic written as $\sum_i X_i^4$ is a multiple of the identity. Z-parity is a symmetry only at $\lambda = 0$; for $\lambda \neq 0$ the conserved operator is the global spin flip $\prod_i X_i$. The repository supplies a symmetry analyzer, a translation-orbit check, a first-order Trotter product of admitted gates, a Q\# emission of those factors, and a certificate whose SHA-256 digest is bound to the gate list. On a 4-site chain the Ising schedule has Z-parity leakage 0, and the spin-flip schedule has $\prod X$ leakage 0 within roundoff. Inserting a forbidden gate fails compilation. A Lean development proves, without project axioms, that every admitted Trotter schedule commutes with the conserved operator on $(\mathbb{C}^2)^{\otimes N}$ for every lattice size and every angle. This paper describes what the code does. It proves operator commutation in Lean for every admitted schedule. It does not claim a continuum scattering amplitude. \end{abstract} \section{Introduction} NISQ scattering experiments typically evolve a Trotter circuit and then discard shots whose measured quantum numbers disagree with the input state. Post-selection of this kind is a diagnostic. It does not make the illegal amplitude unavailable to the device, and it gives a later hardware rewrite no reason to refuse a gate. The Conservation-Preserving Scattering Compiler (CPSC) inverts that order. A schedule is emitted only if every factor preserves the active symmetry and the gate support is closed under lattice translation. The emitted artifact carries a digest of the schedule, so changing any gate changes the digest and the edited circuit no longer matches its certificate. The target is not continuum $\phi^4$, for which Jordan, Lee, and Preskill gave the first quantum scattering algorithm~\cite{jlp2012,jlp2014}. It is the periodic transverse-field Ising model (TFIM) on $N$ qubits, with indices taken mod $N$: \begin{equation} H = -J \sum_{i=0}^{N-1} Z_i Z_{i+1} + \lambda \sum_{i=0}^{N-1} X_i . \label{eq:H} \end{equation} The original draft also carried a quartic term $(g/24)\sum_i X_i^4$. Because $X^2 = I$ for a Pauli operator, this term is a constant: \begin{equation} \frac{g}{24}\sum_{i=0}^{N-1} X_i^4 = \frac{gN}{24}\, I . \end{equation} It shifts the zero of energy and opens no scattering channel. The implementation records the shift and drops it. A genuine $\phi^4$ interaction requires a truncated-oscillator encoding with more than one qubit per site, which is left to future work (Section~\ref{sec:open}). \paragraph{Contributions.} (i) A correct identification of the conserved operator in each coupling regime, with a compile-time mode switch at $\lambda = 0$. (ii) A synthesis path that admits only symmetry-preserving, translation-closed factors and has no post-selection step. (iii) A SHA-256 certificate bound to the admitted schedule, rendered as a Lean fragment that carries a machine-checked operator commutation theorem (Appendix~\ref{app:proofs}). (iv) A Q\# emission whose operations are the hardware image of the admitted factors. \section{Which operator is actually conserved} \label{sec:symmetry} The conserved operator depends on $\lambda$: total Z-magnetization at $\lambda = 0$, and the global spin flip $\PiX$ for $\lambda \neq 0$. The draft listed $\Pi_Q = \sum_i Z_i$ as a symmetry of the interacting theory, which is false once $\lambda \neq 0$. \subsection{Magnetization fails at \texorpdfstring{$\lambda \neq 0$}{lambda != 0}} A single $X_j$ anticommutes with $Z_j$ and commutes with every other $Z_i$. Acting on a computational basis state it flips one spin and changes the magnetization by $\pm 2$: \begin{equation} \Bigl[X_j, \sum_i Z_i\Bigr] = [X_j, Z_j] = -2i\,Y_j \neq 0 . \end{equation} It also anticommutes with the Z-parity $\prod_i Z_i$. The transverse field is a sum of such terms, so neither magnetization nor Z-parity commutes with $H$ when $\lambda \neq 0$. \subsection{The spin flip is conserved for all \texorpdfstring{$\lambda$}{lambda}} The operator that commutes with both the bonds and the field is \begin{equation} \PiX = \prod_{i=0}^{N-1} X_i . \end{equation} Conjugation by $\PiX$ sends each $Z_i$ to $-Z_i$. A bond $Z_a Z_b$ picks up two minus signs and is invariant. Each $X_i$ commutes with $\PiX$ trivially. A lone $Z_i$ picks up one sign and anticommutes. Hence $[H, \PiX] = 0$ for every $J$ and $\lambda$. \subsection{Translation and energy} Translation $T\colon i \mapsto i + 1 \bmod N$ is a symmetry because the couplings are uniform and the lattice is periodic. Energy is not a separate compilation constraint: a time-independent $H$ already satisfies $[H, H] = 0$. A first-order Trotter product does not conserve $H$ exactly, so filtering on $\langle H \rangle$ after a step measures Trotter error, not a conservation-law violation. \subsection{Two compilation modes} \begin{table}[h] \centering \begin{tabular}{@{}lllll@{}} \toprule Mode & Condition & Conserved operator & Admitted & Rejected \\ \midrule Ising & $\lambda = 0$ & $\sum_i Z_i$ (and $\prod_i Z_i$) & ZZ ring, lone Z & single X \\ Spin-flip & $\lambda \neq 0$ & $\PiX = \prod_i X_i$ & ZZ ring, full X orbit & lone Z \\ \bottomrule \end{tabular} \caption{Admission rule per mode.} \label{tab:modes} \end{table} In both modes a schedule must also be a union of cyclic images. One bond is not a translation-invariant interaction; the ring $\{Z_0Z_1, Z_1Z_2, \dots, Z_{N-1}Z_0\}$ is. \section{Compiler} \lean{compile\_scattering} either emits a certified Trotter schedule or raises \lean{CompilationRejected}; there is no third outcome. It runs five steps: \begin{enumerate}[nosep] \item Choose the mode from $\lambda$: Ising if $\lambda = 0$, spin-flip otherwise. \item Check each requested gate against the mode's admission rule (Table~\ref{tab:modes}). Any forbidden gate raises \lean{CompilationRejected}. \item Reject any support that is not closed under the cyclic shift $i \mapsto i + 1 \bmod N$. \item Build a first-order Trotter product of the admitted local terms. \item Bind a certificate to the admitted list, the mode, and the Trotter parameters (Section~\ref{sec:cert}). \end{enumerate} \subsection{Trotter factors} With $n$ steps of size $dt = t/n$, the emitted unitary is \begin{equation} U(t) \approx \Bigl[\, \prod_{\langle a,b\rangle} e^{\,iJ\,dt\,Z_aZ_b} \prod_j e^{-i\lambda\,dt\,X_j} \Bigr]^{n} . \end{equation} ZZ gates apply $\exp(iJ\,dt\,Z_aZ_b)$, matching the $-J$ sign in $H$. X gates apply $\exp(-i\lambda\,dt\,X)$. A lone Z, when admitted in Ising mode, is a spectator: it carries no coupling in $H$ and does not evolve the state. Every factor commutes with the active symmetry, so the product does too. This is why the Trotter error described in Section~\ref{sec:symmetry} cannot leak amplitude out of the symmetry sector, even though it does perturb the energy. Theorem~\ref{thm:main} makes this statement exact and machine-checked. \subsection{Input sectors} In Ising mode the input is a computational basis state $|b\rangle$, which is an eigenstate of $\sum_i Z_i$. In spin-flip mode a raw basis state is not an eigenstate of $\PiX$, so it carries the wrong sector label. The input is instead the even cat state, a $+1$ eigenstate of $\PiX$: \begin{equation} |\psi_0\rangle = \tfrac{1}{\sqrt2}\bigl(|b\rangle + |\bar b\rangle\bigr), \qquad \PiX|\psi_0\rangle = +|\psi_0\rangle , \end{equation} where $\bar b$ is the bitwise complement of $b$. \subsection{No post-selection} The compiler has no post-selection step. Leakage out of the sector is computed only as a check that the emitted product stayed where synthesis put it. \section{Certificate} \label{sec:cert} The certificate is the SHA-256 digest of a canonical JSON payload that fixes the whole schedule. The payload contains the gate names, supports, and kinds; the mode; and $N$, $\lambda$, $J$, total time, and step count. Any edit to these fields changes the digest. The same payload is rendered as a Lean fragment. For the 4-site Ising ring the compiler emits: \begin{Verbatim} def emittedHash : String := "e92f82910385ae3c46acc5479d57f4c6357cbbf9bf77d668e469a64b281db8e5" def emittedGates : List GateKind := [.zz 0 1, .zz 1 2, .zz 2 3, .zz 3 0] theorem emitted_admitted : allPreserve preservesMagnetization emittedGates = true := by rfl theorem emitted_commutes {R : Type} [Lean.Grind.CommRing R] {n : Nat} (ι : R) (ang : Operator.Angles R) (steps : Nat) : Operator.Commutes (Operator.trotterOp (n := n) ι ang emittedGates steps) (Operator.invariant .ising) := Operator.admitted_trotter_commutes .ising ι ang emittedGates emitted_admitted steps \end{Verbatim} \lean{emitted\_admitted} is the Boolean admission check, discharged by reduction; \lean{rfl} fails if a forbidden constructor is inserted. \lean{emitted\_commutes} is the operator statement for the same gate list: every Trotter power of the emitted schedule commutes with the mode's conserved operator. The fragment is checked in \lean{lean/CPSC/Emitted.lean}. \paragraph{Operator commutation.} The file \lean{lean/CPSC/Operator.lean} lifts the Boolean check to operators. A state on $N$ qubits is a map from basis strings to a commutative ring $R$, so $R = \mathbb{C}$ gives $(\mathbb{C}^2)^{\otimes N}$, and operator product is composition. Each gate is written $c\,I + \iota s\,P$ for its Pauli generator $P$; since $P^2 = I$, this is $\exp(i\theta P)$ with $c = \cos\theta$ and $s = \sin\theta$. The file proves that every schedule the analyzer admits, repeated for any number of Trotter steps, commutes with $\sum_i Z_i$ in Ising mode and with $\PiX$ in spin-flip mode (Theorem~\ref{thm:main}). The result holds for every lattice size, ring, and angle, and its only axioms are Lean's standard \lean{propext}, \lean{Classical.choice}, and \lean{Quot.sound}. It also proves that rejection is not vacuous: when $\sin\theta \neq 0$, a transverse rotation moves magnetization and a lone Z rotation breaks $\PiX$ (Proposition~\ref{prop:neg}). The proofs are written out in Appendix~\ref{app:proofs} and the Lean development is mapped in Appendix~\ref{app:lean}. \section{Q\# emission} \lean{qsharp/ConservationPreservingScattering.qs} is the hardware image of the admitted factors, not a second analyzer. Its operations map one-to-one onto the compiler's output (Table~\ref{tab:qsharp}). Admission is decided once, on the host. The Q\# layer re-asserts that decision through \lean{RequireAdmitted} rather than re-deriving it. \begin{table}[h] \centering \begin{tabular}{@{}ll@{}} \toprule Operation & Role \\ \midrule \lean{ApplyZZRing} & The full bond orbit under translation \\ \lean{ApplyTransverseField} & The full X orbit; used only by the spin-flip schedule \\ \lean{IsingEvolution} & Trotter loop for Ising mode \\ \lean{SpinFlipEvolution} & Trotter loop for spin-flip mode \\ \lean{RequireAdmitted} & Fails if the host passes a schedule the analyzer refused \\ \lean{MeasureZParity} & Diagnostic only; it is not the compiler \\ \bottomrule \end{tabular} \caption{Q\# operations.} \label{tab:qsharp} \end{table} \section{Checks} All six numerical checks pass: both legal schedules show zero sector leakage, and all three illegal schedules are rejected at compile time (Table~\ref{tab:checks}). Figures come from the statevector prototype with $N = 4$, $J = 1$, $t = 0.4$, and eight Trotter steps. The \lean{pytest} suite reports 14 passed. \begin{table}[h] \centering \small \begin{tabular}{@{}llllL{5.6cm}@{}} \toprule Case & Mode & Seed & $\lambda$ & Observed \\ \midrule ZZ ring & Ising & \lean{0b0011} & 0 & Emitted; Z-parity leakage 0; certificate matches the ring, not the ring with \lean{X[0]} substituted \\ ZZ ring + \lean{X[2]} & Ising & -- & 0 & Rejected: odd X support changes Z-parity \\ Single bond & Ising & -- & 0 & Rejected: translation orbit not closed \\ ZZ ring + X orbit & Spin-flip & \lean{0b0001} & 0.5 & Emitted; $\prod X$ leakage 0 (roundoff $3.6\times10^{-15}$ clamped) \\ Spin-flip + \lean{Z[1]} & Spin-flip & -- & 0.5 & Rejected: lone Z anticommutes with $\prod X$ \\ Dropped quartic & -- & -- & -- & $Ng/24 = 0.1667$ at $g = 1$, on the identity \\ \bottomrule \end{tabular} \caption{Numerical checks.} \label{tab:checks} \end{table} The Lean side is checked the same way. \lean{lake build} succeeds on Lean 4.22.0 with no external dependencies. \lean{lake env lean Audit.lean} prints the axioms each main theorem depends on; every one lists only \lean{propext}, \lean{Classical.choice}, and \lean{Quot.sound}, and the sources contain no \lean{axiom}, \lean{sorry}, or \lean{native\_decide}. Inserting \lean{.transverseFlip 2} into the emitted Ising gate list makes \lean{emitted\_admitted} fail to compile, so the operator theorem cannot be stated for a tampered schedule. These checks are noiseless. Ideal zero leakage does not survive decoherence on hardware, and the certificate makes no claim that it does. \section{What is not proved} \label{sec:open} Operator commutation is closed (Section~\ref{sec:cert}, Appendix~\ref{app:proofs}). Four obligations remain open: \begin{itemize}[nosep] \item \emph{Instantiation at $\mathbb{C}$.} The proof is over an arbitrary commutative ring with gates written as $c\,I + \iota s\,P$. Connecting it to Mathlib's complex numbers and matrix exponential, so that $\exp(i\theta P) = \cos\theta\, I + i\sin\theta\, P$ is itself machine-checked, is not done. \item A noise bound relating device error rates to sector leakage. \item A truncated-oscillator encoding of genuine $\phi^4$, where the quartic is not an identity. \item A Lean checker wired into CI, so every emitted certificate is checked on commit. \end{itemize} Completeness holds inside each mode by construction of $H$. The Ising limit conserves magnetization, and the transverse-field model conserves $\PiX$. Projecting onto a magnetization sector at $\lambda \neq 0$ is refused, because that projection would discard part of the true evolution. The general construction overlaps with symmetry-sector simulators and with verified circuit compilers. What is specific here is the admission rule for this lattice shadow, the mode switch at $\lambda = 0$, and the digest bound to an admitted schedule whose operator semantics is proved. \section{Related work} Block-diagonalization of a Hamiltonian by a conserved charge is standard in exact diagonalization and tensor-network methods. Symmetry verification and post-selection~\cite{bonetmonroig2018,sagastizabal2019} are the error-mitigation approach this compiler declines to substitute for synthesis. Subspace-preserving evolution in existing quantum toolkits already builds a sector unitary once a symmetry is declared; CPSC differs in deriving which symmetry is valid from $\lambda$ and in refusing the wrong one. Machine-checked circuit semantics exist in other verification stacks, such as the Coq-verified VOQC optimizer~\cite{voqc}, but they do not encode this Hamiltonian or its admission rule. Formalization of free bosonic quantum field theory in Lean~\cite{douglas2026} targets continuum Euclidean axioms, not a lattice scattering schedule. The development here uses Lean~4~\cite{lean4} without Mathlib. Wave-packet scattering is the closest experimental neighbor. Zemlevskiy simulated two-particle wave-packet scattering in 1+1D scalar field theory on 120 qubits of IBM's Heron processor, the first such simulation in an interacting field theory, using symmetry- and locality-informed variational circuits~\cite{zemlevskiy2024}. For the Ising chain itself, Bennewitz et al.\ proposed preparing and colliding Gaussian meson wave packets on spin quantum simulators~\cite{bennewitz2024}, and Hite gave a simplified fermionic wave-packet preparation for the transverse-field Ising model, tested on IonQ hardware~\cite{hite2025}. CPSC currently uses basis and cat-state inputs; admitting wave-packet preparation circuits under the same certificate is a natural extension. \section{Conclusion} For the periodic transverse-field Ising chain, conservation can be enforced at synthesis rather than by discarding shots. The correct symmetry is Z-magnetization at $\lambda = 0$ and the global spin flip $\PiX$ for $\lambda \neq 0$; the draft's quartic term is a constant and is dropped. On a 4-site ring, legal schedules show zero ideal leakage, illegal ones fail to compile, and each emitted schedule carries a digest that breaks under edits. Operator commutation is proved in Lean for every admitted schedule; the next steps are a noise bound and a genuine $\phi^4$ encoding. \paragraph{AI assistance.} Drafting, editing, and the Lean operator development were assisted by Claude (Anthropic). The author reviewed the text; all Lean proofs are checked by the Lean kernel, and all numerical results come from the repository's test suite. \paragraph{Code and license.} Source: \url{https://github.com/AHMADALIPARR/cpsc-qft}. Dual strict copyleft: \lean{LicenseRef-CPSC-ESCL-1.0} OR \lean{AGPL-3.0-only}. Copyright \copyright\ 2026 Ahmad Ali Parr and others. \appendix \section{Operator proofs} \label{app:proofs} This appendix gives the mathematical argument that \lean{lean/CPSC/Operator.lean} checks. Each result names the Lean theorem that proves it. The proofs are elementary; the point of the formalization is that the Boolean admission predicate the compiler uses is now tied, by a kernel-checked proof, to the operator it is meant to approximate. \subsection{Setting} Fix a lattice of $N = n + 1 \ge 1$ sites and a commutative ring $R$. A \emph{basis string} is a map $b\colon \{0,\dots,N-1\} \to \{0,1\}$. A \emph{state} is a map $v$ from basis strings to $R$; for $R = \mathbb{C}$ the states form $(\mathbb{C}^2)^{\otimes N}$ in the computational basis. An \emph{operator} is a map on states, and the product $AB$ is composition. Operators $A$ and $P$ \emph{commute} if $A(Pv) = P(Av)$ for every state $v$ (\lean{Commutes}). Write $\sgn(x) = (-1)^x \in R$ for a bit $x$, $b^{(q)}$ for $b$ with bit $q$ flipped (\lean{flipAt}), and $\bar b$ for $b$ with every bit flipped (\lean{flipAll}). The operators are \begin{align*} (Z_q v)(b) &= \sgn(b_q)\, v(b), & (X_q v)(b) &= v(b^{(q)}), \\ (\PiX v)(b) &= v(\bar b), & (\Mag v)(b) &= m(b)\, v(b), \quad m(b) = \textstyle\sum_k \sgn(b_k). \end{align*} These are the standard actions of $Z_q$, $X_q$, $\prod_k X_k$, and $\sum_k Z_k$ on computational basis states. Fix an element $\iota \in R$ and coefficients $c, s \in R$. The gates are \begin{align*} \mathrm{RZZ}_{pq}(v)(b) &= \bigl(c + \iota s\, \sgn(b_p)\sgn(b_q)\bigr)\, v(b), & \mathrm{RX}_q(v)(b) &= c\, v(b) - \iota s\, v(b^{(q)}), \\ \mathrm{RZ}_q(v)(b) &= \bigl(c + \iota s\, \sgn(b_q)\bigr)\, v(b), & \mathrm{PAIR}_{pq} &= \mathrm{RX}_p\, \mathrm{RX}_q . \end{align*} These are exactly the factors applied by \lean{cpsc.channel}. \subsection{Gates are rotations} \begin{lemma}[Pauli squares] $Z_q^2 = I$, $X_q^2 = I$, and $\sgn(\bar x) = -\sgn(x)$, $\sgn(x)^2 = 1$. \leanref{Z\_sq, X\_sq, sgn\_not, sgn\_sq} \end{lemma} \begin{proof} $\sgn$ takes values $\pm1$ and flipping a bit swaps them. Flipping bit $q$ twice returns $b$. \end{proof} \begin{proposition}[Gate form] \label{prop:form} $\mathrm{RZZ}_{pq} = c\,I + \iota s\, Z_pZ_q$, $\mathrm{RX}_q = c\,I - \iota s\, X_q$, and $\mathrm{RZ}_q = c\,I + \iota s\, Z_q$. If $\iota^2 = -1$ and $c^2 + s^2 = 1$, the gate with $s$ replaced by $-s$ inverts $\mathrm{RX}_q$. \leanref{rzz\_eq, rx\_eq, rz\_eq, rx\_inverse} \end{proposition} \begin{proof} The first three identities follow by evaluating both sides at a basis string. For the inverse, \[ (c\,I + \iota s X_q)(c\,I - \iota s X_q) = c^2 I - \iota^2 s^2 X_q^2 = (c^2 + s^2)\, I = I . \] \end{proof} Over $R = \mathbb{C}$ with $\iota = i$, $c = \cos\theta$, $s = \sin\theta$: since $P^2 = I$ for each generator, the power series gives $\exp(\pm i\theta P) = \cos\theta\, I \pm i \sin\theta\, P$. So the gates are the rotations $e^{i\theta Z_pZ_q}$, $e^{-i\theta X_q}$, and $e^{i\theta Z_q}$. This last identification is the one step not formalized (Section~\ref{sec:open}). \subsection{Commutation is closed under products} \begin{lemma} \label{lem:comp} The identity commutes with every $P$. If $A$ and $B$ commute with $P$, so does $AB$. \leanref{commutes\_id, commutes\_comp} \end{lemma} \begin{proof} $A(B(Pv)) = A(P(Bv)) = P(A(Bv))$. \end{proof} \subsection{Admitted gates commute with the invariant} \begin{lemma} $\overline{b^{(q)}} = \bar b^{(q)}$: flipping one bit commutes with flipping all bits. \leanref{flipAt\_flipAll} \end{lemma} \begin{proposition}[Spin flip] \label{prop:spin} $\mathrm{RZZ}_{pq}$, $\mathrm{RX}_q$, and $\mathrm{PAIR}_{pq}$ commute with $\PiX$, for all $c, s, \iota$. \leanref{rzz\_comm\_PiX, rx\_comm\_PiX, pair\_comm\_PiX} \end{proposition} \begin{proof} For RZZ, both $(\mathrm{RZZ}\,\PiX v)(b)$ and $(\PiX\,\mathrm{RZZ}\, v)(b)$ equal a coefficient times $v(\bar b)$. The coefficients are $c + \iota s\,\sgn(b_p)\sgn(b_q)$ and $c + \iota s\,\sgn(\bar b_p)\sgn(\bar b_q)$, and these agree because the two sign changes cancel. For RX, \[ (\mathrm{RX}_q \PiX v)(b) = c\,v(\bar b) - \iota s\, v(\overline{b^{(q)}}), \qquad (\PiX \mathrm{RX}_q v)(b) = c\,v(\bar b) - \iota s\, v(\bar b^{(q)}), \] which agree by the preceding lemma. PAIR follows by Lemma~\ref{lem:comp}. \end{proof} \begin{proposition}[Magnetization] \label{prop:mag} $\mathrm{RZZ}_{pq}$ and $\mathrm{RZ}_q$ commute with $\Mag$, for all $c, s, \iota$. \leanref{diag\_comm\_Mag, rzz\_comm\_Mag, rz\_comm\_Mag} \end{proposition} \begin{proof} All three are diagonal: each multiplies $v(b)$ by a function of $b$. Diagonal operators commute because $R$ is commutative. \end{proof} \subsection{Rejection is not vacuous} \begin{lemma} \label{lem:magflip} $m(b^{(q)}) = m(b) + \sgn(\bar b_q) - \sgn(b_q) = m(b) - 2\sgn(b_q)$. \leanref{magUpTo\_flipAt, magVal\_flipAt} \end{lemma} \begin{proof} Only the $q$-th term of the sum changes. Lean proves the statement for every partial sum $\sum_{k