Empirical: Hardy's paradox (nonlocality without inequalities)

Category: 3-Local. The combinatorial LHV impossibility is QM-generic (no CSD ontology); promotion-ready to 2-Framework on demand.

What Hardy says

Hardy 1992-1993: for almost all two-qubit entangled states, there exists a choice of two binary measurements on each side (Alice: A, A'; Bob: B, B', outcomes ±1) and a positive joint probability P(A=+1, B=+1) > 0 such that QM also predicts three forbidden joint outcomes:

P(A=+1, B=+1) = α > 0     -- the "Hardy probability"
P(A=+1, B'=-1) = 0        -- forbidden: A=+1 implies B'=+1
P(A'=-1, B=+1) = 0        -- forbidden: B=+1 implies A'=+1
P(A'=+1, B'=+1) = 0       -- forbidden: A' and B' can't both be +1

Under any local hidden-variable model with a joint outcome distribution over (A, A', B, B') ∈ {±1}^4, the four constraints above are jointly unsatisfiable:

1. The positive Hardy probability forces some outcome quadruple x with A(x)=+1, B(x)=+1, p(x) > 0.
2. The constraint P(A=+1, B'=-1) = 0 forces B'(x)=+1 (else x would be a positive contribution to a zero-sum).
3. Similarly, P(A'=-1, B=+1) = 0 forces A'(x)=+1.
4. But then x has A'=+1, B'=+1, so its probability contributes to P(A'=+1, B'=+1), which is zero. Contradiction with p(x) > 0.

This is the structural signature of QM nonlocality "without inequalities": a single-shot algebraic contradiction (like GHZ) but on two qubits and for almost all entangled states (unlike GHZ which requires the specific 3-qubit GHZ state, or CHSH which is a statistical inequality violation).

Distinction from CHSH, GHZ, KS, Mermin-Peres

• CHSH (Bell.lean): statistical inequality, 2-party.
• GHZ (Multipartite/GHZ.lean): algebraic single-shot, 3-party.
• KS (Contextuality/KS18.lean): combinatorial contextuality, single-system.
• Mermin-Peres (Contextuality/MerminPeres.lean): algebraic single-shot, 2-qubit, contextuality.
• Hardy (this file): algebraic single-shot, 2-party, nonlocality. Distinct from GHZ in that it works for almost any entangled 2-qubit state (with appropriate choice of measurements), not just the specific GHZ state.

Experimental verification

• Hardy 1992: Phys. Rev. Lett. 68, 2981 ("Quantum mechanics, local realistic theories, and Lorentz-invariant realistic theories").
• Hardy 1993: Phys. Rev. Lett. 71, 1665 ("Nonlocality for two particles without inequalities for almost all entangled states").
• Lundeen, Steinberg 2009: Phys. Rev. Lett. 102, 020404 (experimental confirmation via weak measurements).

What this file proves

no_lhv_hardy: there is no probability distribution p : (Fin 2)^4 → ℝ (non-negative, marginal sums) satisfying the four Hardy constraints simultaneously.

Combinatorial; cites only the foundational triple.

What this file does not prove

The QM-side identities establishing that some specific 2-qubit state and four observables actually realise the four Hardy constraints predicted in the docstring. (Hardy 1993 gives the construction; a Lean formalisation would parametrise by the entanglement parameter and verify each probability via inner-product / Born computations. Deferred to a follow-up tranche, in the same spirit as the "QM-side operator identities deferred" reading in KS18.)

Coding convention

We index outcome quadruples by Outcome := Fin 2 × Fin 2 × Fin 2 × Fin 2. The coordinates are (A, A', B, B'), with Fin 2-value 1 meaning QM-outcome +1 and Fin 2-value 0 meaning QM-outcome -1.

@[reducible, inline]

abbrev CSD.Empirical.Hardy.Outcome : Type

An LHV outcome quadruple: (A, A', B, B') with each coordinate in Fin 2 (1 = QM outcome +1, 0 = QM outcome -1).

Equations

• CSD.Empirical.Hardy.Outcome = (Fin 2 × Fin 2 × Fin 2 × Fin 2)

theorem CSD.Empirical.Hardy.no_lhv_hardy : ¬∃ (p : Outcome → ℝ), (∀ (x : Outcome), 0 ≤ p x) ∧ 0 < ∑ x : Outcome with x.1 = 1 ∧ x.2.2.1 = 1, p x ∧ ∑ x : Outcome with x.1 = 1 ∧ x.2.2.2 = 0, p x = 0 ∧ ∑ x : Outcome with x.2.1 = 0 ∧ x.2.2.1 = 1, p x = 0 ∧ ∑ x : Outcome with x.2.1 = 1 ∧ x.2.2.2 = 1, p x = 0

No LHV distribution satisfies the four Hardy constraints.

For any probability distribution p : Outcome → ℝ (non-negative) satisfying:

• ∑ x with A(x)=+1, B(x)=+1, p(x) > 0 (positive Hardy probability),
• ∑ x with A(x)=+1, B'(x)=-1, p(x) = 0 (forbidden joint #1),
• ∑ x with A'(x)=-1, B(x)=+1, p(x) = 0 (forbidden joint #2),
• ∑ x with A'(x)=+1, B'(x)=+1, p(x) = 0 (forbidden joint #3),

a contradiction follows by the chain:

1. The positive sum forces some x with A(x)=B(x)=+1, p(x) > 0.
2. The first zero-sum forces B'(x) = +1 (else p(x) = 0).
3. The second zero-sum forces A'(x) = +1.
4. The third zero-sum then forces p(x) = 0, contradicting p(x) > 0.

QM-side Hardy realisation

A specific 2-qubit state and four observables (Pauli Z and X on each side) realising the four Hardy probabilities predicted by QM.

State (unnormalised; the normalisation factor 1/√12 cancels in "= 0" vs "≠ 0" reasoning):

|ψ⟩ ∝ |00⟩ + |01⟩ + |10⟩ - 3|11⟩

Observables: A = B = Z (computational basis, +1 eigenstate |0⟩); A' = B' = X (Hadamard basis, +1 eigenstate |+⟩ = |0⟩ + |1⟩).

Four amplitude identities (squared moduli are the Hardy probabilities):

• ⟨0,0|ψ⟩ = 1 (proportional to P(A=+1, B=+1) = 1/12 > 0)
• ⟨0,−|ψ⟩ = 0 (P(A=+1, B'=-1) = 0)
• ⟨−,0|ψ⟩ = 0 (P(A'=-1, B=+1) = 0)
• ⟨+,+|ψ⟩ = 0 (P(A'=+1, B'=+1) = 0)

The fourth (load-bearing) identity reduces to the integer sum 1 + 1 + 1 + (−3) = 0. This is why the |11⟩-amplitude δ = −3 is load-bearing: the general Hardy algebraic condition α(α² + β² + γ²) + βγδ = 0 (derived from setting ⟨+,+|ψ⟩ = 0) becomes 3 + δ = 0 with α = β = γ = 1.

The construction here is not Hardy's maximum (≈ 9% from the golden-ratio state); the integer-amplitude variant gives Hardy probability 1/12 ≈ 8.3%. The choice is for cleanest Lean algebra — no square-root manipulation, all amplitudes ℤ.

Together with no_lhv_hardy, this closes the Hardy story: QM realises the four constraints; no LHV distribution can.

def CSD.Empirical.Hardy.HardyQM.hardyVec : Fin 2 × Fin 2 → ℂ

The (unnormalised) Hardy state: |ψ⟩ = |00⟩ + |01⟩ + |10⟩ − 3|11⟩.

Equations

• CSD.Empirical.Hardy.HardyQM.hardyVec (⟨0, isLt⟩, ⟨0, isLt_1⟩) = 1
• CSD.Empirical.Hardy.HardyQM.hardyVec (⟨0, isLt⟩, ⟨1, isLt_1⟩) = 1
• CSD.Empirical.Hardy.HardyQM.hardyVec (⟨1, isLt⟩, ⟨0, isLt_1⟩) = 1
• CSD.Empirical.Hardy.HardyQM.hardyVec (⟨1, isLt⟩, ⟨1, isLt_1⟩) = -3

def CSD.Empirical.Hardy.HardyQM.zPlus : Fin 2 → ℂ

|0⟩: the +1 eigenstate of Z.

Equations

• CSD.Empirical.Hardy.HardyQM.zPlus = ![1, 0]

def CSD.Empirical.Hardy.HardyQM.xPlus : Fin 2 → ℂ

|+⟩ = |0⟩ + |1⟩ (unnormalised): the +1 eigenstate of X.

Equations

• CSD.Empirical.Hardy.HardyQM.xPlus = ![1, 1]

def CSD.Empirical.Hardy.HardyQM.xMinus : Fin 2 → ℂ

|−⟩ = −|0⟩ + |1⟩ (unnormalised): the −1 eigenstate of X.

Equations

• CSD.Empirical.Hardy.HardyQM.xMinus = ![-1, 1]

noncomputable def CSD.Empirical.Hardy.HardyQM.jointAmplitude (a b : Fin 2 → ℂ) (ψ : Fin 2 × Fin 2 → ℂ) : ℂ

Joint amplitude ⟨a ⊗ b | ψ⟩ for ψ : Fin 2 × Fin 2 → ℂ and single-qubit bras a, b : Fin 2 → ℂ.

Equations

• CSD.Empirical.Hardy.HardyQM.jointAmplitude a b ψ = ∑ p : Fin 2 × Fin 2, star (a p.1) * star (b p.2) * ψ p

theorem CSD.Empirical.Hardy.HardyQM.hardyAmp_AB : jointAmplitude zPlus zPlus hardyVec = 1

Hardy amplitude 1: ⟨0, 0 | ψ⟩ = 1 (proportional to the positive Hardy probability P(A=+1, B=+1) = 1/12).

theorem CSD.Empirical.Hardy.HardyQM.hardyAmp_A_B'minus : jointAmplitude zPlus xMinus hardyVec = 0

Hardy amplitude 2: ⟨0, − | ψ⟩ = 0 (P(A=+1, B'=-1) = 0).

The only contributing terms have i = 0 (since zPlus 1 = 0): star(−1)·ψ(0,0) + star(1)·ψ(0,1) = −1·1 + 1·1 = 0.

theorem CSD.Empirical.Hardy.HardyQM.hardyAmp_A'minus_B : jointAmplitude xMinus zPlus hardyVec = 0

Hardy amplitude 3: ⟨−, 0 | ψ⟩ = 0 (P(A'=-1, B=+1) = 0).

Symmetric to the previous: only j = 0 contributes, star(−1)·ψ(0,0) + star(1)·ψ(1,0) = −1·1 + 1·1 = 0.

theorem CSD.Empirical.Hardy.HardyQM.hardyAmp_A'_B' : jointAmplitude xPlus xPlus hardyVec = 0

Hardy amplitude 4 (load-bearing): ⟨+, + | ψ⟩ = 0 (P(A'=+1, B'=+1) = 0).

All four ψ terms contribute: 1 + 1 + 1 + (−3) = 0. This is the specific reason δ = −3 is the |11⟩-amplitude.

theorem CSD.Empirical.Hardy.HardyQM.exists_hardy_realisation : ∃ (ψ : Fin 2 × Fin 2 → ℂ) (a : Fin 2 → ℂ) (aPrime : Fin 2 → ℂ) (b : Fin 2 → ℂ) (bPrime : Fin 2 → ℂ) (aPrime_perp : Fin 2 → ℂ) (bPrime_perp : Fin 2 → ℂ), aPrime ≠ 0 ∧ aPrime_perp ≠ 0 ∧ bPrime ≠ 0 ∧ bPrime_perp ≠ 0 ∧ ∑ i : Fin 2, star (aPrime i) * aPrime_perp i = 0 ∧ ∑ i : Fin 2, star (bPrime i) * bPrime_perp i = 0 ∧ jointAmplitude a b ψ ≠ 0 ∧ jointAmplitude a bPrime_perp ψ = 0 ∧ jointAmplitude aPrime_perp b ψ = 0 ∧ jointAmplitude aPrime bPrime ψ = 0

QM realises the Hardy constraints. A specific 2-qubit state and four observables exhibit the four Hardy probability identities, demonstrating that the LHV-impossibility theorem no_lhv_hardy has empirical content (QM violates LHV on this Hardy instance).

Strengthened 2026-08-08 (vacuity audit): the statement now records the witnesses' nondegeneracy — the primed vectors are nonzero and each _perp is orthogonal to its primed partner — so degenerate (zero-vector) witnesses no longer satisfy it; the Hardy content is in the statement, not only in the proof's choice of witnesses.

QM-side Hardy realisation at the golden-ratio maximum

The Hardy probability 1/12 from HardyQM is below Hardy's theoretical maximum (5√5 − 11)/2 ≈ 9.017%. The maximum is achieved at the golden-ratio Hardy state

|ψ_max⟩ ∝ |00⟩ + √φ |01⟩ + √φ |10⟩ − φ² |11⟩

where φ = (1+√5)/2 is the golden ratio. This namespace exhibits the golden-ratio state and verifies the four Hardy amplitude identities for it, completing the "Hardy probability gap" by showing both integer-amplitude (≈ 8.3%) and golden-ratio (≈ 9.017%) realisations.

The eigenstate vectors aPrimeMax = (1, √φ) and bPrimeMinusMax = (-√φ, 1) are the unnormalised +1 and −1 eigenstates of the second-measurement basis on each side (the basis whose +1 eigenvector aligns with the marginal (α|0⟩ + γ|1⟩) ∝ (1|0⟩ + √φ |1⟩) of the partially-traced Hardy state).

Load-bearing identity: the fourth amplitude reduces to 1 + 2φ − φ³. The golden-ratio identity φ³ = 2φ + 1 (proved below from φ² = φ + 1) makes this zero.

The Hardy probability is α² / ‖ψ_max‖² = 1 / (5φ + 3) = (5√5 − 11)/2 after rationalisation. The numerical equality is left as a separate follow-up; this namespace delivers the four amplitude identities needed to satisfy the LHV-impossibility hypothesis.

noncomputable def CSD.Empirical.Hardy.HardyQMMax.phi : ℝ

The golden ratio φ = (1 + √5)/2.

Equations

• CSD.Empirical.Hardy.HardyQMMax.phi = (1 + √5) / 2

theorem CSD.Empirical.Hardy.HardyQMMax.phi_pos : 0 < phi

theorem CSD.Empirical.Hardy.HardyQMMax.phi_sq : phi ^ 2 = phi + 1

The defining identity φ² = φ + 1.

theorem CSD.Empirical.Hardy.HardyQMMax.phi_cube : phi ^ 3 = 2 * phi + 1

The cubic identity φ³ = 2φ + 1 (the load-bearing fact for the fourth Hardy amplitude at the golden-ratio maximum). Derived from φ² = φ + 1: φ³ = φ·φ² = φ(φ + 1) = φ² + φ = (φ + 1) + φ = 2φ + 1.

noncomputable def CSD.Empirical.Hardy.HardyQMMax.sqrtPhi : ℝ

√φ (positive square root of the golden ratio).

Equations

• CSD.Empirical.Hardy.HardyQMMax.sqrtPhi = √CSD.Empirical.Hardy.HardyQMMax.phi

theorem CSD.Empirical.Hardy.HardyQMMax.sqrtPhi_sq : sqrtPhi ^ 2 = phi

noncomputable def CSD.Empirical.Hardy.HardyQMMax.hardyMaxVec : Fin 2 × Fin 2 → ℂ

The golden-ratio Hardy state (unnormalised): |ψ_max⟩ = |00⟩ + √φ |01⟩ + √φ |10⟩ − φ² |11⟩.

Equations

• CSD.Empirical.Hardy.HardyQMMax.hardyMaxVec (⟨0, isLt⟩, ⟨0, isLt_1⟩) = 1
• CSD.Empirical.Hardy.HardyQMMax.hardyMaxVec (⟨0, isLt⟩, ⟨1, isLt_1⟩) = ↑CSD.Empirical.Hardy.HardyQMMax.sqrtPhi
• CSD.Empirical.Hardy.HardyQMMax.hardyMaxVec (⟨1, isLt⟩, ⟨0, isLt_1⟩) = ↑CSD.Empirical.Hardy.HardyQMMax.sqrtPhi
• CSD.Empirical.Hardy.HardyQMMax.hardyMaxVec (⟨1, isLt⟩, ⟨1, isLt_1⟩) = -↑(CSD.Empirical.Hardy.HardyQMMax.phi ^ 2)

noncomputable def CSD.Empirical.Hardy.HardyQMMax.aPrimeMax : Fin 2 → ℂ

|a'⟩ = |0⟩ + √φ |1⟩ (unnormalised; the second-measurement +1 eigenstate aligned with the partially-traced Hardy state).

Equations

• CSD.Empirical.Hardy.HardyQMMax.aPrimeMax = ![1, ↑CSD.Empirical.Hardy.HardyQMMax.sqrtPhi]

noncomputable def CSD.Empirical.Hardy.HardyQMMax.aPrimeMinusMax : Fin 2 → ℂ

|a'_⊥⟩ = −√φ |0⟩ + |1⟩ (unnormalised; the orthogonal complement).

Equations

• CSD.Empirical.Hardy.HardyQMMax.aPrimeMinusMax = ![-↑CSD.Empirical.Hardy.HardyQMMax.sqrtPhi, 1]

theorem CSD.Empirical.Hardy.HardyQMMax.hardyMaxAmp_AB : HardyQM.jointAmplitude HardyQM.zPlus HardyQM.zPlus hardyMaxVec = 1

Max-Hardy amplitude 1: ⟨0, 0 | ψ_max⟩ = 1 (positive).

theorem CSD.Empirical.Hardy.HardyQMMax.hardyMaxAmp_A_B'minus : HardyQM.jointAmplitude HardyQM.zPlus aPrimeMinusMax hardyMaxVec = 0

Max-Hardy amplitude 2: ⟨0, a'_⊥ | ψ_max⟩ = 0. Only i = 0 contributes: star(−√φ)·1 + star(1)·√φ = −√φ + √φ = 0.

theorem CSD.Empirical.Hardy.HardyQMMax.hardyMaxAmp_A'minus_B : HardyQM.jointAmplitude aPrimeMinusMax HardyQM.zPlus hardyMaxVec = 0

Max-Hardy amplitude 3: ⟨a'_⊥, 0 | ψ_max⟩ = 0. Symmetric.

theorem CSD.Empirical.Hardy.HardyQMMax.hardyMaxAmp_A'_B' : HardyQM.jointAmplitude aPrimeMax aPrimeMax hardyMaxVec = 0

Max-Hardy amplitude 4 (load-bearing): ⟨a', a' | ψ_max⟩ = 0.

All four terms contribute: 1·1·1 + 1·√φ·√φ + √φ·1·√φ + √φ·√φ·(−φ²) = 1 + φ + φ − φ·φ² = 1 + 2φ − φ³ = 1 + 2φ − (2φ + 1) = 0, using sqrtPhi_sq : √φ · √φ = φ and phi_cube : φ³ = 2φ + 1.

theorem CSD.Empirical.Hardy.HardyQMMax.exists_hardy_realisation_max : ∃ (ψ : Fin 2 × Fin 2 → ℂ) (a : Fin 2 → ℂ) (aPrime : Fin 2 → ℂ) (b : Fin 2 → ℂ) (bPrime : Fin 2 → ℂ) (aPrime_perp : Fin 2 → ℂ) (bPrime_perp : Fin 2 → ℂ), aPrime ≠ 0 ∧ aPrime_perp ≠ 0 ∧ bPrime ≠ 0 ∧ bPrime_perp ≠ 0 ∧ ∑ i : Fin 2, star (aPrime i) * aPrime_perp i = 0 ∧ ∑ i : Fin 2, star (bPrime i) * bPrime_perp i = 0 ∧ HardyQM.jointAmplitude a b ψ ≠ 0 ∧ HardyQM.jointAmplitude a bPrime_perp ψ = 0 ∧ HardyQM.jointAmplitude aPrime_perp b ψ = 0 ∧ HardyQM.jointAmplitude aPrime bPrime ψ = 0

QM realises the Hardy constraints at the golden-ratio maximum.

Strengthened 2026-08-08 (vacuity audit), as exists_hardy_realisation: nondegeneracy and orthogonality of the witnesses are part of the statement.

Hardy maximum probability value

The Hardy probability for the golden-ratio state evaluates to the closed-form maximum (5√5 − 11)/2 ≈ 9.017%. Three steps:

1. normSq_hardyMaxVec: ‖ψ_max‖² = 5φ + 3 (uses sqrtPhi_sq, phi_sq).
2. hardyMax_value: 1/(5φ + 3) = (5√5 − 11)/2 (rationalisation identity, via (5√5)² = 25·5 = 125 and (5√5−11)(11+5√5) = 4).
3. hardyMax_probability_eq: combines via hardyMaxAmp_AB.

noncomputable def CSD.Empirical.Hardy.HardyQMMax.normSq (ψ : Fin 2 × Fin 2 → ℂ) : ℝ

The squared norm of a 2-qubit state vector.

Equations

• CSD.Empirical.Hardy.HardyQMMax.normSq ψ = ∑ p : Fin 2 × Fin 2, ‖ψ p‖ ^ 2

theorem CSD.Empirical.Hardy.HardyQMMax.normSq_hardyMaxVec : normSq hardyMaxVec = 5 * phi + 3

‖ψ_max‖² = 5φ + 3. Expands the four-term sum: 1 + (√φ)² + (√φ)² + (φ²)² = 1 + φ + φ + (3φ + 2) = 5φ + 3.

theorem CSD.Empirical.Hardy.HardyQMMax.hardyMax_value : 1 / (5 * phi + 3) = (5 * √5 - 11) / 2

The rationalisation identity 1 / (5φ + 3) = (5√5 − 11)/2.

The proof routes via the difference-of-squares (5√5 − 11)(11 + 5√5) = 25·(√5)² − 121 = 125 − 121 = 4 and the substitution 5φ + 3 = (11 + 5√5)/2.

theorem CSD.Empirical.Hardy.HardyQMMax.hardyMax_probability_eq : ‖HardyQM.jointAmplitude HardyQM.zPlus HardyQM.zPlus hardyMaxVec‖ ^ 2 / normSq hardyMaxVec = (5 * √5 - 11) / 2

Hardy's maximum probability value: the QM joint probability |⟨0, 0 | ψ_max⟩|² / ‖ψ_max‖² for the golden-ratio Hardy state equals the closed-form maximum (5√5 − 11)/2 ≈ 9.017%.