Dual-witness certificates and the exact-distance pair of theorems

Certifying a code distance is two-sided. The lower bound says that no lighter logical operator exists, which calls for enumeration or reduction over low-weight operators; the upper bound says that here is one, which needs only a concrete artefact. This module turns the upper-bound side into an independently checkable certificate and joins it with the LeanQEC distance definition into a closed assertion that the distance is exactly $d$.

Dual witnesses

To prove that an operator E is not in the parity-check row space one need not enumerate: it suffices to exhibit a vector w that commutes with every check and anticommutes with E, that is w ∈ ker H and w ⬝ᵥ E = 1.

This is a certificate-shaped wrapper around LeanQEC's not_mem_rowspace_iff_exists_mem_ker: the certificate has two entries and each is checkable on its own, and completeness (E ∉ certificateRowSpace implies such a w exists) is given by that theorem.

The two-matrix form

The table below (M₁ supplies the kernel and M₂ the row space) covers all three classes of code in this package:

Code class	M₁	M₂	weight =
classical linear code	the parity-check matrix H	the empty matrix	weight of a nonzero

codeword |

| CSS code | one side's checks | the other side's checks | weight of an X-type or Z-type logical operator | | general stabilizer code | the symplectic transpose of the generators | the generators themselves | Pauli weight (the two halves together) |

The last class works because the symplectic inner product is ⟨g, v⟩ = (J g) ⬝ᵥ v (the matrix J swaps the Z half with the X half), so commuting with all generators is the same as lying in the row orthogonal complement of J, that is, in ker J.

Main results

• DualWitness: the dual-witness certificate structure, with DualWitness.not_mem_rowSpace as the conclusion the kernel checks.
• exists_dualWitness_iff: the certificate is complete: E ∉ certificateRowSpace is equivalent to the existence of a dual witness.
• minWeight_le_of_witness: the upper-bound theorem: one concrete artefact gives an upper bound on the code distance.
• le_minWeight_of_lower: the lower-bound theorem: a per-operator lower bound gives a lower bound on the code distance.
• eq_minWeight_of_bounds: the exact distance: the two sides together give a distance exactly equal to $d$.

Dual witnesses

structure QECCertificates.DualWitness {n m : ℕ} (H : Matrix (Fin m) (Fin n) (ZMod 2)) (E : Vec n) : Type

Dual witness: orthogonal to (commuting with) every row of the parity-check matrix H, while pairing to 1 with E.

Two entries, each checkable on its own: the first says that it commutes with every check and the second that it anticommutes with E. Together they prove that E is not an element of the stabilizer group, which is the smallest certificate for the judgement that E is a logical operator.

• w : Vec n

  The witness vector.

