Nadarasa · Proofs · Selene/Guppy
Rewriter rules, proved on shots
Each of the five bastard-rewriter rules (F, I, HH, CC, B) is an asserted unitary identity LHS ≡ RHS. We compile both sides into Guppy kernels, run the 6×3 tomography grid (six input states × three measurement bases) on the Selene emulator, and pass the rule iff every cell's |Pₐ(1) − P_B(1)| stays inside the 4σ shot-noise band. The B rule is a classicalpost-measurement identity (Z-basis statistics ignore preceding Z-phases), so it runs on Z basis only — anything else would diverge by design.
rewriter_rules_verified3/3 criteriaEach criterion below is recomputed from the committed rows by quantum/verdicts.py; this chip reads the result rather than restating it.
- pass
all_cells_passEvery conjecture in the batch passed its own tomographic-equivalence test.
measured 5 · threshold 5
- pass
worst_deviation_inside_envelopeThe worst observed deviation across all cells stays inside the tightest 4*sqrt(0.5/shots) envelope used in the batch.
measured 0.0664 · threshold 0.125
- pass
no_record_disagreesNo individual record carries a FAIL verdict.
measured 0 · threshold 0
rules
5/5
shots/cell
512
wall-time
71s
(F) Spider fusion
LHS RZ(0.3π) · RZ(0.45π) ≡ RHS RZ(0.75π)
Thm 8.34 / Cor 8.35 · Z(α)–Z(β) on a wire fuses to Z(α+β).
| prep \ basis | Z | X | Y |
|---|---|---|---|
| |0⟩ | 0.00/0.00 | 0.50/0.47 | 0.50/0.46 |
| |1⟩ | 1.00/1.00 | 0.51/0.49 | 0.49/0.47 |
| |+⟩ | 0.50/0.48 | 0.85/0.84 | 0.19/0.13 |
| |-⟩ | 0.52/0.50 | 0.15/0.14 | 0.87/0.83 |
| |+i⟩ | 0.53/0.54 | 0.87/0.88 | 0.86/0.85 |
| |-i⟩ | 0.47/0.50 | 0.15/0.18 | 0.13/0.13 |
worst tv = 0.0566 · threshold (4σ) = 0.125 · 15.8s
(I) Identity removal
LHS RZ(0π) ≡ RHS ·
Cor 8.35 (special case) · Z(0) on a wire is the wire itself.
| prep \ basis | Z | X | Y |
|---|---|---|---|
| |0⟩ | 0.00/0.00 | 0.52/0.48 | 0.49/0.48 |
| |1⟩ | 1.00/1.00 | 0.48/0.49 | 0.52/0.54 |
| |+⟩ | 0.48/0.55 | 0.00/0.00 | 0.51/0.48 |
| |-⟩ | 0.50/0.51 | 1.00/1.00 | 0.46/0.47 |
| |+i⟩ | 0.51/0.47 | 0.51/0.50 | 0.00/0.00 |
| |-i⟩ | 0.49/0.52 | 0.47/0.50 | 1.00/1.00 |
worst tv = 0.0645 · threshold (4σ) = 0.125 · 16.2s
(HH) Hadamard cancellation
LHS H · H ≡ RHS ·
Cor 9.21 · H·H = identity.
| prep \ basis | Z | X | Y |
|---|---|---|---|
| |0⟩ | 0.00/0.00 | 0.52/0.52 | 0.49/0.49 |
| |1⟩ | 1.00/1.00 | 0.46/0.50 | 0.49/0.51 |
| |+⟩ | 0.50/0.53 | 0.00/0.00 | 0.54/0.50 |
| |-⟩ | 0.50/0.50 | 1.00/1.00 | 0.48/0.49 |
| |+i⟩ | 0.52/0.51 | 0.48/0.50 | 0.00/0.00 |
| |-i⟩ | 0.48/0.46 | 0.50/0.51 | 1.00/1.00 |
worst tv = 0.043 · threshold (4σ) = 0.125 · 16.1s
(CC) Colour change
LHS H · RZ(0.37π) · H ≡ RHS RX(0.37π)
Eq. 9.20 · H·Z(α)·H = X(α).
| prep \ basis | Z | X | Y |
|---|---|---|---|
| |0⟩ | 0.30/0.28 | 0.52/0.49 | 0.97/0.96 |
| |1⟩ | 0.67/0.70 | 0.51/0.44 | 0.05/0.04 |
| |+⟩ | 0.52/0.50 | 0.00/0.00 | 0.47/0.47 |
| |-⟩ | 0.48/0.52 | 1.00/1.00 | 0.48/0.52 |
| |+i⟩ | 0.03/0.04 | 0.54/0.52 | 0.29/0.33 |
| |-i⟩ | 0.97/0.96 | 0.51/0.50 | 0.71/0.68 |
worst tv = 0.0664 · threshold (4σ) = 0.125 · 16.7s
(B) Bastard absorption (Z-basis)
LHS RZ(0.7π) ≡ RHS ·
Thm 8.72 · A classical (post-measurement) Z-spider absorbs adjacent Z-phases: Z-basis readouts are invariant under a preceding Rz(α). Verified by Z-basis-only tomography; X/Y data would diverge and that's the point — bastard is a CLASSICAL rule.
| prep \ basis | Z |
|---|---|
| |0⟩ | 0.00/0.00 |
| |1⟩ | 1.00/1.00 |
| |+⟩ | 0.45/0.51 |
| |-⟩ | 0.53/0.54 |
| |+i⟩ | 0.50/0.52 |
| |-i⟩ | 0.52/0.48 |
worst tv = 0.0605 · threshold (4σ) = 0.125 · 5.7s
Shot-based equivalence tests of the 5 bastard-rewriter rules (F, I, HH, CC, B). Each unitary rule runs the 18-cell tomography grid (6 prep states × 3 measurement bases); the B rule is a classical post-measurement identity so it runs Z-basis only. PASS means worst total-variation distance stays below the 3σ shot-noise band.