LDPC bounds for monic CSS pushouts

Abstract

Basis-preserving monic pushouts of length-two binary CSS complexes satisfy explicit row and column weight bounds.

Definition 1.1 (Based length-two complex).

$$\mathrm{BasedComplex}=\{dim:\mathrm{Fin}\left(3\right)\to \mathbb{N};d2:\mathrm{Matrix}\left(\mathrm{Fin}\left(dim\left(1\right)\right),\mathrm{Fin}\left(dim\left(2\right)\right),\mathrm{ZMod}\left(2\right)\right);d1:\mathrm{Matrix}\left(\mathrm{Fin}\left(dim\left(0\right)\right),\mathrm{Fin}\left(dim\left(1\right)\right),\mathrm{ZMod}\left(2\right)\right);comp:d1\cdot d2=0\}$$

Formalization. D5/S3/Quantum/Information/CssMonicPushoutLdpc.BasedComplex (✓ std3).

Citation. Alexander Cowtan; Simon Burton (2024). CSS code surgery as a universal construction. DOI: 10.22331/q-2024-05-14-1344. URL: https://arxiv.org/abs/2301.13738v6.

Commentary.

A based complex has finite bases in degrees zero, one and two, two binary matrix differentials, and their composite is zero.

Definition 1.2 (Basis matrix).

$$\forall m\in \mathbb{N},\forall n\in \mathbb{N},\forall phi\in \mathrm{Fin}\left(m\right)\to \mathrm{Fin}\left(n\right),\mathrm{basisMatrix}\left(phi\right)=\lambda j\mapsto \lambda a\mapsto \mathrm{ite}\left(phi\left(a\right)=j,1,0\right)$$

Formalization. D5/S3/Quantum/Information/CssMonicPushoutLdpc.basisMatrix (✓ std3).

Citation. Alexander Cowtan; Simon Burton (2024). CSS code surgery as a universal construction. DOI: 10.22331/q-2024-05-14-1344. URL: https://arxiv.org/abs/2301.13738v6.

Commentary.

The matrix has a one in the row selected by the image of a basis element and zero elsewhere.

Definition 1.3 (Basis-preserving chain map).

$$\forall A\in \mathrm{BasedComplex},\forall C\in \mathrm{BasedComplex},\mathrm{BPChainMap}\left(A,C\right)=\{f:\forall i\in \mathrm{Fin}\left(3\right),\mathrm{Fin}\left(\dim \left(A\right)\left(i\right)\right)\to \mathrm{Fin}\left(\dim \left(C\right)\left(i\right)\right);comm2:d2\left(C\right)\cdot \mathrm{basisMatrix}\left(f\left(2\right)\right)=\mathrm{basisMatrix}\left(f\left(1\right)\right)\cdot d2\left(A\right);comm1:d1\left(C\right)\cdot \mathrm{basisMatrix}\left(f\left(1\right)\right)=\mathrm{basisMatrix}\left(f\left(0\right)\right)\cdot d1\left(A\right)\}$$

Formalization. D5/S3/Quantum/Information/CssMonicPushoutLdpc.BPChainMap (✓ std3).

Citation. Alexander Cowtan; Simon Burton (2024). CSS code surgery as a universal construction. DOI: 10.22331/q-2024-05-14-1344. URL: https://arxiv.org/abs/2301.13738v6.

Commentary.

A basis-preserving chain map consists of basis functions in all three degrees whose matrices commute with both differentials.

Definition 1.4 (Monic basis-preserving map).

$$\forall A\in \mathrm{BasedComplex},\forall C\in \mathrm{BasedComplex},\forall phi\in \mathrm{BPChainMap}\left(A,C\right),BPChainMap.Monic\left(phi\right)\iff (\forall i\in \mathrm{Fin}\left(3\right),\mathrm{Injective}\left(\mathrm{mulVec}\left(\mathrm{basisMatrix}\left(f\left(phi,i\right)\right)\right)\right))$$

