Documentation

CsdLean4.Empirical.QM.LeggettGarg

Empirical/QM/LeggettGarg: the Leggett–Garg inequality and its quantum violation #

The Leggett–Garg inequality (LGI) is the temporal analogue of CHSH: a test of macrorealism using a single dichotomic observable Q(t) ∈ {±1} measured at three times. Any macrorealist model (definite values + non-invasive measurability) obeys the K₃ bound

K₃ := ⟨Q₁Q₂⟩ + ⟨Q₂Q₃⟩ − ⟨Q₁Q₃⟩ ≤ 1.

Quantum mechanics violates it. For a two-level system with Q = σ_z precessing under e^{-iΔσ_x} (the QuantumZeno.zenoU rotation), the Born two-time correlation is ⟨QᵢQⱼ⟩ = cos(2Δ_{ij}), giving K₃(Δ) = 2cos(2Δ) − cos(4Δ), which peaks at the Lüders bound 3/2 at Δ = π/6 — well above the macrorealist 1.

Results (all foundational-triple, no sorry):

Experimental verification: Palacios-Laloy et al. 2010 (superconducting qubit); Knee et al. 2012; many since. CSD note: the macrorealist "non-invasive measurability" assumption is exactly what the record layer / de-isolation reading denies — an intermediate measurement forms a record (de-isolates), so CSD is realist yet LG-violating, consistent with QM.

References #

Empirical/CSD/QuantumZeno.lean (zenoU, the qubit rotation + Born machinery); Empirical/QM/Bell.lean / Empirical/QM/Crypto/E91.lean (the CHSH analogue + LHV bound pattern).

Part 1 — the macrorealist (classical) bound K₃ ≤ 1 #

source
theorem CSD.Empirical.QM.LeggettGarg.lg_pointwise {q₁ q₂ q₃ : ℝ} (h₁ : q₁ = 1 ∨ q₁ = -1) (h₂ : q₂ = 1 ∨ q₂ = -1) (h₃ : q₃ = 1 ∨ q₃ = -1) :
q₁ * q₂ + q₂ * q₃ - q₁ * q₃ ≤ 1

Pointwise Leggett–Garg: for q₁, q₂, q₃ ∈ {±1}, q₁q₂ + q₂q₃ − q₁q₃ ≤ 1.

source
theorem CSD.Empirical.QM.LeggettGarg.lg_macrorealist_bound {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Q₁ Q₂ Q₃ : Ω → ℝ) (h₁ : ∀ (ω : Ω), Q₁ ω = 1 ∨ Q₁ ω = -1) (h₂ : ∀ (ω : Ω), Q₂ ω = 1 ∨ Q₂ ω = -1) (h₃ : ∀ (ω : Ω), Q₃ ω = 1 ∨ Q₃ ω = -1) (i₁₂ : MeasureTheory.Integrable (fun (ω : Ω) => Q₁ ω * Q₂ ω) μ) (i₂₃ : MeasureTheory.Integrable (fun (ω : Ω) => Q₂ ω * Q₃ ω) μ) (i₁₃ : MeasureTheory.Integrable (fun (ω : Ω) => Q₁ ω * Q₃ ω) μ) :
∫ (ω : Ω), Q₁ ω * Q₂ ω ∂μ + ∫ (ω : Ω), Q₂ ω * Q₃ ω ∂μ - ∫ (ω : Ω), Q₁ ω * Q₃ ω ∂μ ≤ 1

The macrorealist Leggett–Garg bound K₃ ≤ 1. For any macrorealist model — a probability space carrying three dichotomic ±1 observables Q₁, Q₂, Q₃ — the temporal combination ⟨Q₁Q₂⟩ + ⟨Q₂Q₃⟩ − ⟨Q₁Q₃⟩ ≤ 1. A genuine measure-theoretic hidden-variable bound (the temporal analogue of the CHSH LHV bound), proved from the pointwise inequality by integral monotonicity.

