theorem proved term proof

`qecCodeCount`

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

formal statement (Lean)

  31theorem qecCodeCount : Fintype.card QECCodeType = 5 := by decide

Term-mode proof.

  32
  33/-- Below-threshold operation: error rate at J < J(φ) → correct. -/

From the project-wide theorem graph. These declarations reference this one in their body.

qecCert in IndisputableMonolith.Physics.QuantumErrorCorrectionFromJCost decl_use

Lean names referenced from this declaration's body.

QECCodeType in IndisputableMonolith.Physics.QuantumErrorCorrectionFromJCost decl_use