An append-only echelon rank routine (usable rank readings on wide matrices)

Why it is needed

rowReduce (GF2/RowReduce.lean) returns a mutually reduced set of pivot rows: every time a new pivot is inserted, the new pivot column is back-substituted into all previous rows (the D.map of insertPivot). The consequence is that the large new pivot row w is copied into every previous row element, and the next call to reduceAgainst traverses those copies one by one, so the term size grows multiplicatively with each round. On width 24, 13×13 foldl steps over 24 coordinates should take well under a second, but the measured cost falls off a cliff at about 7 pivots (more than 200 s without converging, peak working set above 200 GB); width 18 is only just feasible and width 24 is unusable.

This module provides an append-only, non-back-substituting companion routine, in which previous rows are left untouched when a new row joins. Mathematically it is still a correct echelon form: the new row is 0 on every earlier pivot column (guaranteed by the fold inside reduceAgainst, see reduceAgainst_get_piv_eq_zero), so the pivot columns are pairwise distinct, and taking the least index then proves the rows linearly independent.

Relation to rowReduce

rankEchelon_eq_length_rowReduce: the two routines return the same number and the same row space, so the rank is rankEchelon. Downstream rank and k claims can therefore switch backends without any change to the mathematics, while rowReduce and all of its downstream theorems (canonical-form uniqueness in GF2/Canonical.lean relies on the RREF produced by back-substitution) are left untouched.

A discipline for the implementation (read before editing)

stepA must be a separate def, and the main loop must be written as List.foldl stepA []. Inlining if hw : reduceAgainst D v = 0 then … else … into the structural recursion makes the elaborator hang (measured: more than 3 minutes with no output, a 3.2 GB working set on a single core), whereas the same logic split into a separate def goes through at once.

Main results

• spanL_rowList_echelonFrom: the row space is unchanged (the code is not modified).
• linearIndependent_get_of_echelon: the rows of the echelon form are linearly independent.
• finrank_spanL_eq_length_echelonFrom / rankEchelon_eq_length_rowReduce: the rank readings.

Append-only pivot insertion and the main loop

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

Append a pivot row to a list of pivot rows: previous rows are left untouched, unlike the back-substitution performed by insertPivot.

Equations

• QECCertificates.insertPivotA D w p = D ++ [(w, p)]

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

One step: reduce v against the current state and, if the result is nonzero, append it as a new pivot row.

Equations

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

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

The echelon form obtained by appending row by row (the main loop of this module).

Equations

• QECCertificates.echelonFrom L = List.foldl QECCertificates.stepA [] L

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

The rank routine: the number of rows of the append-only echelon form.

Equations

• QECCertificates.rankEchelon L = (QECCertificates.echelonFrom L).length

Invariance of the row space

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

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

Appending spans the same row space as appending the original, unreduced row: the reduced vector lies in the original row space.

theorem QECCertificates.spanL_rowList_foldl_stepA {n : ℕ} (D : List (PivRow n)) (L : List (Vec n)) : spanL (rowList (List.foldl stepA D L)) = spanL (rowList D ++ L)

A generalized form of the main loop: starting from D and consuming L, the row space is exactly that of rowList D ++ L.

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

Invariance of the row space: the append-only echelon form spans the same row space as the original list of rows, and so defines the same code.

The echelon invariants

The append-only echelon form satisfies two properties. These are weaker than IsReduced: they do not require an earlier row to be 0 on a later pivot column, and that is exactly the price of dropping back-substitution.

• EchSelf: every row is 1 on its own pivot column
• EchPair: a later row is 0 on the pivot columns of all earlier rows.

EchPair is a product of the fold inside reduceAgainst: while the j-th row is being processed, every already processed row is cleared one at a time on its own pivot column, and adding further rows cannot reintroduce anything, because every row added is 0 on all earlier pivot columns (see reduceAgainst_get_piv_eq_zero).

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

Every row is 1 on its own pivot column.

Equations

