Proof of Lemma 10, p. 10 — the syndrome σX(e) has weight at most ΔB|e|

Proved

QuantumExpander.Decoder.syndrome_weight_le

by mikedeng1 · Oct 15, 2026 · Mathlib 0df444a (Lean v4.33.1)

decodingp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1quantum-ldpc-codes

Let $G = (A \cup B, \mathcal E)$ be a $(\Delta_A, \Delta_B)$ -biregular bipartite graph with $n_B \le n_A$ . For every $X$ error $e \in \mathbb F_2^{A^2 \cup B^2}$ ,

|\sigma_X(e)| \le \Delta_B\,|e| .

Indeed each qubit $\alpha a$ lies in $\Delta_A$ checks of $H_X$ and each qubit $b\beta$ in $\Delta_B$ checks, and $\Delta_A \le \Delta_B$ because $n_A \Delta_A = n_B \Delta_B$ and $n_B \le n_A$ .

The bound converts the syndrome-weight budget of the decoder into an error-weight budget in the proof of Lemma 10.

Preamble

import Mathlib
import Definitions.Def_CodingTheory
import Definitions.Def_TillichZemor_HGP_Setting
import Definitions.Def_QuantumExpander_Decoder_Setting

Formal statement

namespace QuantumExpander.Decoder

theorem syndrome_weight_le {A B : Type*} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B]
    (adj : A → B → Prop) [∀ a b, Decidable (adj a b)] (ΔA ΔB : ℕ)
    (hbi : IsBiregular adj ΔA ΔB) (hn : Fintype.card B ≤ Fintype.card A)
    (e : Qubit A B → ZMod 2) :
    hammingNorm (sigmaX (bipMatrix adj) e) ≤ ΔB * hammingNorm e := by sorry

end QuantumExpander.Decoder

Source

Leverrier, Tillich and Zémor, Quantum expander codes, arXiv:1504.00822v1, p. 10, proof of Lemma 10, "the syndrome σX(e) has weight at most ΔB|e|"

Human review

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

View graph