A checkable certificate for the distance lower bound: handing "no lighter logical operator" to

the kernel

GF2/Witness provides the two-sided interface that pins down the distance, but the lower-bound side still sits at the abstract form "given a per-operator inequality", which is the part LeanQEC delegates to a SAT solver. This module lands it:

is the set of light operators nonempty?
  = over the candidate vectors of "weight ≤ d-1", filter by
    "nonzero ∧ in the kernel ∧ not in the row space" and see whether anything is left

Every piece of the predicate is computable (inKerB and inSpanEch). The row echelon form is computed once before filtering and reused for every candidate, and the candidate set is the weight-bounded enumeration of GF2/WeightEnum: 121 vectors rather than 32768 at $n = 15$. The whole decision is therefore a closed Boolean identity that by decide can settle directly, with the kernel doing the computation. No SAT solver, no native_decide, and no custom axiom is needed.

The two properties of the candidate set (they decide the soundness and the cost of the

certificate)

• Coverage (mem_lightVecs): every vector of weight $\le w$ lies in the candidate set, so "absent from the candidates" means "does not exist at all". This is the source of soundness, and it is exactly what Finset.univ provides for free.
• Count (length_lightVecs): the candidate set has exactly $\sum_{k\le w}\binom nk$ elements. This is the cost of the certificate: for fixed $d$ it is a polynomial of degree $d-1$ in $n$, not $2^n$.

Main results

• lowerHyp_of_lightSet_card_zero: an empty set of light operators implies the per-operator lower bound.
• le_minWeight_of_lightSet_card_zero: the lower-bound certificate; an empty set gives the code distance lower bound d.
• eq_minWeight_of_decide: the checkable certificate form of the exact distance, with the lower bound by decide and an explicit witness for the upper bound; the two sides pinch to "the code distance is exactly $d$".
• lightCand_length_le: the certificate complexity, the candidate space being at most $\sum_{k<d}\binom nk$.

The set of light operators

@[reducible, inline]

abbrev QECCertificates.IsLightUndetectable {n m₁ m₂ : ℕ} (M₁ : Matrix (Fin m₁) (Fin n) (ZMod 2)) (M₂ : Matrix (Fin m₂) (Fin n) (ZMod 2)) (v : Vec n) : Prop

The predicate "undetectable nontrivial operator of weight less than d".

The three pieces together are exactly what the lower bound has to rule out: nonzero, commuting with every check, yet not an element of the check row space. Each piece is computable, so the kernel can reduce the whole predicate; the weight bound is carried by the candidate set itself, lightVecs n (d-1).

Marked abbrev rather than def: def is semireducible, so the instance search for DecidablePred does not unfold it and Finset.filter fails to synthesize a decidable predicate.

Equations

• QECCertificates.IsLightUndetectable M₁ M₂ v = (0 < hammingNorm v ∧ QECCertificates.inKerB M₁ v = true ∧ QECCertificates.inSpanEch (List.ofFn fun (i : Fin m₂) => M₂ i) v = false)

def QECCertificates.lightCand {n m₁ m₂ : ℕ} (M₁ : Matrix (Fin m₁) (Fin n) (ZMod 2)) (M₂ : Matrix (Fin m₂) (Fin n) (ZMod 2)) (d : ℕ) : List (Vec n)

The candidate set for the lower-bound certificate: among the vectors of weight $\le d-1$, those that commute with the checks yet do not lie in the row space.

The candidates come from lightVecs n (d-1), a weight-bounded enumeration rather than the full space. The append-only echelon form of M₂ is shared across all candidates. The bound $d-1$ on the weight is justified because the lower bound only has to rule out operators of weight $< d$ (wtRec_eq_hammingNorm + Nat.lt_iff_le_pred).

Equations

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

def QECCertificates.lightSet {n m₁ m₂ : ℕ} (M₁ : Matrix (Fin m₁) (Fin n) (ZMod 2)) (M₂ : Matrix (Fin m₂) (Fin n) (ZMod 2)) (d : ℕ) : Finset (Vec n)

The set of light operators: the Finset form of the candidate set, in which card = 0 means "there is no lighter logical operator".

Equations

• QECCertificates.lightSet M₁ M₂ d = (QECCertificates.lightCand M₁ M₂ d).toFinset

