| <!-- | |
| Copyright (c) 2026 Ahmad Ali Parr and others. | |
| SPDX-License-Identifier: LicenseRef-CPSC-ESCL-1.0 OR AGPL-3.0-only | |
| --> | |
| # 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`. | |