Rank certificates: finrank (certificateRowSpace H) = #(rows in the row-reduction output)

The rate/rank accounting had one gap: the row-reduction preprocessing was not formalized. A trusted row reduction is available, and this module plugs it in as a rank certificate: reduce the parity-check matrix and count the rows to obtain its rank, a step that is checkable inside the kernel.

Mechanism

The output of rowReduce is a set of mutually reduced pivot rows (IsReduced). Turning it into a rank needs two things:

1. The pivot rows are linearly independent: evaluating at the pivot column of each row, (R1) gives 1 and (R2) gives 0, so a linear combination ∑ cᵢ rᵢ takes the value cⱼ at the pivot column of rⱼ; hence ∑ cᵢ rᵢ = 0 → cⱼ = 0.
2. The rows are pairwise distinct (otherwise the Fin D.length indexing is not injective and item 1 fails). This module proves that the output of rowReduce satisfies the stronger NodupPiv (the pivot columns are pairwise distinct): at the pivot column of a newly inserted row every existing row is 0 while the new row is 1, so the new row cannot coincide with any existing row.

Together the two give finrank (spanL (rowList (rowReduce L))) = (rowReduce L).length, and spanL_rowReduce then transfers the statement to the original list of rows.

Main results

• NodupPiv: the structural invariant that the pivot columns are pairwise distinct (kept throughout rowReduce).
• linearIndependent_rowList_of_isReduced: a mutually reduced list of rows is linearly independent.
• finrank_spanL_eq_length_rowReduce: the rank equals the number of rows of the reduction output.
• Matrix.rank_eq_length_rowReduce: the interface to Matrix.rank of Mathlib.

The invariant that the pivot columns are pairwise distinct

def QECCertificates.NodupPiv {n : ℕ} (D : List (PivRow n)) : Prop

The pivot columns of D are pairwise distinct. This is a structural invariant of the output of rowReduce, and the premise for "the number of rows equals the rank" (otherwise the Fin D.length indexing is not injective).

Equations

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

theorem QECCertificates.nodupPiv_nil {n : ℕ} : NodupPiv []

theorem QECCertificates.map_piv_insertPivot {n : ℕ} (D : List (PivRow n)) (w : Vec n) (p : Fin n) : List.map (fun (x : PivRow n) => x.2) (insertPivot D w p) = List.map (fun (x : PivRow n) => x.2) D ++ [p]

Inserting one row only appends p to the list of pivot columns.

theorem QECCertificates.nodupPiv_insertPivot {n : ℕ} {D : List (PivRow n)} (hD : NodupPiv D) {w : Vec n} {p : Fin n} (hp : p ∉ List.map (fun (x : PivRow n) => x.2) D) : NodupPiv (insertPivot D w p)

theorem QECCertificates.nodupPiv_step {n : ℕ} {D : List (PivRow n)} (hred : IsReduced D) (hD : NodupPiv D) (v : Vec n) : NodupPiv (step D v)

theorem QECCertificates.nodupPiv_rowReduceFrom {n : ℕ} (D : List (PivRow n)) (rest : List (Vec n)) : IsReduced D → NodupPiv D → NodupPiv (rowReduceFrom D rest)

theorem QECCertificates.nodupPiv_rowReduce {n : ℕ} (L : List (Vec n)) : NodupPiv (rowReduce L)

The pivot columns of the output of rowReduce are pairwise distinct.

theorem QECCertificates.IsReduced.tail {n : ℕ} {r : PivRow n} {D : List (PivRow n)} (h : IsReduced (r :: D)) : IsReduced D

The tail of a mutually reduced list is again mutually reduced.

theorem QECCertificates.nodup_of_nodupPiv {n : ℕ} (D : List (PivRow n)) : IsReduced D → NodupPiv D → D.Nodup

Pairwise distinct pivot columns imply pairwise distinct rows.

Linear independence of the pivot rows

theorem QECCertificates.linearIndependent_rowList_of_isReduced {n : ℕ} {D : List (PivRow n)} (hD : IsReduced D) (hnd : NodupPiv D) : LinearIndependent (ZMod 2) fun (i : Fin D.length) => (D.get i).1

A mutually reduced list of rows is linearly independent: evaluating at the pivot column of each row separates the coefficients.

theorem QECCertificates.range_get_eq_rowList {n : ℕ} (D : List (PivRow n)) : (Set.range fun (i : Fin D.length) => (D.get i).1) = {x : Vec n | x ∈ rowList D}

The range of D.get is exactly the list of rows of D.

theorem QECCertificates.card_pivCols_eq_length {n : ℕ} {D : List (PivRow n)} (h : NodupPiv D) : (pivCols D).card = D.length

Pairwise distinct pivot columns imply that the number of pivot columns equals the number of rows.

Main theorems

theorem QECCertificates.finrank_spanL_eq_length_of_isReduced {n : ℕ} {D : List (PivRow n)} (hD : IsReduced D) (hnd : NodupPiv D) : Module.finrank (ZMod 2) ↥(spanL (rowList D)) = D.length

The rank equals the number of rows of the reduction output (stated for an already reduced state).

theorem QECCertificates.finrank_spanL_eq_length_rowReduce {n : ℕ} (L : List (Vec n)) : Module.finrank (ZMod 2) ↥(spanL L) = (rowReduce L).length

Rank certificate (main theorem): the dimension of the space spanned by the list of rows equals the number of rows of the row-reduction output.

The list of pivot rows produced by the reduction is itself the certificate: the kernel only has to count the rows and check IsReduced to verify the rank independently, with no need to trust any external script.

theorem QECCertificates.length_rowReduce_le {n : ℕ} (L : List (Vec n)) : (rowReduce L).length ≤ n

The rank is at most the length of the encoding.

theorem QECCertificates.Matrix.rank_eq_finrank_rowSpace {n m : ℕ} (M : Matrix (Fin m) (Fin n) (ZMod 2)) : M.rank = Module.finrank (ZMod 2) ↥M.certificateRowSpace

Matrix.rank of Mathlib is the dimension of the row space.

theorem QECCertificates.Matrix.rank_eq_length_rowReduce {n m : ℕ} (M : Matrix (Fin m) (Fin n) (ZMod 2)) : M.rank = (rowReduce (List.ofFn fun (i : Fin m) => M i)).length

Rank certificate in matrix form: reduce the rows of the parity-check matrix and count them to obtain its rank.

Matrix.rank is the entry point through which the LeanQEC side of the distance reduction reads a rank; this theorem lets the row reduction verified in this package take over that reading directly.

A nonzero kernel vector when the rank is not full (the bridge on the threshold side)

theorem QECCertificates.exists_ne_zero_mulVec_eq_zero_of_rank_lt {m n : ℕ} (M : Matrix (Fin m) (Fin n) (ZMod 2)) (h : M.rank < n) : ∃ (v : Vec n), M.mulVec v = 0 ∧ v ≠ 0

Full rank fails $\Longrightarrow$ a nonzero kernel vector: when $M.\mathrm{rank}<n$ we have $\ker M\ne0$.

The construction is explicit: after row reduction there are fewer than $n$ pivot columns, hence a free column $j$, and kerVec takes the value 1 on that column (exists_light_mem_kerL); it is orthogonal to every row of $M$, so multiplying by $M$ on the left gives zero.

This is the bridge on the threshold side: every factor of $k=k_1k_2+k_1^\top k_2^\top$ is a $\dim\ker$, whereas what "the kernel is nontrivial" requires is the existence of a nonzero kernel vector, not a dimension. The companion paper argued this conversion only arithmetically; this theorem puts it into the kernel.