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