Formalization. D5/S3/Quantum/Information/CssMonicPushoutLdpc.Monic (✓ std3).

Citation. Alexander Cowtan; Simon Burton (2024). CSS code surgery as a universal construction. DOI: 10.22331/q-2024-05-14-1344. URL: https://arxiv.org/abs/2301.13738v6.

Commentary.

Monicity is degreewise injectivity of the induced matrix maps.

Definition 1.5 (Pushout identification).

$$\forall A\in \mathrm{BasedComplex},\forall C\in \mathrm{BasedComplex},\forall D\in \mathrm{BasedComplex},\forall phi\in \mathrm{BPChainMap}\left(A,C\right),\forall psi\in \mathrm{BPChainMap}\left(A,D\right),\forall i\in \mathrm{Fin}\left(3\right),\forall x\in \mathrm{Sum}\left(\mathrm{Fin}\left(\dim \left(C\right)\left(i\right)\right),\mathrm{Fin}\left(\dim \left(D\right)\left(i\right)\right)\right),\forall y\in \mathrm{Sum}\left(\mathrm{Fin}\left(\dim \left(C\right)\left(i\right)\right),\mathrm{Fin}\left(\dim \left(D\right)\left(i\right)\right)\right),\mathrm{glue}\left(phi,psi,i\right)\left(x,y\right)\iff (\exists a\in \mathrm{Fin}\left(\dim \left(A\right)\left(i\right)\right),(x=\mathrm{inl}\left(f\left(phi,i\right)\left(a\right)\right))\wedge (y=\mathrm{inr}\left(f\left(psi,i\right)\left(a\right)\right)))$$

Formalization. D5/S3/Quantum/Information/CssMonicPushoutLdpc.glue (✓ std3).

Citation. Alexander Cowtan; Simon Burton (2024). CSS code surgery as a universal construction. DOI: 10.22331/q-2024-05-14-1344. URL: https://arxiv.org/abs/2301.13738v6.

Commentary.

The relation identifies the image of one apex basis element in the left foot with its image in the right foot.

Definition 1.6 (Pushout basis).

$$\forall A\in \mathrm{BasedComplex},\forall C\in \mathrm{BasedComplex},\forall D\in \mathrm{BasedComplex},\forall phi\in \mathrm{BPChainMap}\left(A,C\right),\forall psi\in \mathrm{BPChainMap}\left(A,D\right),\forall i\in \mathrm{Fin}\left(3\right),\mathrm{PBasis}\left(phi,psi\right)\left(i\right)=\mathrm{Quot}\left(\mathrm{glue}\left(phi,psi\right)\left(i\right)\right)$$

Formalization. D5/S3/Quantum/Information/CssMonicPushoutLdpc.PBasis (✓ std3).

Citation. Alexander Cowtan; Simon Burton (2024). CSS code surgery as a universal construction. DOI: 10.22331/q-2024-05-14-1344. URL: https://arxiv.org/abs/2301.13738v6.

Commentary.

The pushout basis is the quotient of the disjoint union by the identification relation.

Definition 1.7 (Degree-two block differential).

$$\forall C\in \mathrm{BasedComplex},\forall D\in \mathrm{BasedComplex},sumD2\left(C,D\right)=\mathrm{fromBlocks}\left(d2\left(C\right),0,0,d2\left(D\right)\right)$$

Formalization. D5/S3/Quantum/Information/CssMonicPushoutLdpc.sumD2 (✓ std3).

Source. Repository-derived.

Acknowledgement. Alexander Cowtan; Simon Burton (2024). CSS code surgery as a universal construction. DOI: 10.22331/q-2024-05-14-1344. URL: https://arxiv.org/abs/2301.13738v6.

Commentary.

The direct-sum differential is the block diagonal matrix with the two input differentials.

Definition 1.8 (Degree-one block differential).

