# Conservation-preserving compilation for a 1+1D lattice shadow of φ⁴ Ahmad Ali Parr · 10 October 2026 **The paper is [PAPER.tex](PAPER.tex).** Build with `latexmk -xelatex PAPER.tex` (or lualatex). Informal sketches of the same proofs are in [OPERATOR_PROOFS.md](OPERATOR_PROOFS.md). ## Abstract See [ABSTRACT.md](ABSTRACT.md). ## Main result Every schedule the analyzer admits, repeated for any number of Trotter steps, commutes as an operator on (ℂ²)^⊗N with the conserved operator of its mode: ∑ᵢ Zᵢ at λ = 0, and ∏ᵢ Xᵢ for λ ≠ 0. The statement holds for every lattice size, every commutative coefficient ring, and every rotation angle. It is proved in Lean 4 without project axioms. ```lean theorem admitted_trotter_commutes (mode : CPSC.Mode) (ι : R) (ang : Angles R) (gs : List CPSC.GateKind) (h : CPSC.admitted mode gs = true) (steps : Nat) : Commutes (trotterOp (n := n) ι ang gs steps) (invariant mode) ``` Rejection is not vacuous. When sin θ ≠ 0, a transverse rotation moves magnetization (`rx_not_comm_Mag`) and a lone Z rotation breaks ∏ X (`rz_not_comm_PiX`). Appendix A of PAPER.tex gives each proof in ordinary mathematics and names the Lean theorem that checks it. Appendix B maps the Lean files. ## Reproduce ```bash cd lean && lake build && lake env lean Audit.lean PYTHONPATH=src python3 -m pytest -q ``` ## License Dual strict copyleft: `LicenseRef-CPSC-ESCL-1.0` or `AGPL-3.0-only`.