pith. machine review for the scientific record. sign in
def definition def or abbrev

depolarizing

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  65noncomputable def depolarizing (p : ℝ) (hp : 0 ≤ p ∧ p ≤ 1) : ErrorModel := {

proof body

Definition body.

  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 -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (12)

Lean names referenced from this declaration's body.