$$\forall C\in \mathrm{BasedComplex},\forall D\in \mathrm{BasedComplex},sumD1\left(C,D\right)=\mathrm{fromBlocks}\left(d1\left(C\right),0,0,d1\left(D\right)\right)$$

Formalization. D5/S3/Quantum/Information/CssMonicPushoutLdpc.sumD1 (✓ std3).

Source. Repository-derived.

Acknowledgement. Alexander Cowtan; Simon Burton (2024). CSS code surgery as a universal construction. DOI: 10.22331/q-2024-05-14-1344. URL: https://arxiv.org/abs/2301.13738v6.

Commentary.

The direct-sum differential is the block diagonal matrix with the two input differentials.

Definition 1.9 (Degree-two pushout differential).

$$\forall A\in \mathrm{BasedComplex},\forall C\in \mathrm{BasedComplex},\forall D\in \mathrm{BasedComplex},\forall phi\in \mathrm{BPChainMap}\left(A,C\right),\forall psi\in \mathrm{BPChainMap}\left(A,D\right),pushoutD2\left(phi,psi\right)=\lambda (X:\mathrm{PBasis}\left(phi,psi,1\right))\mapsto \lambda (Y:\mathrm{PBasis}\left(phi,psi,2\right))\mapsto Finset.sum\left(\mathrm{filter}\left(\lambda x\mapsto Quot.mk\left(\mathrm{glue}\left(phi,psi,1\right),x\right)=X,Finset.univ\right),\lambda x\mapsto sumD2\left(C,D\right)\left(x,Quot.out\left(Y\right)\right)\right)$$

Formalization. D5/S3/Quantum/Information/CssMonicPushoutLdpc.pushoutD2 (✓ std3).

Citation. Alexander Cowtan; Simon Burton (2024). CSS code surgery as a universal construction. DOI: 10.22331/q-2024-05-14-1344. URL: https://arxiv.org/abs/2301.13738v6.

Commentary.

Each output coefficient is the sum of the selected representative coefficients over its quotient class.

Definition 1.10 (Degree-one pushout differential).

$$\forall A\in \mathrm{BasedComplex},\forall C\in \mathrm{BasedComplex},\forall D\in \mathrm{BasedComplex},\forall phi\in \mathrm{BPChainMap}\left(A,C\right),\forall psi\in \mathrm{BPChainMap}\left(A,D\right),pushoutD1\left(phi,psi\right)=\lambda (X:\mathrm{PBasis}\left(phi,psi,0\right))\mapsto \lambda (Y:\mathrm{PBasis}\left(phi,psi,1\right))\mapsto Finset.sum\left(\mathrm{filter}\left(\lambda x\mapsto Quot.mk\left(\mathrm{glue}\left(phi,psi,0\right),x\right)=X,Finset.univ\right),\lambda x\mapsto sumD1\left(C,D\right)\left(x,Quot.out\left(Y\right)\right)\right)$$

Formalization. D5/S3/Quantum/Information/CssMonicPushoutLdpc.pushoutD1 (✓ std3).

Citation. Alexander Cowtan; Simon Burton (2024). CSS code surgery as a universal construction. DOI: 10.22331/q-2024-05-14-1344. URL: https://arxiv.org/abs/2301.13738v6.

Commentary.

Each output coefficient is the sum of the selected representative coefficients over its quotient class.

Definition 1.11 (Maximum row weight).

$$\forall I\in \mathrm{Type},\forall K\in \mathrm{Type},[\mathrm{Fintype}\left(I\right)][\mathrm{Fintype}\left(K\right)]\forall M\in \mathrm{Matrix}\left(I,K,\mathrm{ZMod}\left(2\right)\right),\mathrm{maxRowWeight}\left(M\right)=\sup \left(Finset.univ,\lambda i\mapsto \mathrm{card}\left(\mathrm{filter}\left(\lambda j\mapsto M\left(i,j\right)\ne 0,Finset.univ\right)\right)\right)$$

