Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Optimized Mermin equals optimized Bell

Open
QAlgorithms.Papers.Independent.Intakethird100.P80.mermin_bell_equality

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

For the fixed Mermin and optimized Bell experiments of Appendix III, their optimized strengths agree both when settings must be independent and when correlations are allowed:

SMerminUC=SBell optimizedUC,SMerminCOR=SBell optimizedCOR.S^{\rm UC}_{\rm Mermin}=S^{\rm UC}_{\rm Bell\ optimized},\qquad S^{\rm COR}_{\rm Mermin}=S^{\rm COR}_{\rm Bell\ optimized}.SMerminUC​=SBell optimizedUC​,SMerminCOR​=SBell optimizedCOR​.

This is the equality for non-uniform optimized sampling described in Section V. It does not identify their distinct uniform strengths or certify rounded optimizer entries at unused settings.

Preamble
import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P80
Formal statement
noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P80

open scoped BigOperators ENNReal Topology Classical

open MeasureTheory Filter

/-- PDF p.9, Section V (Tables XXIV–XXVII, p.23): Mermin and optimized Bell have equal
optimized product and correlated strengths. Their UNIFORM strengths are not equated. -/
theorem mermin_bell_equality :
    uncorrelatedStrength mermin = uncorrelatedStrength optimizedBell ∧
    correlatedStrength mermin = correlatedStrength optimizedBell := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P80

end
Source
The statistical strength of nonlocality proofs, arXiv:quant-ph/0307125v2, PDF p. 9, Section V: optimized Mermin equals optimized Bell strength
Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

Let QMQ_MQM​ be the table for two parties with three settings each and binary outcomes, whose value for each equal-outcome pair is 1/21/21/2 when the settings agree and 1/81/81/8 when they differ, and whose value for each unequal-outcome pair is 000 when the settings agree and 3/83/83/8 when they differ. Let QBQ_BQB​ be the table for two parties with two settings each and binary outcomes, whose equal-outcome/unequal-outcome values are (1/2,0)(1/2,0)(1/2,0) at setting (0,0)(0,0)(0,0), (1/8,3/8)(1/8,3/8)(1/8,3/8) at setting (0,1)(0,1)(0,1), and (3/8,1/8)(3/8,1/8)(3/8,1/8) at settings (1,0)(1,0)(1,0) and (1,1)(1,1)(1,1), with each value assigned to each individual outcome pair of that kind. For either scenario, let AAA be its setting space, VVV the space of binary assignments viav_{ia}via​ to every party and every one of its settings, ΔA,ΔV\Delta_A,\Delta_VΔA​,ΔV​ their probability simplices, and U⊆ΔA\mathcal U\subseteq\Delta_AU⊆ΔA​ the distributions factoring into single-party setting distributions. For p∈ΔVp\in\Delta_Vp∈ΔV​, define Lp(a,x)=∑v: ∀i, vi,ai=xip(v)L_p(a,x)=\sum_{v:\,\forall i,\ v_{i,a_i}=x_i}p(v)Lp​(a,x)=∑v:∀i, vi,ai​​=xi​​p(v). Define KQ(s,p)K_Q(s,p)KQ​(s,p) from q(a,x)=s(a)Q(a,x)q(a,x)=s(a)Q(a,x)q(a,x)=s(a)Q(a,x) and r(a,x)=s(a)Lp(a,x)r(a,x)=s(a)L_p(a,x)r(a,x)=s(a)Lp​(a,x) as +∞+\infty+∞ if some q(a,x)>0q(a,x)>0q(a,x)>0 has r(a,x)=0r(a,x)=0r(a,x)=0, and otherwise as the nonnegative part of ∑a,xq(a,x)log⁡2(q(a,x)/r(a,x))\sum_{a,x}q(a,x)\log_2(q(a,x)/r(a,x))∑a,x​q(a,x)log2​(q(a,x)/r(a,x)), with zero-qqq summands set to 000. Define

U(Q)=sup⁡s∈Uinf⁡p∈ΔVKQ(s,p),C(Q)=sup⁡s∈ΔAinf⁡p∈ΔVKQ(s,p),U(Q)=\sup_{s\in\mathcal U}\inf_{p\in\Delta_V}K_Q(s,p), \qquad C(Q)=\sup_{s\in\Delta_A}\inf_{p\in\Delta_V}K_Q(s,p),U(Q)=s∈Usup​p∈ΔV​inf​KQ​(s,p),C(Q)=s∈ΔA​sup​p∈ΔV​inf​KQ​(s,p),

as extended nonnegative real numbers. The declaration asserts U(QM)=U(QB)U(Q_M)=U(Q_B)U(QM​)=U(QB​) and C(QM)=C(QB)C(Q_M)=C(Q_B)C(QM​)=C(QB​).

Human review
  • Endorsed by Shuze Chen · Nov 1, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Gohan · Nov 1, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me