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

Outcome

• Current Submission sub_ccemg7au1r (art_psvmexkh73): T = 380, 1373 CX (cap 2436), 30 qubits, no ancillas. Verified, score 380 (vrn_9yu8cfkcsx; stage 195 s, decided by alternating).
• Earlier submissions:
  • sub_cafufbw0x1, T = 390: verified (vrn_15iq1wa2qa).
  • sub_ii8h6yw58u, T = 390 in a different layout: inconclusive (vrn_28t1tgrfyo, alternating ran out of budget).
• Lower T-counts exist but I could not make them provable within the 420 s budget:
  • 203 T: Karatsuba rank-39 decomposition + TODD;
  • 332-359 T: TODD that also changes the x,y-only parities.

Structure of the problem

• Cancelling H·H pairs makes the reference classical: c_out = A·c ⊕ G(x,y), where G = GF(2^10) multiplication mod z^10+z^3+1 (x = q0..9, y = q10..19, c = q20..29) and A = the 9 CNOTs.
• The non-Clifford part is H_c·(-1)^{Σ c_k G_k(x,y)}·H_c, a cubic phase polynomial. The 19 maximal same-target Toffoli runs are anti-diagonal blocks i+j = s.

What determines provability (most important learning)

• The deployed stage normalises the reference's ccx into the 15-gate Clifford+T form. Its combined QCEC run segfaults; it then falls back to ZX (probably_not on any non-phase-folding rewrite), simulation (only "probably") and the alternating DD checker. So a sub-410 circuit must be gate-level aligned with the expanded reference for the alternating checker to finish within 420 s.
• Locally, QCEC cannot even prove expanded ref vs raw ref in 120 s on this 30-qubit instance. Global rewrites (Karatsuba, unconstrained TODD, CNOT-at-end variants) all time out.
• Reproduce the deployed behaviour locally with qcec.verify(expanded_ref, cand, run_alternating_checker only); expanded_ref = each ccx replaced by the qelib1 decomposition.

Method of the verified 380

1. Take the ccx-expanded reference and cancel adjacent H·H pairs. Each T position gets a path-sum parity over x, y and one frame variable τ_b per block (39 variables). Phase folding gives 410 odd parities.
2. Run a TODD-style (Heyfron–Campbell) reduction (own C code) with two restrictions:
   • only moves z with no τ bits, so each frame-attached parity stays in its block;
   • the x,y-only parities (x_i⊕y_j) frozen, with even-parity kernel vectors only. Best of ~1,950 seeds = 380; the floor appears to be 380, reached by several seeds.
3. Build in place:
   • keep every H/CX of the skeleton;
   • surviving parities keep their phase at their original T gate, and deleted T gates are removed;
   • new parities become self-contained gadgets (CX ladder into the block target, T, undo) right after the block's first H;
   • the exact Z8 Clifford residual (S; CZ = H·CX·H) is applied at block starts and at the end.
4. Sign optimisation: choose each odd coefficient's sign to minimise the residual CZ count (80 → 42). This took the local DD proof from >420 s to 123 s. It is the key trick for keeping the checker fast.
5. Checks:
   • Z8 multilinear residual (exact);
   • sparse-state simulation against the reference on random basis inputs;
   • local QCEC alternating checker against the expanded reference.

Dead ends

• Gray-ordered parity accumulation on the block target (to save CX) breaks the DD proof, even at 410 T.
• Changing any x,y-only parities breaks the DD proof, even with only 4-6 weight-≤3 moves (368 / 358 T). The 345 T variant has 1924 CX and also times out.
• Placing new gadgets at the deleted T positions was slower than at block starts.
• Iterated local search with random tensor-preserving kicks found nothing below 380.
• Per-block cubic-free constructions: 2r+1 parities per block is impossible (a cubic-form invariant), and TODD finds the CCZ form locally optimal per block. All savings come from cross-block moves.

Advice for whoever works on this next

• Work within the aligned family. Ideas:
  • better search in the frozen-x,y space (FastTODD-style moves, exhaustive kernel choice);
  • TODD moves whose z includes τ bits within one block;
  • an alternative way to realise x,y-only changes that stays DD-friendly. For example, keep the original x_i⊕y_j gadgets and add/cancel inside the same Toffoli segment.
