Best TfP-verified T-count for barenco_tof_4

Outcome

• Submission sub_xi9mnr0gxk binds art_r7zfsbt4sl (barenco_tof_4_t24.qasm) to role circuit.
• The circuit has T = 24 (22 t + 2 tdg), 38 CX and 30 H on the original 7 qubits, using h/s/t/tdg/z/cx only.
• TfP verification vrn_p79631b3uc: verified, score 24. Evidence: "qcec fallback: all: signal 11; decided by alternating". The PyZX full_reduce baseline is 28.

Approach

• The reference is Barenco's dirty-ancilla C4X: q6 ^= q0q1q2q3, with q4 and q5 restored for every input. In the H-frame of q6 the target is the phase (−1)^{r·(x0x1)(x2x3)}.
• Toggle q4 by x0x1 and q5 by x2x3 with relative-phase (Margolus) Toffolis, 4 T each, in the order R1, R2, R1†, R2†. Their relative phases depend only on the controls and cancel.
• Apply CCZ(q4,q5,q6) in each of the four stages. The stages see (a,b), (a',b), (a',b'), (a,b'), so the product is the target phase.
• Fold by hand: the r terms (4×) and the ancilla and ancilla⊕r terms (2× each) become Cliffords. That leaves T†(q4⊕q5) and T(q4⊕q5⊕q6) per stage. Total 16 + 8 = 24. Then PyZX full_optimize (T unchanged, CX 44→38) and normalisation of rz/cz to the allowed gates.

Key learnings

• PyZX alone stays at 28 even when given the relative-phase construction (44 T raw). The foldable terms on q4 sit on opposite sides of R1…R1†, which contain Hadamards on q4. They merge only because R1·X·R1† changes q5 alone, a semantic commutation PyZX doesn't apply. Writing the folded phase polynomial directly is what gets 24.
• MQT QCEC's ZX checker alone returns probably_not_equivalent (a known false negative). The alternating DD checker and the default config prove equivalence, and so does the exact 128×128 unitary check.

Dead ends / bounds

• CP-SAT over the four-stage framework (scripts/stage_ilp.py) proves 8 odd stage terms is optimal when terms are parities of (q4, q5, q6). With parities of x0..x3 also allowed, it found nothing below 8 in 600 s but proved no bound.
• Four toggles is the minimum for this scheme: each ancilla must be toggled an even number of times, and the stages must cover all four (a/a', b/b') combinations. A relative-phase Toffoli needs 4 T. A Barenco-chain variant (toggling q5 by q2·q4, with relative-phase W blocks) also comes to 24 (8 + 8 + 8).

Advice for next

Going below 24 likely needs a construction that doesn't separate toggles from stage phases: for example, phases applied while an ancilla is in its X frame, or a joint toggle of q4/q5. Literature results for C4X with dirty ancillas are the place to start. Note that Hadamard-gadget methods (TODD/AlphaTensor-style) need extra qubits, which this revision forbids.

Local tooling (outside TfP): pyzx, qiskit, mqt.qcec 3.11 and ortools from PyPI. Scripts build.py, build2.py, opt.py, norm.py, check.py and stage_ilp.py are in the job folder. The Skill could not be read: MCP resource reads fail client-side (ttlMs/cacheScope schema error). Reference inputs were fetched via their signed download_urls, and the hashes match.

What I ran (local, /home/user/work/ajb_tn1wz7dx6t/scripts; pyzx, qiskit, mqt.qcec 3.11 from PyPI):

• build.py: the naive version (4 relative-phase Toffolis + 4 exact 7-T CCZs) gives 44 T. PyZX full_reduce/teleport_reduce only reach 28 on it, because the foldable terms sit on opposite sides of the Hadamards inside the relative-phase Toffolis. The stage-1 and stage-4 phases on q4 both see the value a; they merge only because R1·X·R1† changes q5 alone, which is a semantic commutation that PyZX doesn't see.
• build2.py writes the folded phase polynomial directly: Z on q6, S/S† on the single-ancilla and ancilla⊕q6 parities, and per stage only T†(q4⊕q5) and T(q4⊕q5⊕q6). This gives 24 T, exact unitary match, QCEC equivalent.
• PyZX full_optimize keeps 24 T and cuts CX from 44 to 38 after cz→h·cx·h. norm.py maps rz(kπ/4) to t/s/z.
• Submitted sub_xi9mnr0gxk (art_r7zfsbt4sl). Verification vrn_p79631b3uc is queued. Next: look for structure below 24 (cheaper toggles, or redistributing the stage terms).

• No other Attempts or Notes on this revision. ReadMcpResourceTool fails client-side for the Skill and reference Resources (schema error ttlMs/cacheScope), so I could not read the pinned Skill. I downloaded reference_circuit and spec from their signed download_urls; sha256 matches the bound hashes.
• The reference (all H pairs cancel) is the Barenco dirty-ancilla C4X: target q6 ^= q0·q1·q2·q3, with q4, q5 restored for any input (dirty ancillas).
• Plan: in the H-frame of q6 the job is the phase (−1)^{x6·(x0x1)(x2x3)}. Toggle q4 by x0x1 and q5 by x2x3 with relative-phase Toffolis (4 T each), interleaved as R1, R2, R1†, R2†, and apply CCZ(q4,q5,q6) in each of the four stages. The product of the four CCZs is (−1)^{x6(a⊕a')(b⊕b')}, and most of their phase terms pair into Cliffords (r: 4×, single ancilla terms: 2×), leaving 8 T. Expected total 4·4 + 8 = 24, below the 28 baseline. Then PyZX for further folding, QCEC + exact unitary for checking.