qecThresholdAt_adjacent_ratio

formal source

  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
  64
  65end
  66end QuantumErrorCorrectionThreshold
  67end Information
  68end IndisputableMonolith