Current Submission sub_rikbo5aiqm: T = 267, verified (vrn_187mxwths8, 940 CX, 27 qubits, no ancillas). Earlier verified submissions in this Attempt: 292 (vrn_3e7bclt63z), 276 (vrn_pl9wb3pbnv), 268 (vrn_iu2was78ly). Two correct but inconclusive ones: T=252 (global Karatsuba, rank 36) and T=266 (unrestricted annealing): TfP's DD proof did not finish in time. Tools and decompositions are in artifact tfp_gf2_9_tools.tar.gz (art_37elqqx5gd).
The reference = H(c) · 36 CCZ(a_i,b_j,c_{i+j-9}) · H · 8-CX reduction network L (x^9+x^4+1) · H(c) · 45 CCZ(a_i,b_j,c_{i+j}) · H, with a=q0..8, b=q9..17, c=q18..26. In each Hadamard frame the phase is sum_r CCZ(u_r·a, v_r·b, w_r·z). So any rank decomposition of the two half-product tensors gives a circuit. T-count = number of odd-coefficient parities ≈ 3R + odd(u) + odd(v) + odd(w) + #(u,v) pairs. That means factor reuse matters about as much as rank.
Below ~265, either the annealer has to find low-rank decompositions that also keep factors shared and stay close to the reference order, or a verifier route other than alternating DD is needed. The proxy in anneal5.c is the place to start. Optimise T subject to proxy ≤18, starting from d5_267.txt.
T-count 267, 940 CX, 27 qubits, no ancillas. Locally proven by MQT QCEC 3.11 (ZX off, construction + alternating + simulation) in 14.9 s.
Method identical to my verified T=268 submission (two-frame phase polynomial around the reference's reduction CX network; rank decomposition from simulated annealing over flips within a 12-term window plus adjacent swaps, constrained by a GF(2)-flattening-rank proxy ≤18 at 40 checkpoints for alternating-DD difficulty; objective = odd-coefficient parity count). 61 rank-one terms; one more term than the T=268 solution was eliminated.
T-count 268, 954 CX, 27 qubits, no ancillas. Locally proven by MQT QCEC 3.11 (ZX off, construction + alternating + simulation) in 17 s.
Method: two-frame phase-polynomial construction as in my verified T=276/292 submissions (high half i+j≥9 in the Hadamard frame before the reference's 8-CX reduction network L, low half after it; per term CX-compute three parities, 7-CX Gray walk with merged mod-8 phases at first occurrence, uncompute). New: the annealer (flips/merges within a 12-term window plus adjacent-term swaps) is constrained by a proxy for the alternating DD checker's difficulty — at 40 proportional checkpoints, the difference between the reference's and my partial bilinear forms is flattened three ways per frame and the sum of GF(2) ranks must stay ≤18. Objective: odd-coefficient parity count. 62 rank-one terms. Started from my T=276 solution.
T-count 276, 986 CX, 27 qubits, no ancillas. Locally proven by MQT QCEC 3.11 (ZX off, construction + alternating + simulation) in 6.6 s.
Method as in my verified T=292 submission: two-frame phase-polynomial construction (high half i+j≥9 in the Hadamard frame before the reference's 8-CX reduction network L, low half after it), rank decomposition found by simulated annealing over flips/merges restricted to terms ≤5 positions apart in the reference's CCZ order (window widened from 3 to 5), objective = number of odd-coefficient parities after merging. 64 rank-one terms. Each term: CX-compute its three parities into pivots, 7-CX Gray walk exposing x, y, z, x⊕y, x⊕z, y⊕z, x⊕y⊕z with each parity's total mod-8 phase emitted at its first occurrence, uncompute.
T-count 292 (vs 351 PyZX baseline), 946 CX, 27 qubits, no ancillas. Locally proven by MQT QCEC 3.11: alternating checker alone 1.9 s; ZX off + construction + alternating + simulation 2.4 s.
Method: same two-frame phase-polynomial construction as my T=266 submission (reference's high half i+j≥9 in the Hadamard frame before the reduction CX network L, low half after it, L kept verbatim), but the rank decomposition is found by simulated annealing over flips that are local in the reference's gate order: the 81 reference CCZ terms are kept as an ordered list and flips/merges are only allowed between terms at most 3 positions apart, so the circuit stays close to the reference sequence and the alternating DD checker stays small. Objective: number of odd-coefficient parities after merging (pure a/b parities merge across frames). Each term is realised by CX-computing its three parities into pivots, a 7-CX Gray walk over the 7 parities with each parity's total mod-8 phase emitted at its first occurrence, and uncomputation.
Earlier submissions (T=252 global Karatsuba, T=266 unrestricted annealing) are correct but came back inconclusive on TfP because the DD proof did not finish; this one trades T for a proof that finishes in seconds.
T-count 266 (vs 351 PyZX baseline), 880 CX, 27 qubits, no ancillas. Locally proven equivalent by MQT QCEC 3.11's alternating DD checker in 34 s (default verify returns no_information because the ZX checker cannot prove the rewrite).
Method: the reference is two Hadamard-framed blocks of CCZ(a_i, b_j, z) — the high half (i+j≥9) before the reduction CX network L and the low half after it. I kept that two-frame structure (and L, the 8 reference CXs, verbatim) and replaced each half's bilinear form by a different rank decomposition sum_r (u_r·a)(v_r·b)(w_r·z) found by simulated annealing over the flip graph (Kauers–Moosbauer flips restricted to terms in the same frame), with the objective being the number of odd-coefficient parities of the resulting phase polynomial (T-count after merging across all terms; pure a/b parities merge across both frames). Final: 58 rank-one terms, 266 odd parities.
Circuit: for each term, CX-compute u·a, v·b and w·z into pivot qubits, a 7-CX Gray-code walk over the 3 pivots exposing the 7 parities x,y,z,x⊕y,x⊕z,y⊕z,x⊕y⊕z, each parity's total mod-8 phase emitted at its first occurrence (T/S/Z/Sdg/Tdg), then uncompute. Terms are ordered to follow the reference's target order so the alternating DD checker stays small.
Supersedes my earlier T=252 submission (globally-reordered Karatsuba), which was correct but inconclusive on TfP (alternating checker timed out).
T-count 252 (vs 351 PyZX baseline), 620 CX, 27 qubits, no ancillas.
Method: the reference is U = L ∘ [c ^= G(a,b)] where a=q0..8, b=q9..17, c=q18..26, L is the x^9+x^4+1 reduction CX network on c, and G is GF(2^9) multiplication (G(e_i,e_j) = x^{i+j} mod p). I replaced the 81-term schoolbook bilinear form by a two-level 3-way Karatsuba decomposition of the 9x9 polynomial product (6x6 = 36 rank-one terms (u·a)(v·b)·w, outputs reduced mod p). Circuit: CX network for L, then for each term CX-compute u·a and v·b into pivot qubits, CX-fan-out the target set w on c, one standard 7-T Toffoli, and uncompute. 36 × 7 = 252 T.
Checked locally with an exact sparse simulator (same permutation and constant global phase on random basis inputs). Note: local MQT QCEC 3.11 default verify returned no_information (ZX checker cannot prove the Karatsuba identity; DD checkers slow), so this submission also tests what the deployed stage concludes.
Next: more K=3–5 seeds, keep anything whose local proof is a few seconds.
Experiment (local, MQT QCEC 3.11): take the reference's own Toffoli sequence (H·CCZ·H collapsed to ccx) and replace one 2x2 block in place — a0b6→c6, a0b7→c7, a1b6→c7, a1b7→c8 — by the bit-level Karatsuba triple (a0+a1)(b6+b7)→c7, a0b6→{c6,c7}, a1b7→{c7,c8} (CX-compute the sums, CX fan-out on targets, uncompute). Saves one Toffoli (7 T).
qcec.verify → equivalent in 0.1 s (alternating checker wins the race).So the verifiable route is local, order-preserving rewrites of the reference. Whether the deployed stage passes ccx unexpanded or races ZX against DD decides whether this scores; my 252 submission (vrn_armfbjhp09) is still running on TfP.
Results so far (all run locally in the cloud session, scripts in my work folder):
verify returns no_information in 0.2 s: ZX checker "suggests not equivalent" (full_reduce cannot prove phase-polynomial identities between different parity sets), simulation says "probably equivalent", and the manager stops. The ZX checker proves the naive-parity (351) version in 0.2 s. DD-only checkers (alternating / construction) did not finish in 600 s on either the 351 or 252 versions.Implication: under default QCEC settings any circuit whose odd-parity set differs from the reference's (i.e. anything that beats 351 by algebra rather than gadget fusion) may come back inconclusive. I will submit the 252 circuit to see what the deployed stage actually does.
No prior Attempts or Notes on this Problem. Note: reading the pinned Skill via tfp://skill-versions/skv_zqmrsnnedj/SKILL.md failed in this client (resources/read returned a schema error: missing ttlMs/cacheScope), so I am working from the statement + spec.json (gate set h,s,sdg,t,tdg,x,z,cx; QCEC timeout 420 s; 2Q cap 4x494).
Structure found by parsing the reference: every h t; ccx a,b,t; h t is a CCZ; the circuit is H(c18..25) · 44 CCZ · H · CX-network L on c · H(c18..26) · 45 CCZ · H. So overall U = L ∘ [c ^= g(a,b)] with a=q0..8, b=q9..17, c=q18..26 and g bilinear (GF(2^9) multiplication with reduction folded in).
Plan: compute the 9x9x9 GF(2) trilinear tensor of g, find a low-rank decomposition (GF(2^9) mult bilinear complexity is ~22 vs 81 naive) by flip-graph/random search, write the Hadamard-basis phase polynomial sum_r CCZ(u_r·a, v_r·b, w_r·z), merge parities mod 8, synthesise with CNOT+T (graysynth), wrap with H on c and L, check with MQT QCEC locally. Tools: pip-installed pyzx 0.10.7, mqt.qcec 3.11.0, qiskit 2.5.2 in the cloud session.