Formalization. D5/S3/Quantum/Information/CssMonicPushoutLdpc.maxRowWeight (✓ std3).

Source. Repository-derived.

Acknowledgement. Alexander Cowtan; Simon Burton (2024). CSS code surgery as a universal construction. DOI: 10.22331/q-2024-05-14-1344. URL: https://arxiv.org/abs/2301.13738v6.

Commentary.

The maximum row weight is the finite supremum of the cardinalities of nonzero row supports.

Definition 1.12 (Maximum column weight).

$$\forall I\in \mathrm{Type},\forall K\in \mathrm{Type},[\mathrm{Fintype}\left(I\right)][\mathrm{Fintype}\left(K\right)]\forall M\in \mathrm{Matrix}\left(I,K,\mathrm{ZMod}\left(2\right)\right),\mathrm{maxColWeight}\left(M\right)=\mathrm{maxRowWeight}\left(\mathrm{transpose}\left(M\right)\right)$$

Formalization. D5/S3/Quantum/Information/CssMonicPushoutLdpc.maxColWeight (✓ std3).

Source. Repository-derived.

Acknowledgement. Alexander Cowtan; Simon Burton (2024). CSS code surgery as a universal construction. DOI: 10.22331/q-2024-05-14-1344. URL: https://arxiv.org/abs/2301.13738v6.

Commentary.

The maximum column weight is the maximum row weight of the transpose.

Definition 1.13 (Uniform LDPC family).

$$\forall d2w\in \mathbb{N}\to \mathrm{Prod}\left(\mathbb{N},\mathbb{N}\right),\forall d1w\in \mathbb{N}\to \mathrm{Prod}\left(\mathbb{N},\mathbb{N}\right),\mathrm{IsLDPC}\left(d2w,d1w\right)\iff (\exists w\in \mathbb{N},\forall n\in \mathbb{N},(\mathrm{fst}\left(d2w\left(n\right)\right)\le w)\wedge ((\mathrm{snd}\left(d2w\left(n\right)\right)\le w)\wedge ((\mathrm{fst}\left(d1w\left(n\right)\right)\le w)\wedge (\mathrm{snd}\left(d1w\left(n\right)\right)\le w))))$$

Formalization. D5/S3/Quantum/Information/CssMonicPushoutLdpc.IsLDPC (✓ std3).

Citation. Alexander Cowtan; Simon Burton (2024). CSS code surgery as a universal construction. DOI: 10.22331/q-2024-05-14-1344. URL: https://arxiv.org/abs/2301.13738v6.

Commentary.

One natural-number bound controls both row and column weights of both differentials at every family index.

Definition 1.14 (Degree-two weights).

$$\forall E\in \mathrm{BasedComplex},weights2\left(E\right)=(\mathrm{maxRowWeight}\left(d2\left(E\right)\right),\mathrm{maxColWeight}\left(d2\left(E\right)\right))$$

Formalization. D5/S3/Quantum/Information/CssMonicPushoutLdpc.weights2 (✓ std3).

Source. Repository-derived.

Acknowledgement. Alexander Cowtan; Simon Burton (2024). CSS code surgery as a universal construction. DOI: 10.22331/q-2024-05-14-1344. URL: https://arxiv.org/abs/2301.13738v6.

Commentary.

The pair records maximum row and column weights of the degree-two differential.

Definition 1.15 (Degree-one weights).

$$\forall E\in \mathrm{BasedComplex},weights1\left(E\right)=(\mathrm{maxRowWeight}\left(d1\left(E\right)\right),\mathrm{maxColWeight}\left(d1\left(E\right)\right))$$

Formalization. D5/S3/Quantum/Information/CssMonicPushoutLdpc.weights1 (✓ std3).

Source. Repository-derived.

Acknowledgement. Alexander Cowtan; Simon Burton (2024). CSS code surgery as a universal construction. DOI: 10.22331/q-2024-05-14-1344. URL: https://arxiv.org/abs/2301.13738v6.

