Observables in LCS Games

This module defines the algebraic properties of quantum observables in the context of Linear Constraint System (LCS) games. An observable is represented as a self-adjoint, involutive operator.

Key Definitions

• IsObservable: A property of an element $O$ in a star-ring if $O^2=1$ and $O^\dagger=O$.
• observableOfMeasurementSystem: Constructs an observable from a binary projector measurement $P$ as $O = P_0 - P_1$.

Key Lemmas

• isObservable_observableOfMeasurementSystem: Verifies that the difference of projectors in a binary measurement forms a valid observable.

structure MIPRE.LCS.IsObservable {R : Type u_1} [Ring R] [StarRing R] (O : R) : Prop

A binary observable in a star-ring: a self-adjoint involution.

• involutive : O * O = 1

  The observable squares to one.

• self_adjoint : star O = O

  The observable is self-adjoint.

def MIPRE.LCS.observableOfMeasurementSystem {R : Type u_1} [Ring R] (f : ZMod 2 → R) : R

The ±1-observable P₀ - P₁ associated with a binary measurement.

Equations

• MIPRE.LCS.observableOfMeasurementSystem f = f 0 - f 1

theorem MIPRE.LCS.isObservable_observableOfMeasurementSystem {R : Type u_1} [Ring R] [StarRing R] (f : ZMod 2 → R) (h : IsMeasurementSystem f) : IsObservable (observableOfMeasurementSystem f)

theorem MIPRE.LCS.binary_measurement_eq_projector {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] (f : ZMod 2 → R) (h : IsMeasurementSystem f) (y : ZMod 2) : f y = (1 / 2) • (1 + (-1) ^ y.val • observableOfMeasurementSystem f)