HGP, part three: the cleaning argument and the X distance lower bound #
The first part gave the construction and CSS orthogonality, the second the compression identity $H_Xv=0 \iff H_1U=RH_2$, the transposed-code relation and the single-block weight lower bound. This part adds the cleaning/quotient argument for mixed blocks (both blocks nonzero at once), so that the X distance lower bound of the HGP holds for every nontrivial logical operator:
$$d_X \ge \min(d_1,\; d_2^\top),\qquad d_1 = \min\ker H_1,\quad d_2^\top = \min\ker H_2^\top.$$
1. The cleaning lemma (the core of this part) #
Let $v = (U,R) \in \ker H_X$, that is $H_1U = RH_2$, and let $|v|$ denote the weight.
- Row cleaning (
blockL_rows_mem_of_small): if $|v| < d_1$, then every row of $U$ lies in the row space of $H_2$. Proof: if some row $U_{a\cdot}$ has nonzero dot product with $z\in\ker H_2$, let $x_a := U_{a\cdot}\cdot z$; the compression identity gives $H_1 x = 0$, while $x \ne 0$ and $|x| \le |v| < d_1$, contradicting "every kernel vector has weight at least $d_1$". - Column cleaning (
blockR_cols_mem_of_small): if $|v| < d_2^\top$, then every column of $R$ lies in the column space of $H_1$ (the symmetric argument, with $w\in\ker H_1^\top$).
Both are weight-counting arguments: the contradiction comes from the direct clash between "every kernel vector has weight at least the distance" and "the support of that vector is a subset of the support of $v$". No enumeration is needed.
2. Consistency (the cleaning certificate) #
Row cleaning gives $C_0$ with $C_0H_2 = U$; column cleaning makes every column of
$\rho := R + H_1C_0$ lie in the column space of $H_1$, with $\rho H_2 = 0$. This part proves
(exists_cleaning_cert) that
$$\text{the columns all lie in }\mathrm{col}(H_1)\;\wedge\;\rho H_2 = 0 \;\Longrightarrow\; \exists D,\; H_1D = \rho \;\wedge\; DH_2 = 0.$$
The construction is explicit: the columns of $\rho$ are read back through rowReduce
(colList H₁) by col_decomp, the coefficients are the entries of the pivot rows, and then the
preimage preimage is applied.
3. Assembly #
$C := C_0 + D$ satisfies both $CH_2 = U$ and $H_1C = R$, so
$v = (CH_2,\, H_1C) = \sum_{a,d}C_{ad}\cdot(\text{row }(a,d)\text{ of }H_Z)$
lies in $\mathrm{row}\,H_Z$ (sum_smul_hgpHZ_apply + mem_spanL_hgpHZ_of_blocks).
Main results #
exists_ker_dot_ne_zero_of_not_mem/mem_spanL_of_forall_dot_eq_zero: the separation lemma, that the row space is exactly the orthogonal complement of the kernel (realised constructively through the elimination residual and a kernel vector).blockL_rows_mem_of_small/blockR_cols_mem_of_small: the two cleaning lemmas.exists_cleaning_cert: the consistency construction of the cleaning certificate.hgp_X_distance_ge: $v\in\ker H_X$, $v\notin\mathrm{row}H_Z$, $v\ne0$ $\Longrightarrow \min(d_1, d_2^\top) \le |v|$, the general lower bound for X-type logical operators, complementary to the single-block lower bound of the second part (which needs no quotient).
1. Row and column lists, and preimages #
The columns of a matrix, as a list of Vec (the vector length is the number of rows).
Equations
Instances For
A vector in the row span is a linear combination of the rows with some coefficient vector:
∃ λ, ∀ j, Σ_t λ_t M_{tj} = y_j.
The preimage of right multiplication: M *ᵥ preimage M y = y whenever y lies in the column
span (see preimage_spec).
Equations
- QECCertificates.preimage M y = if h : ∃ (x : QECCertificates.Vec k), M.mulVec x = y then Classical.choose h else 0
Instances For
2. Separation lemma: the row space is the orthogonal complement of the kernel #
Separation lemma: a vector outside the row space has nonzero dot product with some kernel vector.
The construction is explicit: reduce y against the output of the elimination, so that the
residual y' is nonzero (otherwise y would lie in the row space) and vanishes on the pivot
columns; take the free column j at which y' is nonzero, and kerVec D j is the required kernel
vector (it is 1 on the free column j and 0 on the other free columns, while y' is nonzero only
on free columns).
3. Weight counting: row-wise and column-wise dot products do not increase the weight #
4. The cleaning lemmas #
Row cleaning: if $|v| < d_1$, every row of blockL v lies in the row space of H₂.
The proof uses the matrix-level form of the compression identity: if some row has nonzero dot
product with z ∈ ker H₂, then blockL v *ᵥ z ≠ 0, whereas
H₁ *ᵥ (blockL v *ᵥ z) = (H₁ * blockL v) *ᵥ z = (blockR v * H₂) *ᵥ z = blockR v *ᵥ (H₂ *ᵥ z) = 0,
which contradicts d₁.
Column cleaning: if $|v| < d_2^\top$, every column of blockR v lies in the column space of
H₁.
The dual matrix-level argument: the transposed-code identity for (blockR v)ᵀ *ᵥ w gives
H₂ᵀ *ᵥ ((blockR v)ᵀ *ᵥ w) = (blockL v)ᵀ *ᵥ (H₁ᵀ *ᵥ w) = 0.
5. Consistency: column decomposition and the cleaning certificate #
Column decomposition (read back from the elimination): if every column of M lies in the
span
of the row list c, the pivot rows of the elimination output give an explicit set of coefficients:
M i j = Σ_{ri} M ri.2 j * ri.1 i.
Cleaning certificate (consistency): a matrix ρ whose columns all lie in the column space
of
H₁ and which satisfies ρ H₂ = 0 can be written as H₁ D with D H₂ = 0, that is, it can be
cleaned.
Construction: D = Σ_{ri} preimage(ri.1) ⊗ (row ri.2 of ρ), where ri runs over the pivot rows of
rowReduce (colList H₁) (col_decomp supplies the coefficients).
6. Assembly: combinations of the rows of H_Z, and the main theorem #
A vector of the form (C H₂, H₁ C) is a linear combination of the rows of H_Z (computed
entrywise).
A vector whose two blocks are C H₂ and H₁ C lies in the row space of H_Z (the same
object as
Matrix.certificateRowSpace in LeanQEC).
X distance lower bound for the HGP (the cleaning theorem): a nonzero X-type operator outside
the row space of H_Z, that is a nontrivial X-type logical operator, has weight at least
$\min(d_1, d_2^\top)$, the smaller of the left code distance and the transposed code distance.
This is complementary to the single-block lower bounds of the second part: those need no "outside the row space" hypothesis, whereas this theorem also covers mixed blocks (both blocks nonzero at once), at the cost of being stated in the quotient.
6. Each of the two premises of the cleaning lower bound can be dropped: only one route #
counts
The two steps of the cleaning lower bound hgp_X_distance_ge each need a weight hypothesis:
row cleaning needs $|v|<d_1$, column cleaning needs $|v|<d_2^\top$. This section shows that each
step can be replaced by a kernel condition, leaving the lower bound with a single factor:
- Row cleaning (the rows of
blockL vlie in the row space of $H_2$) holds unconditionally when $\ker H_1=0$ or $\ker H_2=0$. In the first case $H_1$ is injective: the identity of that step maps $u:=U z$ to $H_1u=0$, so $u=0$. In the second case the orthogonality to be proved is vacuous, since $\ker H_2$ contains only $0$. - Column cleaning (the columns of
blockR vlie in the column space of $H_1$) is discharged symmetrically by $\ker H_1^\top=0$ (the column space is already full) or by $\ker H_2^\top=0$ (where $y:=R^\top w$ is pinned to $0$ by $H_2^\top y=0$ together with injectivity).
The four distance theorems are the output of this section: the first two give $d_2^\top\le|v|$ (the factor $d_1$ does not participate), the last two give $d_1\le|v|$ ($d_2^\top$ does not participate). This is exactly the case in which the certificate kernel of one route is trivial: a downstream development uses it to close the "$\ge$" half of C1 on the residual classes.
6.1. Four lemmas on dropping a cleaning step #
Row cleaning (branch $\ker H_1=0$): when $H_1$ is injective, every row of blockL v lies in
the row space of $H_2$ unconditionally.
This is isomorphic to blockL_rows_mem_of_small, except that the "contradiction with $d_1$" step
is replaced by injectivity: the identity of that step already sends $u:=U z$ into $\ker H_1$,
so $u=0$; neither $u\ne 0$ nor a weight hypothesis is needed.
Row cleaning (branch $\ker H_2=0$): when $H_2$ is injective the orthogonality hypothesis is
vacuous: the required $\langle U_{a\cdot},z\rangle=0$ is asked only for $z\in\ker H_2$, where
$z=0$ is the only element. (This branch therefore does not need the compression identity: the
conclusion mentions only blockL v and $H_2$.)
Column cleaning (branch $\ker H_1^\top=0$): here the columns of $H_1$ already span the whole
of Vec r₁, so the conclusion holds unconditionally. (Again the compression identity is not
needed.)
Column cleaning (branch $\ker H_2^\top=0$): isomorphic to blockR_cols_mem_of_small, but
the
"contradiction with $d_2^\top$" step is replaced by injectivity: the identity already sends
$y:=R^\top w$ into $\ker H_2^\top$, so $y=0$.
6.2. Two assembly theorems, each dropping one step #
Cleaning lower bound with row cleaning free: as soon as the rows of blockL v lie in the
row
space of $H_2$ unconditionally, the single factor $d_2^\top$ suffices; the rest is word for
word hgp_X_distance_ge (column cleaning still uses $|v|<d_2^\top$).
Cleaning lower bound with column cleaning free: as soon as the columns of blockR v lie in
the column space of $H_1$ unconditionally, the single factor $d_1$ suffices (row cleaning still
uses $|v|<d_1$).
6.3. Four distance theorems #
Lower bound for $d_X$ (branch $\ker H_1=0$): when $H_1$ is injective the single factor $d_2^\top$ suffices.
Lower bound for $d_X$ (branch $\ker H_2=0$): when $H_2$ is injective the single factor $d_2^\top$ suffices.
Lower bound for $d_X$ (branch $\ker H_2^\top=0$): when $H_2^\top$ is injective the single factor $d_1$ suffices.
Lower bound for $d_X$, the branch where the certificate kernel is trivial: if $\ker H_1^\top = 0$, then every X-type logical operator has weight $\ge d_1$.
Which gap this fills: the cleaning lower bound hgp_X_distance_ge gives $\min(d_1,d_2^\top)$,
and $d_2^\top$ may be strictly smaller yet unattainable; "the certificate kernel of the right
route is trivial" ($\ker H_1^\top=0$) is exactly that situation. The theorem says that the smaller
value then does not participate in the lower bound and $d_1$ alone suffices.
Proof (isomorphic to the cleaning lower bound, but using only row cleaning plus a
surjectivity): suppose $|v|<d_1$. Row cleaning gives $U = C\,H_2$ (where $U$ is blockL v), so
the remainder $\rho := R + H_1C$ satisfies $\rho H_2 = 0$. Now $\ker H_1^\top = 0$ together with
the separation lemma mem_spanL_of_forall_dot_eq_zero gives that the columns of $H_1$ are
surjective (every vector of Vec r₁ lies in the span of $\mathrm{colList}\,H_1$), so every
column of $\rho$ lies there too. Both conditions are met, and exists_cleaning_cert gives $D$ with
$H_1D = \rho$ and $DH_2 = 0$, so v and (C+D) form a stabilizer and $v$ lies in the row space,
contradicting that $v$ is not a logical operator.