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

Programming a GHZ circuit in Mercury, then the compile-time rejection and the admitted Ising ring
Mercury circuit demo (MP4) · GHZ ladder written, rejected, replaced by an admitted ZZ ring

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