• QECCertificates.EchSelf D = ∀ (i : Fin D.length), (D.get i).1 (D.get i).2 = 1

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

A later row is 0 on the pivot columns of all earlier rows.

Equations

• QECCertificates.EchPair D = ∀ (i j : Fin D.length), i < j → (D.get j).1 (D.get i).2 = 0

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

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

theorem QECCertificates.EchPair.head_rows {n : ℕ} {r : PivRow n} {D : List (PivRow n)} (h : EchPair (r :: D)) (r' : PivRow n) : r' ∈ D → r'.1 r.2 = 0

A direct consequence of EchPair: every row after the head row is 0 on the pivot column of the head row.

theorem QECCertificates.reduceAgainst_get_piv_eq_zero {n : ℕ} {D : List (PivRow n)} (v : Vec n) (h1 : EchSelf D) (h2 : EchPair D) (i : Fin D.length) : reduceAgainst D v (D.get i).2 = 0

The key step: once the fold inside reduceAgainst has finished, the accumulator is 0 on every pivot column of that state.

The induction separates the head row from the rest. For the remaining rows it uses the induction hypothesis, which holds for an arbitrary starting vector; for the pivot column of the head row it uses the fact that the remaining rows are all 0 on that column, so the fold does not change it, together with the starting vector already being zero there.

Linear independence of the echelon rows

theorem QECCertificates.linearIndependent_get_of_echelon {n : ℕ} {D : List (PivRow n)} (h1 : EchSelf D) (h2 : EchPair D) : LinearIndependent (ZMod 2) fun (i : Fin D.length) => (D.get i).1

The rows of an echelon form are linearly independent.

Take the least index j whose coefficient in the linear combination is nonzero and evaluate on the pivot column of row j: terms with index below j have coefficient 0, and rows with index above j are 0 on that column by EchPair, so the combination takes the value g j ≠ 0 there, contradicting the combination being zero.

Preservation of the invariants by stepA and the main loop

theorem QECCertificates.echSelf_nil {n : ℕ} : EchSelf []

theorem QECCertificates.echPair_nil {n : ℕ} : EchPair []

theorem QECCertificates.length_append_singleton {n : ℕ} (D : List (PivRow n)) (x : PivRow n) : (D ++ [x]).length = D.length + 1

theorem QECCertificates.get_append_singleton_cast {n : ℕ} (D : List (PivRow n)) (x : PivRow n) (i : Fin D.length) : (D ++ [x]).get ⟨↑i, ⋯⟩ = D.get i

The i-th element of (D ++ [x]), for i within D, is the i-th element of D.

For a variable D, (D ++ [x]).length is not defeq to D.length + 1, so the index is written out explicitly as ⟨i.val, _⟩ rather than with Fin.cast, which avoids moving proofs around at the level of Fin.

theorem QECCertificates.get_append_singleton_last {n : ℕ} (D : List (PivRow n)) (x : PivRow n) : (D ++ [x]).get ⟨D.length, ⋯⟩ = x

The last element of (D ++ [x]) is x.

theorem QECCertificates.EchSelf_append {n : ℕ} (D : List (PivRow n)) (x : PivRow n) (hD : EchSelf D) (hx : x.1 x.2 = 1) : EchSelf (D ++ [x])

theorem QECCertificates.EchPair_append {n : ℕ} (D : List (PivRow n)) (x : PivRow n) (hD : EchPair D) (hx : ∀ (i : Fin D.length), x.1 (D.get i).2 = 0) : EchPair (D ++ [x])

theorem QECCertificates.EchSelf_stepA {n : ℕ} {D : List (PivRow n)} (h1 : EchSelf D) (v : Vec n) : EchSelf (stepA D v)

theorem QECCertificates.EchPair_stepA {n : ℕ} {D : List (PivRow n)} (h1 : EchSelf D) (h2 : EchPair D) (v : Vec n) : EchPair (stepA D v)

theorem QECCertificates.echSelf_echelonFrom_foldl {n : ℕ} (D : List (PivRow n)) (L : List (Vec n)) (h1 : EchSelf D) (h2 : EchPair D) : EchSelf (List.foldl stepA D L) ∧ EchPair (List.foldl stepA D L)

theorem QECCertificates.echelonFrom_ech {n : ℕ} (L : List (Vec n)) : EchSelf (echelonFrom L) ∧ EchPair (echelonFrom L)

The append-only echelon form satisfies the two invariants.

Rank readings

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

The rank equals the number of rows of the append-only echelon form.

theorem QECCertificates.rankEchelon_eq_length_rowReduce {n : ℕ} (L : List (Vec n)) : rankEchelon L = (rowReduce L).length

The bridge theorem: the append-only echelon form and rowReduce give the same rank.

Both are outputs of the same greedy pivot count, with the same row space, and in both cases the number of rows is the rank. Downstream rank and k claims can therefore switch backends without any change to the mathematics; rowReduce and its downstream users (canonical-form uniqueness in GF2/Canonical.lean relies on the RREF produced by back-substitution) are untouched.

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

The interface in matrix form: the rank of a parity-check matrix.

A fast backend for the membership test (echelonFrom in place of rowReduce)

inSpanB in GF2/Membership.lean decides row-space membership from the output of rowReduce. Where the test is recomputed for every candidate, as in the weight-bounded enumeration of lightCand, this is a difference of orders of magnitude: on width 24, rowReduce takes more than 200 s from the 7th row onwards, whereas echelonFrom takes milliseconds.

The key observation: the membership test does not need the full reduction (RREF) produced by rowReduce; the append-only echelon form suffices. The elimination argument inside reduceAgainst uses only EchPair, that is, a later row being 0 on an earlier row's pivot column, and the step that the RREF used to carry (a vector that lies in the row space and is 0 on every pivot column must be zero) is supplied instead by taking the least index in the coefficient representation.

theorem QECCertificates.eq_zero_of_mem_spanL_of_piv_eq_zero {n : ℕ} {D : List (PivRow n)} (h1 : EchSelf D) (h2 : EchPair D) {w : Vec n} (hw : w ∈ spanL (rowList D)) (h0 : ∀ (i : Fin D.length), w (D.get i).2 = 0) : w = 0

In echelon form, all pivot columns zero implies zero: if w lies in the span of rowList D and is 0 on every pivot column of D, then w = 0.

The argument: take a coefficient representation w = Σ cᵢ rᵢ and let j be the least index with cⱼ ≠ 0. Evaluating on pⱼ, the terms with i > j vanish by EchPair and those with i < j have coefficient 0, so w pⱼ = cⱼ ≠ 0, contradicting the hypothesis. This is exactly the part that the symmetry condition (R2) of IsReduced used to carry.

theorem QECCertificates.reduceAgainst_echelonFrom_eq_zero_of_mem_spanL {n : ℕ} {L : List (Vec n)} {v : Vec n} (hv : v ∈ spanL L) : reduceAgainst (echelonFrom L) v = 0

The reduction vanishes exactly on the row space (echelon backend): the output of echelonFrom annihilates the span of the original list of rows.

This is parallel to reduceAgainst_eq_zero_of_mem_spanL in GF2/Membership.lean, the IsReduced version, but the hypotheses here use only EchSelf and EchPair; the step that the RREF used to carry is supplied by eq_zero_of_mem_spanL_of_piv_eq_zero.

Computable membership test: echelon backend

The same mathematical content and the same interface shape as inSpanB in GF2/Membership.lean, with only the reduction backend changed. Where the test is run once per candidate, as in the weight-bounded enumeration of lightCand, which has 2325 candidates for $[[24,3,4]]$, this is a difference of orders of magnitude: on width 24, rowReduce fails to converge after the 7th row and takes more than 200 s, whereas echelonFrom takes milliseconds.

def QECCertificates.inSpanEch {n : ℕ} (L : List (Vec n)) (v : Vec n) : Bool

Computable row-space membership test (echelon backend).

Equations

• QECCertificates.inSpanEch L v = decide (QECCertificates.reduceAgainst (QECCertificates.echelonFrom L) v = 0)

theorem QECCertificates.inSpanEch_sound {n : ℕ} {L : List (Vec n)} {v : Vec n} (h : inSpanEch L v = true) : v ∈ spanL L

theorem QECCertificates.inSpanEch_complete {n : ℕ} {L : List (Vec n)} {v : Vec n} (hv : v ∈ spanL L) : inSpanEch L v = true

theorem QECCertificates.inSpanEch_iff {n : ℕ} (L : List (Vec n)) (v : Vec n) : inSpanEch L v = true ↔ v ∈ spanL L

Semantic equivalence of the membership test (echelon backend): the same Boolean value as inSpanB.

Explicit rank certificates

The cost of row reduction rises steeply with width. Where the width is large enough that rowReduce and echelonFrom no longer finish, the rank can still be obtained by checking a certificate. There is a cheap criterion on each side:

• Lower bound: produce a list D of candidate rows with pairwise distinct pivots, each of them lying in spanL L. If those rows are defined as linear combinations of rows of L, assembled term by term with Submodule.add_mem, membership is algebraic and independent of the width, while distinctness of the pivots is a finite check that decide can perform. Hence D.length ≤ dim spanL L (length_le_finrank_spanL_of_certificate).
• Upper bound: produce redundant generators, that is, write L as A ++ B and prove that every row of B lies in spanL A; then dim spanL L ≤ A.length (finrank_spanL_append_le_of_mem). Each redundancy is a single equality check of the form "this row is a sum of rows", which decide can perform.

Both are row-by-row or relation-by-relation checks, so their cost is linear in the width. Concrete upstream rank certificates are outside this import.

theorem QECCertificates.finrank_spanL_le_length {n : ℕ} (A : List (Vec n)) : Module.finrank (ZMod 2) ↥(spanL A) ≤ A.length

The dimension of spanL A is at most the length of A: A is a generating set.

theorem QECCertificates.finrank_spanL_le_of_mem_of_subset {n : ℕ} {A L : List (Vec n)} (h : ∀ v ∈ L, v ∈ spanL A) : Module.finrank (ZMod 2) ↥(spanL L) ≤ A.length

A rank upper bound from redundant generators (set form): if every row of L lies in spanL A, then dim spanL L ≤ A.length. The list A need not be a prefix of L, since spanL sees only the underlying set, so picking head rows of L that span the whole list and having the whole list generated by those head generators come to the same thing. This form also applies when a spanning subset is not a prefix of the row list.

theorem QECCertificates.finrank_spanL_append_le_of_mem {n : ℕ} (A B : List (Vec n)) (h : ∀ v ∈ B, v ∈ spanL A) : Module.finrank (ZMod 2) ↥(spanL (A ++ B)) ≤ A.length

A rank upper bound from redundant generators (prefix form): write the list of rows as A ++ B; if every row of B lies in spanL A, then the dimension of the whole list is at most A.length.

theorem QECCertificates.length_le_finrank_spanL_of_certificate {n : ℕ} {L : List (Vec n)} {D : List (PivRow n)} (hsub : ∀ (i : Fin D.length), (D.get i).1 ∈ spanL L) (h1 : EchSelf D) (h2 : EchPair D) : D.length ≤ Module.finrank (ZMod 2) ↥(spanL L)

A rank lower bound from a certificate: if every row of D lies in spanL L and D satisfies the echelon invariants, then D.length ≤ dim spanL L.

theorem QECCertificates.inSpanEch_eq_false_iff {n : ℕ} (L : List (Vec n)) (v : Vec n) : inSpanEch L v = false ↔ v ∉ spanL L

Negative form (echelon backend): consumed on the lower-bound side.