def definition def or abbrev

`qecCert`

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

formal statement (Lean)

  50def qecCert : QECCert where
  51  five_codes := qecCodeCount

proof body

Definition body.

  52  threshold_zero := below_threshold_correct
  53  error_positive := logical_error_positive
  54  dft8_count := dft8_eq_8
  55
  56end IndisputableMonolith.Physics.QuantumErrorCorrectionFromJCost

depends on (6)

Lean names referenced from this declaration's body.

dft8_eq_8 in IndisputableMonolith.Mathematics.FourierAnalysisFromRS decl_use
below_threshold_correct in IndisputableMonolith.Physics.QuantumErrorCorrectionFromJCost decl_use
dft8_eq_8 in IndisputableMonolith.Physics.QuantumErrorCorrectionFromJCost decl_use
logical_error_positive in IndisputableMonolith.Physics.QuantumErrorCorrectionFromJCost decl_use
QECCert in IndisputableMonolith.Physics.QuantumErrorCorrectionFromJCost decl_use
qecCodeCount in IndisputableMonolith.Physics.QuantumErrorCorrectionFromJCost decl_use