This preprint constructs finite rational proof objects for both sides of the quantum value of I3322 Bell inequality. Let 𝑄t denote the supremum over finite-dimensional tensor-product binary measurements and𝑄c the commuting-operator value. On the complete word space of total length at most four, we construct a rational Gram certificate. The full signed setting-relabeling stabilizer is the dihedral group of order eight, reducing the certificate to five rational blocks. Ex-act affine reconstruction and a uniform diagonal shift of certified positive interior prove: 𝑄c (𝐼3322) ≤ 62718846253/250000000000 = 0.250875385012. Independently, a local-dimension-499 strategy specified by rational projectors and a nonzero unnormalized rational Schmidt vector has exact normalized value 𝐿499 = 0.25087538451397653548 . . .. Con-sequently, 𝐿499 ≤ 𝑄t(𝐼3322) ≤ 𝑄c (𝐼3322) ≤ 0.250875385012, with endpoint difference below 5 × 10−10. The lower certificate also proves 𝑄t(𝐼3322) > 1/4. Every theorem is checked using exact rational or integer arithmetic; floating-point computation is used only to discover candidates. Complete certificates, source code, tests, and reproducibility materials are archived at: doi:10.5281/zenodo.21462892.
This preprint constructs finite rational proof objects for both sides of the quantum value of I3322 Bell inequality. Let 𝑄t denote the supremum over finite-dimensional tensor-product binary measurements and𝑄c the commuting-operator value. On the complete word space of total length at most four, we construct a rational Gram certificate. The full signed setting-relabeling stabilizer is the dihedral group of order eight, reducing the certificate to five rational blocks. Ex-act affine reconstruction and a uniform diagonal shift of certified positive interior prove: 𝑄c (𝐼3322) ≤ 62718846253/250000000000 = 0.250875385012. Independently, a local-dimension-499 strategy specified by rational projectors and a nonzero unnormalized rational Schmidt vector has exact normalized value 𝐿499 = 0.25087538451397653548 . . .. Con-sequently, 𝐿499 ≤ 𝑄t(𝐼3322) ≤ 𝑄c (𝐼3322) ≤ 0.250875385012, with endpoint difference below 5 × 10−10. The lower certificate also proves 𝑄t(𝐼3322) > 1/4. Every theorem is checked using exact rational or integer arithmetic; floating-point computation is used only to discover candidates. Complete certificates, source code, tests, and reproducibility materials are archived at: doi:10.5281/zenodo.21462892.
We determine the quantum value of the three-setting, two-outcome Bell functional I3322. The value is the unique intersection q† of an analytic A-high stable curve of the exact Jacobi characteristic map with a central reverser curve. A computer-assisted proof isolates this intersection in a rational interval of width 10−55, beginning 0.2508753845139765356173366109459512989013219739714764755. We prove that the supremum over finite-dimensional tensor-product strategies, the unrestricted spatial value and the commuting-operator value all equal q†. No finite-dimensional strategy attains the value, whereas a normal infinite-dimensional spatial strategy and a commuting GNS strategy do. The proof combines an exact Bellman/path variational reduction, extraction of a positive bilateral calibrated Jacobi fibre from a maximizing weak-star state, a reflected-fibre central-incidence theorem and interval certificates for the unique stable/central intersection. A separate operator-positive three-remainder decomposition gives the commuting upper bound. The complete verification record is archived at DOI 10.5281/zenodo.22160086.
Let S be the common tensor-product and commuting-operator supremum of the I3322 Bell functional in the Collins-Gisin normalization. Starting from a certified value window and Bellman/path equivalence, we prove that no finite-dimensional quantum strategy attains S, whereas a spatial strategy on ℓ2(Z)⊗ℓ2(Z) does. The finite-dimensional statement includes mixed states and binary POVMs. Consequently Cq(3,3;2,2) is not closed and Cqs(3,3;2,2)∖Cq(3,3;2,2) is nonempty. We also establish the dimension complexity D(ε)=Θ(log(1/ε)): approaching S requires and suffices local dimension logarithmic in inverse error. The constructive upper bound is D(ε)≤23.9010650log(1/ε) for all sufficiently small ε, with natural logarithms; the lower constants are existential. The proofs use critical Bellman storage, spectral transport and normalizable orbit measures. A finite weighted-flow argument supplies the unrestricted quantitative lower bound without identifying distinct joint spectral components. This revision replaces an unsupported step in the earlier lower argument and records additional proof corrections. Prior numerical certification and independent concurrent attainment results are credited. Exact arithmetic and Lean 4 check specified numerical, scalar and finite accounting facts; the complete analytic proof is not formalized.
This record contains the manuscript and complete verification artifact for the Bell inequality J62_4422 of Pál and Vértesi.It certifies the exact rational bracket750075557472719639 / 10^18 ≤ β_Q ≤ 750091086083765047288227625 / 10^27,and exact attainment of 3/4 by the stated two-qubit strategy. The lower endpoint is an exact rational strategy. The upper endpoint is certified by a sum-of-squares chain for the retained 365-word relaxation level.The Krawczyk certificate localizes the underlying KKT zero and establishes a strict local maximum, including negativity of the border form in all 256 boundary strata; it does not establish global optimality of that localized point. Accordingly, this work does not claim the exact quantum value, qubit-restricted optimality, minimum optimizer dimension, or global optimality of the localized KKT point.The archive includes SHA-256 manifests, standard-library replay programs, independently written certificate checks, mutation controls, and pinned full Krawczyk replays. The acceptance programs are fail-closed under optimized Python. The manuscript and certificates are licensed CC BY 4.0; verification code is licensed MIT.Version 1.1 is a hygiene-only update: it replaces one machine-local default path in a helper with the portable repository root ".", updates the corresponding checker and certificate source bindings, and leaves the mathematical calculation, inputs, claims, and replay outputs unchanged.
A post-release exact-arithmetic audit found a load-bearing global-amplitude gap in the Bellman upper-bound assembly of the earlier releases (v1.0.0-v1.2.0). Those releases are preserved as historical records; their exact-optimum, nonattainment, spatial-separation, and nonclosure claims are under correction and are not asserted by this version. What this version rigorously and unconditionally certifies: 0.2508753845015185 < omega_tensor <= omega_commuting <= 0.250875388108398 (window width 3.61e-9), with the lower endpoint an explicit 255-dimensional rational tensor-product strategy verified in exact arithmetic and independently reconstructed at 160-digit interval precision, and the upper endpoint an exact rational Bellman subsolution with an endpoint-clustered 25,601-knot witness, independently reconstructed cell by cell. The certificate stack, the audit that found the gap, a structural explanation (Bellman contact versus amplitude-normalization duality), and one recorded failed quantitative prediction are all included. Every load-bearing claim maps to replayable source and a frozen receipt.
We give exact rational certificates for two results in the bipartite Bell scenario with three two-outcome measurements per party. First, the maximum of the I3322 (Froissart) functional over the almost-quantum set -- the 1+AB level of the Navascues-Pironio-Acin (NPA) hierarchy -- is certified to lie between 0.2514708838 and 0.2514709016 (width <2×10−8), in the normalization with classical bound 0 and quantum maximum ≈0.2508754; to our knowledge no value for this landmark had been published. Second, we exhibit a single exact rational behavior T∗ carrying certificates in both directions: a rational moment matrix proving T∗ almost-quantum, and a rational dual object proving that every NPA level-2 completion of T∗ requires slack at least q=4.5934×10−4, so that T∗ is not quantum. The strict inclusion Q⊊Q~ in the minimal three-setting scenario is thereby established end-to-end with no reliance on floating-point computation. Anatomically, the witness is locally quantum: all nine of its 2×2 correlator subtables pass the Tsirelson-Landau-Masanes criterion, so its non-quantumness is irreducibly a three-setting phenomenon, concentrated in ordering-dependent pseudo-moments coupling each party's third setting to the other's first two; the level-2 certificate is equivalently an exact sum-of-squares identity that any quantum state values nonnegatively and the witness is forced to value at −q. The certificates follow the rational rounding-projection-lifting programme recently developed for noncommutative optimization; for NPA moment matrices in canonical form the required projection reduces to a per-moment uniform shift, making certification essentially free at these sizes, and we work the programme in both the feasibility and infeasibility directions on one witness. Machine-checkable certificates and verifiers requiring only the Python standard library accompany the paper. Files in this record: the paper (PDF); exact rational certificates for both theorems (i3322_1AB_certificate.json, i3322_level2_infeasibility_certificate.json); standalone verifiers requiring only the Python 3 standard library (verify_i3322_certificate.py, verify_level2_certificate.py); and the generating scripts (certify_landmark.py, certify_level2.py). See README_ancillary.txt for which artifact proves which theorem and how to run the verifiers. v2: corrects the mechanism attribution in Sec. 5 (anatomy) and adds the archive reference to Data Availability; theorems, certificates, and verifiers unchanged.
The noise threshold below which the qubit depolarizing channel retains positive quantum capacity has been studied since 1996. The classic constructions come with exact finite formulae, but in every reported threshold to date -- most recently the record of Agarwal et al. -- the final step, the sign of the coherent information at the reported point, is a floating-point evaluation. We give the first exact-arithmetic, independently machine-checkable positivity proofs in this regime: an explicit 45-copy rank-two input state A, published as a 1,472-byte witness, with certified Ic>0 at the exact rational p=16239/250000=0.064956 (per-Pauli convention; total error rate 3p=0.194868) -- beyond both the best value printed in the Agarwal et al. paper (0.064657) and the strongest state in the same authors' public repository (≈0.064911), both numerical. Because the depolarizing family is a semigroup under composition, fixed-input coherent information is nonincreasing in p on [0,1/4], so a single certified point extends to the entire interval below it. The same machinery confines the positivity boundaries of A and of the strongest public state of Agarwal et al. to disjoint rational intervals separated by more than 1/25000 -- to our knowledge the first proven ordering of the positivity boundaries of two explicit competing code states. Every computational claim in the paper reduces to a finite list of big-integer comparisons, checkable by a dependency-free few-hundred-line verifier whose soundness rests on three self-contained half-page lemmas. Payloads, certificates, and verifier accompany the paper as a supplementary artifact.