qecThresholdAt

formal source

  30noncomputable section
  31
  32/-- QEC threshold at φ-ladder rung `k` below unity (higher rung = lower threshold). -/
  33def qecThresholdAt (k : ℕ) : ℝ := phi ^ (-(k : ℤ)) / 2
  34
  35theorem qecThresholdAt_pos (k : ℕ) : 0 < qecThresholdAt k := by
  36  unfold qecThresholdAt
  37  exact div_pos (zpow_pos Constants.phi_pos _) (by norm_num)
  38
  39theorem qecThresholdAt_succ_ratio (k : ℕ) :
  40    qecThresholdAt (k + 1) = qecThresholdAt k * phi⁻¹ := by
  41  unfold qecThresholdAt
  42  have hphi_ne := Constants.phi_ne_zero
  43  have : phi ^ (-((k : ℤ) + 1)) = phi ^ (-(k : ℤ)) * phi⁻¹ := by
  44    rw [show (-((k : ℤ) + 1)) = -(k : ℤ) + (-1 : ℤ) by ring]
  45    rw [zpow_add₀ hphi_ne]; simp
  46  have hcast : ((k + 1 : ℕ) : ℤ) = (k : ℤ) + 1 := by push_cast; ring
  47  rw [hcast, this]; ring
  48
  49theorem qecThresholdAt_adjacent_ratio (k : ℕ) :
  50    qecThresholdAt (k + 1) / qecThresholdAt k = phi⁻¹ := by
  51  rw [qecThresholdAt_succ_ratio]
  52  field_simp [(qecThresholdAt_pos k).ne']
  53
  54structure QECThresholdCert where
  55  threshold_pos : ∀ k, 0 < qecThresholdAt k
  56  one_step_ratio : ∀ k, qecThresholdAt (k + 1) = qecThresholdAt k * phi⁻¹
  57  adjacent_ratio : ∀ k, qecThresholdAt (k + 1) / qecThresholdAt k = phi⁻¹
  58
  59/-- QEC threshold certificate. -/
  60def qecThresholdCert : QECThresholdCert where
  61  threshold_pos := qecThresholdAt_pos
  62  one_step_ratio := qecThresholdAt_succ_ratio
  63  adjacent_ratio := qecThresholdAt_adjacent_ratio