Documentation

CsdLean4.Empirical.QM.Multipartite.GHZ

Empirical: GHZ paradox (Mermin all-or-nothing form) #

Category: 3-Local (currently placed under CsdLean4/Empirical/Multipartite/ alongside CSD-specific empirical-prediction re-exports). The content itself is QM-generic — no CSD ontology, no OnticSetup / SectorData / singlet machinery — and is promotion-ready to 2-Framework on demand. Extraction to CsdLean4/Framework/QM/ or upstreaming to Mathlib/QuantumMechanics/GHZParadox.lean is deferred until LF4 creates the Framework/ subtree (CONVENTIONS.md §1.Cat-2).

Mermin (1990) form of the Greenberger–Horne–Zeilinger paradox. The three-qubit GHZ state |GHZ⟩ = (|000⟩ + |111⟩) / √2 satisfies four algebraic identities:

⟨GHZ| σ_x ⊗ σ_x ⊗ σ_x |GHZ⟩ = +1
⟨GHZ| σ_x ⊗ σ_y ⊗ σ_y |GHZ⟩ = −1
⟨GHZ| σ_y ⊗ σ_x ⊗ σ_y |GHZ⟩ = −1
⟨GHZ| σ_y ⊗ σ_y ⊗ σ_x |GHZ⟩ = −1

Multiplying the latter three gives −1. Under any local hidden-variable (LHV) model that pre-assigns ±1 values to each wing's σ_x and σ_y measurements, the LHV product simplifies (each value squared is 1) to λ(0,x)² λ(0,y)² λ(1,x)² λ(1,y)² λ(2,x)² λ(2,y)² = +1, contradicting QM's −1.

This is the structural signature of QM non-locality: a single-shot algebraic contradiction, not a statistical violation of an inequality like CHSH. The Lean theorem no_lhv_assignment_for_ghz is False, not a strict inequality.

Sign convention #

|GHZ⟩ = (|000⟩ + |111⟩) / √2 with the LF3 Pauli packing (CsdLean4/LF3/Setup.lean's pauliDot, where (0,0) = a_z, (0,1) = a_x − i a_y, (1,0) = a_x + i a_y, (1,1) = −a_z). For a = (1,0,0) (X-axis, chshA in Bell.lean) and a = (0,1,0) (Y-axis, chshA'), this gives the standard σ_x = [[0,1],[1,0]], σ_y = [[0,−i],[i,0]]. The four Mermin expectations then evaluate as above; see the private example block below for the explicit basis-vector computation that pins each sign.

Experimental provenance #

Caveat on ontic grounding #

These predictions verify CSD-against-QM equivalence on the projective side. Full ontic grounding (Σ as a compact Kähler manifold, μL as the Kähler volume form, the GHZ state as a Dirac concentration on a specific projective ray) is the LF4 §8 obligation. Until then the empirical content is conditional on the CSD ontic axioms supplying the bridge data and the Dirac-concentration preparation.

The GHZ state and its basis components #

source
noncomputable def CSD.Empirical.GHZ.ghzState :
EuclideanSpace ℂ (Fin 2 × Fin 2 × Fin 2)

The three-qubit GHZ state |GHZ⟩ = (|000⟩ + |111⟩) / √2, with (0, 0, 0) and (1, 1, 1) the canonical basis indices in Fin 2 × Fin 2 × Fin 2 matching the LF3 bipartite singlet's (0, 1) = |+−⟩, (1, 0) = |−+⟩ convention.

