docs/SPECIFICATION.md

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

# Specification

## 1. Objects

A QFT specification is a tuple $\mathcal{S} = (\mathcal{H}, H, \mathcal{G})$.

- $\mathcal{H} = (\mathbb{C}^2)^{\otimes N}$, computational basis ordered little-endian.
- $H$ is the periodic transverse-field Ising Hamiltonian in Section 2.
- $\mathcal{G}$ is generated by the cyclic shift $T$ and by global $Z$ parity. Continuous $U(1)$ charge is not a symmetry of this $H$, because the transverse field flips $Q = \sum_i Z_i$ by $\pm 2$. The conserved charge used by the compiler is the $\mathbb{Z}_2$ parity $P_Z = \prod_i Z_i$, which does commute with every $X_i$ and every $ZZ$ term. Total magnetization is conserved only at $\lambda = 0$.

This corrects the draft spec, which listed $\Pi_Q = \sum_i Z_i$ as conserved for the interacting theory. It is not, once $\lambda \neq 0$.

A conservation invariant is a Hermitian operator $\Pi$ with $[H, \Pi] = 0$. A scattering channel is a pair of joint eigenspaces of the commuting family $\{\Pi_\chi\}$ with the same eigenvalues. A compiled circuit is a gate list intended to approximate $e^{-iHt}$ while remaining in the commutant of that family. A proof certificate is a Lean witness of that commutation, sector by sector. The witness is not yet constructed.

## 2. Hamiltonian

$$
H = -J \sum_{i=0}^{N-1} Z_i Z_{i+1} + \lambda \sum_{i=0}^{N-1} X_i
+ \frac{g}{24} \sum_{i=0}^{N-1} X_i^4
$$

with $Z_N = Z_0$. Since $X^4 = I$, the last sum is $(g/24) N \, I$ and does not affect scattering. The implemented operator omits it and records the identity.

At $\lambda = 0$, $H$ is diagonal and conserves magnetization $Q = \sum_i Z_i$. For $\lambda \neq 0$ the compiler must not claim magnetization conservation. It claims parity conservation, which holds for all $\lambda, J$.

## 3. Symmetry-constrained manifold

$$
\mathcal{M}_{\mathrm{sym}}
  = \{ U \in U(2^N) \mid [U, P_Z] = 0,\ [U, T] = 0 \}
$$

Translation invariance of $H$ puts $e^{-iHt}$ in the commutant of $T$. Parity does the same for $P_Z$. Completeness (obligation 3) is the statement that exact evolution already lies in $\mathcal{M}_{\mathrm{sym}}$. The compiler's job is to refuse gates that leave it, including gates introduced by a later hardware rewrite.

The group average

$$
\mathcal{P}(O) = \frac{1}{N} \sum_{k=0}^{N-1} T^{-k} O T^{k}
$$

projects onto translation-invariant operators. It is a synthesis constraint, not a post-selection on shots. Applying it to a Trotter factor that already came from a translation-invariant $H$ changes nothing. Applying it to an asymmetric gate (a defect, a boundary drive, a mis-routed CNOT pattern that is not shift-equivalent) either restores invariance or, in the analyzer, rejects the gate if the projection is not unitary on the code subspace.

Charge projection for $\mathbb{Z}_2$ is the average $(O + P_Z O P_Z)/2$.

## 4. Channel-space form

Let $\lambda$ run over joint eigenvalues of $(P_Z, P)$, where $P$ is lattice momentum, $T\lvert p\rangle = e^{-ip}\lvert p\rangle$, $p = 2\pi n / N$. Then

$$
U_{\mathrm{QFT}} = \bigoplus_\lambda U_\lambda
$$

on the exact evolution. The compiled operator is the direct sum of the blocks the synthesizer actually built. Blocks with $\lambda \neq \lambda_{\mathrm{in}}$ are absent from the gate list, not zeroed after measurement.

## 5. Algorithm (PCSS)

1. Symmetry analysis. From $\mathcal{S}$, take the commutant generators that are cheap to test: $P_Z$ always; $Q = \sum Z_i$ only if $\lambda = 0$; $T$ always.
2. Channel generation. Read $\lambda_{\mathrm{in}}$ from the input. The allowed subspace is the matching joint eigenspace. For a computational-basis input this is a single parity (and, if $\lambda = 0$, a single magnetization).
3. Constrained synthesis. Trotterize only terms that commute with the active generators. Map to hardware only through rewrites that are themselves certified, or reject the rewrite.
4. Certificate. Emit the Lean statement for the concrete gate list. Until the proof is filled, the certificate is an interface plus the Python rejection log.
5. Execution. Hardware noise can still leak. The certificate does not claim otherwise. Shot filters remain a diagnostic for the device, not a substitute for the compiler check.

## 6. Proof obligations

See `lean/CPSC/Certificate.lean` and `docs/OPEN_PROBLEMS.md`.

- Commutation: each emitted gate $G$ satisfies $[G, \Pi_\chi] = 0$.
- Leakage: the ideal compiled unitary has zero amplitude between distinct $\lambda$ sectors.
- Completeness: $e^{-iHt} \in \mathcal{M}_{\mathrm{sym}}$ whenever $[H, \Pi_\chi] = 0$.