Binary matrix row spaces and logical-operator distance

Ported to Lean Pool from QCL-SUAT/Lean-QEC at a0855f8a6374c1dda2097bbf07f33ba53760fdcd. Declarations are placed in QECCertificates, with three uniquely named extensions of Matrix; imports and module syntax are updated. The span-generator equivalence has its quantifiers corrected.

Lean-QEC, Copyright 2026 The Lean-QEC Authors (Mattias Ehatamm, Yi Lee, Xiaodi Wu, Runzhou Tao). This product includes software developed as part of the paper "End-to-End Formalization of Quantum Error Correction" (arXiv:2605.16523). Licensed under the Apache License, Version 2.0.

@[instance_reducible]

noncomputable instance QECCertificates.submoduleSetFintype {n : ℕ} (C : Submodule (ZMod 2) (Fin n → ZMod 2)) : Fintype ↑↑C

Equations

• QECCertificates.submoduleSetFintype C = inferInstance

theorem QECCertificates.zmod2_val_eq_one_of_ne_zero (a : ZMod 2) (ha : a ≠ 0) : ↑a = 1

theorem QECCertificates.zmod2_val_eq_zero_of_ne_one (a : ZMod 2) (ha : a ≠ 1) : ↑a = 0

def Matrix.certificateRowSpace {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Semiring γ] (M : Matrix α β γ) : Submodule γ (β → γ)

The submodule spanned by the rows of a matrix.

Equations

• M.certificateRowSpace = Submodule.span γ (Set.range M)

theorem QECCertificates.Matrix.row_mem_rowSpace {α : Type u_1} {β : Type u_2} {γ : Type u_3} {i : α} [Semiring γ] {M : Matrix α β γ} : M i ∈ M.certificateRowSpace

theorem QECCertificates.Submodule.mem_span_range_iff_sum {α : Type u_1} {n : ℕ} (x : Fin n → ZMod 2) (v : α → Fin n → ZMod 2) : x ∈ Submodule.span (ZMod 2) (Set.range v) ↔ ∃ (S : Finset α), ∑ s ∈ S, v s = x

noncomputable def QECCertificates.minWeightKernelOutsideRowSpace {n k₁ k₂ : ℕ} (M₁ : Matrix (Fin k₁) (Fin n) (ZMod 2)) (M₂ : Matrix (Fin k₂) (Fin n) (ZMod 2)) : ℕ

Minimum Hamming weight in the first kernel outside the second row space, or n + 1 if empty.

Equations

