Lean 4 proof that the finite-dimensional pure-projective I3322 supremum equals the Pál–Vértesi variational supremum and is not attained in that class.
-
Updated
Aug 28, 2026 - Lean
#
i3322
Here are 2 public repositories matching this topic...
Exact tensor-product and commuting-operator I3322 quantum supremum with finite-dimensional nonattainment and independently replayable certificates.
reproducible-research interval-arithmetic quantum-information mathematical-physics operator-algebras computer-assisted-proof device-independent quantum-correlations quantum-foundations bell-inequalities quantum-nonlocality tsirelson-bound i3322
-
Updated
Sep 3, 2026 - Python
Add this topic to your repo
To associate your repository with the i3322 topic, visit your repo's landing page and select "manage topics."