GF(2) vector algebra primitives (coding-theory layer)

This module is the linear-algebra basis of the coding-theory layer: it collects the parity-check matrices, stabilizers and logical operators of a quantum error-correcting code into the GF(2) vector space Vec n = Fin n → ZMod 2, and supplies the primitives that row reduction and kernel-basis extraction are built from.

Alignment with LeanQEC: the row-space object is LeanQEC's Matrix.certificateRowSpace, reused directly (it is defined as Submodule.span (Set.range M)); this module's spanL is the equivalent formulation on the row-list side, and the bridge lemma Matrix.rowSpace_eq_spanL_ofFn connects the two. The row-space theorems already available in LeanQEC therefore apply directly to the row lists of this package.

Main definitions

• Vec n: a GF(2) vector of length n (a bit string).
• spanL L: the subspace spanned by a list of rows, that is, the row space.
• addSmul v r c: adds c • r to v. Over GF(2), taking c = v i and r i = 1 clears the i-th coordinate.

Main results

• addSmul_apply: the componentwise formula (v + c • r) i = v i + c * r i.
• addSmul_cancel: in characteristic 2, (v + c • r) + c • r = v; row operations are invertible.
• spanL_map_addSmul_append: applying that operation to a whole list of rows and then appending the new row leaves the row space unchanged.
• Matrix.rowSpace_eq_spanL_ofFn: the bridge to the LeanQEC row-space representation.

@[reducible, inline]

abbrev QECCertificates.Vec (n : ℕ) : Type

A GF(2) vector of length n. Under the symplectic representation a single Pauli operator of a quantum error-correcting code is a pair of such vectors.

Equations

• QECCertificates.Vec n = (Fin n → ZMod 2)

Generic utilities, shared by the modules that assemble matrices from literals

The three definitions e, zeroRows and add_eq_zero_iff_eq live here rather than in any particular code family: they are general-purpose tools, needed by every module that assembles a parity-check matrix from literals or that uses the characteristic-2 cancellation law, so the instance-level modules do not each carry a copy of their own.

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

The unit vector at the i-th coordinate of GF(2) (a basis of Vec n).

Equations

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

def QECCertificates.zeroRows (n : ℕ) : Matrix (Fin 0) (Fin n) (ZMod 2)

The zero-row matrix: a classical code takes it as the row-space argument of minWeightKernelOutsideRowSpace (giving certificateRowSpace = ⊥), so that set reduces to the nonzero vectors in the kernel.

Equations

• QECCertificates.zeroRows n i = i.elim0

theorem QECCertificates.add_eq_zero_iff_eq (a b : ZMod 2) : a + b = 0 ↔ a = b

In characteristic 2, a + b = 0 ↔ a = b.

def QECCertificates.support {n : ℕ} (v : Vec n) : Finset (Fin n)

The support: the positions of the nonzero components.

Equations

• QECCertificates.support v = {i : Fin n | v i ≠ 0}

@[simp]

theorem QECCertificates.mem_support {n : ℕ} {v : Vec n} {i : Fin n} : i ∈ support v ↔ v i ≠ 0

theorem QECCertificates.weight_eq_hammingNorm {n : ℕ} (v : Vec n) : (support v).card = hammingNorm v

The weight used for the code distance: the size of the support, agreeing with hammingNorm of mathlib and LeanQEC.

@[simp]

theorem QECCertificates.add_self {n : ℕ} (v : Vec n) : v + v = 0

Characteristic 2: a vector over GF(2) added to itself is zero.

theorem QECCertificates.eq_one_of_ne_zero {a : ZMod 2} (h : a ≠ 0) : a = 1

Over GF(2), nonzero means 1.

Row space

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

The subspace spanned by a list of rows, that is, the row space. The generating set is the set of elements of the list, which can be exchanged for the Set.range formulation (see spanL_ofFn_eq_span_range).

Equations

• QECCertificates.spanL L = Submodule.span (ZMod 2) {x : QECCertificates.Vec n | x ∈ L}

theorem QECCertificates.mem_spanL {n : ℕ} {L : List (Vec n)} {x : Vec n} : x ∈ spanL L ↔ x ∈ Submodule.span (ZMod 2) {y : Vec n | y ∈ L}

theorem QECCertificates.subset_spanL {n : ℕ} {L : List (Vec n)} {x : Vec n} (h : x ∈ L) : x ∈ spanL L

theorem QECCertificates.spanL_nil {n : ℕ} : spanL [] = ⊥

theorem QECCertificates.spanL_append {n : ℕ} (A B : List (Vec n)) : spanL (A ++ B) = spanL A ⊔ spanL B

