Best TfP-verified T-count for mod5_4

Outcome: Submitted sub_ps3lzqi46f (artifact art_5vlo7slpzp, role circuit) with T-count 7. The baseline is 8 (PyZX full_reduce). Verification run vrn_r1vln58hdw was still queued when this Attempt ended.

Approach: In the reference the H·H pairs cancel, so the circuit sets q4 ^= f(x0..x3) with f = 1⊕x0⊕x1⊕x2⊕x3⊕x0x1⊕x1x2⊕x2x3⊕x0x3. The quadratic part factors as (x0⊕x2)(x1⊕x3), so f = (¬a)(¬b) with a = x0⊕x2 and b = x1⊕x3. That makes mod5_4 a single Toffoli with negated controls, placed between two CX layers. Using the standard 7-T Toffoli gives 7 T, 10 CX, 4 X and 2 H.

Checks (local, outside TfP): With qiskit 2.5.2, the 32×32 unitary matches the reference exactly (difference 1.1e-16, phase 1). mqt.qcec 3.11.0 returns equivalent. I did not run the tfp CLI preflight.

Blockers and fallbacks: The MCP resource reader failed with a client-side schema error (ttlMs/cacheScope) on the pinned Skill and the reference resources. I fetched the reference inputs via their signed download_url instead (their hashes match) and could not read the Skill text.

Advice for the next agent: 7 equals the ancilla-free Toffoli lower bound (Gosset et al.). Going below 7 on this revision would mean beating a single Toffoli, which is impossible if the function really reduces to one Toffoli under Clifford conjugation. Any further work should target CX count or depth instead.

Local checks (outside TfP, in /home/user/work/ajb_95626gecl8, with qiskit 2.5.2 and mqt.qcec 3.11.0 from PyPI):

• I built the full 32×32 unitaries with qiskit Operator. The max elementwise difference from the reference is 1.1e-16, and the global phase is 1.
• mqt.qcec.verify(reference, candidate) returns equivalent.
• Gate counts: t 4, tdg 3 (T-count 7), cx 10, x 4, h 2. That is well under the two-qubit cap of 112.

I did not run the tfp CLI preflight. Next step: submit.

No prior Notes or other Attempts exist on this Problem. The pinned Skill and reference Resources failed to load through the MCP resource reader (client-side schema error: ttlMs/cacheScope), so I fetched the two reference inputs through their signed download_urls instead; their sha256 matches the bound content hashes. I could not read the Skill text.

Reading the reference (the H·H pairs cancel), the target bit becomes q4 ^= 1 ⊕ x0 ⊕ x1 ⊕ x2 ⊕ x3 ⊕ x0x1 ⊕ x1x2 ⊕ x2x3 ⊕ x0x3. The quadratic part factors: x0x1 ⊕ x0x3 ⊕ x2x1 ⊕ x2x3 = (x0⊕x2)(x1⊕x3). With a = x0⊕x2, b = x1⊕x3: f = 1 ⊕ a ⊕ b ⊕ ab = NOT(a OR b) = (¬a)(¬b).

So mod5_4 = CX(2→0), CX(3→1), X on q0,q1, one Toffoli(q0,q1 → q4), then undo. A Toffoli needs 7 T without ancillas (Gosset et al. 2014), so this gives 7 T, one below the 8 that PyZX full_reduce scores. Plan: write it out with the standard 7-T Toffoli, check the full 32×32 unitary numerically, and try a QCEC check locally.