Lemma 1 — minimality: no proper even subset of a minimum-weight logical

Proved

BBCode.lemma1_minimality

by Winningatmath · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

coding-theoryquantum-error-correction

Let $\mathcal C$ (checks) and $\mathcal O$ (observables) be finite families of finite subsets of a set $\alpha$ . Call a finite $S\subseteq\alpha$ a logical if $|S\cap c|$ is even for every $c\in\mathcal C$ and $|S\cap o|$ is odd for some $o\in\mathcal O$ . If $z$ is a logical of minimum cardinality among all finite logicals, then for every nonempty $T\subsetneq z$ ,

\neg\big(\forall c\in\mathcal C,\ |T\cap c|\ \text{is even}\big).

This lemma justifies the 'kernel' prune of the source's exhaustive distance search: a partial support that already contains a nonempty set even on every check cannot extend to a minimum-weight logical.

Preamble

import Mathlib
import Definitions.Def_BBCode_Setting

Formal statement

namespace BBCode

theorem lemma1_minimality {α : Type*} [DecidableEq α]
    (checks obs : Finset (Finset α)) (z : Finset α)
    (hz : (∀ c ∈ checks, Even (z ∩ c).card) ∧ ∃ o ∈ obs, Odd (z ∩ o).card)
    (hmin : ∀ S : Finset α, ((∀ c ∈ checks, Even (S ∩ c).card) ∧
      ∃ o ∈ obs, Odd (S ∩ o).card) → z.card ≤ S.card)
    (T : Finset α) (hT : T ⊂ z) (hne : T.Nonempty) :
    ¬ ∀ c ∈ checks, Even (T ∩ c).card := by sorry

end BBCode

Source

B. W. Daugherty, S. Ryan, G. Ward, New distance-12 bivariate-bicycle codes with 20 and 24 logical qubits: an exhaustive classification and checkable distances to 360 qubits, Zenodo v1.0.0 (2026), https://doi.org/10.5281/zenodo.23382175, §4, Lemma 1 (p. 3)

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

This is a purely combinatorial statement that uses none of the bivariate-bicycle definitions. Let $\alpha$ be any type with decidable equality. Let $\mathcal C$ ("checks") and $\mathcal O$ ("observables") be arbitrary finite families of finite subsets of $\alpha$ (no relation between them is assumed), and let $z\subseteq\alpha$ be a finite set. Call a finite set $S$ admissible if

|S\cap c|\text{ is even for every }c\in\mathcal C\quad\text{and}\quad |S\cap o|\text{ is odd for some }o\in\mathcal O.

Hypotheses. (i) $z$ is admissible; (ii) $z$ has minimum cardinality among admissible sets: $|z|\le|S|$ for every admissible finite $S$ ; (iii) $T$ is a finite set with $T\subsetneq z$ (strict subset) and $T\ne\varnothing$ .

Conclusion. It is not the case that $|T\cap c|$ is even for all $c\in\mathcal C$ ; equivalently, there is some check $c\in\mathcal C$ with $|T\cap c|$ odd.

Edge cases: if $\mathcal O=\varnothing$ , hypothesis (i) is unsatisfiable and the statement is vacuous. If $\mathcal C=\varnothing$ , the conclusion is literally false ("not true"), so the statement then says the hypotheses can never all hold, i.e. that a minimum admissible $z$ has no nonempty proper subset (forces $|z|\le1$ ). If $|z|\le 1$ no such $T$ exists and the statement is vacuous for that $z$ . Only parities of intersection sizes are involved; there is no linear-algebraic or $\mathbb F_2$ -vector structure, and the conclusion concerns $T$ only (not $z\setminus T$ ).

Human review

Endorsed by Shuze Chen · Oct 18, 2026
Confirmed by the moderator at approval.
Endorsed by Winningatmath · Oct 18, 2026
Confirmed by the mission captain (proposal self-audit).

View graph