 109    - n: Block length
 110    - k: Message length
 111    - d: Minimum distance (corrects ⌊(d-1)/2⌋ errors) -/
 112structure ClassicalCode where
 113  n : ℕ  -- Block length
 114  k : ℕ  -- Message length
 115  d : ℕ  -- Minimum distance
 116  k_le_n : k ≤ n
 117  d_pos : d > 0
 118
 119/-- The 3-qubit repetition code.
 120
 121    |0⟩ → |000⟩
 122    |1⟩ → |111⟩
 123
 124    Corrects single bit-flip errors. -/
 125def repetitionCode3 : ClassicalCode := {
 126  n := 3,
 127  k := 1,
 128  d := 3,
 129  k_le_n := by norm_num,
 130  d_pos := by norm_num
 131}
 132
 133/-! ## CSS Codes -/
 134
 135/-- CSS (Calderbank-Shor-Steane) codes are built from two classical codes.
 136
 137    C₁ ⊇ C₂ (C₂ is a subcode of C₁)
 138
 139    - C₁ corrects bit-flip errors
 140    - C₂⊥ corrects phase-flip errors -/
 141structure CSSCode where
 142  c1 : ClassicalCode  -- For bit-flip correction

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.