ErrorModel

formal source

  49deriving Repr, DecidableEq
  50
  51/-- Probability distribution over Pauli errors. -/
  52structure ErrorModel where
  53  p_I : ℝ  -- Probability of no error
  54  p_X : ℝ  -- Probability of bit flip
  55  p_Y : ℝ  -- Probability of Y error
  56  p_Z : ℝ  -- Probability of phase flip
  57  nonneg_I : p_I ≥ 0
  58  nonneg_X : p_X ≥ 0
  59  nonneg_Y : p_Y ≥ 0
  60  nonneg_Z : p_Z ≥ 0
  61  normalized : p_I + p_X + p_Y + p_Z = 1
  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