Kernel-basis extraction and completeness

Lean-QEC's kernel basis (a basis of the null space of a parity-check matrix) is produced by an external Python script, and the correctness of that script is not part of the trusted base: the companion paper states that only the rank and the orthogonality are checked after the fact. This module supplies a proof inside the kernel: a set of generators is read directly off the pivot structure of row reduction, and ker(H) = span(kernel generators)

is closed in both directions inside the Lean kernel. With it, the step "the kernel basis is produced by an external script" drops out of the trusted base.

Mechanism

Row reduction outputs a mutually reduced set of pivot rows D (see IsReduced). The pivot columns are the occupied columns and the remaining columns are the free columns. For each free column j the kernel vector is taken to be kerVec D j := e_j + ∑_{r ∈ D} (r_j) · e_{pivot(r)}

that is, e_j corrected along the pivot directions by the entry of each row in column j. Orthogonality comes from (R2): every row takes the value 1 at its own pivot column and 0 at the pivot columns of the other rows, so the two kinds of contribution cancel exactly.

Main results

• kerVec_mem_kerL: a kernel vector really does lie in the kernel (the soundness direction).
• kerL_le_spanL_kerBasis: every vector in the kernel is a linear combination of the kernel generators (the completeness direction).
• kerL_rowReduce: ker H = span (kerBasis (rowReduce H)), bringing the two sides together.
• hammingNorm_kerVec_le / kerVec_ne_zero / exists_light_mem_kerL: the Singleton-type count; when the kernel is nontrivial it contains a nonzero element of weight at most the rank plus one. The frontier argument in the companion paper uses exactly this step.

def QECCertificates.unitVec {n : ℕ} (i : Fin n) : Vec n

The unit vector e_i (1 at the i-th coordinate and 0 elsewhere).

Equations

• QECCertificates.unitVec i j = if j = i then 1 else 0

@[simp]

theorem QECCertificates.unitVec_apply {n : ℕ} (i j : Fin n) : unitVec i j = if j = i then 1 else 0

Single-term summation helpers (collapsing a column-selection sum to one term)

theorem QECCertificates.sum_mul_ite_self {n : ℕ} (u : Vec n) (a : Fin n) : (∑ i : Fin n, u i * if i = a then 1 else 0) = u a

∑ i, u i * (if i = a then 1 else 0) = u a.

theorem QECCertificates.sum_mul_ite_eq {n : ℕ} (u : Vec n) (a : Fin n) (c : ZMod 2) : (∑ i : Fin n, u i * if a = i then c else 0) = u a * c

∑ i, u i * (if a = i then c else 0) = u a * c.

theorem QECCertificates.sum_ite_self {n : ℕ} (u : Vec n) (a : Fin n) : (∑ i : Fin n, if i = a then u i else 0) = u a

∑ i, (if i = a then u i else 0) = u a.

The kernel

def QECCertificates.kerL {n : ℕ} (L : List (Vec n)) : Submodule (ZMod 2) (Vec n)

The kernel of a list of rows: all vectors orthogonal to every row (zero GF(2) dot product).

This is the algebraic description of the error space of a quantum error-correcting code, namely the Pauli operators commuting with every parity-check row. It is tied to LeanQEC's LinearMap.ker M.toLin' through mem_ker_iff_dotProd_rows_eq_zero.

Equations

