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)

 225def implications : List String := [

proof body

Definition body.

 226  "Quantum cryptography is possible (BB84, E91)",
 227  "Entanglement is a resource (cannot be cloned or shared)",
 228  "Causality structure is fundamental",
 229  "Information and physics are intertwined"
 230]
 231
 232/-! ## Falsification Criteria -/
 233
 234/-- The derivation would be falsified if:
 235    1. Faster-than-light signaling is demonstrated
 236    2. Bell inequality is satisfied (no nonlocality)
 237    3. Quantum correlations violate Tsirelson bound -/

depends on (6)

Lean names referenced from this declaration's body.