• Always sign-optimise the Clifford residual before testing; it roughly halves the checker time.
• Tooling notes:
  • The MCP resource reader failed on Skill resources (client schema error), so the pinned Skill was not read. Reference inputs came from their download_url, with hashes matching.
  • Claude Code Remote get_session was unavailable, so usage was not reported.
  • The tfp CLI preflight cannot run here (no Docker).

Scripts (local only): parse.py, tensor.py, flip.py, polyflip.py, compose.py, synth.py, todd*.c, aligned*.py, inplace*.py, signopt.py, sparsecheck.py, check*.py.

• sub_cafufbw0x1: verified, score 390 (vrn_15iq1wa2qa). The stage took 422 s and was decided by alternating.
• sub_ccemg7au1r: verified, score 380 (vrn_9yu8cfkcsx). The stage took 195 s and was decided by alternating.
  • Construction: frozen-x,y constrained TODD, best of ~430 seeds = 380, built in place on the ccx-expanded skeleton.
  • Each odd coefficient's sign (±1/±3) is chosen by greedy local search to minimise the residual CZ fix-ups (80 → 42 CZ). Each sign flip toggles the CZ need on every pair in the parity's support.
  • This cut local alternating-DD time from >420 s to 123 s for the 380 circuit, and from 163 s to 75 s for the 390 circuit.
• Dead ends this phase (all exact by Z8 residual and sparse simulation, all under the CX cap, all timed out at 420 s locally):
  • TODD allowed to change the x,y-only parities with resulting weight ≤ 3: 345 T, 1924 CX.
  • Only 4 or 6 such moves on top of the 380 set: 368 / 358 T.
  • So any change to the x,y-only gadget set seems fatal for the DD proof on this 30-qubit instance, while frame-attached changes inserted at block starts are tolerated.
  • Placing new gadgets at the deleted T positions instead of at block starts was slower: 324 s vs 163 s for the same 390 set.
• Next: iterated local search (random tensor-preserving kicks with weight-≤3 z, then greedy) inside the frozen family, to look below 380.

• sub_ii8h6yw58u (390 T, reference-aligned blocks with self-contained gadgets) came back inconclusive (vrn_28t1tgrfyo).
  • Stage log: all segfaulted, ZX said probably_not, simulation said probably_equivalent, alternating gave no_information after 421 s, and construction gave no_information after 132 s.
  • Locally the same file proves against the raw reference in 14 s.
• Reproduced locally: expanding every reference ccx with the qelib1 15-gate decomposition makes QCEC's alternating checker unable to prove even expanded-ref vs raw-ref within 120 s (it overran to 235 s). So the deployed stage very likely normalises the reference's ccx too, and a candidate must align gate-by-gate with the expanded Toffolis.
• What works locally, all on the expanded skeleton (cancel H·H, keep every H/CX, change only phases and add a few gadgets):
  • In-place phase folding (410): proves vs the expanded reference in 19-46 s.
  • Constrained frozen-x,y TODD in place (390): proves in 163 s.
• Submitted the in-place 390 as sub_cafufbw0x1 (vrn_15iq1wa2qa) to confirm against the platform.
• Lessons on the alternating DD checker on 30 qubits:
  • Gray-ordered parity accumulation on the block target (long-lived accumulators) broke the proof even at 410 T. Self-contained gadgets did not.
  • Dense x,y-only parities from unconstrained TODD need too many CX for the 2436 cap.
  • Each additional deviation from the reference skeleton increases checker time.

• Variants of the rank-39 decomposition plus TODD reach 203 T (best of ~30 runs; typical 205-217). All are exact by my Z8 residual check and random phase simulation.
• But MQT QCEC (3.x, local): default verify() returns no_information in 8 s, because ZX says probably-not and simulation says probably-equal. With the alternating DD checker alone, all three runs hit no_information at the 400-420 s timeout:
  1. the TODD circuit as H·W·H after the reference CNOTs;
  2. the same with the CNOT map moved to the end, so the alternating product stays H·diag·H shaped;
  3. a purely classical Karatsuba circuit (39 ccx on fan-out parities, 273 T).
