theorem
proved
wrapper
codeThreshold_pos
No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
33theorem codeThreshold_pos (k : ℕ) : 0 < codeThreshold k :=
proof body
One-line wrapper that applies inv_pos.mpr.
34 inv_pos.mpr (pow_pos phi_pos k)
35
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
-
qecThresholdCert
in IndisputableMonolith.Information.QECThresholdFromPhiLadder
decl_use
depends on (1)
Lean names referenced from this declaration's body.
-
codeThreshold
in IndisputableMonolith.Information.QECThresholdFromPhiLadder
decl_use