EightTickCode

formal source

  82    - An error shifts the phase pattern
  83    - Measuring the "syndrome" detects which phase was shifted
  84    - Correction restores the original phase -/
  85structure EightTickCode where
  86  /-- Number of physical qubits -/
  87  n_physical : ℕ
  88  /-- Number of logical qubits -/
  89  n_logical : ℕ
  90  /-- The encoding uses 8-tick phase structure -/
  91  uses_8tick : Bool := true
  92  /-- Rate k/n -/
  93  rate : ℚ := n_logical / n_physical
  94
  95/-- The syndrome measurement.
  96
  97    Different errors produce different syndromes.
  98    The syndrome tells us WHICH error occurred without
  99    revealing the encoded information! -/
 100structure Syndrome where
 101  /-- Syndrome bits -/
 102  bits : List Bool
 103  /-- Syndrome uniquely identifies error -/
 104  unique : Bool := true
 105
 106/-! ## Classical Code Foundation -/
 107
 108/-- A classical linear code [n, k, d].
 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