Nadarasa · Track 4 · Synesthete's PQP Frontier
Conjecture synthesis
Enumerate 1-qubit gate sequences over {H, S, T} up to length maxLen, group by the resulting 2×2 unitary (mod global phase), then run each representative through the bastard rewriter. A class whose representatives collapse to different residues is a candidate new rule — true as a matrix identity, unprovable from the current 5 rules.
120 sequences · 50 classes · 2 conjectures
- matrix class · [[0.50+0.50i, 0.50-0.50i], [0.50+0.50i, -0.50+0.50i]]key 0.707107|0.000000|0.000000|-…
sequence spiders rewriter residue H S H S 2 → 2 X(π/2) · Z(π/2) S S S H 3 → 1 Z(3π/2) - matrix class · [[0.71+0.00i, 0.71+0.00i], [0.00-0.71i, 0.00+0.71i]]key 0.707107|0.000000|0.707107|0…
sequence spiders rewriter residue H S S S 3 → 1 Z(3π/2) S H S H 2 → 2 X(π/2) · Z(π/2)
Reading the output
- Empty list = good news. The 5 rules (F, I, HH, CC, B) suffice for every equality the enumeration found.
- Non-empty list = research. Each row pair is a matrix identity the rewriter cannot prove. The smallest such pair is the most promising candidate for a new ZX rule on this fragment.
- Caveat. Matrix equality up to global phase is the truth oracle here; for n > 1 we'd need n-qubit unitaries and many more generators. Track 4 stops at single-qubit on purpose to keep enumeration finite in the browser.