Inspect what the QEC artifacts actually prove
Select a bounded code, inspect its stabilizer matrix and exact single-error syndrome map, then open either the deterministic round trace or generated feed-forward carrier in Playground.
QEC correction-map inspector
Every view is projected from the built-in, identity-hashed correction artifacts. The lab exposes the checked algebra and the execution boundary side by side.
The round trace is an exact algebraic correction-map projection, not a noisy multi-round decoder, fault-tolerance proof, threshold estimate, or hardware result. Syndrome extraction circuits and logical encoding remain outside this lab.
- Data qubits
- 5
- Syndrome bits
- 4
- Code distance
- 3
- Covered errors
- 15
- Unique syndromes
- 15
- Runtime evidence
- Tier 1 exhaustive
Stabilizer generator matrix
The 4 declared generators have verified GF(2) rank 4 and commute pairwise.
fnv1a32:d41e0bd1| Generator | q0 | q1 | q2 | q3 | q4 |
|---|---|---|---|---|---|
| S0 | X | Z | Z | X | I |
| S1 | I | X | Z | Z | X |
| S2 | X | I | X | Z | Z |
| S3 | Z | X | I | X | Z |
Exact correction lookup
Closed-world correction map for the declared single physical Pauli error model.
0001 → X0 · X0
| Syndrome | Correction | Covered error class |
|---|---|---|
| 0001 | X(q[0]) | X0 |
| 0010 | Z(q[2]) | Z2 |
| 0011 | X(q[4]) | X4 |
| 0100 | Z(q[4]) | Z4 |
| 0101 | Z(q[1]) | Z1 |
| 0110 | X(q[3]) | X3 |
| 0111 | Y(q[4]) | Y4 |
| 1000 | X(q[1]) | X1 |
| 1001 | Z(q[3]) | Z3 |
| 1010 | Z(q[0]) | Z0 |
| 1011 | Y(q[0]) | Y0 |
| 1100 | X(q[2]) | X2 |
| 1101 | Y(q[1]) | Y1 |
| 1110 | Y(q[2]) | Y2 |
| 1111 | Y(q[3]) | Y3 |
Deterministic round trace
A three-round NM-RFC-0016 experiment injects X0 in round 1 and projects every result from the exact correction artifact.
fnv1a32:6871b2fa- Round 0
- Injection
- none
- Syndrome
- 0000
- Correction
- none
- Residual
- Clean
- Logical invariant
- Holds for the clean round
- Round 1
- Injection
- X0
- Syndrome
- 0001
- Correction
- X0
- Residual
- Identity modulo stabilizer
- Logical invariant
- Holds within the published model
- Round 2
- Injection
- none
- Syndrome
- 0000
- Correction
- none
- Residual
- Clean
- Logical invariant
- Holds for the clean round
Decoder artifact: fnv1a32:d41e0bd1. No client-side correction is recomputed.
Open round trace in PlaygroundEvidence boundary
The exact algebraic map covers the declared single-physical-Pauli error set only. It does not prove noisy execution, repeated rounds, decoder latency, logical error rate, or fault tolerance.
Inspect generated feed-forward carrier
The source measures dedicated syndrome-register qubits and applies the verified lookup map. It intentionally does not synthesize code encoding or stabilizer-measurement circuits.
module qec_lab_qec_perfect5_code;
@target("browser-stabilizer");
fn main() {
let q: QReg<9> = qreg[9];
// Decoder carrier only: syndrome extraction and logical encoding are outside this lab.
let s0: Bit = measure(q[5]);
let s1: Bit = measure(q[6]);
let s2: Bit = measure(q[7]);
let s3: Bit = measure(q[8]);
if (s0 == 0 && s1 == 0 && s2 == 0 && s3 == 1) { X(q[0]); }
if (s0 == 0 && s1 == 0 && s2 == 1 && s3 == 0) { Z(q[2]); }
if (s0 == 0 && s1 == 0 && s2 == 1 && s3 == 1) { X(q[4]); }
if (s0 == 0 && s1 == 1 && s2 == 0 && s3 == 0) { Z(q[4]); }
if (s0 == 0 && s1 == 1 && s2 == 0 && s3 == 1) { Z(q[1]); }
if (s0 == 0 && s1 == 1 && s2 == 1 && s3 == 0) { X(q[3]); }
if (s0 == 0 && s1 == 1 && s2 == 1 && s3 == 1) { Y(q[4]); }
if (s0 == 1 && s1 == 0 && s2 == 0 && s3 == 0) { X(q[1]); }
if (s0 == 1 && s1 == 0 && s2 == 0 && s3 == 1) { Z(q[3]); }
if (s0 == 1 && s1 == 0 && s2 == 1 && s3 == 0) { Z(q[0]); }
if (s0 == 1 && s1 == 0 && s2 == 1 && s3 == 1) { Y(q[0]); }
if (s0 == 1 && s1 == 1 && s2 == 0 && s3 == 0) { X(q[2]); }
if (s0 == 1 && s1 == 1 && s2 == 0 && s3 == 1) { Y(q[1]); }
if (s0 == 1 && s1 == 1 && s2 == 1 && s3 == 0) { Y(q[2]); }
if (s0 == 1 && s1 == 1 && s2 == 1 && s3 == 1) { Y(q[3]); }
return 0;
}