Canonical form uniqueness: the elimination output of a row space is a canonical invariant

An earlier module supplies the trusted row reduction rowReduce (the row space is preserved and the output is mutually reduced) and proves that its length is the rank. This module adds the last piece: the elimination output is the canonical form of the row space, that is, two row lists spanning the same row space have the same set of rows after elimination. Whether two codes agree can then be decided by the kernel by comparing elimination outputs directly, instead of expanding to $2^n$ vectors and comparing them one by one.

Why IsEchelon is needed

IsReduced alone does not determine the canonical form: for [(r, p)], every non-zero component column p of r satisfies the mutual-reduction invariant ((R2) imposes no constraint when there is a single row). What the row space really determines is pivot column = the first non-zero column of the row (leadIdx), and an elimination output satisfies exactly that. It is recorded as a separate structural invariant:

IsEchelon D := IsReduced D ∧ every row is zero before its pivot column.

Skeleton of the proof

1. Read-off (readOff): readOff D w = Σ_{ri ∈ D} (w ri.2) • ri.1. When D is mutually reduced this is the identity map on the row space (readOff_eq_of_mem_spanL, proved by Submodule.span_induction: it is the identity on the generators and linear under addition and scalar multiplication). This lemma translates "an element of the row space" into "its values on the pivot columns", and it is the entry point for every structural assertion.
2. The row-space characterisation of the pivot set (exists_piv_eq_leadIdx_of_mem_spanL): the first non-zero column of any non-zero element of the row space is a pivot column of D. The proof is the read-off computed term by term: take the pivot row whose coefficient is non-zero and whose pivot is smallest; pivot rows above it vanish in that column (IsEchelon) and the coefficients below it are zero.
3. Putting the two together: when two echelon row lists span the same row space, the characterisation above pins the two pivot sets to the same set (hPiv12/hPiv21), and read-off together with (R1)/(R2) then pins each row as well.

Main results

• readOff_eq_of_mem_spanL: the read-off is the identity on the row space.
• pivRow_mem_iff_of_spanL_eq: canonical form uniqueness.
• isEchelon_rowReduce, rowReduce_mem_iff_of_spanL_eq: the output set of rowReduce depends only on the row space (it is a canonical invariant).

Read-off

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

Read-off: recombines the values of w on its pivot columns, following the pivot rows of D. When D is mutually reduced it is the identity map on the row space.

Equations

• QECCertificates.readOff D w = ∑ ri ∈ D.toFinset, w ri.2 • ri.1

@[simp]

theorem QECCertificates.readOff_nil {n : ℕ} (w : Vec n) : readOff [] w = 0

theorem QECCertificates.readOff_apply {n : ℕ} (D : List (PivRow n)) (w : Vec n) (i : Fin n) : readOff D w i = ∑ ri ∈ D.toFinset, w ri.2 * ri.1 i

Componentwise form: the smul expanded into scalar multiplication.

theorem QECCertificates.readOff_add {n : ℕ} (D : List (PivRow n)) (x y : Vec n) : readOff D (x + y) = readOff D x + readOff D y

theorem QECCertificates.readOff_smul {n : ℕ} (D : List (PivRow n)) (c : ZMod 2) (x : Vec n) : readOff D (c • x) = c • readOff D x

theorem QECCertificates.readOff_eq_of_mem_spanL {n : ℕ} {D : List (PivRow n)} (hD : IsReduced D) {w : Vec n} (hw : w ∈ spanL (rowList D)) : readOff D w = w

Main lemma (read-off = identity): when D is mutually reduced, the read-off is the identity map on the row space of D.

The proof follows Submodule.span_induction: on a generator, the pivot column of ri collapses the sum to a single term (the remaining terms are killed by (R2)); the zero, addition and scalar cases are given by readOff_add/readOff_smul.

theorem QECCertificates.eq_zero_of_mem_spanL_of_piv_zero {n : ℕ} {D : List (PivRow n)} (hD : IsReduced D) {w : Vec n} (hw : w ∈ spanL (rowList D)) (h0 : ∀ ri ∈ D, w ri.2 = 0) : w = 0

