pith. machine review for the scientific record. sign in
def definition def or abbrev

implications

show as:
view Lean formalization →

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)

 234def implications : List String := [

proof body

Definition body.

 235  "Scalable quantum computers",
 236  "Quantum communication over noisy channels",
 237  "Quantum memory for quantum networks",
 238  "Fault-tolerant universal gate sets"
 239]
 240
 241/-! ## Falsification Criteria -/
 242
 243/-- The derivation would be falsified if:
 244    1. QEC doesn't relate to 8-tick structure
 245    2. Error thresholds have no τ₀ connection
 246    3. 8-tick codes perform worse than random -/

depends on (3)

Lean names referenced from this declaration's body.