• QECCertificates.kerL L = { carrier := {x : QECCertificates.Vec n | ∀ r ∈ L, r ⬝ᵥ x = 0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem QECCertificates.mem_kerL {n : ℕ} {L : List (Vec n)} {x : Vec n} : x ∈ kerL L ↔ ∀ r ∈ L, r ⬝ᵥ x = 0

theorem QECCertificates.kerL_eq_of_spanL_eq {n : ℕ} {A B : List (Vec n)} (h : spanL A = spanL B) : kerL A = kerL B

The kernel depends only on the row space: two lists of rows with the same row space give the same kernel.

Pivot columns and free columns

def QECCertificates.pivCols {n : ℕ} (D : List (PivRow n)) : Finset (Fin n)

The set of pivot columns.

Equations

• QECCertificates.pivCols D = (List.map (fun (x : QECCertificates.PivRow n) => x.2) D).toFinset

def QECCertificates.IsFreeCol {n : ℕ} (D : List (PivRow n)) (j : Fin n) : Prop

A free column: a column that is not the pivot column of any row.

Equations

• QECCertificates.IsFreeCol D j = ∀ ri ∈ D, ri.2 ≠ j

theorem QECCertificates.mem_pivCols {n : ℕ} {D : List (PivRow n)} {i : Fin n} : i ∈ pivCols D ↔ ∃ ri ∈ D, ri.2 = i

theorem QECCertificates.IsReduced.row_apply_piv {n : ℕ} {D : List (PivRow n)} (hD : IsReduced D) {ri rj : PivRow n} (hri : ri ∈ D) (hrj : rj ∈ D) : ri.1 rj.2 = if ri = rj then 1 else 0

The paired form of (R2): the entry of any pivot row at any pivot column is of Kronecker type.

Kernel vectors

def QECCertificates.kerVec {n : ℕ} (D : List (PivRow n)) (j : Fin n) : Vec n

The kernel vector attached to the free column j: e_j plus the pivot corrections determined by the entries of the rows in column j.

Equations

• QECCertificates.kerVec D j i = (if i = j then 1 else 0) + ∑ ri ∈ D.toFinset, if ri.2 = i then ri.1 j else 0

theorem QECCertificates.kerVec_apply {n : ℕ} (D : List (PivRow n)) (j i : Fin n) : kerVec D j i = (if i = j then 1 else 0) + ∑ ri ∈ D.toFinset, if ri.2 = i then ri.1 j else 0

theorem QECCertificates.kerVec_apply_free {n : ℕ} {D : List (PivRow n)} {j i : Fin n} (hi : IsFreeCol D i) : kerVec D j i = if i = j then 1 else 0

On a free column the kernel vector is just e_j: every correction term vanishes.

theorem QECCertificates.kerVec_apply_piv {n : ℕ} {D : List (PivRow n)} (hD : IsReduced D) {j : Fin n} {rk : PivRow n} (hrk : rk ∈ D) : kerVec D j rk.2 = (if rk.2 = j then 1 else 0) + rk.1 j

On a pivot column the kernel vector reads off the corresponding entry of that row.

theorem QECCertificates.kerVec_mem_kerL {n : ℕ} {D : List (PivRow n)} (hD : IsReduced D) (j : Fin n) : kerVec D j ∈ kerL (rowList D)

Soundness direction: a kernel vector really does lie in the kernel of these rows.

The proof cancels two sums: the dot product of rk with the kernel vector is expanded into a double sum, the order of summation is exchanged, and the Kronecker form of (R1)/(R2) collapses the inner sum to a single term.

The Singleton-type count: how light a kernel vector is

theorem QECCertificates.kerVec_ne_zero {n : ℕ} {D : List (PivRow n)} {j : Fin n} (hj : IsFreeCol D j) : kerVec D j ≠ 0

A kernel vector is nonzero: on a free column it is just e_j, so it cannot be the zero vector.

theorem QECCertificates.hammingNorm_kerVec_le {n : ℕ} (D : List (PivRow n)) (j : Fin n) : hammingNorm (kerVec D j) ≤ D.length + 1

The Singleton-type count: the support of a kernel vector lies in $\{j\}\cup$ the pivot columns, so its weight is at most $1+\#D$.

This holds for every column j, free or not: kerVec D j can be nonzero only at j and at the pivot columns, and every other column is free and hence vanishes by kerVec_apply_free. There are exactly #D pivot columns, and #D is the rank. Together with kerVec_ne_zero this makes "a nontrivial kernel $\Rightarrow$ there is a nonzero kernel vector of weight $\le\rho+1$" a theorem rather than an informal remark.

Kernel generators

def QECCertificates.kerBasis {n : ℕ} (D : List (PivRow n)) : List (Vec n)

The kernel generators: each free column yields one kernel vector. (There are exactly n − #D free columns, so the number of generators is the dimension of the kernel; see the completeness half of kerL_rowReduce.)

Equations

• QECCertificates.kerBasis D = List.map (QECCertificates.kerVec D) (List.filter (fun (j : Fin n) => decide (j ∉ QECCertificates.pivCols D)) (List.finRange n))

theorem QECCertificates.mem_kerBasis {n : ℕ} {D : List (PivRow n)} {x : Vec n} : x ∈ kerBasis D ↔ ∃ j ∉ pivCols D, kerVec D j = x

Completeness

theorem QECCertificates.eq_sum_of_piv_support {n : ℕ} {D : List (PivRow n)} (hD : IsReduced D) {z : Vec n} (hz : ∀ (i : Fin n), (∀ ri ∈ D, ri.2 ≠ i) → z i = 0) (m : Fin n) : z m = ∑ rl ∈ D.toFinset, if rl.2 = m then z rl.2 else 0

A vector supported on the pivot columns is recovered from the pivot columns.

theorem QECCertificates.eq_zero_of_piv_support {n : ℕ} {D : List (PivRow n)} (hD : IsReduced D) {z : Vec n} (hz : ∀ (i : Fin n), (∀ ri ∈ D, ri.2 ≠ i) → z i = 0) (hzker : ∀ ri ∈ D, ri.1 ⬝ᵥ z = 0) : z = 0

The entries at the pivot columns determine everything: a vector supported on the pivot columns that also lies in the kernel must be zero.

theorem QECCertificates.kerL_le_spanL_kerBasis {n : ℕ} {D : List (PivRow n)} (hD : IsReduced D) : kerL (rowList D) ≤ spanL (kerBasis D)

Completeness direction: every vector in the kernel is a linear combination of the kernel generators.

Agreement with the original code

theorem QECCertificates.kerL_rowReduce {n : ℕ} (L : List (Vec n)) : kerL L = spanL (kerBasis (rowReduce L))

Main theorem: the kernel equals the space spanned by the kernel generators. The list of rows is first put through the trusted row reduction, and the kernel generators are read directly off the pivot structure that it outputs; the whole chain closes inside the kernel.

theorem QECCertificates.exists_light_mem_kerL {n : ℕ} (L : List (Vec n)) {j : Fin n} (hj : IsFreeCol (rowReduce L) j) : ∃ v ∈ kerL L, v ≠ 0 ∧ hammingNorm v ≤ (rowReduce L).length + 1

The row-list form of the frontier-argument step: as long as rowReduce L still has a free column, that is, as long as the kernel is nontrivial, the kernel of L contains a nonzero element of weight $\le 1+\#(rowReduce L)$.

Now $\#(rowReduce L)$ is the rank of L, so this is the full statement that a matrix of rank $\rho$ has a nonzero kernel vector of weight $\le\rho+1$: existence comes from the completeness direction of kerL_rowReduce, while nonzeroness and the weight bound come from the two results above.

theorem QECCertificates.exists_light_mem_kerL_apply {n : ℕ} (L : List (Vec n)) {j : Fin n} (hj : IsFreeCol (rowReduce L) j) : kerVec (rowReduce L) j ∈ kerL L ∧ hammingNorm (kerVec (rowReduce L) j) ≤ (rowReduce L).length + 1 ∧ kerVec (rowReduce L) j j = 1

The indexed form: the kernel vector given by the free column j lies in the kernel, has weight at most the rank plus one, and takes the value $1$ at j.

The clause "takes the value 1 at j" is needed for the frontier argument: the witness construction for the hypergraph product requires the seed kernel vector to be nonzero at some index (s a₀ = 1 in xwLeft).

Agreement with the LeanQEC matrix interface

theorem QECCertificates.LinearMap.ker_eq_kerL_ofFn {n m : ℕ} (M : Matrix (Fin m) (Fin n) (ZMod 2)) : (Matrix.toLin' M).ker = kerL (List.ofFn fun (i : Fin m) => M i)

The kernel of a parity-check matrix (LeanQEC's LinearMap.ker M.toLin') agrees with the kernel of its list of rows. This bridge lets the row-space theorems already available in LeanQEC act directly on kerL of this module.

theorem QECCertificates.LinearMap.ker_eq_spanL_kerBasis_ofFn {n m : ℕ} (M : Matrix (Fin m) (Fin n) (ZMod 2)) : (Matrix.toLin' M).ker = spanL (kerBasis (rowReduce (List.ofFn fun (i : Fin m) => M i)))

Main theorem for external use (LeanQEC interface version): the kernel of a parity-check matrix M equals the space spanned by the kernel generators. The generators are read directly off the list of rows of M by the trusted row reduction, and the whole procedure closes inside the kernel.