Proofs
Draft · v0.2 · Unreviewed
← Index/Project · Nadarasa ReductionDraft · v0.2 · Selene Emulator

Nadarasa · Proofs · Selene/Guppy · v0.3.7

Conjectures, proved + promoted

Two passes on every flagged conjecture: (1) Selene shot-tomography confirms the equality is physical (PASS = the TS oracle is honest), and (2) the new rule (N) Euler-normalisation pass on the bastard-rewriter collapses every matrix-equivalent representative to a single canonical residue. A PROMOTED badge means the rewriter now proves the equality itself — the conjecture is closed.

→ Track B: 2-qubit oracle synthesis lifts the same enumeration to {H⊗I, I⊗H, CZ, S⊗I, I⊗S} over 4×4 unitaries.

verdict verifiedconjectures_1q_verified3/3 criteria

Each criterion below is recomputed from the committed rows by quantum/verdicts.py; this chip reads the result rather than restating it.

  • passall_cells_pass

    Every conjecture in the batch passed its own tomographic-equivalence test.

    measured 11 · threshold 11

  • passworst_deviation_inside_envelope

    The worst observed deviation across all cells stays inside the tightest 4*sqrt(0.5/shots) envelope used in the batch.

    measured 0.0833 · threshold 0.1443

  • passno_record_disagrees

    No individual record carries a FAIL verdict.

    measured 0 · threshold 0

Rule (N) promotion — Headline

11/11 conjectures promoted · 0 partially reduced · 0 unchanged. Across 363 sequences at maxLen = 5, every matrix-equivalent class now shares one residue — the rewriter is empirically complete on the 1-qubit Clifford+T fragment up to this length.

Selene PASS

11/11

shots/cell

384

wall-time

183s

(1) matrix class

[[0.71+0.00i, 0.71+0.00i], [0.71+0.00i, -0.71+0.00i]]

H ≡ SHSHS

residues (base): ∅ ↔ X(π/2) · Z(π/2) · Z(π/2)
spiders: 0→0 vs 3→3

+ Euler (N): 2 → 1 distinct residues · canonical = X(π/2) · Z(π/2) · Z(π/2)

Selene PASS · 18/18PROMOTED
prep \ basisZXY
|0⟩
0.50/0.50
0.00/0.00
0.49/0.52
|1⟩
0.49/0.55
1.00/1.00
0.50/0.47
|+⟩
0.00/0.00
0.47/0.51
0.52/0.46
|-⟩
1.00/1.00
0.52/0.49
0.50/0.52
|+i⟩
0.51/0.52
0.52/0.45
1.00/1.00
|-i⟩
0.47/0.52
0.52/0.49
0.00/0.00

worst tv = 0.0677 · threshold (4σ) = 0.1443 · 16.4s

(2) matrix class

[[0.71+0.00i, 0.00+0.71i], [0.00+0.71i, 0.71+0.00i]]

SHS ≡ HSSSH

residues (base): Z(π/2) · Z(π/2) ↔ X(3π/2)
spiders: 2→2 vs 3→1

+ Euler (N): 2 → 1 distinct residues · canonical = X(π/2) · Z(π) · Z(π)

Selene PASS · 18/18PROMOTED
prep \ basisZXY
|0⟩
0.52/0.48
0.50/0.50
0.00/0.00
|1⟩
0.51/0.46
0.47/0.51
1.00/1.00
|+⟩
0.54/0.50
0.00/0.00
0.51/0.53
|-⟩
0.53/0.54
1.00/1.00
0.49/0.48
|+i⟩
1.00/1.00
0.47/0.47
0.51/0.49
|-i⟩
0.00/0.00
0.54/0.51
0.54/0.51

worst tv = 0.0521 · threshold (4σ) = 0.1443 · 16.8s

(3) matrix class

[[1.00+0.00i, 0.00+0.00i], [0.00+0.00i, 0.00-1.00i]]

SSS ≡ HSHSH

residues (base): Z(3π/2) ↔ X(π/2) · Z(π/2)
spiders: 3→1 vs 2→2

+ Euler (N): 2 → 1 distinct residues · canonical = Z(3π/2)

Selene PASS · 18/18PROMOTED
prep \ basisZXY
|0⟩
0.00/0.00
0.52/0.51
0.53/0.46
|1⟩
1.00/1.00
0.53/0.51
0.49/0.48
|+⟩
0.49/0.52
0.47/0.46
1.00/1.00
|-⟩
0.51/0.52
0.56/0.49
0.00/0.00
|+i⟩
0.46/0.54
0.00/0.00
0.49/0.51
|-i⟩
0.49/0.45
1.00/1.00
0.48/0.51

