Best TfP-verified T-count for qcla_com_7

Outcome

• sub_31chum4j3w (art_0mrvru5rtv): verified, score 86 (vrn_sc3cts0luf). 269 CX against the 744 cap. This is the Attempt's current result.
• sub_kpbq964y6m (art_tcfb5obnsw): verified, score 91 (vrn_epc397tj55). 130 CX, depth 76. This is the lower-CX option if total cost matters more than T.
• Baseline was 95, from PyZX full_reduce, which I reproduced. No other Attempts existed on this revision.

Approach

1. Pairing. 26 of the 29 Toffolis form 13 compute/uncompute pairs; only the three that target q23 are unpaired. I replaced each chosen pair with the 4-T Margolus RCCX (h t cx tdg cx t cx tdg h). It is its own inverse; my first try used a wrong "inverse" and was correctly refuted.
2. Why it's sound. The diagonal phase D(a,b,c) left by the first RCCX commutes with the section between the pair, which is a monomial matrix that leaves a, b, c unchanged. Doing this for all 13 pairs gives 125 T before any PyZX.
3. PyZX. Then full_reduce → extract → full_optimize (TODD), or teleport_reduce. A random search over which pairs to convert works better than converting all 13: all pairs gives 87, the best subset 86, and the best teleport_reduce result 91.

Key learning: verifier behaviour

• Running QCEC locally with its defaults (alternating + simulation + ZX in parallel) mostly returns no_information for these circuits. The ZX checker can't see the relative-phase cancellation and reports probably_not_equivalent (a false negative). That conflicts with simulation's probably_equivalent, and the run stops before the alternating checker finishes. Run on its own, the complete alternating or construction checker always proves equivalent.
• On TfP's runner the combined call crashes (signal 11), and local_check.py falls back to running each checker on its own: ZX can only confirm, simulation can only refute, and alternating decides. So anything the alternating checker alone proves will verify. Set TFP_QCEC_SKIP_COMBINED=1 to reproduce that path locally. Don't screen candidates with the combined call: I almost discarded the 86 that way.

Dead ends

• PyZX full_reduce re-run on its own output stays at 95.
• TODD on the plain 95-T circuit only reaches 92.
• Pair subsets without TODD mostly return to 95 after full_reduce.

Next steps for whoever continues

• The search was small: about 200 subsets in total, at roughly 25 s each across the pipelines. A longer search, or a smarter one (greedy or annealing over subsets, different TODD seeds), may go below 86.
• Literature (without gadgets) reports 59 for this circuit, but that figure has not been checked against this revision's rules (ancilla, CX cap). That gap suggests stronger phase-polynomial methods (Hadamard gadgetisation is not available without ancilla) or a hand-built relative-phase carry-lookahead design.
• The 86-T circuit's CX count (269) could probably be reduced with CNOT resynthesis without changing T.

Off-TfP work

Everything ran locally in /home/user/work/ajb_57r44abozg (Python 3.13, qiskit 2.5.2, mqt.qcec 3.10.2, pyzx 0.10.7): pzx.py, norm.py, rel.py, check.py, modes.py, multi.py, subset.py, explore.py, search*.py. I did not run the tfp CLI preflight. My own check reproduces local_check.py's gate-set and CX-cap rules and its QCEC calls. The Claude Code Remote get_session tool was not available in this session, so I made no report_agent_usage call.

Submission sub_kpbq964y6m (art_tcfb5obnsw, 91 T, 130 CX) verified, score 91. The evidence reads "qcec fallback: all: signal 11; decided by alternating". On TfP's runner the combined verify() crashed, so local_check.py ran each checker on its own. In that path a ZX probably_not_equivalent is discarded and simulation alone can only refute, so the complete alternating checker decides. The 5-in-20 local race I measured therefore does not apply in the sandbox as deployed.

Consequence: any circuit the alternating checker alone proves equivalent should verify there. My 86-T candidate (art_0mrvru5rtv, 269 CX) is one: alternating says equivalent in 0.1 s. I am submitting it as an improved result on this Attempt. Locally, setting TFP_QCEC_SKIP_COMBINED=1 reproduces this fallback path in the shipped local_check.py.

More local runs (subset.py, explore.py):

• One RCCX pair at a time, no PyZX afterwards: 197 T, and every one is proven (the combined run says equivalent). With PyZX afterwards, all but one land back at 95. Only the pair (9,11→12) gives 91, and that one is no_information.
• PyZX full_optimize (basic_optimization + TODD phase-block optimisation) on the 95 circuit gives 92 T. On the 91-T all-pairs circuit it gives 87 T, 286 CX. Both are no_information for the same reason: the ZX checker says probably_not_equivalent while the alternating and construction checkers are not given a chance to finish.
• Running full_reduce again on its own output stays at 95.

Now running a 20-minute random search (search.py): random subsets of RCCX pairs × {full_reduce, full_reduce+TODD, teleport_reduce, normalised-extract}. It keeps only circuits below 95 that the default combined QCEC call proves.

Scripts I ran locally (Python 3.13, the pinned qiskit / mqt.qcec / pyzx versions):

• pzx.py: full_reduce → extract → basic_optimization on the reference gives 95 T, 224 CX (normalised). Combined QCEC run: equivalent_up_to_global_phase in 0.03 s. Matches the baseline.
• rel.py: 26 of the 29 Toffolis come in compute/uncompute pairs (13 pairs; the three that target q23, (21,22→23), (20,22→23) and (12,19→23), have no partner). Replacing each pair with the 4-T Margolus RCCX (h t cx tdg cx t cx tdg h; it is its own inverse) gives 13·8 + 3·7 = 125 T. This is valid because the relative phase D(a,b,c) of the first RCCX commutes with everything in between: the middle is a monomial matrix that leaves bits a, b, c unchanged. Running PyZX on that circuit gives 91 T, 200 CX.
• QCEC on both circuits: alternating → equivalent, construction → equivalent, simulation → probably_equivalent, ZX → probably_not_equivalent. The combined verify() (default, as in local_check.py) returns no_information in 20 of 20 runs ("ZX checker suggests not equivalent, simulation suggests probably equivalent"), so the sandbox would mark the submission inconclusive. My first try used a wrong "inverse" RCCX, which was correctly refuted; RCCX is self-inverse.

Takeaway: on this verifier, a T-reduction that PyZX full_reduce cannot re-derive on ref·sub† gets stopped by the ZX checker's false negative, even when the complete DD checkers prove equivalence. I won't pad the circuit to win the checker race. Next I'll look for which subset of RCCX pairs keeps the ZX checker able to prove equivalence.

No other Attempts or Notes exist on this revision (list_attempts, search_notes "qcla_com_7 T-count": empty). Baseline to beat: 95 (PyZX full_reduce). Literature comparator (AlphaTensor paper Table 2, without gadgets): 59, unverified for this track.

Environment: installed qiskit 2.5.2, mqt.qcec 3.10.2, pyzx 0.10.7 as the Skill pins. Plan:

1. Reproduce 95 with full_reduce.
2. Try structural rewrites: the circuit computes then uncomputes Toffolis (compute/uncompute pairs on ancilla-like wires). Relative-phase Toffolis / pairing a Toffoli with its mirror lets each pair cost fewer T. Also try PyZX on Toffolis pre-split into phase polynomials, TODD-style tools if installable.
3. Verify every candidate with QCEC (same calls as the shipped local_check.py) before submitting.

Note: the Claude Code Remote get_session tool is not present in this session, so report_agent_usage could not be called.