The vanishing lemma: an element of the row space that takes the value zero on every pivot column is the zero vector. (A corollary of the read-off, and the direct form of "the values on the pivot columns determine everything".)

The echelon structure: the pivot column is the first non-zero column

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

Echelon and mutually reduced: IsReduced together with "everything before the pivot column is zero".

The second condition pins the pivot column to leadIdx (the first non-zero column of the row). Without it, [(r, p)] (with p any non-zero component column of r) is mutually reduced, and the canonical form is not unique.

Equations

• QECCertificates.IsEchelon D = (QECCertificates.IsReduced D ∧ ∀ ri ∈ D, ∀ i < ri.2, ri.1 i = 0)

theorem QECCertificates.ne_zero_of_piv_eq_one {n : ℕ} {v : Vec n} {p : Fin n} (h : v p = 1) : v ≠ 0

A row that takes the value 1 on its pivot column is non-zero.

theorem QECCertificates.leadIdx_le_of_ne_zero {n : ℕ} {v : Vec n} (h : v ≠ 0) {i : Fin n} (hi : v i ≠ 0) : leadIdx v h ≤ i

theorem QECCertificates.eq_zero_of_lt_leadIdx {n : ℕ} {v : Vec n} (h : v ≠ 0) {i : Fin n} (hi : i < leadIdx v h) : v i = 0

Everything before leadIdx is zero.

theorem QECCertificates.leadIdx_eq_piv_of_isEchelon {n : ℕ} {D : List (PivRow n)} (h : IsEchelon D) {ri : PivRow n} (hri : ri ∈ D) {hne : ri.1 ≠ 0} : leadIdx ri.1 hne = ri.2

The pivot column of an echelon row list is the leadIdx of its row.

The row-space characterisation of the pivot set

theorem QECCertificates.exists_piv_eq_leadIdx_of_mem_spanL {n : ℕ} {D : List (PivRow n)} (hD : IsEchelon D) {w : Vec n} (hw : w ∈ spanL (rowList D)) (hw0 : w ≠ 0) : ∃ ri ∈ D, ri.2 = leadIdx w hw0

Main lemma (pivot characterisation): in the row space spanned by an echelon row list, the first non-zero column of any non-zero element is one of the pivot columns of that list.

The characterisation uses only the row space itself, so it turns the "pivot set" into an invariant of the row space, and canonical form uniqueness follows.

Canonical form uniqueness

theorem QECCertificates.pivRow_mem_iff_of_spanL_eq {n : ℕ} {D₁ D₂ : List (PivRow n)} (h₁ : IsEchelon D₁) (h₂ : IsEchelon D₂) (hspan : spanL (rowList D₁) = spanL (rowList D₂)) (x : PivRow n) : x ∈ D₁ ↔ x ∈ D₂

Canonical form uniqueness: two echelon mutually reduced row lists that span the same row space have the same set of rows.

Hence the output of rowReduce is a canonical invariant of the row space: two codes agree exactly when the row sets of their elimination outputs agree (rowReduce_mem_iff_of_spanL_eq).

Canonical invariance of the elimination output

theorem QECCertificates.isEchelon_rowReduce {n : ℕ} (L : List (Vec n)) : IsEchelon (rowReduce L)

The elimination output is an echelon mutually reduced row list: its pivot columns are exactly the leadIdx values at insertion time.

theorem QECCertificates.rowReduce_mem_iff_of_spanL_eq {n : ℕ} {L₁ L₂ : List (Vec n)} (h : spanL L₁ = spanL L₂) (x : PivRow n) : x ∈ rowReduce L₁ ↔ x ∈ rowReduce L₂

Canonical invariance (main theorem): two row lists with the same row space have the same set of rows after elimination.

This is the decidable criterion, inside the kernel, for whether two codes are the same: compare the row sets of their elimination outputs.