README.md

---
license: other
license_name: cpsc-escl-1.0-or-agpl-3.0-only
license_link: https://huggingface.co/Snapkitty/cpsc-qft/blob/main/LICENSE
tags:
- snapkitty
- october-2026-drop
- ruby
- python
- lean4
- qsharp
- quantum-field-theory
- lattice
- compiler
- quantum-computing
---

> Mirrored from [https://github.com/AHMADALIPARR/cpsc-qft](https://github.com/AHMADALIPARR/cpsc-qft) at commit `34c4bab`. Part of the **SnapKitty October 2026 main drop**. Paper: [Snapkitty/cpsc-qft-paper](https://huggingface.co/datasets/Snapkitty/cpsc-qft-paper).

<!--
Copyright (c) 2026 Ahmad Ali Parr and others.
SPDX-License-Identifier: LicenseRef-CPSC-ESCL-1.0 OR AGPL-3.0-only
This file is dual-licensed under the CPSC Eclipse Strict Copyleft License v1.0
or the GNU AGPL v3 only. Both are strict copyleft.
-->

# CPSC — Conservation-Preserving Scattering Compiler

> 💬 **Feedback wanted.** Build or tests failed for you, or reproduced the results? [Open a discussion](https://huggingface.co/Snapkitty/cpsc-qft/discussions/new). Part of our [flagship releases](https://huggingface.co/collections/Snapkitty/flagship-releases-october-2026-6acd83199105403d2fc0a4f2).

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](paper/PAPER.md).

Repository: [AHMADALIPARR/cpsc-qft](https://github.com/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{sym}} = \{ U \in U(2^N) \mid [U, \Pi_\chi] = 0 \;\forall\, \chi \in \{P, Q\} \}
$$

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
$$

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

<p align="center">
  <a href="docs/mercury-circuit-demo.mp4">
    <img src="docs/mercury-circuit-demo.gif" alt="Programming a GHZ circuit in Mercury, then the compile-time rejection and the admitted Ising ring" width="720">
  </a>
  <br>
  <a href="docs/mercury-circuit-demo.mp4">Mercury circuit demo (MP4)</a>
  · GHZ ladder written, rejected, replaced by an admitted ZZ ring
</p>

## Site

GitHub Pages serves `docs/`. The console is [qsim.html](https://ahmadaliparr.github.io/cpsc-qft/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

```bash
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](LICENSE), [NOTICE](NOTICE), and [LICENSES/](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](mailto:A.parr@belespritdaccord.uk?subject=Commercial%20license:%20cpsc-qft)** · A.parr@belespritdaccord.uk