depolarizing

formal source

  62
  63/-- The depolarizing channel with error probability p.
  64    All errors equally likely. -/
  65noncomputable def depolarizing (p : ℝ) (hp : 0 ≤ p ∧ p ≤ 1) : ErrorModel := {
  66  p_I := 1 - p,
  67  p_X := p / 3,
  68  p_Y := p / 3,
  69  p_Z := p / 3,
  70  nonneg_I := by linarith [hp.right],
  71  nonneg_X := by linarith [hp.left],
  72  nonneg_Y := by linarith [hp.left],
  73  nonneg_Z := by linarith [hp.left],
  74  normalized := by ring
  75}
  76
  77/-! ## The 8-Tick Error Correction Principle -/
  78
  79/-- In RS, the 8-tick phases provide natural error detection:
  80
  81    - Physical qubits are encoded in 8-tick phase patterns
  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.