`MeasurementAngle`

definition

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Quantum.BellInequality on GitHub at line 44.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  41/-! ## Measurement Settings -/
  42
  43/-- A measurement direction (simplified to an angle). -/
  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.

papers checked against this theorem

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