Computable membership tests: exact distances by kernel reduction

The abstract Submodule.span predicate does not by itself provide a computable membership test. This module supplies a verified decision procedure for finite binary row spaces and kernels. The abstract minimum-weight definition is noncomputable; these tests support certificates that can instead be reduced in the kernel. It turns membership in a row space and membership in a kernel into Boolean computations that the kernel can reduce, and proves that they agree exactly with the subspace semantics.

A lower bound of the form "no logical operator of smaller weight exists" can then be written as a closed Boolean equality whose truth value the kernel obtains by reduction (by decide): no SAT solver, no native_decide, no custom axioms. This is the step that removes the external solver from the trusted base.

The two tests

• Row space: inSpanB L v := reduceAgainst (rowReduce L) v = 0. Row reduction sends L to a mutually reduced set of pivot rows, and those pivots then eliminate v column by column: v lies in the row space exactly when nothing but zero remains. The two directions are supplied by add_reduceAgainst_mem (where the reduced vector lands) and by reduceAgainst_self_mem (the reduction vanishes on the generators, and linearity extends this to the whole row space).
• Kernel: inKerB M x := ∀ i, (M i) ⬝ᵥ x = 0, orthogonality row by row, a finite conjunction. It is aligned exactly with LeanQEC's mem_ker_iff_dotProd_rows_eq_zero.

Main results

• inSpanB_iff / inKerB_iff: the semantic equivalence theorems for the two tests (soundness and completeness).
• reduceAgainst_add / reduceAgainst_smul: the reduction operator is linear.
• reduceAgainst_eq_zero_of_mem_spanL: the reduction vanishes exactly on the row space.

Linearity of the reduction operator

theorem QECCertificates.reduceAgainst_zero {n : ℕ} (D : List (PivRow n)) : reduceAgainst D 0 = 0

The reduction maps zero to zero.

theorem QECCertificates.reduceAgainst_add {n : ℕ} (D : List (PivRow n)) (u v : Vec n) : reduceAgainst D (u + v) = reduceAgainst D u + reduceAgainst D v

The reduction is additive.

theorem QECCertificates.reduceAgainst_smul {n : ℕ} (D : List (PivRow n)) (c : ZMod 2) (v : Vec n) : reduceAgainst D (c • v) = c • reduceAgainst D v

The reduction is homogeneous over scalars.

def QECCertificates.reduceAgainstLin {n : ℕ} (D : List (PivRow n)) : Vec n →ₗ[ZMod 2] Vec n

The reduction operator as a linear map.

Equations

• QECCertificates.reduceAgainstLin D = { toFun := QECCertificates.reduceAgainst D, map_add' := ⋯, map_smul' := ⋯ }

theorem QECCertificates.reduceAgainst_self_mem {n : ℕ} {D : List (PivRow n)} (hD : IsReduced D) {ri : PivRow n} (hri : ri ∈ D) : reduceAgainst D ri.1 = 0

The reduction vanishes on the generators: for a mutually reduced set of pivot rows, eliminating a row by the set itself sends that row to zero.

This is the precise form of idempotence for row reduction: when the process reaches a row's own pivot column the row is annihilated outright, and no later row can disturb that column again, because (R2) keeps every other row zero there.

theorem QECCertificates.reduceAgainst_eq_zero_of_mem_spanL {n : ℕ} {D : List (PivRow n)} (hD : IsReduced D) {v : Vec n} (hv : v ∈ spanL (rowList D)) : reduceAgainst D v = 0

The reduction vanishes exactly on the row space: when D is mutually reduced, reduceAgainst D annihilates spanL (rowList D).

The proof is the standard argument that linearity plus vanishing on the generators gives vanishing on the whole span: spanL (rowList D) is spanned by rowList D, on which reduceAgainst D vanishes, so spanL (rowList D) is contained in comap (reduceAgainstLin D) ⊥.

The row-space membership test

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

Computable row-space membership test: reduce L to a mutually reduced set of pivot rows, then eliminate v with those pivots.

Elimination leaves zero exactly when v lies in the row space of L (inSpanB_iff). The whole test is a fold over a List, so the kernel can reduce it directly, which turns the statement that a given vector is not a stabilizer into a closed proposition that a single by decide settles.

Equations

• QECCertificates.inSpanB L v = decide (QECCertificates.reduceAgainst (QECCertificates.rowReduce L) v = 0)

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

Soundness: if inSpanB reports true then v really lies in the row space.

Immediate from add_reduceAgainst_mem (v plus the reduced vector lies in the row space) once the reduced vector is zero.

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

Completeness: if v lies in the row space then inSpanB reports true.

Immediate from reduceAgainst_eq_zero_of_mem_spanL, together with invariance of the row space.

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

Semantic equivalence of the membership test: the computable test and subspace membership agree exactly.

This is the single entry point for handing distance and rank questions to the kernel: any Boolean conclusion obtained by decide can be translated back into the language of Submodule through this theorem, and so be connected to the existing theorems of LeanQEC.

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

Semantic equivalence, negative form (consumed on the lower-bound side): reports false exactly when the vector is not in the row space.

The kernel membership test

def QECCertificates.inKerB {n k : ℕ} (M : Matrix (Fin k) (Fin n) (ZMod 2)) (x : Vec n) : Bool

Computable kernel membership test: orthogonality with every row of the parity-check matrix, which over GF(2) is commutation.

The shape matches LeanQEC's mem_ker_iff_dotProd_rows_eq_zero: expanding kernel membership x ∈ LinearMap.ker M.toLin' gives exactly this row-by-row conjunction.

Equations

• QECCertificates.inKerB M x = (List.ofFn fun (i : Fin k) => decide (M i ⬝ᵥ x = 0)).all id

theorem QECCertificates.inKerB_iff {n k : ℕ} (M : Matrix (Fin k) (Fin n) (ZMod 2)) (x : Vec n) : inKerB M x = true ↔ x ∈ (Matrix.toLin' M).ker

Semantic equivalence of the kernel test: inKerB reports true exactly when x lies in the kernel as LeanQEC defines it.

The bridging lemma is LeanQEC's own mem_ker_iff_dotProd_rows_eq_zero, so the computable test and the upstream semantics are connected with no intermediate layer and no additional trusted assumption.