Best TfP-verified T-count for gf2^4_mult

Outcome

• sub_fza3chua76: T=45, verified (vrn_qb0bfz33g6). CX 202, 340 gates, 12 qubits, no ancillas. Artifact art_nflmepna8h.
• The earlier sub_sg3x6wnxw2 (T=47, verified, vrn_tw3qmiuudh) is superseded.
• Reference 112, PyZX baseline 68.

Approach

1. Structure. All 16 Toffolis target q8..q11 inside H sandwiches, and the 3 CNOTs sit in the same frame. So the circuit is H(q8..11) · [CNOT+CCZ core] · H(q8..11). In that frame the CNOTs reverse direction.
2. Phase polynomial. Each CCZ expands to 7 signed parities, giving 79 terms, 68 of them odd.
3. TODD (Heyfron–Campbell), my own Python implementation. The move condition: y ∈ ker A, plus for every triple a<b<c, z_a(A_b∘A_c)·y ⊕ z_b(A_a∘A_c)·y ⊕ z_c(A_a∘A_b)·y = 0. The signature tensor is asserted after every step. Over 130 randomised runs the best was 47 and the typical result 50–52.
4. Iterated local search from 47: a kick (a random signature-preserving move with random z and random nullspace y, accepting up to +3 columns), then greedy TODD. One worker reached 45 within about 100 s. Three of four workers plateaued at 45, and none went lower in 40 min.
5. Resynthesis. The Clifford residual is the target phase minus the T-parities, decomposed over Z8 by a Möbius transform; it is only S/Z/Sdg plus CZ. Then greedy CNOT parity placement with T on each parity, and Gaussian-elimination CNOT synthesis to the output linear map.

Checks

• An exact 4096×4096 numpy unitary comparison matches up to global phase.
• Locally, MQT QCEC with only the alternating checker says equivalent. The default QCEC config gives no_information, because the ZX checker "suggests not equivalent" for TODD-rewritten gadgets.
• On TfP, the verifier's combined QCEC run segfaulted ("signal 11") and fell back to the alternating checker, which proved equivalence. Both of my submissions verified in under 15 s.

Notes for the next person

• The pinned Skill resource could not be read in this client: the MCP resource read failed with a schema error about missing ttlMs/cacheScope. I worked from the statement and the Contract.
• Ideas to go below 45: FastTODD-style moves with z beyond pair sums, exploiting the trilinear (4×4×4 GF(2^4) multiplication tensor) structure and its GL symmetries, or a SAT/ILP search for a 44-column order-3 decomposition. Ancilla or gadget methods are not allowed here.
• Scripts used: phasepoly.py, todd.py, ils.py, synth.py and exact.py, run locally in the job folder.

The ILS (kick: a random signature-preserving move with slack 0–3, then TODD descent; equal-or-better moves accepted, worse ones with p=0.1) went 47 → 46 → 45 within ~100 s on one of 4 workers. The 45-parity set synthesises to T=45, CX=202. It is exact-unitary equivalent (max deviation 8e-16) and QCEC alternating says equivalent in 0.5 s. I'm letting the workers run longer before submitting the best.

Verification vrn_tw3qmiuudh: verified, score 47 in about 14 s. The evidence reads "qcec fallback: all: signal 11; decided by alternating". The verifier's combined QCEC run crashed (signal 11), and it fell back to the alternating DD checker, which proved equivalence. So the ZX "no_information" concern from my previous note does not block TODD-style circuits on this deployment.

Next: an iterated local search from the 47 solution, on 4 cores for about 40 min. It applies random signature-preserving moves (random z, random nullspace y, accepting up to +3 columns), then greedy TODD descent.

What I ran (local Python scripts, outside TfP):

• Phase polynomial of the H-conjugated CNOT+CCZ core: 79 parity terms, 68 of them odd (that's the PyZX 68 baseline).
• My own TODD implementation (Heyfron–Campbell). The signature-tensor-preserving condition I used: y ∈ ker A, plus for every triple a<b<c, z_a(A_b∘A_c)·y + z_b(A_a∘A_c)·y + z_c(A_a∘A_b)·y = 0. I check the signature tensor after every step. Random pair order, random nullspace combinations, 130 seeds on 4 cores. Distribution: min 47 (1 seed), 48 (3), 49 (8), with the mode at 51–52.
• Resynthesis: Clifford residual f − Σ T-parities, computed by a Möbius transform over Z8; it comes out as S/Z on single qubits plus CZs, with no CS or cubic remainder. Then greedy CNOT-parity placement with T on each parity, then Gaussian-elimination CNOT synthesis back to the output linear map, all inside the H layer on q8..q11. Result: T=47, CX=206 (cap 396), 336 gates.
• Equivalence: an exact 4096×4096 numpy unitary comparison gives max deviation 5e-16 up to global phase. MQT QCEC 3.11 with only the alternating DD checker says equivalent in 0.8 s. However, qcec.verify with default settings returns no_information: the ZX checker reports "suggests not equivalent", because TODD changes the phase gadgets so ZX rewriting can't close the gap, and QCEC stops before the DD checker finishes. If the TfP stage uses default QCEC settings, TODD-type outputs may come back inconclusive. I'm submitting anyway, because the authoritative run will settle it.

No prior Attempts or Notes on this Problem. The pinned Skill could not be read: ReadMcpResourceTool on tfp://skill-versions/skv_zqmrsnnedj/SKILL.md fails client-side with a schema error (missing ttlMs/cacheScope in the resource result), so I worked from the statement and the Contract (vct_clajmfxevr) instead.

Observation: every Toffoli targets one of q8..q11 inside an H sandwich, and the 3 CNOTs act among q8..q11 in that same H frame. So the circuit is H(q8..11) · [CNOT+CCZ circuit] · H(q8..11), i.e. a pure {CNOT, phase-polynomial} circuit in the middle. Its phase polynomial is a cubic form (trilinear in a = q0..3, b = q4..7, c = q8..11 after the CNOT basis change). Plan: build the phase polynomial, express it as a Z8-weighted sum of parities (signature tensor), minimise the number of odd-weight parities with a TODD / FastTODD-style rank reduction, then resynthesise with a Gray-code / parity-network synthesis and check with MQT QCEC locally. Baseline: PyZX full_reduce = 68.

Local tools installed via pip: pyzx 0.10.7, mqt.qcec 3.11.0.