Prove2Me

Sec. IV, p. 3 — the eight syndromes; only 'no error' and 'error in all three channels' coincide

Proved
LoockCVQEC.RepCode.syndrome_table

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

continuous-variablep2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1quantum-error-correctionsyndrome

Let xˉ2>0\bar x_2>0. For a set S⊆{1,2,3}S\subseteq\{1,2,3\} of erring channels let σ(S)∈R2\sigma(S)\in\mathbb R^2 be the displacement of ancilla modes 2 and 3 after decoding, i.e. the last two coordinates of D xˉ21SD\,\bar x_2\mathbf 1_S for the tritter matrix DD. Then

σ(∅)=(0,0),σ({1})=(23 xˉ2,0),σ({2})=(−xˉ26,xˉ22),σ({3})=(−xˉ26,−xˉ22),σ({1,2})=(xˉ26,xˉ22),σ({1,3})=(xˉ26,−xˉ22),σ({2,3})=(−23 xˉ2,0),σ({1,2,3})=(0,0),\begin{aligned}&\sigma(\emptyset)=(0,0),\quad \sigma(\{1\})=\big(\sqrt{\tfrac23}\,\bar x_2,0\big),\quad \sigma(\{2\})=\big(-\tfrac{\bar x_2}{\sqrt6},\tfrac{\bar x_2}{\sqrt2}\big),\quad \sigma(\{3\})=\big(-\tfrac{\bar x_2}{\sqrt6},-\tfrac{\bar x_2}{\sqrt2}\big),\\ &\sigma(\{1,2\})=\big(\tfrac{\bar x_2}{\sqrt6},\tfrac{\bar x_2}{\sqrt2}\big),\quad \sigma(\{1,3\})=\big(\tfrac{\bar x_2}{\sqrt6},-\tfrac{\bar x_2}{\sqrt2}\big),\quad \sigma(\{2,3\})=\big(-\sqrt{\tfrac23}\,\bar x_2,0\big),\quad \sigma(\{1,2,3\})=(0,0),\end{aligned}

with the signs (0,0),(+,0),(−,+),(−,−),(+,+),(+,−),(−,0),(0,0)(0,0),(+,0),(-,+),(-,-),(+,+),(+,-),(-,0),(0,0) the paper lists. Moreover, for all S,TS,T,

σ(S)=σ(T)  ⟺  S=T  or  {S,T}={∅,{1,2,3}}.\sigma(S)=\sigma(T)\iff S=T\ \text{ or }\ \{S,T\}=\{\emptyset,\{1,2,3\}\}.

So the only ambiguity in the syndrome is between no error and an error in every channel; every other pattern, including double errors, is identified.

Formalization Note Channel jj of the paper is Lean index j−1j-1; Finset.univ is {1,2,3}\{1,2,3\}.

Differences from the source:

  • reading: the syndromes are listed by signs only: (0,0), (+,0), (−,+), (−,−), (+,+), (+,−), (−,0), (0,0) → the exact ancilla displacements (last two coordinates of D x̄₂1_S), whose signs are the listed ones for x̄₂ > 0; reason: the values are the ancilla shifts of Eq. (8); they determine the page's signs
  • reading: "the only ambiguity" is all three errors vs no error; "all the other cases … can be identified" → σ(S) = σ(T) ↔ S = T ∨ {S, T} = {∅, univ}; reason: the precise content of the identification claim
  • encoding: modes and channels numbered 1, 2, 3 → Fin 3, Lean index j − 1 for the paper's mode j; reason: Lean convention; same instances
Preamble
import Mathlib
import Definitions.Def_LoockCVQEC_RepCode_Protocol
Formal statement
namespace LoockCVQEC.RepCode

open Real

theorem syndrome_table (d : ℝ) (hd : 0 < d) :
    (syndrome d ∅ = (0, 0)
      ∧ syndrome d {0} = (√(2 / 3) * d, 0)
      ∧ syndrome d {1} = (-(1 / √6 * d), 1 / √2 * d)
      ∧ syndrome d {2} = (-(1 / √6 * d), -(1 / √2 * d))
      ∧ syndrome d {0, 1} = (1 / √6 * d, 1 / √2 * d)
      ∧ syndrome d {0, 2} = (1 / √6 * d, -(1 / √2 * d))
      ∧ syndrome d {1, 2} = (-(√(2 / 3) * d), 0)
      ∧ syndrome d Finset.univ = (0, 0))
    ∧ ∀ S T : Finset (Fin 3), syndrome d S = syndrome d T ↔
        (S = T ∨ (S = ∅ ∧ T = Finset.univ) ∨ (S = Finset.univ ∧ T = ∅)) := by sorry

end LoockCVQEC.RepCode
Source
van Loock, A note on quantum error correction with continuous variables, arXiv:0811.3616v1, p. 3, Sec. IV ("The only ambiguity …", "The syndrome results …")
Human review

  • Endorsed by Shuze Chen · Oct 23, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 23, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph