Snapkitty/cpsc-qft

Mirrored from https://github.com/AHMADALIPARR/cpsc-qft at commit 34c4bab. Part of the SnapKitty October 2026 main drop. Paper: Snapkitty/cpsc-qft-paper.

CPSC — Conservation-Preserving Scattering Compiler

Proof-carrying lattice scattering for 1+1D scalar field theory. Conservation laws are compilation constraints, not post-selection filters.

Status: operator commutation closed. Every schedule the analyzer admits, Trotterized for any number of steps, commutes as an operator on (R²)^⊗N with the conserved operator of its mode (∑ Z at λ = 0, ∏ X for λ ≠ 0). The proof is in lean/CPSC/Operator.lean and uses no project axioms. Analyzer, orbit check, Trotter product, digest binding, and Q# emission all run. Paper: paper/PAPER.md.

Repository: AHMADALIPARR/cpsc-qft

Claim, precisely

Current NISQ scattering experiments often evolve a Trotter circuit and discard shots whose measured quantum numbers disagree with the input. CPSC inverts that. The compiler is only allowed to emit unitaries on the joint symmetry manifold

$${\mathcal{M}}_{\mathrm{s}\mathrm{y}\mathrm{m}}=\{U\in U(2^N)\mid [U,{\mathrm{\Pi }}_{\chi }]=0\mathrm{\forall }\chi \in \{P,Q\}\}\backslash mathcal\{M\}\_\{\backslash mathrm\{sym\}\}\; =\; \backslash \{\; U\; \backslash in\; U(2^N)\; \backslash mid\; [U,\; \backslash Pi\_\backslash chi]\; =\; 0\; \backslash ;\backslash forall\backslash ,\; \backslash chi\; \backslash in\; \backslash \{P,\; Q\backslash \}\; \backslash \}$$

and must attach a certificate that every emitted gate stays on that manifold. Energy is not an independent constraint: a time-independent Hamiltonian already satisfies $[H, H] = 0$, so $e^{-iHt}$ conserves energy exactly. The non-trivial compilation constraints are the symmetries of $H$ (here lattice momentum and a $\mathbb{Z}_2$ charge).

What is actually conserved in this model

The working model is a periodic qubit lattice standing in for the Ising limit of 1+1D $\phi^4$, not continuum $\phi^4$.

$$H=-J\sum _{i=0}^{N-1}{Z}_i{Z}_{i+1}+\lambda \sum _{i=0}^{N-1}{X}_{i}H\; =\; -J\; \backslash sum\_\{i=0\}^\{N-1\}\; Z\_i\; Z\_\{i+1\}\; +\; \backslash lambda\; \backslash sum\_\{i=0\}^\{N-1\}\; X\_i$$

The quartic written as $(g/4!)\sum_i X_i^4$ is identically proportional to the identity, because $X^2 = I$. It is recorded in src/cpsc/hamiltonian.py and then dropped. A faithful lattice $\phi^4$ needs a truncated real field per site (or a higher spin), which is listed as an open problem.

Quantity	Operator	Status in this repo
Charge $Q$	$\sum_i Z_i$	Proved. Admitted Ising schedules commute with $\sum Z$. A transverse flip moves magnetization and is rejected.
Spin flip	$\prod_i X_i$	Proved for $\lambda \neq 0$. Admitted spin-flip schedules commute with $\prod X$. A lone $Z$ breaks it and is rejected.
Momentum $P$	Generator of the cyclic shift $T$	Specified. Translation averaging is implemented classically for diagonal checks; block synthesis is not.
Energy $E$	$H$ itself	Automatic for exact $e^{-iHt}$. Not a separate compilation filter.

Mercury circuit demo (MP4) · GHZ ladder written, rejected, replaced by an admitted ZZ ring

Site

GitHub Pages serves docs/. The console is qsim.html. Rebuild it from the frontend with frontend/web/build.sh, which copies the bundle into docs/.

Layout

docs/SPECIFICATION.md     mathematical construction and PCSS workflow
docs/CHANNEL_PRUNING.md   channel rules and what they do not mean
docs/OPEN_PROBLEMS.md     remaining obligations (operator proof closed)
lean/CPSC/Operator.lean   closed operator commutation proof
lean/CPSC/Lemmas.lean     bridge theorems (completeness, non-vacuous rejection)
lean/Audit.lean           axiom audit (propext, Classical.choice, Quot.sound only)
lean/CPSC/Emitted.lean    sample certificate carrying emitted_commutes
qsharp/                   Ising and spin-flip Trotter operations
src/cpsc/                 analyzer, compiler, certificate binder
tests/                    adversarial rejection, orbit check, digest binding
paper/PAPER.md            paper landing page
paper/OPERATOR_PROOFS.md  mathematical write-up of the Lean theorems

Run the analyzer

python -m venv .venv && source .venv/bin/activate
pip install -e ".[dev]"
pytest -q
python -m cpsc.demo

Python 3.11+. No quantum hardware required. The demo is a statevector check on $N \le 8$.

Certificate story

The analyzer admits a schedule or rejects it. For every admitted schedule the Lean development proves the operator identity: the Trotter product of any length commutes with the mode invariant. See lean/CPSC/Operator.lean (admitted_trotter_commutes) and lean/Audit.lean. Rejection is not vacuous: with a nonzero rotation a transverse flip moves magnetization and a lone Z breaks $\prod X$. Emitted certificates carry the corresponding theorem (emitted_commutes).

Relation to existing methods

This is not a new symmetry. Block-diagonalization by a conserved charge is textbook. Symmetry-protected codes and subspace-preserving compilations (Qiskit Pauli evolution in a symmetry sector, PennyLane symmetry projection, verified quantum circuits in SQIR/Coq) already exist. The architectural bet is narrower: treat the allowed scattering channel of a lattice QFT as the synthesis domain, and ship the channel membership proof with the circuit. See docs/OPEN_PROBLEMS.md before citing novelty.

License

Dual strict copyleft. You may use this repository under either:

• the CPSC Eclipse Strict Copyleft License, Version 1.0 (LicenseRef-CPSC-ESCL-1.0), or
• the GNU Affero General Public License, Version 3 only (AGPL-3.0-only).

Both options are strict copyleft, including network use. This is not the Eclipse Public License, and it is not Apache-2.0. There is no classpath exception and no permissive relicensing. Headers on each source file are part of the notice. See LICENSE, NOTICE, and LICENSES/.

💼 Commercial License

This repository is published under CPSC-ESCL-1.0 or AGPL-3.0. Building a commercial product or service? A proprietary commercial license from Snapkitty Collective LLC lets you ship this code on terms other than CPSC-ESCL-1.0 or AGPL-3.0.

→ Get a commercial license · A.parr@belespritdaccord.uk