Commentary.

The pair records maximum row and column weights of the degree-one differential.

Definition 1.16 (Cowtan–Burton Conjecture D.1).

$$claim=(\forall A\in \mathbb{N}\to \mathrm{BasedComplex},\forall C\in \mathbb{N}\to \mathrm{BasedComplex},\forall D\in \mathbb{N}\to \mathrm{BasedComplex},\forall phi\in \left(\forall n\in \mathbb{N},\mathrm{BPChainMap}\left(A\left(n\right),C\left(n\right)\right)\right),\forall psi\in \left(\forall n\in \mathbb{N},\mathrm{BPChainMap}\left(A\left(n\right),D\left(n\right)\right)\right),(\forall n\in \mathbb{N},BPChainMap.Monic\left(phi\left(n\right)\right))\Rightarrow ((\forall n\in \mathbb{N},BPChainMap.Monic\left(psi\left(n\right)\right))\Rightarrow ((\mathrm{IsLDPC}\left(\lambda n\mapsto weights2\left(A\left(n\right)\right),\lambda n\mapsto weights1\left(A\left(n\right)\right)\right))\Rightarrow ((\mathrm{IsLDPC}\left(\lambda n\mapsto weights2\left(C\left(n\right)\right),\lambda n\mapsto weights1\left(C\left(n\right)\right)\right))\Rightarrow ((\mathrm{IsLDPC}\left(\lambda n\mapsto weights2\left(D\left(n\right)\right),\lambda n\mapsto weights1\left(D\left(n\right)\right)\right))\Rightarrow (\mathrm{IsLDPC}\left(\lambda n\mapsto (\mathrm{maxRowWeight}\left(pushoutD2\left(phi\left(n\right),psi\left(n\right)\right)\right),\mathrm{maxColWeight}\left(pushoutD2\left(phi\left(n\right),psi\left(n\right)\right)\right)),\lambda n\mapsto (\mathrm{maxRowWeight}\left(pushoutD1\left(phi\left(n\right),psi\left(n\right)\right)\right),\mathrm{maxColWeight}\left(pushoutD1\left(phi\left(n\right),psi\left(n\right)\right)\right))\right)))))))$$

Formalization. D5/S3/Quantum/Information/CssMonicPushoutLdpc.claim (✓ std3).

Citation. Alexander Cowtan; Simon Burton (2024). CSS code surgery as a universal construction. DOI: 10.22331/q-2024-05-14-1344. URL: https://arxiv.org/abs/2301.13738v6.

Commentary.

Conjecture D.1 (Appendix D, p. 18): “Let C• ←f• A• →g• D• be a basis-preserving monic span in Ch(MatF2), and let Q• be the pushout chain complex of this monic span. Further, let the monic span be a representative of a family of monic spans which are parameterised by some n ∈ ℕ, and let A•, C• and D• be the Z-type complexes of quantum LDPC codes. Then (Q•, Q•) is also LDPC.” The Lean proposition expands the source objects and counts.

Theorem 1.17 (The proved LDPC closure).

