Verified GF(2) row reduction

LeanQEC lists "row reduction itself is not formalized" as its most concrete remaining engineering gap: "A verified row-reduction routine would close this remaining preprocessor step." This module supplies that step, turning the row simplification of a parity-check matrix into a machine-checked algorithm, so that the preprocessing no longer requires trusting an external script.

Invariants

The state of the reduction is a list of pivot rows PivRow n = Vec n × Fin n, a row vector together with the column at which it pivots. IsReduced D requires:

• (R1) every row takes the value 1 at its own pivot column
• (R2) every row takes the value 0 at the pivot column of every other row.

(R2) is symmetric: it does not presuppose an order on the rows, so the result is independent of the elimination order. This is what makes all the correctness proofs below go through.

Main results

• reduceAgainst_apply_piv: the reduced vector is 0 at every pivot column.
• add_reduceAgainst_mem: v + reduceAgainst D v lies in the row space of D.
• spanL_rowReduce: the row space is unchanged, so the code is not modified.
• isReduced_rowReduce: the output satisfies IsReduced.

@[reducible, inline]

abbrev QECCertificates.PivRow (n : ℕ) : Type

A pivot row: a row vector together with the column at which it pivots, that is, its leading nonzero entry.

Equations

• QECCertificates.PivRow n = (QECCertificates.Vec n × Fin n)

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

The row part of a list of pivot rows.

Equations

• QECCertificates.rowList D = List.map (fun (x : QECCertificates.PivRow n) => x.1) D

@[simp]

theorem QECCertificates.rowList_nil {n : ℕ} : rowList [] = []

@[simp]

theorem QECCertificates.rowList_cons {n : ℕ} (ri : PivRow n) (D : List (PivRow n)) : rowList (ri :: D) = ri.1 :: rowList D

@[simp]

theorem QECCertificates.rowList_append {n : ℕ} (D E : List (PivRow n)) : rowList (D ++ E) = rowList D ++ rowList E

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

The mutual-reduction invariant: (R1) every row is 1 at its own pivot column, and (R2) every row is 0 at the pivot column of every other row.

Equations

• QECCertificates.IsReduced D = ((∀ ri ∈ D, ri.1 ri.2 = 1) ∧ ∀ ri ∈ D, ∀ rj ∈ D, ri ≠ rj → ri.1 rj.2 = 0)

theorem QECCertificates.isReduced_nil {n : ℕ} : IsReduced []

theorem QECCertificates.IsReduced.pivot_inj {n : ℕ} {D : List (PivRow n)} (h : IsReduced D) (ri : PivRow n) : ri ∈ D → ∀ rj ∈ D, ri.2 = rj.2 → ri = rj

Immediate consequence of (R2): the pivot columns are pairwise distinct.

Reduction: clearing a row at every pivot column

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

Eliminate v at its pivot column using each row of D. Over GF(2) the coefficient is exactly the component of v at that column.

Equations

• QECCertificates.reduceAgainst D v = List.foldl (fun (w : QECCertificates.Vec n) (ri : QECCertificates.PivRow n) => w + w ri.2 • ri.1) v D

@[simp]

theorem QECCertificates.reduceAgainst_nil {n : ℕ} (v : Vec n) : reduceAgainst [] v = v

theorem QECCertificates.reduceAgainst_cons {n : ℕ} (ri : PivRow n) (D : List (PivRow n)) (v : Vec n) : reduceAgainst (ri :: D) v = reduceAgainst D (v + v ri.2 • ri.1)

theorem QECCertificates.reduceAgainst_eq_zero_of_rows_zero {n : ℕ} {D : List (PivRow n)} {q : Fin n} {v : Vec n} (hrows : ∀ ri ∈ D, ri.1 q = 0) (hv : v q = 0) : reduceAgainst D v q = 0

If every row of D is 0 at column q and v q = 0, then the reduced vector is still 0 at position q.

theorem QECCertificates.reduceAgainst_apply_piv {n : ℕ} {D : List (PivRow n)} (hD : IsReduced D) (v : Vec n) (ri : PivRow n) : ri ∈ D → reduceAgainst D v ri.2 = 0

Core lemma: when D is mutually reduced, the reduced vector is 0 at every pivot column.

theorem QECCertificates.add_reduceAgainst_mem {n : ℕ} (D : List (PivRow n)) (v : Vec n) : v + reduceAgainst D v ∈ spanL (rowList D)

Where the reduced part lands: v + reduceAgainst D v is a linear combination of the row vectors of D.