• mem_ker : self.w ∈ (Matrix.toLin' H).ker

  Orthogonal to every check row.

• pairing : self.w ⬝ᵥ E = 1

  Pairs to 1 with the target operator (that is, anticommutes over GF(2)).

theorem QECCertificates.DualWitness.not_mem_rowSpace {n m : ℕ} {H : Matrix (Fin m) (Fin n) (ZMod 2)} {E : Vec n} (hw : DualWitness H E) : E ∉ H.certificateRowSpace

Certificate soundness: holding a dual witness proves that E is not in the parity-check row space, hence that it is a logical operator.

theorem QECCertificates.exists_dualWitness_iff {n m : ℕ} (H : Matrix (Fin m) (Fin n) (ZMod 2)) (E : Vec n) : (∃ (x : DualWitness H E), True) ↔ E ∉ H.certificateRowSpace

Certificate completeness: E is not in the row space if and only if a dual witness exists.

Completeness is LeanQEC's not_mem_rowspace_iff_exists_mem_ker; this package wraps its existential output in the shape of a checkable certificate.

The two-sided characterization of the code distance

@[reducible]

def QECCertificates.undetectableSet {n m₁ m₂ : ℕ} (M₁ : Matrix (Fin m₁) (Fin n) (ZMod 2)) (M₂ : Matrix (Fin m₂) (Fin n) (ZMod 2)) : Set (Vec n)

The set of undetectable nontrivial operators: orthogonal to every row of M₁ but not an element of the row space of M₂.

ker M₁ \ certificateRowSpace M₂ is exactly the space of logical operators modulo stabilizers: operators that are not detected and are yet not elements of the stabilizer group, so they really do flip the logic. The @[reducible] marker lets instance search unfold this definition for the Set.toFinset uses below.

Equations

• QECCertificates.undetectableSet M₁ M₂ = ↑(Matrix.toLin' M₁).ker \ ↑M₂.certificateRowSpace

@[reducible, inline]

noncomputable abbrev QECCertificates.codeDistance {n m : ℕ} (H : Matrix (Fin m) (Fin n) (ZMod 2)) : ℕ

The code distance: LeanQEC's minWeightKernelOutsideRowSpace (the least weight of an undetectable nontrivial operator, taking the value n + 1 when the set is empty), specialized to the diagonal case in which the parity-check matrix and the row space are one and the same.

It is literally the same as the upstream definition, so the conclusions of this module feed straight back into the LeanQEC distance reduction chain. For the general two-matrix case, use minWeightKernelOutsideRowSpace directly.

Equations

• QECCertificates.codeDistance H = QECCertificates.minWeightKernelOutsideRowSpace H H

theorem QECCertificates.mem_image_hammingNorm_of_witness {n m₁ m₂ : ℕ} (M₁ : Matrix (Fin m₁) (Fin n) (ZMod 2)) (M₂ : Matrix (Fin m₂) (Fin n) (ZMod 2)) {E : Vec n} {d₀ : ℕ} (hker : E ∈ (Matrix.toLin' M₁).ker) (hnot : E ∉ M₂.certificateRowSpace) (hw : hammingNorm E = d₀) : d₀ ∈ Finset.image hammingNorm (undetectableSet M₁ M₂).toFinset

An undetectable nontrivial operator of weight d₀ puts d₀ among the values over which the minimum is taken.

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

The upper-bound theorem: if an undetectable nontrivial operator of weight d₀ exists, then the code distance is at most d₀.

This is the witness upper bound: the certificate is a concrete low-weight logical operator, and the kernel only has to check the three assertions E ∈ ker M₁, E ∉ certificateRowSpace M₂ and hammingNorm E = d₀.

theorem QECCertificates.le_minWeight_of_lower {n m₁ m₂ : ℕ} (M₁ : Matrix (Fin m₁) (Fin n) (ZMod 2)) (M₂ : Matrix (Fin m₂) (Fin n) (ZMod 2)) {d₀ : ℕ} (hd : d₀ ≤ n) (h : ∀ E ∈ (Matrix.toLin' M₁).ker, E ∉ M₂.certificateRowSpace → d₀ ≤ hammingNorm E) : d₀ ≤ minWeightKernelOutsideRowSpace M₁ M₂

The lower-bound theorem: if every undetectable nontrivial operator has weight at least d₀, then the code distance is at least d₀.

The lower-bound side admits no short certificate unless there is a structural argument, which is why LeanQEC reduces to SAT and UNSAT; this theorem provides the common interface at which a lower-bound result and an upper-bound witness meet. For a computable certificate on the lower-bound side see QECCertificates.GF2.LowerBound.

theorem QECCertificates.eq_minWeight_of_bounds {n m₁ m₂ : ℕ} (M₁ : Matrix (Fin m₁) (Fin n) (ZMod 2)) (M₂ : Matrix (Fin m₂) (Fin n) (ZMod 2)) {d₀ : ℕ} (hd : d₀ ≤ n) {E : Vec n} (hker : E ∈ (Matrix.toLin' M₁).ker) (hnot : E ∉ M₂.certificateRowSpace) (hw : hammingNorm E = d₀) (hlower : ∀ F ∈ (Matrix.toLin' M₁).ker, F ∉ M₂.certificateRowSpace → d₀ ≤ hammingNorm F) : minWeightKernelOutsideRowSpace M₁ M₂ = d₀

The exact distance (the two sides together): equal lower and upper bounds give a distance exactly equal to $d$.

This is the formal skeleton of an exact-distance assertion: the lower bound is proved in the kernel (or reduced through SAT and LRAT) and the upper bound is supplied by a concrete low-weight logical operator.