theorem QECCertificates.mem_lightSet {n m₁ m₂ : ℕ} {M₁ : Matrix (Fin m₁) (Fin n) (ZMod 2)} {M₂ : Matrix (Fin m₂) (Fin n) (ZMod 2)} {d : ℕ} {v : Vec n} : v ∈ lightSet M₁ M₂ d ↔ v ∈ lightCand M₁ M₂ d

Membership characterization, expanding lightSet into the candidate set and the predicate.

theorem QECCertificates.mem_lightCand {n m₁ m₂ : ℕ} {M₁ : Matrix (Fin m₁) (Fin n) (ZMod 2)} {M₂ : Matrix (Fin m₂) (Fin n) (ZMod 2)} {d : ℕ} {v : Vec n} : v ∈ lightCand M₁ M₂ d ↔ v ∈ lightVecs n (d - 1) ∧ IsLightUndetectable M₁ M₂ v

The lower-bound certificate

theorem QECCertificates.lowerHyp_of_lightSet_card_zero {n m₁ m₂ : ℕ} (M₁ : Matrix (Fin m₁) (Fin n) (ZMod 2)) (M₂ : Matrix (Fin m₂) (Fin n) (ZMod 2)) {d : ℕ} (h : (lightSet M₁ M₂ d).card = 0) (E : Fin n → ZMod 2) : E ∈ (Matrix.toLin' M₁).ker → E ∉ M₂.certificateRowSpace → d ≤ hammingNorm E

The lower-bound certificate, checkable form: an empty set of light operators implies that the code distance is at least d.

The proof is contraposition, coverage and translation. If an undetectable operator of weight below d existed, its weight would be nonzero, since otherwise it would lie in the row space and contradict undetectability, and a weight $\le d-1$ places it in the weight-bounded enumeration (mem_lightVecs; the soundness of this certificate rests entirely on that coverage theorem). The lemmas inKerB_iff and inSpanEch_eq_false_iff then translate it into the two certificates of the decision layer, and mem_lightCand puts it back into the set, contradicting emptiness.

theorem QECCertificates.le_minWeight_of_lightSet_card_zero {n m₁ m₂ : ℕ} (M₁ : Matrix (Fin m₁) (Fin n) (ZMod 2)) (M₂ : Matrix (Fin m₂) (Fin n) (ZMod 2)) {d : ℕ} (hd : d ≤ n) (h : (lightSet M₁ M₂ d).card = 0) : d ≤ minWeightKernelOutsideRowSpace M₁ M₂

The lower-bound theorem, checkable certificate form: an empty lightSet gives the distance lower bound.

The List-form lower-bound entry point (for large candidate sets)

lightSet is the Finset form of the candidate list. Deduplication inside List.toFinset compares vectors pairwise, so its cost can dominate a large enumeration. The three results below have the same mathematical content as the lightSet family, with the hypothesis replaced by lightCand M₁ M₂ d = [], avoiding that deduplication.

theorem QECCertificates.lowerHyp_of_lightCand_nil {n m₁ m₂ : ℕ} (M₁ : Matrix (Fin m₁) (Fin n) (ZMod 2)) (M₂ : Matrix (Fin m₂) (Fin n) (ZMod 2)) {d : ℕ} (h : lightCand M₁ M₂ d = []) (E : Fin n → ZMod 2) : E ∈ (Matrix.toLin' M₁).ker → E ∉ M₂.certificateRowSpace → d ≤ hammingNorm E

The lower-bound certificate, List form: an empty candidate list implies that the code distance is at least d.

theorem QECCertificates.le_minWeight_of_lightCand_nil {n m₁ m₂ : ℕ} (M₁ : Matrix (Fin m₁) (Fin n) (ZMod 2)) (M₂ : Matrix (Fin m₂) (Fin n) (ZMod 2)) {d₀ : ℕ} (hd : d₀ ≤ n) (h : lightCand M₁ M₂ d₀ = []) : d₀ ≤ minWeightKernelOutsideRowSpace M₁ M₂

The lower-bound theorem, List form.

theorem QECCertificates.eq_minWeight_of_lightCand_nil {n m₁ m₂ : ℕ} (M₁ : Matrix (Fin m₁) (Fin n) (ZMod 2)) (M₂ : Matrix (Fin m₂) (Fin n) (ZMod 2)) {d : ℕ} (hd : d ≤ n) (hlow : lightCand M₁ M₂ d = []) {E : Vec n} (hker : E ∈ (Matrix.toLin' M₁).ker) (hnot : E ∉ M₂.certificateRowSpace) (hw : hammingNorm E = d) : minWeightKernelOutsideRowSpace M₁ M₂ = d

The exact distance, List form: the same shape as eq_minWeight_of_decide with the lower-bound hypothesis replaced by an empty candidate list; used for instances with large candidate sets.

theorem QECCertificates.eq_minWeight_of_decide {n m₁ m₂ : ℕ} (M₁ : Matrix (Fin m₁) (Fin n) (ZMod 2)) (M₂ : Matrix (Fin m₂) (Fin n) (ZMod 2)) {d : ℕ} (hd : d ≤ n) (hlow : (lightSet M₁ M₂ d).card = 0) {E : Vec n} (hker : E ∈ (Matrix.toLin' M₁).ker) (hnot : E ∉ M₂.certificateRowSpace) (hw : hammingNorm E = d) : minWeightKernelOutsideRowSpace M₁ M₂ = d

The exact distance, checkable certificate form: the lower bound by decide and an explicit witness for the upper bound pinch to an equality.

This is a uniform proof template for concrete parity-check matrices. For a code, only four things have to be supplied: (i) two parity-check matrices, (ii) an explicit low-weight logical operator E, (iii) three closed assertions the kernel can compute, namely that E is in the kernel, that E is not in the row space, and that hammingNorm E = d, and (iv) an empty lightSet. No step refers to an external solver or to a custom axiom.

Certificate complexity

theorem QECCertificates.lightCand_length_le {n m₁ m₂ : ℕ} (M₁ : Matrix (Fin m₁) (Fin n) (ZMod 2)) (M₂ : Matrix (Fin m₂) (Fin n) (ZMod 2)) {d : ℕ} (hd : 1 ≤ d) : (lightCand M₁ M₂ d).length ≤ ∑ k ∈ Finset.range d, n.choose k

The size of the candidate space for the lower-bound certificate: at most $\sum_{k<d}\binom nk$.

This is the visible content of the certificate-complexity statement for the distance decision: the candidate set is a weight-bounded enumeration, not $2^n$, and the enumeration length is exactly given by binomial coefficients (length_lightVecs). For fixed $d$ this is a polynomial of degree $d-1$ in $n$: 121 candidates at $n = 15, d = 3$, against $32768$ for the full space.

theorem QECCertificates.lightSet_card_le {n m₁ m₂ : ℕ} (M₁ : Matrix (Fin m₁) (Fin n) (ZMod 2)) (M₂ : Matrix (Fin m₂) (Fin n) (ZMod 2)) {d : ℕ} (hd : 1 ≤ d) : (lightSet M₁ M₂ d).card ≤ ∑ k ∈ Finset.range d, n.choose k

The same statement in Finset form.

Convenience lemmas for computable membership checks

theorem QECCertificates.mem_ker_of_inKerB {n m : ℕ} (M : Matrix (Fin m) (Fin n) (ZMod 2)) {v : Vec n} (h : inKerB M v = true) : v ∈ (Matrix.toLin' M).ker

Kernel membership from a computable decision.

theorem QECCertificates.not_mem_rowSpace_of_dualCheck {n m : ℕ} (H : Matrix (Fin m) (Fin n) (ZMod 2)) {E w : Vec n} (hk : inKerB H w = true) (hp : w ⬝ᵥ E = 1) : E ∉ H.certificateRowSpace

The dual witness route: w ∈ ker H together with w ⬝ᵥ E = 1 implies E ∉ certificateRowSpace H.

Both assertions are row-by-row pairings, so row reduction is not needed. This route can avoid expensive reduction on wide matrices when a dual witness is available.

theorem QECCertificates.not_mem_rowSpace_of_inSpanB_false {n m : ℕ} (M : Matrix (Fin m) (Fin n) (ZMod 2)) {v : Vec n} (h : inSpanB (List.ofFn fun (i : Fin m) => M i) v = false) : v ∉ M.certificateRowSpace

Non-membership in the row space from the full row-reduction decision procedure.

Note: this lemma runs rowReduce internally and is expensive on wide matrices; for those, use not_mem_rowSpace_of_dualCheck, the dual witness route, instead.