pith. machine review for the scientific record. sign in
def

qecThresholdCert

definition
show as:
view math explainer →
module
IndisputableMonolith.Information.QuantumErrorCorrectionThreshold
domain
Information
line
60 · github
papers citing
none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Information.QuantumErrorCorrectionThreshold on GitHub at line 60.

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

  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.