Equations
Instances For

    Basis evaluations of ghzState #

    The state is nonzero only at (0,0,0) and (1,1,1), each with amplitude 1/√2. The remaining six basis components are zero. These are auxiliary lemmas for the expectation reducer below.

    source
    theorem CSD.Empirical.GHZ.ghz_apply_000 :
    ghzState.ofLp (0, 0, 0) = (↑√2)⁻¹
    source
    theorem CSD.Empirical.GHZ.ghz_apply_001 :
    ghzState.ofLp (0, 0, 1) = 0
    source
    theorem CSD.Empirical.GHZ.ghz_apply_010 :
    ghzState.ofLp (0, 1, 0) = 0
    source
    theorem CSD.Empirical.GHZ.ghz_apply_011 :
    ghzState.ofLp (0, 1, 1) = 0
    source
    theorem CSD.Empirical.GHZ.ghz_apply_100 :
    ghzState.ofLp (1, 0, 0) = 0
    source
    theorem CSD.Empirical.GHZ.ghz_apply_101 :
    ghzState.ofLp (1, 0, 1) = 0
    source
    theorem CSD.Empirical.GHZ.ghz_apply_110 :
    ghzState.ofLp (1, 1, 0) = 0
    source
    theorem CSD.Empirical.GHZ.ghz_apply_111 :
    ghzState.ofLp (1, 1, 1) = (↑√2)⁻¹
    source
    theorem CSD.Empirical.GHZ.ghz_norm :
    ‖ghzState‖ = 1

    The GHZ state is unit-normalised. Both nonzero amplitudes are 1/√2; sum of |1/√2|² + |1/√2|² = 1/2 + 1/2 = 1.

    Tripartite Pauli operators #

    source
    noncomputable def CSD.Empirical.GHZ.sigmaDotTriple (a b c : LF3.DetectorSetting) :
    Matrix (Fin 2 × Fin 2 × Fin 2) (Fin 2 × Fin 2 × Fin 2) ℂ

    The tripartite Pauli operator σ·a ⊗ σ·b ⊗ σ·c on the three-qubit Hilbert space, right-associated as Matrix (Fin 2 × (Fin 2 × Fin 2)) (Fin 2 × (Fin 2 × Fin 2)) ℂ.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem CSD.Empirical.GHZ.sigmaDotTriple_sq (a b c : LF3.DetectorSetting) :
      sigmaDotTriple a b c * sigmaDotTriple a b c = 1

      (σ·a ⊗ σ·b ⊗ σ·c)² = I on three qubits. Each σ·a is its own square root of the identity (pauliDot_sq); the Kronecker product is multiplicative.

      source
      theorem CSD.Empirical.GHZ.sigmaDotTriple_isHermitian (a b c : LF3.DetectorSetting) :
      (sigmaDotTriple a b c).IsHermitian

      The tripartite Pauli operator is Hermitian. Each pauliDot a is Hermitian (pauliDot_isHermitian); Kronecker conjugation distributes.

      GHZ expectation reducer #

      The GHZ analogue of LF3.expectation_formula. For any (Fin 2 × Fin 2 × Fin 2)-indexed matrix M, the expectation ⟨GHZ| M |GHZ⟩ reduces to a half-sum over the four corner entries at (0,0,0) and (1,1,1). Of the 64 = 8 × 8 terms in the double-sum unfolding, 60 vanish (each has a factor of zero from one of the six off-corner basis components); the surviving 4 each factor through (1/√2)² = 1/2.

      source
      theorem CSD.Empirical.GHZ.ghz_expectation_formula (M : Matrix (Fin 2 × Fin 2 × Fin 2) (Fin 2 × Fin 2 × Fin 2) ℂ) :
      inner ℂ ghzState ((Matrix.toEuclideanLin M) ghzState) = 1 / 2 * (M (0, 0, 0) (0, 0, 0) + M (0, 0, 0) (1, 1, 1) + M (1, 1, 1) (0, 0, 0) + M (1, 1, 1) (1, 1, 1))

      The four Mermin expectation theorems #

      chshA = (1, 0, 0) (X-axis) and chshA' = (0, 1, 0) (Y-axis) from Bell.lean. pauliDot chshA = σ_x = [[0,1],[1,0]] and pauliDot chshA' = σ_y = [[0,−i],[i,0]].

      source
      theorem CSD.Empirical.GHZ.ghz_expectation_xxx :
      (inner ℂ ghzState ((Matrix.toEuclideanLin (sigmaDotTriple Bell.chshA Bell.chshA Bell.chshA)) ghzState)).re = 1

      GHZ ⟨XXX⟩ = +1. Mermin 1990 identity #1.

      source
      theorem CSD.Empirical.GHZ.ghz_expectation_xyy :
      (inner ℂ ghzState ((Matrix.toEuclideanLin (sigmaDotTriple Bell.chshA Bell.chshA' Bell.chshA')) ghzState)).re = -1

      GHZ ⟨XYY⟩ = −1. Mermin 1990 identity #2.

      source
      theorem CSD.Empirical.GHZ.ghz_expectation_yxy :
      (inner ℂ ghzState ((Matrix.toEuclideanLin (sigmaDotTriple Bell.chshA' Bell.chshA Bell.chshA')) ghzState)).re = -1

      GHZ ⟨YXY⟩ = −1. Mermin 1990 identity #3.

      source
      theorem CSD.Empirical.GHZ.ghz_expectation_yyx :
      (inner ℂ ghzState ((Matrix.toEuclideanLin (sigmaDotTriple Bell.chshA' Bell.chshA' Bell.chshA)) ghzState)).re = -1

      GHZ ⟨YYX⟩ = −1. Mermin 1990 identity #4.

      LHV impossibility (Mermin all-or-nothing) #

      source
      inductive CSD.Empirical.GHZ.PauliAxis :
      Type

      Two-element type indexing the X and Y measurement axes.

      Instances For
        source
        @[instance_reducible]
        instance CSD.Empirical.GHZ.instDecidableEqPauliAxis :
        DecidableEq PauliAxis
        Equations
        source
        theorem CSD.Empirical.GHZ.no_lhv_assignment_for_ghz :
        ¬∃ (lambda : Fin 3 → PauliAxis → ℤ), (∀ (i : Fin 3) (ax : PauliAxis), lambda i ax = 1 ∨ lambda i ax = -1) ∧ lambda 0 PauliAxis.x * lambda 1 PauliAxis.x * lambda 2 PauliAxis.x = 1 ∧ lambda 0 PauliAxis.x * lambda 1 PauliAxis.y * lambda 2 PauliAxis.y = -1 ∧ lambda 0 PauliAxis.y * lambda 1 PauliAxis.x * lambda 2 PauliAxis.y = -1 ∧ lambda 0 PauliAxis.y * lambda 1 PauliAxis.y * lambda 2 PauliAxis.x = -1

        No LHV ±1 assignment satisfies the four Mermin product constraints simultaneously.

        Under any local hidden-variable model that pre-assigns ±1 ∈ ℤ values to each of the six measurement settings (wing ∈ Fin 3) × (axis ∈ {x, y}), the product λ(0,x)·λ(1,x)·λ(2,x) must equal QM's +1 from ghz_expectation_xxx, while the three products λ(0,x)·λ(1,y)·λ(2,y), λ(0,y)·λ(1,x)·λ(2,y), λ(0,y)·λ(1,y)·λ(2,x) must each equal −1 from the XYY, YXY, YYX expectations.

        Multiplying all four product constraints: the LHS factors into λ(0,x)² · λ(0,y)² · λ(1,x)² · λ(1,y)² · λ(2,x)² · λ(2,y)², which is 1 (each squared ±1 value is 1). The RHS is (+1)·(−1)·(−1)·(−1) = −1. Contradiction.

        This is the structural (single-shot, algebraic) signature of QM non-locality, distinct from CHSH's statistical inequality violation: the conclusion is False, not a strict inequality.

        Experimental verification: Pan, Bouwmeester, Daniell, Weinfurter, Zeilinger 2000, Nature 403, 515.