paper/PAPER.md

Conservation-preserving compilation for a 1+1D lattice shadow of φ⁴

Ahmad Ali Parr · 10 October 2026

The paper is PAPER.tex. Build with latexmk -xelatex PAPER.tex (or lualatex). Informal sketches of the same proofs are in OPERATOR_PROOFS.md.

Abstract

See 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.

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

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.