theorem proved term proof

`recognitionQuantum_pos`

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

formal statement (Lean)

  34theorem recognitionQuantum_pos : 0 < recognitionQuantum := by

Term-mode proof.

  35  unfold recognitionQuantum; linarith [phi_gt_onePointFive]
  36
  37/-- RS prediction for surface code threshold: J(φ) / 10. -/

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

surfaceCodeThreshold_pos in IndisputableMonolith.QuantumComputing.ErrorCorrectionThresholdFromJCost decl_use

Lean names referenced from this declaration's body.

phi_gt_onePointFive in IndisputableMonolith.Constants decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
recognitionQuantum in IndisputableMonolith.QuantumComputing.ErrorCorrectionThresholdFromJCost decl_use