$$\forall A\in \mathbb{N}\to \mathrm{BasedComplex},\forall C\in \mathbb{N}\to \mathrm{BasedComplex},\forall D\in \mathbb{N}\to \mathrm{BasedComplex},\forall phi\in \left(\forall n\in \mathbb{N},\mathrm{BPChainMap}\left(A\left(n\right),C\left(n\right)\right)\right),\forall psi\in \left(\forall n\in \mathbb{N},\mathrm{BPChainMap}\left(A\left(n\right),D\left(n\right)\right)\right),(\forall n\in \mathbb{N},BPChainMap.Monic\left(phi\left(n\right)\right))\Rightarrow ((\forall n\in \mathbb{N},BPChainMap.Monic\left(psi\left(n\right)\right))\Rightarrow ((\mathrm{IsLDPC}\left(\lambda n\mapsto weights2\left(A\left(n\right)\right),\lambda n\mapsto weights1\left(A\left(n\right)\right)\right))\Rightarrow ((\mathrm{IsLDPC}\left(\lambda n\mapsto weights2\left(C\left(n\right)\right),\lambda n\mapsto weights1\left(C\left(n\right)\right)\right))\Rightarrow ((\mathrm{IsLDPC}\left(\lambda n\mapsto weights2\left(D\left(n\right)\right),\lambda n\mapsto weights1\left(D\left(n\right)\right)\right))\Rightarrow (\mathrm{IsLDPC}\left(\lambda n\mapsto (\mathrm{maxRowWeight}\left(pushoutD2\left(phi\left(n\right),psi\left(n\right)\right)\right),\mathrm{maxColWeight}\left(pushoutD2\left(phi\left(n\right),psi\left(n\right)\right)\right)),\lambda n\mapsto (\mathrm{maxRowWeight}\left(pushoutD1\left(phi\left(n\right),psi\left(n\right)\right)\right),\mathrm{maxColWeight}\left(pushoutD1\left(phi\left(n\right),psi\left(n\right)\right)\right))\right))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Information/CssMonicPushoutLdpc.result (✓ std3). ∎

Resolves. Problems/cowtan-burton-2024-css-monic-pushout-ldpc (proved) by D5/S3/Quantum/Information/CssMonicPushoutLdpc.result.

Source. Repository-derived.

Acknowledgement. Alexander Cowtan; Simon Burton (2024). CSS code surgery as a universal construction. DOI: 10.22331/q-2024-05-14-1344. URL: https://arxiv.org/abs/2301.13738v6.

Commentary.

Monicity makes each quotient fibre contain at most one basis element from either foot. A quotient column is the image of any representative column, and its support has cardinality at most that of the input column, while a row support injects into the disjoint union of one row from each foot. Thus the column bound is the maximum of the two input column weights and the row bound is their sum. Applying these bounds pointwise gives the uniform family bound with constant wC + wD; no bound on the apex is required.

References

• Truth anchor: D5/S3/Quantum/Information/CssMonicPushoutLdpc.BPChainMap
• Truth anchor: D5/S3/Quantum/Information/CssMonicPushoutLdpc.BasedComplex
• Truth anchor: D5/S3/Quantum/Information/CssMonicPushoutLdpc.IsLDPC
• Truth anchor: D5/S3/Quantum/Information/CssMonicPushoutLdpc.Monic
• Truth anchor: D5/S3/Quantum/Information/CssMonicPushoutLdpc.PBasis
• Truth anchor: D5/S3/Quantum/Information/CssMonicPushoutLdpc.basisMatrix
• Truth anchor: D5/S3/Quantum/Information/CssMonicPushoutLdpc.claim
• Truth anchor: D5/S3/Quantum/Information/CssMonicPushoutLdpc.glue
• Truth anchor: D5/S3/Quantum/Information/CssMonicPushoutLdpc.maxColWeight
• Truth anchor: D5/S3/Quantum/Information/CssMonicPushoutLdpc.maxRowWeight
• Truth anchor: D5/S3/Quantum/Information/CssMonicPushoutLdpc.pushoutD1
• Truth anchor: D5/S3/Quantum/Information/CssMonicPushoutLdpc.pushoutD2
• Truth anchor: D5/S3/Quantum/Information/CssMonicPushoutLdpc.result
• Truth anchor: D5/S3/Quantum/Information/CssMonicPushoutLdpc.sumD1
• Truth anchor: D5/S3/Quantum/Information/CssMonicPushoutLdpc.sumD2
• Truth anchor: D5/S3/Quantum/Information/CssMonicPushoutLdpc.weights1
• Truth anchor: D5/S3/Quantum/Information/CssMonicPushoutLdpc.weights2