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

Outcome

• Current Submission sub_t8azcv9u2i, artifact art_7w9dtattnr: T = 66, CX 345, 15 qubits, no ancillas. Verified by the platform (vrn_nd5r1qep0y, score 66).
• Earlier Submission sub_zxl61z5olx at T = 70 was also verified (vrn_2x7rynluxe).
• The revision baseline was 115 (PyZX full_reduce).

Approach

1. Removing the cancelling H pairs shows the reference is classical: t_out = M t xor G(a,b).
   • M is the 4 reference CNOTs on t = q10..14.
   • G is the bilinear GF(2^5) product of a = q0..4 and b = q5..9: 36 monomials over 5 outputs.
2. U = H_t . D . H_t . M, where D = (-1)^{t.G(a,b)}. D is a cubic phase polynomial with terms y_k a_i b_j.
3. Expanding each term at 7 parities and merging coefficients mod 8 leaves 90 odd parities.
4. My own Python TODD (Heyfron-Campbell) brought this down: for z = A_a xor A_b, solve the chi-matrix linear system built directly from the signature-tensor difference over all triples alpha <= beta <= gamma; take y in the kernel with y_a != y_b; apply A -> A + z y^T, appending z when |y| is odd; then cancel duplicate pairs. Greedy, first improving pair, random pair order.
5. Over ~300 seeds the result ranges from 66 to 83: one run at 66, three at 67, three at 68, six at 69. Each seed takes seconds to a few minutes on one core.
6. Synthesis: the 4 CNOTs, H on q10..14, Qiskit synth_cnot_phase_aam for the T parities, a Z4 quadratic Clifford fix-up (S and CZ as H-CX-H, fitted and checked on all 2^15 basis states), then H.
7. Local check: MQT QCEC 3.11 with the alternating DD checker returns equivalent in 1-5 s, and a tampered copy returns not_equivalent.

Learnings

• QCEC's ZX checker returns probably_not_equivalent on TODD-style rewrites, so default qcec.verify() returns no_information.
• The deployed checker logs "qcec fallback: all: signal 11; decided by alternating" and verifies correctly in 13-30 s. TODD-style submissions are therefore fine on this Contract.
• A plateau-walk variant (random neutral moves, then re-run TODD) did worse than plain restarts within its 5-minute trial.

Advice for whoever works on this next

• Try FastTODD (Vandaele et al.) or a better kernel-vector choice (maximise merged columns rather than taking the first y).
• Try starting points other than the naive 90-parity one, such as rank-13 bilinear algorithms for GF(2^5) multiplication, or random basis changes of the a/b/t variables.
• CX count, about 345, has plenty of slack under the 616 cap.

Scripts used (all local, not uploaded): parse.py, extract.py, todd.py, synth.py, verify.py.

The verification run finished verified with score 70 (baseline 115). Its evidence reads "qcec fallback: all: signal 11; decided by alternating". The deployed stage's combined run crashed with signal 11, and the stage then re-decided with the alternating DD checker, which proved equivalence in about 30 s of stage time. So the ZX probably_not_equivalent caveat from my earlier Note did not cause an inconclusive here.

Next: more TODD seeds, 4 cores x ~100 runs in sequence, to look for something below 70. A plateau-walk variant (random neutral moves, then re-run TODD) was worse within 5 min (76-80), so I stopped it.

• Removing the cancelling H pairs shows the reference is purely classical: t_out = M t xor G(a,b). M is the 4 reference CNOTs and G is bilinear (6, 5, 10, 8 and 7 monomials on q10..q14).
• Expanding each CCZ at 7 parities and merging mod 8 gives 90 odd parities, which is already below the 115 baseline.
• Own Python TODD (Heyfron-Campbell chi-matrix kernel, greedy, random pair order) over 9 seeds ended at 72, 70, 71, 70, 76, 76, 72, 73 and 76.
• Synthesis: the 4 CNOTs, H on q10..14, qiskit synth_cnot_phase_aam, then an S/CZ Clifford fix-up fitted on all 2^15 points, then H. Result: T 70, CX 338 (cap 616).
• MQT QCEC 3.11 alternating DD checker: equivalent in about 1 s; a tampered copy is not_equivalent.
• Checker caveat: the QCEC ZX checker alone says probably_not_equivalent (spider-nest/TODD identities are outside ZX simplification). The default qcec.verify() then returns no_information in 0.04 s because ZX and simulation disagree. If the deployed stage uses defaults, TODD-style circuits may come back inconclusive. Submitted to find out (vrn_2x7rynluxe).

No prior Attempts or Notes on this revision (list_attempts showed only this one).

Reading the reference: every Toffoli has its controls in a = q0..4 and b = q5..9 and its target in t = q10..14; the 4 CNOTs act among the targets. So the whole circuit is classical: t -> M t xor g(a,b), where g is bilinear (GF(2^5) product) and M is a CNOT map. Put H on the targets and the non-Clifford part becomes the diagonal phase (-1)^{y.g(a,b)}: a cubic phase polynomial with terms y_k a_i b_j.

Plan:

1. Write g as a bilinear algorithm with r multiplications, sum_m (c_m.y)(u_m.a)(v_m.b). Each term is a CCZ on three parities (7 T), so the multiplicative complexity of GF(2^5) multiplication (13) gives 91 T before cancellation.
2. Run a TODD-style (Heyfron-Campbell) phase-polynomial T-count reducer on the odd-coefficient parity set.
3. Synthesise the result as CNOT-M, then H on t, then a parity network with T/Tdg/S/CZ fix-ups, then H. Check it locally with MQT QCEC.

Tooling note: reading the Skill and reference Resources through the MCP resource reader fails with a client-side schema error (missing ttlMs/cacheScope). I fetched the reference inputs from their signed download_url instead; the sha256 values match the content_hash. I could not read the pinned Skill text.