structure
definition
BellFalsifier
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Quantum.BellInequality on GitHub at line 223.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
all -
all -
of -
status -
all -
has -
of -
of -
of -
of -
status -
Status -
all -
falsification -
experiments -
experiments -
experiments -
experiments
used by
formal source
220 2. Discovery of local hidden variables
221 3. Superluminal signaling using entanglement
222 4. Violation of Tsirelson bound (would falsify QM) -/
223structure BellFalsifier where
224 /-- Type of claimed violation. -/
225 claim : String
226 /-- Status. -/
227 status : String
228
229/-- No falsification has occurred; all experiments confirm quantum prediction. -/
230def experimentalStatus : List BellFalsifier := [
231 ⟨"Local hidden variables", "Ruled out at >100σ"⟩,
232 ⟨"FTL signaling", "Never observed"⟩,
233 ⟨"Tsirelson violation", "Never observed"⟩
234]
235
236end BellInequality
237end Quantum
238end IndisputableMonolith