1
Rem 1: Base Field
2
Rem 2: Notation Conventions
3
Rem 3: Expanding Matrix Definition
4
Def 1: Chain Complex
5
Def 2: Cochains and Cohomology
6
Def 3: Classical Code
7
Def 4: CSS Code
8
Def 5: LDPC Code
9
Def 6: Subsystem CSS Code
10
Def 7: Cell Complex
11
Def 8: Cycle Graph
12
Def 9: Double Complex
13
Def 10: Total Complex
14
Def 11: Tensor Product Double Complex
15
Thm 2: Small Double Complex Homology
16
Def 12: Fiber Bundle Double Complex
17
Thm 3: Fiber Bundle Homology
18
Def 13: Augmented Complex
19
Thm 4: Projection Induces Isomorphism
20
Def 14: Graph Expansion
21
Def 15: Tanner Code Local System
22
Def 16: Dual Code
23
Def 17: Binary Entropy Function
24
Def 18: Cheeger Constant
25
Lem 1: Relative Cheeger Inequality
26
Thm 5: Alon–Boppana Bound
27
Thm 6: Alon–Chung Bound
28
Cor 1: Alon–Chung Contrapositive
29
Def 19: Edge Boundary and Vertex Incidence for Cell Complexes
30
Lem 2: Edge-to-Vertex Expansion
31
Lem 3: Relative Vertex-to-Edge Expansion
32
Thm 7: Sipser–Spielman Expander Code Distance
33
Thm 8: Expander Violated Checks
34
Thm 9: Expander Bit Degree
35
Thm 10: Gilbert–Varshamov Plus
36
Def 20: Cayley Graph
37
Def 21: LPS Expander Graphs
38
Thm 11: LPS Graphs are Ramanujan
39
Def 22: Balanced Product of Vector Spaces
40
Def 23: Balanced Product Chain Complex
41
Lem 4: Künneth Formula for Balanced Products
42
Def 24: Quotient Graph Trivialization
43
Def 25: Invariant Labeling
44
Def 26: Balanced Product Tanner Cycle Code
45
Def 27: Horizontal/Vertical Homology Splitting
46
Def 28: Iota and Pi Maps
47
Thm 12: Encoding Rate (Circle Case)
48
Def 29: Horizontal Subsystem Balanced Product Code
49
Thm 13: Homological Distance Bound
50
Thm 14: Cohomological Distance Bound
51
Cor 2: Subsystem Code Parameters
52
Def 30: Unipotent Subgroup for LPS Graphs
53
Thm 15: Explicit Family of Quantum Codes
54
Cor 3: Distance-Balanced Family of Quantum Codes
55
Overview: Balanced Product Codes Formalization
Dependency graph
MerLean-example
doxtor6
1
Rem 1: Base Field
2
Rem 2: Notation Conventions
3
Rem 3: Expanding Matrix Definition
4
Def 1: Chain Complex
5
Def 2: Cochains and Cohomology
6
Def 3: Classical Code
7
Def 4: CSS Code
8
Def 5: LDPC Code
9
Def 6: Subsystem CSS Code
10
Def 7: Cell Complex
11
Def 8: Cycle Graph
12
Def 9: Double Complex
13
Def 10: Total Complex
14
Def 11: Tensor Product Double Complex
15
Thm 2: Small Double Complex Homology
16
Def 12: Fiber Bundle Double Complex
17
Thm 3: Fiber Bundle Homology
18
Def 13: Augmented Complex
19
Thm 4: Projection Induces Isomorphism
20
Def 14: Graph Expansion
21
Def 15: Tanner Code Local System
22
Def 16: Dual Code
23
Def 17: Binary Entropy Function
24
Def 18: Cheeger Constant
25
Lem 1: Relative Cheeger Inequality
26
Thm 5: Alon–Boppana Bound
27
Thm 6: Alon–Chung Bound
28
Cor 1: Alon–Chung Contrapositive
29
Def 19: Edge Boundary and Vertex Incidence for Cell Complexes
30
Lem 2: Edge-to-Vertex Expansion
31
Lem 3: Relative Vertex-to-Edge Expansion
32
Thm 7: Sipser–Spielman Expander Code Distance
33
Thm 8: Expander Violated Checks
34
Thm 9: Expander Bit Degree
35
Thm 10: Gilbert–Varshamov Plus
36
Def 20: Cayley Graph
37
Def 21: LPS Expander Graphs
38
Thm 11: LPS Graphs are Ramanujan
39
Def 22: Balanced Product of Vector Spaces
40
Def 23: Balanced Product Chain Complex
41
Lem 4: Künneth Formula for Balanced Products
42
Def 24: Quotient Graph Trivialization
43
Def 25: Invariant Labeling
44
Def 26: Balanced Product Tanner Cycle Code
45
Def 27: Horizontal/Vertical Homology Splitting
46
Def 28: Iota and Pi Maps
47
Thm 12: Encoding Rate (Circle Case)
48
Def 29: Horizontal Subsystem Balanced Product Code
49
Thm 13: Homological Distance Bound
50
Thm 14: Cohomological Distance Bound
51
Cor 2: Subsystem Code Parameters
52
Def 30: Unipotent Subgroup for LPS Graphs
53
Thm 15: Explicit Family of Quantum Codes
54
Cor 3: Distance-Balanced Family of Quantum Codes
55
Overview: Balanced Product Codes Formalization