docs/OPEN_PROBLEMS.md

Open problems

Marked POSSIBLY_NOVEL in the draft. The honest status is: executable prototype with a Boolean certificate. Operator commutation is now proved in Lean; prior art is not cleared.

Discharged in the prototype

1. Boolean admission. lean/CPSC/Certificate.lean reduces the 4-site ring and both adversarial extensions by rfl.
2. Digest binding. cpsc.certificate hashes the schedule. Editing a gate makes Certificate.matches false.
3. Mode switch. λ = 0 rejects a single X. λ ≠ 0 rejects a lone Z. Translation orbits must be closed.
4. Operator commutation. lean/CPSC/Operator.lean proves that every admitted Trotter schedule commutes with ∑ Z or ∏ X on (R²)⊗N, for any commutative ring R, lattice size, and angles. No project axioms; see lean/Audit.lean.

Obligations not discharged

1. Instantiation at ℂ and Matrix.exp. The proof is over an arbitrary commutative ring with gates written as c·I + ι s·P; identifying these with exp(iθP) over ℂ is the standard P² = I argument, stated in the file but not formalized against Mathlib.
2. Leakage under hardware noise. Ideal leakage on N = 4 is zero; device leakage is unmodeled.
3. Momentum as an eigenspace, rather than orbit closure of the gate support.
4. A non-trivial φ⁴ encoding. X^4 = I on qubits. The next model is a truncated oscillator per site.
5. A Lean binary in CI. lake build passes locally on Lean 4.22.0; no CI workflow runs it yet.
6. Python and Lean disagree on rx_pair in Ising mode. SymmetryAnalyzer admits parity_even at λ = 0 (see test_legal_circuit_admitted), while preservesMagnetization (.parityEvenPair _ _) is false, because X_a X_b changes magnetization. At λ = 0 the pair evolves with angle 0, so the state is unaffected, but a certificate emitted for such a schedule fails emitted_admitted. One of the two rules should change.

Collisions

• Post-selection on symmetry bits (symmetry verification, symmetry-protected mitigation) is the method this repo refuses to call a compiler.
• Subspace-preserving compilation and Pauli twirling / sector projection in Qiskit and PennyLane already build the block-diagonal evolution for a declared symmetry.
• Verified circuit compilers (VOQC, SQIR, CertiQ-style stacks) already attach machine-checked semantics to gate lists. They do not know about $\phi^4$.
• SPT phases are a property of a ground state, not of a synthesizer. The analogy in the draft is motivational only.

What would make the novelty claim true

A released artifact where (i) the channel projector is derived from a stated lattice QFT, (ii) every hardware rewrite is rejected or proved inside the commutant, and (iii) a Lean checker fails closed on an edited circuit. The prototype now rejects illegal gates and binds a digest. An edited schedule with a forbidden gate now fails the Lean check, and the operator identity for an admitted schedule is a theorem.