I3322 in Lean 4

This repository formalizes Theorems 1 and 2 of The quantum supremum of the I3322 Bell inequality is not attained in finite dimension. The paper gives the mathematical argument; the tables below locate its definitions and proof steps in Lean. All references use arXiv:2608.29734v1 (PDF).

Definitions and statements

Start with Statement.lean. It collects every project-specific definition needed to read the two theorems, with paper references beside the formulas. Its final section connects these definitions to the existing proof by proving equality of the complete sets of values.

Names in this table have prefix I3322.Statement.

Paper	Lean declaration
Sec. II A; pure states and projective measurements in Sec. III A	QuantumStrategy, QuantumStrategy.expectation
Eq. (1): Bell functional	QuantumStrategy.value
Eq. (2): quantum supremum	quantumSupremum
Eqs. (4)–(5): PV coefficients and value	s, d, PVChain.value
Eq. (7): finite PV domain and supremum	PVChain, betaPV
Theorem 1, Eq. (8): $I^*=\beta_{\mathrm{PV}}$	variational
Theorem 2: finite-dimensional nonattainment	finiteDimensional_nonattainment
Sec. II B: every PV value is a quantum value	pvValue_attained
Eq. (30): $1/4<\beta_{\mathrm{PV}}<1/3$	betaPV_bounds

Lean counts measurements and Schmidt coefficients from zero: alice 0 is $A_1$ and amplitude 0 is $\lambda_1$. States and Schmidt coefficients may be unnormalized; the definitions divide by $\langle\psi|\psi\rangle$ and $\sum_i\lambda_i^2$, respectively. Both suprema are Mathlib's sSup, which is the least upper bound of a set of reals that is nonempty and bounded above and is 0 otherwise; the file proves both properties for both sets. The last two rows are consistency checks: the Bell functional and Born rule reproduce Eq. (5) on the PV family, and $\beta_{\mathrm{PV}}$ lies in the interval of Eq. (30).

Proof correspondence

Names below have prefix I3322. Links open the relevant proof declarations.

Paper	Lean declaration
Sec. II B: realization of Eq. (5)	PVRealization.exists_quantumStrategy
Eqs. (19), (23): marginals and $\Phi(\theta)$	CouplingTable.row, column, score
Lemma 2, Eq. (24): spectral-weight bound	QuantumStrategy.tableBound
Eqs. (25)–(26); Appendix B: matching conditions	CouplingTable.Ensemble.walkEnsemble_diagonalMatches, walkEnsemble_junctionMatches
Lemma 3, Eq. (27): $\Phi(\theta)\leq\beta_{\mathrm{PV}}$	CouplingTable.Ensemble.score_le_betaPV
Eq. (30); Appendix C: coarse bounds	quarter_lt_betaPV, betaPV_lt_third
Lemma 4, Eqs. (31)–(33): consequences of equality	CouplingTable.exists_supportSpine, CouplingTable.SupportSpine.toValueSpine, CouplingTable.equalityChainOfTable
Lemma 5, Eqs. (40), (42): optimality conditions	ChainStationarity.weighted_stationarity_of_finite_windows, label_stationarity_of_finite_windows, ValueSpine.clamped_label_stationarity
Lemma 5, Eqs. (41)–(42): contradiction	EqualityChain.false, CouplingTable.score_ne_betaPV
Theorems 1–2	MainTheorems.lean

The formal proof differs from the paper in two places. For Lemma 2, Lean applies Cauchy–Schwarz to Alice's and Bob's spectral decompositions separately and then symmetrizes the joint weights, averaging the entries at $(a,b)$ and $(-b,-a)$. For Lemmas 4–5, Lean extends the selected finite sequence of positive entries to a two-sided sequence whose spectral labels and coefficient ratios are constant beyond both endpoints, and obtains the condition of Eq. (40) from bounds on finite truncations. The PV realization uses zero padding to local dimension $2n+1$, which leaves the value in Eq. (5) unchanged.

Graph PDF · Figure source and build instructions

Scope. The formal theorems quantify over arbitrary finite-dimensional complex pure states and binary projective measurements. The purification and Naimark reduction in Sec. III A, and the compactness arguments for Corollaries 1–2, are not formalized. Neither an exact value of $\beta_{\mathrm{PV}}$ nor infinite-dimensional attainment is asserted.

Build and audit

From the repository root:

lake exe cache get
lake build I3322
lake env lean Audit.lean

The build and audit include Statement.lean. The final theorems have no reduction hypotheses; helper arguments such as tableBound are supplied by proved theorems. The audit reports only [propext, Classical.choice, Quot.sound]. The source contains no sorry, admit, or custom axiom.

Lean, mathlib and Physlib are pinned to v4.32.0; exact dependency commits are in lake-manifest.json. Citation · MIT License.