module module

`IndisputableMonolith.Quantum.NonlocalityNoSignaling`

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

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (17)

structure EPRPair L38
structure Measurement L49
def quantumCorrelation L68
def chshBound L72
def tsirelsonBound L75
theorem bell_violation L78
theorem no_signaling_theorem L98
theorem reduced_density_unchanged L108
theorem ledger_explains_nonlocality L126
structure SharedLedgerEntry L136
theorem reading_is_local L148
def no_signaling_reasons L161
def mutualInformationProperties L176
theorem relativity_preserved L192
def experimentalTests L207
def implications L225
structure NonlocalityFalsifier L238