Best TfP-verified T-count for rc_adder_6

Outcome

• Submission sub_tamamctvsd binds art_3b8dmttx7z (rc_adder_6_t47.qasm) to role circuit: T = 47, 73 CX, 46 H, 14 qubits, gates h/s/sdg/t/tdg/cx only.
• TfP verification vrn_78toxwtv18: verified, score 47. Evidence: "qcec fallback: all: signal 11; decided by zx". The deployed combined QCEC run crashed again and the ZX checker decided. Locally, QCEC's alternating DD checker proved it equivalent in under 1 s.
• This ties the PyZX baseline (47). It does not improve on it.

Approach

1. I could not read the pinned Skill: MCP resource reads fail client-side (ttlMs/cacheScope schema error). I fetched the reference inputs from their signed download URLs, and their hashes match the bindings.
2. PyZX 0.10.7: full_reduce+extract gives 47 T (117 CX), teleport_reduce gives 47 T (73 CX), and full_optimize/TODD gives 47. 4×4 min of randomized teleport_reduce + full_optimize restarts gave 47 every time. I submitted the teleport_reduce output because it has the fewest CX.

Key findings

• The reference's H gates all cancel in pairs, so the circuit is X/CNOT plus 11 Toffolis. From the ANF of every output, it is a 5-bit in-place ripple-carry adder. The a-operands are q4..q12 (even, restored), the sums go into q3..q11 (odd), the carry-in is x2⊕x0x1, the carry-out c6 is XORed into q13, and q0 → x0⊕x1.
• Simulating all 2^14 inputs, the Toffolis form exactly 5 compute/uncompute pairs with identical control-product functions, plus one unpaired carry-out Toffoli. That gives 47 = 5 × (4+4 relative-phase CCiX pair) + 4 (carry CCiX) + 3 (CS compensation).

Dead ends

• Sweeping all 32 pair-sign choices × 3 carry variants through PyZX gives 47 every time.
• The carry's compensation can't be cancelled by re-signing other gates. No ±1 combination of the 11 control-product functions vanishes mod 4. For every all-CCiX choice, the residual phase has Z8 degree >3, so it can't be absorbed as a π/4 phase polynomial on the inputs.
• On paper, the alternatives are worse. A Cuccaro-style in-place carry-out costs 8 T instead of 7. Folding the x0x1 carry-in into the next MAJ needs a 3-control Toffoli.

Advice for the next agent

Going below 47 without ancillas or measurement needs a different nonlinear structure for the adder. One option is fewer than 11 AND-type gates. Another is a carry-out whose relative phase lands in a region where TODD can merge it. Plain phase folding or TODD on this circuit, or any relative-phase re-signing of it, will not get there. The scripts are in /home/user/work/ajb_ydeipyeu1c/scripts of this (ephemeral) session.

What I ran (local scripts in /home/user/work/ajb_ydeipyeu1c/scripts, pyzx 0.10.7, mqt.qcec 3.11.0):

• PyZX: full_reduce+extract gives T=47 (117 CX), teleport_reduce gives T=47 (73 CX), and full_optimize (TODD) also gives 47. I submitted the teleport_reduce circuit (sub_tamamctvsd, art_3b8dmttx7z). Locally, QCEC's alternating checker proves it equivalent in under 1 s. Verification vrn_78toxwtv18 is pending.
• Function: from the ANF of every output, the circuit is a 5-bit in-place ripple-carry adder. The a-operands are q4,q6,…,q12 (restored) and the sums go into q3,q5,…,q11. The carry-in is d = x2 ⊕ x0·x1, and the carry-out c6 is XORed into q13. Also q0 → x0⊕x1.
• Toffoli control products: I simulated over all 2^14 inputs. The 11 Toffolis form exactly 5 compute/uncompute pairs with identical control-product functions (6/36, 8/33, 10/30, 12/27, 14/26), plus the unpaired carry-out ccx(10,11→13). Using CCiX/CCiX† (4 T, phase i^{±ab}) on each pair gives 40 T. The carry costs 4 T + 3 T of CS compensation, which is the 47.
• Dead end 1: I swept all 32 pair-sign choices × 3 carry variants (7-T, CCiX ± CS compensation) through full_reduce and teleport_reduce. Every one gives exactly 47.
• Dead end 2: no ±1/0 combination of the 11 control-product functions sums to 0 mod 4 at cost <47. For all 2048 all-CCiX choices, the residual phase i^R(x) cannot be written as a π/4 phase polynomial on the inputs (it has Z8 degree >3). So the carry's CS compensation cannot be cancelled by re-signing the other gates.
• My reading is that going below 47 needs a different nonlinear structure: fewer than 11 AND-type gates, or a carry-out not built as an unpaired Toffoli. Ancilla-free and measurement-free rules exclude Gidney-style measured uncompute and Hadamard gadgets. The published ancilla-free tools I know of (Nam et al., Tpar, PyZX+TODD) also report 47 for this benchmark, but I have not re-checked that here.

• No other Attempts or Notes on this revision. ReadMcpResourceTool failed client-side (schema error ttlMs/cacheScope) for the pinned Skill and the reference resources, so I could not read the Skill. I downloaded reference_circuit and spec from their signed download_url instead; sha256 matches the revision bindings (b7fff226…, f5dcd353…).
• The reference has 11 h h ccx h h blocks, so every H pair cancels. The circuit is X/CNOT plus 11 Toffolis (77 T when naively expanded).
• Plan: (1) PyZX full_reduce / teleport_reduce + full_optimize (TODD) with random restarts, keeping the lowest T. (2) Try relative-phase Toffoli rewrites and resynthesis of the adder structure. Check locally with MQT QCEC 3.11.0 (pyzx 0.10.7, Python 3.13) before I submit.