slug: cowtan-burton-2024-css-monic-pushout-ldpc
bibkey: cowtanburton2024csssurgery
doi: 10.22331/q-2024-05-14-1344
url: https://arxiv.org/abs/2301.13738v6
triage: theorem
motivation_gids:
  - D5/S3/Quantum/Information/CssMonicPushoutLdpc.result

Cowtan–Burton Conjecture D.1: LDPC monic CSS pushouts

Problem

Alexander Cowtan and Simon Burton, CSS code surgery as a universal construction, Quantum 8 (2024), 1344, arXiv:2301.13738v6, Appendix D, Conjecture D.1:

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. Formulating this conjecture properly requires specifying what it means for a monic span to be parameterised.

The settlement is Proved for the proposition in #19488, interpreting parameterisation as an arbitrary natural-indexed family.

Statement echo

Write $E_i=\mathrm{Fin}(C.\dim (i))\bigsqcup \mathrm{Fin}(D.\dim (i))$ and $q_i:E_i\to \mathrm{PBasis}(\phi ,\psi ,i)$ for the quotient map. Under both monicity hypotheses, D5.S3.Quantum.Information.CssMonicPushoutLdpc.pushoutD2_representative_independent proves, for every $Y:\mathrm{PBasis}(\phi ,\psi ,2)$, $y:E_2$ with $q_2(y)=Y$, and $X:\mathrm{PBasis}(\phi ,\psi ,1)$,

$$pushoutD2(\phi ,\psi )(X,Y)=\sum _{x\in E_1,q_1(x)=X}sumD2(C,D)(x,y).$$

D5.S3.Quantum.Information.CssMonicPushoutLdpc.pushoutD1_representative_independent proves the analogous formula for $Y:\mathrm{PBasis}(\phi ,\psi ,1)$, $y:E_1$ with $q_1(y)=Y$, and $X:\mathrm{PBasis}(\phi ,\psi ,0)$:

$$pushoutD1(\phi ,\psi )(X,Y)=\sum _{x\in E_0,q_0(x)=X}sumD1(C,D)(x,y).$$

Thus the two matrices represent the induced maps $[y]\mapsto [\partial y]$, independently of the selected representative. The degree-two and degree-one formulas use BPChainMap.comm2 and BPChainMap.comm1, respectively. The identity ${\partial }_1^Q{\partial }_2^Q=0$ is checked by the pinned experiment below; it is not delivered as a Lean theorem.

The categorical universal property is proved in prose here, rather than by a Lean categorical theorem. In degree $i$, take the free binary vector space on $\mathrm{PBasis}(\phi ,\psi ,i)$. Its maps from the two feet send a basis vector $x$ to $[x]$ and agree on every apex basis vector. Any two linear maps from the feet agreeing on the apex assign equal values to each generating glued pair, so extend uniquely to a linear map on the quotient basis. The representative formulas above identify its differentials with $[y]\mapsto [\partial y]$. If the two maps from the feet are chain maps, that extension commutes with the differential on every quotient generator, hence everywhere by linearity. Uniqueness follows because those generators span. This identifies the construction with the basis-preserving pushout of Lemma 5.4.

Motivation

LDPC closure supplies a uniform bound for the checks and qubit incidences of code surgery. The precise estimates distinguish the role of monicity from assumptions on the apex, homology and code distance.

Gap

The row-support bound needs the two summands to embed into the quotient. The matching fact is an application of Mathlib’s existing set-pushout injectivity theorem, not new content. The new estimate injects an output row support into the disjoint union of at most one row from each input block.

Route

monic_basis_injective turns the component matrix hypothesis into injectivity of each basis function. matching transports Mathlib’s set-pushout inclusions to PBasis. quotient_column_card_le applies Finsupp.mapDomain_support and finite image-cardinality bounds to bound a fiber-summed column support by the original support. quotient_block_row_bound injects the selected quotient row support into two input row supports. Both column bounds choose a representative of each quotient class and use the private representative-independence lemma to express its column as the quotient image of that representative column. The generic block column estimate bounds this image whether the representative belongs to the $C$ basis or the $D$ basis. Both row bounds use the quotient row-support estimate. All four private bounds feed result.

For input bounds $w_C,w_D$, the row estimate is at most $w_C+w_D$ and the column estimate is at most $\max (w_C,w_D)\le w_C+w_D$. Applying these estimates to both degrees at every index proves the family bound. This derivation does not use the apex sparsity hypothesis.

Falsifier

A span satisfying the binding monicity and LDPC hypotheses but violating an asserted weight bound would contradict result. The non-monic Appendix D examples illustrate why dropping monicity allows unbounded row merging; they are not counterexamples to the theorem.

Evidence

The kernel-checked public theorem is D5.S3.Quantum.Information.CssMonicPushoutLdpc.result. The representative-independence lemmas and support estimates are private helpers used in its derivation. The proofs use pinned Mathlib and declarations of the same module; there are no frozen D5 prerequisites.

Historical literature completeness remains ASSUMED-UNVERIFIED.

Escape audit unfinished: #19605, target D5.S3.Quantum.Information.CssMonicPushoutLdpc.result. No successful four-slot registration is asserted.

Experiment

Published numerical check. Command: python3 /tmp/op-cb2301/check.py, using the exact check.py bytes extracted from the pinned directory; exit 0. Script SHA-256: 44a0f10bac1c34fa1cb087d5abe4600f34445a22bf7bba4dd6f79920fc3d8740.

Computed scope: 3000 random based monic spans; representative independence in 3000/3000, square-zero in 3000/3000, zero violations of either weight bound in either degree. Appendix D non-monic examples at $m=2,3,5,10$ have merged row weights $3,4,6,11=m+1$. The check reports RESULT PASS. These finite computations are supplementary evidence. The private representative-independence lemmas prove the representative formulas in the derivation of result; square-zero has only the computed evidence stated here. They establish no bounds on homology or distance.

Triage

What the settlement shows

The decisive mechanism is a row-support injection, together with a column support-image inclusion. Monicity makes the quotient classes contain at most one basis element from each foot. This gives single-span estimates, then uniform family estimates without an apex sparsity bound. The support-image estimate itself does not use monicity; the column bounds use monicity when identifying the images of different representatives. The generic support lemmas apply beyond chain complexes to block matrices with fiber-sum row maps and chosen columns.

The Appendix D obstruction is unbounded merging of rows when the legs fail to be monic. The computed examples demonstrate it only at the four stated sizes; the source provides the general example. No optimality classification, homology bound or code-distance bound is claimed. The source’s code-surgery constructions receive an LDPC support estimate under the binding monic-span hypotheses; their other hypotheses and quantitative conclusions are not altered.

ASSUMED-UNVERIFIED

Literature completeness is ASSUMED-UNVERIFIED. The preregistration records source v1/v6, selected later works (arXiv:2407.09423, 2503.05003, 2505.01370 and 2510.14895), and an incompletely verified thesis attestation. No general monic-span LDPC settlement was found in that inspected scope. The independent thesis retrieval and the full citing-literature screen are incomplete. Mathematical proof of the binding support statement does not certify novelty or complete the unfinished escape audit. The categorical universal property is established by the prose derivation above, not a Lean categorical theorem.