• The sibling gf2^5 Problem verified via the deployed checker's alternating fallback, but that was 15 qubits. At 30 qubits the intermediate DDs of a structurally different circuit (c ⊕ bilinear(x,y) permutations, or H_c·cubic-phase·H_c) are too large. The contract's 420 s budget would very likely make these inconclusive, so I am not submitting them.
• New plan: keep the circuit aligned with the reference so that the alternating product stays near identity. Keep each per-target Toffoli block in reference order. Replace the block's c-containing gadgets: a rank-2r alternating form needs only 2r+1 parities (U(I+J)Uᵀ), so each block costs 2r+2 instead of ≈3r. Push all x,y-only gadgets to the end; they commute with every ccx/cx in the circuit, so the alternating product differs from identity only by a diagonal phase on x,y. Then merge and TODD-reduce that x,y-only set.

What I ran locally (all in /home/user/work/ajb_h6f0qv813y, Python + a small C program):

• A flip-graph random walk directly on the 10x10x10 field tensor from the 100-term schoolbook decomposition stalls at rank 75-85, so it is not useful from that start.
• A flip graph on small polynomial multiplication tensors finds M(2)=3, M(3)=6, M(4)=9, M(5)=13 quickly (M(5)=13 needs a few million steps / several seeds).
• Karatsuba composition M(2)∘M(5), reduced mod z^10+z^3+1, gives a 39-term bilinear decomposition of the field tensor. As CCZs on parities that is 7·39 = 273 distinct odd parities, with no cancellation between terms.
• I wrote my own TODD (Heyfron–Campbell) in C. For each column pair z = a_α⊕a_β it changes basis so that z = e_p, then finds y in ker[A'; A'_b∘A'_c (b,c≠p)] with y_α≠y_β, applies A += z·yᵀ (appending z if |y| is odd) and cancels duplicate columns. 273 → 221 in about 18 s. The signature tensor is preserved: an exact Z8 multilinear residual check shows only Clifford terms remain (linear coefficients even, quadratic ≡ 0 mod 4, cubic ≡ 0 mod 8).
• Synthesis: the 9 reference CNOTs first, then H on c, then a GraySynth parity network for the odd terms and S/Z for the even linear residual. The quadratic residual is applied as CZ = h·cx·h, then H on c. Putting the CZ residual into the parity network instead blew CX up to 2871, over the cap. Done separately it gives 221 T and 1941 CX (cap 2436).
• A random-input classical phase simulation of the synthesized diagonal (3000 inputs) matches ω^{4f(x)}. MQT QCEC equivalence check is running locally.

Environment notes: the connector's resource reader (ReadMcpResourceTool) fails client-side schema validation (missing ttlMs/cacheScope), so I could not read the pinned SKILL.md; I fetched the two reference inputs via their download_url (sha256 matches the revision bindings). Claude Code Remote get_session tool is not available in this session, so usage was not reported.

Findings from parsing the reference (my own script, cancels adjacent H pairs per qubit):

• After cancelling H·H pairs the circuit is purely classical: 100 ccx with controls x=q0..9, y=q10..19, targets c=q20..29, and 9 cx among targets.
• Net map: c_out = A·c ⊕ G(x,y) where G_k(x,y) = coefficient k of x(z)·y(z) mod (z^10+z^3+1); 148 trilinear monomials x_i y_j c_k.
• Hence U = CNOT(A) · H_c · diag((-1)^{Σ_k c_k G_k(x,y)}) · H_c. The T-count is that of the cubic phase polynomial f = Σ c_k G_k(x,y), i.e. the min number of odd-weight parities whose F2 signature tensor equals f's.
• Any bilinear decomposition f = Σ_{m=1..r} α_m(x) β_m(y) γ_m(c) gives ≤ 7r T (CCZ on three parities), less after cancelling repeated parities across terms. Karatsuba-type rank is ~33-39 for 10x10 field multiplication, so ≈230-270 T before merging, vs the 410 baseline.

Plan: flip-graph random walk (Kauers–Moosbauer style) over F2 for low-rank decompositions of the 10x10x10 tensor, score each by the number of distinct odd-multiplicity parities among the 7r vectors, optionally run a TODD-style reduction, then synthesize with CNOT/T and check equivalence with MQT QCEC locally.