Part 2 — the quantum two-time correlation (Born + qubit precession) #

source
def CSD.Empirical.QM.LeggettGarg.sgn :
Fin 2 → ℝ

σ_z eigenvalue of the computational basis state i: +1 for |0⟩, −1 for |1⟩.

Equations
Instances For
    source
    noncomputable def CSD.Empirical.QM.LeggettGarg.bornTP (Δ : ℝ) (s t : Fin 2) :
    ℝ

    Born transition probability |⟨e_t, e^{-iΔσ_x} e_s⟩|² between σ_z-eigenstates under precession by Δ (zenoU Δ).

    Equations
    Instances For
      source
      theorem CSD.Empirical.QM.LeggettGarg.inner_single_zenoU (Δ : ℝ) (s t : Fin 2) :
      inner ℂ (EuclideanSpace.single t 1) ((Matrix.toEuclideanLin (CSDBridge.QuantumZeno.zenoU Δ)) (EuclideanSpace.single s 1)) = CSDBridge.QuantumZeno.zenoU Δ t s

      The Born transition amplitude is the matrix entry: ⟨e_t, zenoU Δ · e_s⟩ = (zenoU Δ) t s.

      source
      theorem CSD.Empirical.QM.LeggettGarg.bornTP_eq (Δ : ℝ) (s t : Fin 2) :
      bornTP Δ s t = ‖CSDBridge.QuantumZeno.zenoU Δ t s‖ ^ 2

      The Born transition probability is |matrix entry|².

      source
      noncomputable def CSD.Empirical.QM.LeggettGarg.lgCorr (Δ : ℝ) :
      ℝ

      The Born two-time correlation ⟨Q(0)Q(Δ)⟩ of σ_z under precession by Δ, with intermediate collapse: ∑_{s,t} sgn(s)·sgn(t)·½·|⟨e_t, zenoU Δ · e_s⟩|².

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem CSD.Empirical.QM.LeggettGarg.lgCorr_eq (Δ : ℝ) :
        lgCorr Δ = Real.cos (2 * Δ)

        The quantum two-time correlation equals cos(2Δ) — derived from zenoU, not asserted.

        Part 3 — the K₃ combination and its quantum violation #

        source
        noncomputable def CSD.Empirical.QM.LeggettGarg.lgK (Δ : ℝ) :
        ℝ

        The Leggett–Garg K₃ combination for equal time-steps Δ: K₃(Δ) = ⟨Q₁Q₂⟩ + ⟨Q₂Q₃⟩ − ⟨Q₁Q₃⟩ = 2·lgCorr Δ − lgCorr (2Δ) (adjacent pairs at separation Δ, outer pair at separation 2Δ).

        Equations
        Instances For
          source
          theorem CSD.Empirical.QM.LeggettGarg.lg_qm_value (Δ : ℝ) :
          lgK Δ = 2 * Real.cos (2 * Δ) - Real.cos (4 * Δ)

          The quantum Leggett–Garg value K₃(Δ) = 2cos(2Δ) − cos(4Δ).

          source
          theorem CSD.Empirical.QM.LeggettGarg.lg_violation :
          lgK (Real.pi / 6) = 3 / 2

          The quantum violation: K₃(π/6) = 3/2 — the Lüders bound, exceeding the macrorealist 1.

          source
          def CSD.Empirical.QM.LeggettGarg.lgMacrorealistBoundValue :
          ℝ

          The macrorealist Leggett–Garg bound value 1.

          Equations
          Instances For
            source
            theorem CSD.Empirical.QM.LeggettGarg.lg_macrorealist_bound_violated :
            lgMacrorealistBoundValue < lgK (Real.pi / 6)

            The macrorealist bound is violated: 1 < K₃(π/6) = 3/2. The numerical gap is the empirical falsification of macrorealism (Palacios-Laloy 2010 and successors).