`Outcome`

definition

show as: view math explainer →

module: IndisputableMonolith.Quantum.BellInequality
domain: Quantum
line: 47 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Quantum.BellInequality on GitHub at line 47.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  44abbrev MeasurementAngle := ℝ
  45
  46/-- A measurement outcome (+1 or -1). -/
  47inductive Outcome where
  48  | plus : Outcome
  49  | minus : Outcome
  50deriving DecidableEq, Repr
  51
  52/-- Convert outcome to numerical value. -/
  53def Outcome.toReal : Outcome → ℝ
  54  | Outcome.plus => 1
  55  | Outcome.minus => -1
  56
  57/-! ## Entangled State -/
  58
  59/-- A Bell pair (maximally entangled two-qubit state). -/
  60structure BellPair where
  61  /-- Identifier for this entangled pair. -/
  62  id : ℕ
  63  /-- The shared ledger entry (abstract). -/
  64  sharedEntry : True
  65  /-- Correlation type (singlet, triplet, etc.). -/
  66  correlationType : String
  67
  68/-- Create a singlet Bell pair: |ψ⟩ = (|01⟩ - |10⟩)/√2 -/
  69def singlet (id : ℕ) : BellPair :=
  70  ⟨id, trivial, "singlet"⟩
  71
  72/-! ## Quantum Correlations -/
  73
  74/-- Quantum correlation function for singlet state.
  75    E(a,b) = -cos(a - b) -/
  76noncomputable def quantumCorrelation (a b : MeasurementAngle) : ℝ :=
  77  -Real.cos (a - b)

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.