Choosing a pivot and inserting

theorem QECCertificates.support_nonempty {n : ℕ} {v : Vec n} (h : v ≠ 0) : {i : Fin n | v i ≠ 0}.Nonempty

def QECCertificates.leadIdx {n : ℕ} (v : Vec n) (h : v ≠ 0) : Fin n

The position of the first nonzero component, defined when v ≠ 0.

Equations

• QECCertificates.leadIdx v h = {i : Fin n | v i ≠ 0}.min' ⋯

theorem QECCertificates.leadIdx_spec {n : ℕ} (v : Vec n) (h : v ≠ 0) : v (leadIdx v h) ≠ 0

theorem QECCertificates.leadIdx_eq_one {n : ℕ} (v : Vec n) (h : v ≠ 0) : v (leadIdx v h) = 1

def QECCertificates.insertPivot {n : ℕ} (D : List (PivRow n)) (w : Vec n) (p : Fin n) : List (PivRow n)

Insert the new row w, whose pivot column is p, into the set of pivot rows: first clear the old rows at column p, then append w.

Equations

• QECCertificates.insertPivot D w p = List.map (fun (ri : QECCertificates.PivRow n) => (ri.1 + ri.1 p • w, ri.2)) D ++ [(w, p)]

theorem QECCertificates.rowList_insertPivot {n : ℕ} (D : List (PivRow n)) (w : Vec n) (p : Fin n) : rowList (insertPivot D w p) = List.map (fun (r : Vec n) => r + r p • w) (rowList D) ++ [w]

theorem QECCertificates.spanL_rowList_insertPivot {n : ℕ} (D : List (PivRow n)) (w : Vec n) (p : Fin n) : spanL (rowList (insertPivot D w p)) = spanL (rowList D ++ [w])

Insertion does not change the row space.

theorem QECCertificates.isReduced_insertPivot {n : ℕ} {D : List (PivRow n)} (hD : IsReduced D) {w : Vec n} {p : Fin n} (hp : w p = 1) (hz : ∀ ri ∈ D, w ri.2 = 0) : IsReduced (insertPivot D w p)

Insertion preserves the mutual-reduction invariant: it requires w to be 0 at every pivot column of D and 1 at the new pivot column.

The main loop

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

One step: reduce v and, if the result is nonzero, insert it as a new pivot row.

Equations

• One or more equations did not get rendered due to their size.

theorem QECCertificates.spanL_rowList_step {n : ℕ} (D : List (PivRow n)) (v : Vec n) : spanL (rowList (step D v)) = spanL (rowList D ++ [v])

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

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

Insert the rows of rest one by one, starting from the accumulated state D.

Equations

• QECCertificates.rowReduceFrom D [] = D
• QECCertificates.rowReduceFrom D (v :: rest) = QECCertificates.rowReduceFrom (QECCertificates.step D v) rest

@[simp]

theorem QECCertificates.rowReduceFrom_nil {n : ℕ} (D : List (PivRow n)) : rowReduceFrom D [] = D

@[simp]

theorem QECCertificates.rowReduceFrom_cons {n : ℕ} (D : List (PivRow n)) (v : Vec n) (rest : List (Vec n)) : rowReduceFrom D (v :: rest) = rowReduceFrom (step D v) rest

theorem QECCertificates.spanL_rowList_rowReduceFrom {n : ℕ} (D : List (PivRow n)) (rest : List (Vec n)) : spanL (rowList (rowReduceFrom D rest)) = spanL (rowList D ++ rest)

theorem QECCertificates.isReduced_rowReduceFrom {n : ℕ} {D : List (PivRow n)} (hD : IsReduced D) (rest : List (Vec n)) : IsReduced (rowReduceFrom D rest)

def QECCertificates.rowReduce {n : ℕ} (L : List (Vec n)) : List (PivRow n)

Verified row reduction: reduce a list of rows to a mutually reduced set of pivot rows.

Equations

• QECCertificates.rowReduce L = QECCertificates.rowReduceFrom [] L

theorem QECCertificates.spanL_rowReduce {n : ℕ} (L : List (Vec n)) : spanL (rowList (rowReduce L)) = spanL L

The row space is unchanged: elimination does not change the row space, hence does not change the code it defines.

theorem QECCertificates.isReduced_rowReduce {n : ℕ} (L : List (Vec n)) : IsReduced (rowReduce L)

The output is mutually reduced: the result is a set of pivot rows, each of them 1 at its own pivot column and 0 at the others.