The row space of an appended list is the supremum of the row spaces of the two parts.

theorem QECCertificates.spanL_singleton {n : ℕ} (v : Vec n) : spanL [v] = ZMod 2 ∙ v

The row space spanned by a single vector.

theorem QECCertificates.spanL_append_singleton {n : ℕ} (A : List (Vec n)) (v : Vec n) : spanL (A ++ [v]) = spanL A ⊔ ZMod 2 ∙ v

The single-row version: the row space after appending one row is the supremum of the original row space and that row.

theorem QECCertificates.spanL_mono_of_subset {n : ℕ} {A B : List (Vec n)} (h : A ⊆ B) : spanL A ≤ spanL B

The row space is monotone with respect to inclusion of lists.

theorem QECCertificates.add_add_left_cancel {n : ℕ} (v w : Vec n) : v + w + v = w

The characteristic-2 cancellation identity (v + w) + v = w.

theorem QECCertificates.add_add_same_left {n : ℕ} (v w : Vec n) : v + (v + w) = w

The characteristic-2 cancellation identity v + (v + w) = w.

theorem QECCertificates.add_add_same_right {n : ℕ} (v w : Vec n) : v + (w + v) = w

The characteristic-2 cancellation identity v + (w + v) = w.

theorem QECCertificates.mem_spanL_append_singleton_of_add_mem {n : ℕ} {A : List (Vec n)} {v w : Vec n} (h : v + w ∈ spanL A) : w ∈ spanL (A ++ [v])

If v + w lies in the row space of A, then appending w and appending v span the same row space. (The row produced by elimination differs from the original one by a vector that is already in the row space, so the row space is unchanged.)

theorem QECCertificates.spanL_append_eq_of_add_mem {n : ℕ} {A : List (Vec n)} {v w : Vec n} (h : v + w ∈ spanL A) : spanL (A ++ [w]) = spanL (A ++ [v])

Equality of the row spaces, obtained from the previous statement.

theorem QECCertificates.spanL_ofFn_eq_span_range {n m : ℕ} (f : Fin m → Vec n) : spanL (List.ofFn f) = Submodule.span (ZMod 2) (Set.range f)

The bridge to the Set.range formulation: the row space of List.ofFn f is the space spanned by the range of f.

theorem QECCertificates.Matrix.rowSpace_eq_spanL_ofFn {n m : ℕ} (M : Matrix (Fin m) (Fin n) (ZMod 2)) : M.certificateRowSpace = spanL (List.ofFn fun (i : Fin m) => M i)

Bridge to LeanQEC: Matrix.certificateRowSpace M (that is, Submodule.span (Set.range M)) equals the spanL of the row list of M. The row-space theorems of LeanQEC therefore apply directly to the row lists of this package.

Elementary row operations

def QECCertificates.addSmul {n : ℕ} (v r : Vec n) (c : ZMod 2) : Vec n

Adds c • r to v. Over GF(2), taking c = v i and r i = 1 clears exactly the i-th coordinate of v.

Equations

• QECCertificates.addSmul v r c = v + c • r

@[simp]

theorem QECCertificates.addSmul_apply {n : ℕ} (v r : Vec n) (c : ZMod 2) (i : Fin n) : addSmul v r c i = v i + c * r i

theorem QECCertificates.addSmul_zero_coord {n : ℕ} (v r : Vec n) (i : Fin n) (hr : r i = 1) : addSmul v r (v i) i = 0

With c = v i and r i = 1, the operation clears the i-th coordinate.

theorem QECCertificates.addSmul_cancel {n : ℕ} (v r : Vec n) (c : ZMod 2) : addSmul v r c + c • r = v

In characteristic 2 a row operation is invertible: adding and then adding back leaves the row unchanged.

theorem QECCertificates.addSmul_mem_span {n : ℕ} {S : Set (Vec n)} {v r : Vec n} (c : ZMod 2) (hv : v ∈ Submodule.span (ZMod 2) S) (hr : r ∈ Submodule.span (ZMod 2) S) : addSmul v r c ∈ Submodule.span (ZMod 2) S

A whole-list row operation preserves the row space

theorem QECCertificates.spanL_map_addSmul_append {n : ℕ} (A : List (Vec n)) (w : Vec n) (f : Vec n → ZMod 2) : spanL (List.map (fun (r : Vec n) => r + f r • w) A ++ [w]) = spanL (A ++ [w])

Preservation of the row space (whole-list version): replacing every row r of a list A by r + f r • w and then appending w at the end gives the same row space as appending w to A.

This is the correctness skeleton of row reduction: elimination performs only the one operation of adding the new row to an old row with a coefficient, which does not change the spanned subspace and hence does not change the code.