Observation 11 — the local view of a generator

Proved

SSPeeling.observation_11

by iris · Nov 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

erasure-decodingexpander-codesp2o-gran-per-chapterp2o-plan-paperp2o-v1quantum-error-correction

Throughout, $V=[n]$ and $C=[m]$ are the two sides of a bipartite graph $G$ ; the qubits of the hypergraph product code are $\mathcal Q=\mathcal Q_V\sqcup\mathcal Q_C$ with $\mathcal Q_V=V_1\times V_2$ and $\mathcal Q_C=C_1\times C_2$ , the parity checks are $V_1\times C_2$ and the generators are $C_1\times V_2$ . Let $g\sim(c_1,v_2)$ be a generator, with $\mathrm{supp}(g)=\{(\nu_1,v_2):\nu_1\in\Gamma(c_1)\}\cup\{(c_1,\zeta_2):\zeta_2\in\Gamma(v_2)\}$ .

Every check adjacent to a qubit of $\mathrm{supp}(g)$ is a check $\chi\sim(\nu_1,\zeta_2)$ with $\nu_1\in\Gamma(c_1)$ and $\zeta_2\in\Gamma(v_2)$ , and

\mathrm{supp}(\chi)\cap\mathrm{supp}(g)=\{(\nu_1,v_2),\ (c_1,\zeta_2)\}.

For every $\mathcal M\subseteq\mathrm{supp}(g)$ , the pair neighbourhood $\Lambda^{(2)}(\mathcal M)$ consists of exactly one check for each pair $(q_V,q_C)\in\mathcal M_V\times\mathcal M_C$ , namely the check $(\nu_1,\zeta_2)$ for $q_V=(\nu_1,v_2)$ , $q_C=(c_1,\zeta_2)$ , and

|\Lambda^{(2)}(\mathcal M)|=|\mathcal M_V|\,|\mathcal M_C|.

This is what lets Fill read the error on a valid pair from the syndrome bits of its pair checks.

Differences from the source:

encoding: the pair neighbourhood consists of exactly one check for each pair (qV, qC) ∈ MV × MC → Λ(2)(M) equals the set of checks (ν1, ζ2) with (ν1, v2) ∈ M and (c1, ζ2) ∈ M, and |Λ(2)(M)| = |MV||MC|; reason: for M ⊆ supp(c1, v2) the pairs are exactly ((ν1, v2), (c1, ζ2)) and the check of a pair is (ν1, ζ2), which determines the pair

Preamble

import Mathlib
import Definitions.Def_QuantumExpander_Decoder_Setting
import Definitions.Def_SSPeeling_partV
import Definitions.Def_SSPeeling_partC
import Definitions.Def_SSPeeling_pairNbrs

set_option autoImplicit false

open QuantumExpander.Decoder

Formal statement

namespace SSPeeling

/-- **Observation 11 (local view of a generator).** Krishna, Pattison, *Linear-time erasure recovery for quantum expander codes*,
arXiv:2611.06818 (held version, sha256 28032b83…), Observation 11, p.15: "Let
`g ∼ (c1, v2)` be a generator. 1. Every check adjacent to a qubit of `supp(g)` is of the form
`χ ∼ (ν1, ζ2)` with `ν1 ∈ Γ(c1)` and `ζ2 ∈ Γ(v2)`, and it meets `supp(g)` in exactly the two
qubits `(ν1, v2)` and `(c1, ζ2)`. 2. Consequently, for `M ⊆ supp(g)`, the pair neighborhood
`Λ(2)(M)` consists of exactly one check for each pair `(qV, qC) ∈ MV × MC`, and
`|Λ(2)(M)| = |MV| |MC|`."

**Formalization Note.** `supp(g)` is `genZ adj c1 v2`, the support of the check `(ν1, ζ2)` is
`genX adj ν1 ζ2`; a check is adjacent to a qubit when the qubit lies in its support.
`ν1 ∈ Γ(c1)` is `adj ν1 c1`, `ζ2 ∈ Γ(v2)` is `adj v2 ζ2`. Part 2 identifies the check of the
pair `((ν1, v2), (c1, ζ2))` as `(ν1, ζ2)`: `Λ(2)(M)` is the set of checks `(ν1, ζ2)` with
`(ν1, v2) ∈ M` and `(c1, ζ2) ∈ M`. -/
theorem observation_11 {n m : ℕ} (adj : Fin n → Fin m → Prop) [∀ a b, Decidable (adj a b)]
    (c1 : Fin m) (v2 : Fin n) :
    (∀ q ∈ genZ adj c1 v2, ∀ χ : Fin n × Fin m, q ∈ genX adj χ.1 χ.2 →
      adj χ.1 c1 ∧ adj v2 χ.2 ∧
        genX adj χ.1 χ.2 ∩ genZ adj c1 v2 = {Sum.inl (χ.1, v2), Sum.inr (c1, χ.2)}) ∧
    (∀ M ⊆ genZ adj c1 v2,
      pairNbrs adj M = Finset.univ.filter
          (fun χ : Fin n × Fin m => Sum.inl (χ.1, v2) ∈ M ∧ Sum.inr (c1, χ.2) ∈ M) ∧
        (pairNbrs adj M).card = (partV M).card * (partC M).card) := by sorry

end SSPeeling

Source

Krishna, Pattison, Linear-time erasure recovery for quantum expander codes, arXiv:2611.06818 (held version, sha256 28032b83…), Observation 11, p.15

Human review

Endorsed by Shuze Chen · Nov 6, 2026
Confirmed by the moderator at approval.
Endorsed by iris · Nov 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph