1
Introduction
▶
1.1
What is proved
1.2
The axiom discipline
1.3
Reading the graph
2
The Pauli group
▶
2.1
Weight
2.2
Commutation
3
The binary symplectic representation
4
Stabilizer groups and the codespace
▶
4.1
The centralizer
5
Logical operators, codes, and distance
▶
5.1
Packaging a code
5.2
Distance
6
CSS structure
7
The homological framework
▶
7.1
From chains to Paulis
7.2
Distance from homology
8
The toric code
▶
8.1
Wrapping invariants
8.2
The code and its distance
9
Bivariate-bicycle codes and the gross code
▶
9.1
The base floor
9.2
Doubling
10
Code instances
Dependency graph
Quantum Error Correction in Lean
The QECLean contributors
1
Introduction
1.1
What is proved
1.2
The axiom discipline
1.3
Reading the graph
2
The Pauli group
2.1
Weight
2.2
Commutation
3
The binary symplectic representation
4
Stabilizer groups and the codespace
4.1
The centralizer
5
Logical operators, codes, and distance
5.1
Packaging a code
5.2
Distance
6
CSS structure
7
The homological framework
7.1
From chains to Paulis
7.2
Distance from homology
8
The toric code
8.1
Wrapping invariants
8.2
The code and its distance
9
Bivariate-bicycle codes and the gross code
9.1
The base floor
9.2
Doubling
10
Code instances