repetitionCode3

formal source

 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
 143  c2 : ClassicalCode  -- For phase-flip correction (via dual)
 144  containment : c2.k ≤ c1.k  -- C₂ ⊆ C₁
 145
 146/-- The Steane [[7,1,3]] code.
 147
 148    Based on the [7,4,3] Hamming code.
 149    Encodes 1 logical qubit in 7 physical qubits.
 150    Corrects any single-qubit error. -/
 151def steaneCode : CSSCode := {
 152  c1 := { n := 7, k := 4, d := 3, k_le_n := by norm_num, d_pos := by norm_num },
 153  c2 := { n := 7, k := 3, d := 4, k_le_n := by norm_num, d_pos := by norm_num },
 154  containment := by norm_num
 155}