worst tv = 0.0781 · threshold (4σ) = 0.1443 · 16.1s

(4) matrix class

[[0.50+0.50i, 0.50-0.50i], [0.50+0.50i, -0.50+0.50i]]

HSHS ≡ SSSH

residues (base): X(π/2) · Z(π/2) ↔ Z(3π/2)
spiders: 2→2 vs 3→1

+ Euler (N): 2 → 1 distinct residues · canonical = X(π/2) · Z(π/2)

Selene PASS · 18/18PROMOTED
prep \ basisZXY
|0⟩
0.55/0.48
0.00/0.00
0.51/0.51
|1⟩
0.49/0.49
1.00/1.00
0.52/0.50
|+⟩
0.51/0.52
0.48/0.49
0.00/0.00
|-⟩
0.51/0.50
0.50/0.50
1.00/1.00
|+i⟩
0.00/0.00
0.47/0.55
0.53/0.49
|-i⟩
1.00/1.00
0.51/0.50
0.47/0.47

worst tv = 0.0807 · threshold (4σ) = 0.1443 · 16.6s

(5) matrix class

[[0.71+0.00i, 0.71+0.00i], [0.00-0.71i, 0.00+0.71i]]

HSSS ≡ SHSH

residues (base): Z(3π/2) ↔ X(π/2) · Z(π/2)
spiders: 3→1 vs 2→2

+ Euler (N): 2 → 1 distinct residues · canonical = X(π/2) · Z(π/2)

Selene PASS · 18/18PROMOTED
prep \ basisZXY
|0⟩
0.48/0.44
0.48/0.47
1.00/1.00
|1⟩
0.51/0.53
0.54/0.48
0.00/0.00
|+⟩
0.00/0.00
0.48/0.47
0.48/0.51
|-⟩
1.00/1.00
0.51/0.49
0.50/0.45
|+i⟩
0.48/0.55
1.00/1.00
0.51/0.52
|-i⟩
0.49/0.52
0.00/0.00
0.48/0.47

worst tv = 0.0625 · threshold (4σ) = 0.1443 · 16.1s

(6) matrix class

[[0.50+0.50i, 0.50-0.50i], [-0.50+0.50i, -0.50-0.50i]]

HSHSS ≡ SSSHS

residues (base): X(π/2) · Z(π) ↔ Z(3π/2) · Z(π/2)
spiders: 3→2 vs 4→2

+ Euler (N): 2 → 1 distinct residues · canonical = X(π/2) · Z(π)

Selene PASS · 18/18PROMOTED
prep \ basisZXY
|0⟩
0.52/0.50
0.46/0.49
0.00/0.00
|1⟩
0.50/0.51
0.53/0.48
1.00/1.00
|+⟩
0.50/0.49
1.00/1.00
0.48/0.51
|-⟩
0.55/0.49
0.00/0.00
0.47/0.51
|+i⟩
0.00/0.00
0.49/0.51
0.44/0.47
|-i⟩
1.00/1.00
0.47/0.47
0.53/0.52

worst tv = 0.0573 · threshold (4σ) = 0.1443 · 16.3s

(7) matrix class

[[0.50+0.50i, 0.50-0.50i], [0.00+0.71i, -0.71+0.00i]]

HSHST ≡ SSSHT

residues (base): X(π/2) · Z(3π/4) ↔ Z(3π/2) · Z(π/4)
spiders: 3→2 vs 4→2

+ Euler (N): 2 → 1 distinct residues · canonical = X(π/2) · Z(3π/4)

Selene PASS · 18/18PROMOTED
prep \ basisZXY
|0⟩
0.51/0.46
0.15/0.18
0.17/0.14
|1⟩
0.51/0.50
0.88/0.86
0.87/0.84
|+⟩
0.51/0.50
0.84/0.84
0.12/0.17
|-⟩
0.48/0.48
0.15/0.17
0.84/0.84
|+i⟩
0.00/0.00
0.46/0.50
0.52/0.53
|-i⟩
1.00/1.00
0.48/0.48
0.50/0.48

worst tv = 0.0495 · threshold (4σ) = 0.1443 · 16.4s

(8) matrix class

[[0.71+0.00i, 0.71+0.00i], [0.50-0.50i, -0.50+0.50i]]

HSSST ≡ SHSHT

residues (base): Z(7π/4) ↔ X(π/2) · Z(π/2) · Z(π/4)
spiders: 4→1 vs 3→3

+ Euler (N): 2 → 1 distinct residues · canonical = X(π/2) · Z(π/2) · Z(π/4)