• QECCertificates.minWeightKernelOutsideRowSpace M₁ M₂ = match (Finset.image hammingNorm (↑(Matrix.toLin' M₁).ker \ ↑M₂.certificateRowSpace).toFinset).min with | none => n + 1 | some a => a

theorem QECCertificates.min_weight_ker_not_mem_rowspace_pos {n k₁ k₂ : ℕ} {M₁ : Matrix (Fin k₁) (Fin n) (ZMod 2)} {M₂ : Matrix (Fin k₂) (Fin n) (ZMod 2)} : 0 < minWeightKernelOutsideRowSpace M₁ M₂

theorem QECCertificates.mem_ker_iff_dotProd_rows_eq_zero {n k : ℕ} (M : Matrix (Fin k) (Fin n) (ZMod 2)) (x : Fin n → ZMod 2) : x ∈ (Matrix.toLin' M).ker ↔ ∀ (i : Fin k), M i ⬝ᵥ x = 0

theorem QECCertificates.ker_dotProduct_rowSpace_eq_zero {n k : ℕ} (M : Matrix (Fin k) (Fin n) (ZMod 2)) (y x : Fin n → ZMod 2) (hy : y ∈ (Matrix.toLin' M).ker) (hx : x ∈ M.certificateRowSpace) : y ⬝ᵥ x = 0

theorem QECCertificates.dual_eq_dotProduct {n : ℕ} (f : Module.Dual (ZMod 2) (Fin n → ZMod 2)) (v : Fin n → ZMod 2) : f v = (fun (i : Fin n) => f (Pi.single i 1)) ⬝ᵥ v

theorem QECCertificates.exists_ker_dotProduct_eq_one_of_not_mem_rowSpace {n k : ℕ} (M : Matrix (Fin k) (Fin n) (ZMod 2)) (x : Fin n → ZMod 2) (hx : x ∉ M.certificateRowSpace) : ∃ y ∈ (Matrix.toLin' M).ker, y ⬝ᵥ x = 1

theorem QECCertificates.not_mem_rowspace_iff_exists_mem_ker {n k : ℕ} (M : Matrix (Fin k) (Fin n) (ZMod 2)) (x : Fin n → ZMod 2) : x ∉ M.certificateRowSpace ↔ ∃ y ∈ (Matrix.toLin' M).ker, y ⬝ᵥ x = 1

theorem QECCertificates.ex_mem_submodule_non_orth_iff_non_orth_mem_basis {n : ℕ} (S : Set (Fin n → ZMod 2)) (x : Fin n → ZMod 2) : (∃ y ∈ Submodule.span (ZMod 2) S, y ⬝ᵥ x = 1) ↔ ∃ s ∈ S, s ⬝ᵥ x = 1

A binary vector pairs nontrivially with the span exactly when it does with a generator.

theorem QECCertificates.weight_le_disj {n k : ℕ} {z : Fin n → ZMod 2} : hammingNorm z ≤ k ↔ ∑ i : Fin n, ↑(z i) ≤ k

theorem QECCertificates.sum_id_dotProduct_eq {n : ℕ} (S : Finset (Fin n → ZMod 2)) (x : Fin n → ZMod 2) : S.sum id ⬝ᵥ x = ∑ s ∈ S, s ⬝ᵥ x

theorem QECCertificates.exists_dotProduct_one_of_sum {n : ℕ} {S : Finset (Fin n → ZMod 2)} {y x : Fin n → ZMod 2} (hS_sum : S.sum id = y) (hy : y ⬝ᵥ x = 1) : ∃ s ∈ S, s ⬝ᵥ x = 1

theorem QECCertificates.Matrix.mem_rowSpace_ZMod2 {n₁ n₂ : ℕ} {M : Matrix (Fin n₁) (Fin n₂) (ZMod 2)} {x : Fin n₂ → ZMod 2} : x ∈ M.certificateRowSpace ↔ ∃ S ⊆ Finset.image M Finset.univ, S.sum id = x

theorem QECCertificates.exists_row_of_exists_mem_rowspace_non_orth {n k : ℕ} {M : Matrix (Fin k) (Fin n) (ZMod 2)} {x y : Fin n → ZMod 2} (hy₁ : y ∈ M.certificateRowSpace) (hy₂ : y ⬝ᵥ x = 1) : ∃ (r : Fin k), M r ⬝ᵥ x = 1

def Matrix.certificateMutuallyOrthogonalRows {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [Fintype γ] [Mul δ] [AddCommMonoid δ] (M₁ : Matrix α γ δ) (M₂ : Matrix β γ δ) : Prop

Every row of the first matrix is orthogonal to every row of the second.

Equations

• M₁.certificateMutuallyOrthogonalRows M₂ = ∀ (a : α) (b : β), M₁ a ⬝ᵥ M₂ b = 0

def Matrix.certificateIsKernelFor {k₁ k₂ n : ℕ} (M₁ : Matrix (Fin k₁) (Fin n) (ZMod 2)) (M₂ : Matrix (Fin k₂) (Fin n) (ZMod 2)) : Prop

The first matrix row space equals the kernel of the second matrix.

Equations

• M₁.certificateIsKernelFor M₂ = (M₁.certificateRowSpace = (Matrix.toLin' M₂).ker)

theorem QECCertificates.Matrix.is_ker_for_of_rank_sum_mutually_orth {k₁ k₂ r₁ r₂ n : ℕ} (M₁ : Matrix (Fin k₁) (Fin n) (ZMod 2)) (M₂ : Matrix (Fin k₂) (Fin n) (ZMod 2)) (hr₁ : r₁ ≤ M₁.rank) (hr₂ : r₂ ≤ M₂.rank) (hrn : r₁ + r₂ = n) (ho : M₁.certificateMutuallyOrthogonalRows M₂) : M₂.certificateIsKernelFor M₁

theorem QECCertificates.Matrix.rank_le_of_submatrix_independent {k r n : ℕ} (M : Matrix (Fin r) (Fin n) (ZMod 2)) (inds : Fin k → Fin r) (_inds_mono : StrictMono inds) (h_ind : LinearIndependent (ZMod 2) (M.submatrix inds id)) : k ≤ M.rank