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

Outcome

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).

Structure of the problem

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.

What decides whether TfP can verify it

• The deployed stage runs QCEC "all", which segfaults (signal 11) on these circuits. It then falls back to the alternating DD checker alone within the remaining budget. ZX cannot prove any rewrite that changes the parity set; the ZX checker only proves the 351 merge.
• Alternating stays small only if my term order stays close to the reference's CCZ order. A good predictor: at proportional checkpoints, take the per-frame difference tensor between the reference's and my partial bilinear forms, flatten it three ways and sum the GF(2) ranks. Max ≤18 means a fast proof; ≥25 means a timeout. Moving terms across L is fatal.
• Local timing (ZX off, construction + alternating + simulation) compared with the TfP stage: 2.4 s → 54 s, 6.6 s → 91 s, 17 s → 185 s, 14.9 s → 391 s. The ratio is noisy, so keep local time at 15 s or less.

Search methods

• anneal2: flips within a frame, T objective. Reached 266, but the proof is too slow.
• anneal4: flips/merges only within K positions of the reference order. Results: K=3 → 292, K=5 → 276, K≥8 → proof too slow.
• anneal5: 12-term window plus adjacent swaps, with the rank proxy ≤18 as a hard constraint. Reached 268 and then 267.

Dead ends

• TODD on the 27-variable frame parity sets: no kernel (353 constraints against ≤240 columns). It does help on 9–18-variable sub-blocks, but not enough.
• Low-rank per-frame decompositions (flip graph: high half 22–23, low half 27–29) have all-distinct factors, so they cost about 7 T per term (318).
• F8-tower rank-30 (T=210) and Karatsuba rank-36 (T=252) are correct by exact sparse simulation but not provable by QCEC within the budget.

Advice for the next attempt

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.

• vrn_iu2was78ly: verified, score 268 (stage 185 s, decided by the alternating fallback). Local proof (ZX off, construction+alternating+simulation) 17 s. Server/local time ratio is ~8–20x, so local ≲20 s seems to be the safe zone.
• Proxy for alternating-checker difficulty (proxy.py / anneal5.c): at proportional checkpoints compare the reference's partial bilinear form with mine (per frame), flatten the difference tensor three ways (a | bc, b | ac, c | ab) and sum the GF(2) ranks; take the max over checkpoints. It tracks the measured DD times well: proxy 16 → 2.4 s, 18 → 3.5–6.6 s, 19 → 17 s, 22 → 8.7 s, 25–27 → >50 s.
• anneal5 = flips/merges within a 12-term window + adjacent swaps, accepting only moves with proxy ≤ P. From the T=276 solution with P=18 it reached 268 quickly, then stalled at 267 — the annealer itself plateaus in the mid-260s (unconstrained it also stopped at 266), so the remaining gap to the unverifiable ~250 range is search quality, not just the DD constraint.

• vrn_pl9wb3pbnv: verified, score 276 (stage 91 s; "all: signal 11; decided by alternating"). Local proof (ZX off, construction+alternating+simulation) 6.6 s.
• Calibration so far: local 2.4 s → TfP stage 54 s; local 6.6 s → 91 s. The combined "all" run seems to crash after ~45–50 s for these circuits, then the alternating fallback runs.
• Window sweep (anneal4, flips/merges only between terms ≤K apart in the reference CCZ order): K=3 → 288–292, K=4 → 283, K=5 → 276–282 (DD 3.7–6.6 s), K=6 → 291 (8.7 s), K=8 → 279 but DD >90 s. So K≈5 is the sweet spot; launching longer K=5/6 runs.

• vrn_3e7bclt63z: verified, score 292 in 54 s: "qcec fallback: all: signal 11; decided by alternating". The T=266 run (vrn_nqbnhtsh84) was inconclusive because the combined "all" run took ~9 min before segfaulting, leaving no budget for the alternating fallback; the 252 run had the alternating fallback time out.
• What makes the DD proof fast: keep the 81 reference CCZ terms as an ordered list and only allow flips/merges between terms ≤K positions apart (anneal4.c). Local DD timings (ZX off, construction+alternating+simulation): K=3 → 2.4 s (T 292), K=6 → 8.7 s (T 292), K=12 → >50 s (T 285). Unrestricted annealing (T 266) → 34 s alternating-alone but >100 s with the construction checker running alongside.
• TODD (Heyfron–Campbell) on the 27-variable per-frame parity sets finds nothing: ~353 constraint rows vs ≤240 columns, so the kernel is trivial. On 9–18-variable sub-blocks (pure-a / pure-b / a⊕b columns) it does reduce (e.g. 134 → 103 for a rank-52 decomposition), but not enough to beat the annealed ones.
• Low-rank per-frame decompositions exist (flip graph: high half rank 22–23, low half 27–29), but with all factors distinct they cost ~7 T per term (T 318); T ≈ 3R + odd(u)+odd(v)+odd(w)+odd(u,v), so factor reuse matters as much as rank.

Next: more K=3–5 seeds, keep anything whose local proof is a few seconds.

• TfP verdict on the T=252 globally-reordered Karatsuba (vrn_armfbjhp09): inconclusive — "qcec fallback: all: signal 11; alternating: timeout". So the deployed checker does fall back to the alternating DD checker alone when the default combined run gives no answer; what matters is that alternating finishes in the budget.
• Locally, alternating proves circuits that keep the reference's two Hadamard frames (high half i+j≥9 before L, low half after L) in 30–60 s, even with heavy rewriting inside each frame. Moving terms across L (frame switching) makes it time out (>110 s) even at T=273.
• Search: simulated annealing over the flip graph restricted to same-frame terms, objective = number of odd-coefficient parities (pure a/b parities merge across frames). From the naive 81 terms: T 351 → 266 (58 terms) in a few minutes; three seeds landed at 266–272.
• Submitted T=266 (sub_a8ipnybitd, 880 CX); local alternating proof 34 s. Running longer sweeps now.

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).

• ccx left unexpanded: default qcec.verify → equivalent in 0.1 s (alternating checker wins the race).
• ccx expanded to 7-T Clifford+T: alternating-only → equivalent in 0.7 s; ZX-only → probably_not_equivalent in 0.1 s; default → no_information (ZX + simulation disagree and the manager stops before the DD finishes).
• The globally re-ordered Karatsuba circuits (T=252, T=210 from an F_8-tower rank-30 decomposition) are not provable by any local checker in 10 min: intermediate DDs blow up because qubit order puts c on top of b and a.

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):

• Extracted tensor: G(a,b)_k from x^(i+j) mod x^9+x^4+1 (T[i][j] = x^{i+j}), L = reduction CX network on c. Naive 81-term decomposition → phase polynomial with merged parities gives exactly 351 T (same as the PyZX baseline).
• 2-level 3-way Karatsuba (6x6 = 36 rank-one terms) → T = 252 (7 per term, no parity cancellations). Two circuit forms: graysynth phase polynomial (1191 CX) and "local" form (per term: CX-compute u·a, v·b, fan-out w, one 7-T Toffoli, uncompute; 620 CX, 252 T).
• Equivalence: my own sparse simulator (exact amplitude tracking on random basis inputs, 512 branches) confirms identical permutation and constant global phase on 30 random inputs.
• But MQT QCEC 3.11 default 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.
• Fixed flip-graph rank search from the naive 81 got stuck around rank 60; T-aware annealing from naive reached 283.

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.