Optimized Mermin equals optimized Bell
OpenQAlgorithms.Papers.Independent.Intakethird100.P80.mermin_bell_equalityFor 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:
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.
import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P80
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
Read-back
What the Lean code literally says, in plain math · gpt-6.1-sol
Let be the table for two parties with three settings each and binary outcomes, whose value for each equal-outcome pair is when the settings agree and when they differ, and whose value for each unequal-outcome pair is when the settings agree and when they differ. Let be the table for two parties with two settings each and binary outcomes, whose equal-outcome/unequal-outcome values are at setting , at setting , and at settings and , with each value assigned to each individual outcome pair of that kind. For either scenario, let be its setting space, the space of binary assignments to every party and every one of its settings, their probability simplices, and the distributions factoring into single-party setting distributions. For , define . Define from and as if some has , and otherwise as the nonnegative part of , with zero- summands set to . Define
as extended nonnegative real numbers. The declaration asserts and .
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.