Selene PASS · 18/18PROMOTED
prep \ basisZXY
|0⟩
0.51/0.49
0.15/0.14
0.89/0.86
|1⟩
0.52/0.48
0.86/0.85
0.17/0.17
|+⟩
0.00/0.00
0.49/0.51
0.54/0.51
|-⟩
1.00/1.00
0.54/0.50
0.48/0.50
|+i⟩
0.48/0.47
0.86/0.86
0.88/0.85
|-i⟩
0.46/0.52
0.16/0.13
0.13/0.15

worst tv = 0.0573 · threshold (4σ) = 0.1443 · 16.8s

(9) matrix class

[[0.71+0.00i, 0.00+0.71i], [0.00-0.71i, -0.71+0.00i]]

SHSSS ≡ SSHSH

residues (base): Z(3π/2) · Z(π/2) ↔ X(π/2) · Z(π)
spiders: 4→2 vs 3→2

+ Euler (N): 2 → 1 distinct residues · canonical = X(π/2) · Z(π)

Selene PASS · 18/18PROMOTED
prep \ basisZXY
|0⟩
0.46/0.46
0.55/0.52
1.00/1.00
|1⟩
0.51/0.50
0.49/0.50
0.00/0.00
|+⟩
0.50/0.53
1.00/1.00
0.50/0.48
|-⟩
0.52/0.54
0.00/0.00
0.53/0.45
|+i⟩
1.00/1.00
0.49/0.48
0.51/0.49
|-i⟩
0.00/0.00
0.46/0.50
0.49/0.51

worst tv = 0.0781 · threshold (4σ) = 0.1443 · 17.2s

(10) matrix class

[[0.71+0.00i, 0.50-0.50i], [0.71+0.00i, -0.50+0.50i]]

SSSTH ≡ THSHS

residues (base): Z(7π/4) ↔ X(π/2) · Z(π/2) · Z(π/4)
spiders: 4→1 vs 3→3

+ Euler (N): 2 → 1 distinct residues · canonical = X(π/2) · Z(π/2) · Z(π/4)

Selene PASS · 18/18PROMOTED
prep \ basisZXY
|0⟩
0.55/0.51
0.00/0.00
0.50/0.52
|1⟩
0.48/0.48
1.00/1.00
0.49/0.54
|+⟩
0.15/0.17
0.51/0.46
0.14/0.13
|-⟩
0.84/0.86
0.48/0.47
0.88/0.85
|+i⟩
0.14/0.16
0.48/0.53
0.85/0.87
|-i⟩
0.84/0.84
0.49/0.52
0.12/0.16

worst tv = 0.0521 · threshold (4σ) = 0.1443 · 16.6s

(11) matrix class

[[0.50+0.50i, 0.00+0.71i], [0.50-0.50i, -0.71+0.00i]]

STHSH ≡ THSSS

residues (base): X(π/2) · Z(3π/4) ↔ Z(3π/2) · Z(π/4)
spiders: 3→2 vs 4→2

+ Euler (N): 2 → 1 distinct residues · canonical = X(π/2) · Z(3π/4)

Selene PASS · 18/18PROMOTED
prep \ basisZXY
|0⟩
0.49/0.54
0.48/0.47
1.00/1.00
|1⟩
0.48/0.51
0.49/0.52
0.00/0.00
|+⟩
0.17/0.13
0.86/0.88
0.48/0.47
|-⟩
0.85/0.86
0.13/0.14
0.52/0.44
|+i⟩
0.89/0.86
0.85/0.83
0.50/0.53
|-i⟩
0.14/0.15
0.14/0.13
0.48/0.54

worst tv = 0.0833 · threshold (4σ) = 0.1443 · 17.4s

Each conjecture is an equality the TS-side matrix oracle asserts but the bastard rewriter cannot prove. We confirm the oracle on Selene shots: for the shortest representative vs a contrasting longer one, the 18-cell tomography grid must agree within shot noise. PASS = the conjecture is physically real, the rewriter has a genuine completeness gap. FAIL = the TS oracle has a bug.

v0.3.7 Track A: added rule (N) Euler normalisation to the bastard-rewriter. A single-qubit wire's interior is replaced by the canonical Z(γ)·X(β)·Z(α) form via direct 2×2 matrix decomposition. Sound by construction (drops only global phase, which rule B already discards). Conjectures whose representatives now share a single residue are promoted from open candidates to proved-equal-by-the-rewriter.

Arun Nadarasa · Refutation-first research notebook · Selene emulator runs, source open
Credit is aspirational until independently verified · © 2026