`QECThresholdCert`

definition

show as: view math explainer →

module: IndisputableMonolith.Information.QuantumErrorCorrectionThreshold
domain: Information
line: 54 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Information.QuantumErrorCorrectionThreshold on GitHub at line 54.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.