Renou et al. (2021) showed that real and complex quantum theory can be told apart in a network with two independent sources: a Bell-type quantity T reaches 6√2 in complex quantum theory, while real quantum theory with independent sources obeys T ≲ 7.66. We narrow the real-theory value from both sides. (i) An explicit real strategy with independent sources reaches T = 4√3 ≈ 6.9282 exactly; the value is verified in Lean. (ii) T ≤ 7.6568542496 for real quantum theory, below the published 7.6605: an exact integer certificate, accepted by a checker whose soundness is proved in Lean, bounds a symmetry-reduced semidefinite relaxation, and a written proof shows every real strategy with independent sources is feasible for it. (iii) With two measurements for Alice, T ≤ 7.1927385035 for all strategies with independent sources, real or complex, by a scalar-extended two-copy inflation; a single shared source reaches 2+4√2 there. (iv) Explicit hidden cross-source correlations that let a real description exceed the bound, with thresholds of 0.56, 0.50 and 0.47 bit for three constructions. An explicit point shows that this relaxation cannot give less than 2+4√2, so its value is fixed to within 1.3e-11. The optimal real value remains open in [4√3, 7.6568542496]. The deposit contains the note, the certificates (text and binary), a dependency-free Python checker, the Lean sources of the proved checker and of the strategy's value, and the scripts that build, export and attack the certificates. Version 3: the real-theory bound is tightened from 7.6568542701 to 7.6568542496 (a certificate of the same kind on a more accurate solve; the earlier certificate is kept), and an explicit point of the relaxation at exactly 2+4√2 is added. Nothing stated in versions 1 and 2 is withdrawn. Version 2 had made the archive's Lean folders complete Lake projects.
Renou et al. (2021) showed that real and complex quantum theory can be told apart in a network with two independent sources: a Bell-type quantity T reaches 6√2 in complex quantum theory, while real quantum theory with independent sources obeys T ≲ 7.66. We narrow the real-theory value from both sides. (i) An explicit real strategy with independent sources reaches T = 4√3 ≈ 6.9282 exactly; the value is verified in Lean. (ii) T ≤ 7.6568542496 for real quantum theory, below the published 7.6605: an exact integer certificate, accepted by a checker whose soundness is proved in Lean, bounds a symmetry-reduced semidefinite relaxation, and a written proof shows every real strategy with independent sources is feasible for it. (iii) With two measurements for Alice, T ≤ 7.1927385035 for all strategies with independent sources, real or complex, by a scalar-extended two-copy inflation; a single shared source reaches 2+4√2 there. (iv) Explicit hidden cross-source correlations that let a real description exceed the bound, with thresholds of 0.56, 0.50 and 0.47 bit for three constructions. An explicit point shows that this relaxation cannot give less than 2+4√2, so its value is fixed to within 1.3e-11. The optimal real value remains open in [4√3, 7.6568542496]. The deposit contains the note, the certificates (text and binary), a dependency-free Python checker, the Lean sources of the proved checker and of the strategy's value, and the scripts that build, export and attack the certificates. Version 3: the real-theory bound is tightened from 7.6568542701 to 7.6568542496 (a certificate of the same kind on a more accurate solve; the earlier certificate is kept), and an explicit point of the relaxation at exactly 2+4√2 is added. Nothing stated in versions 1 and 2 is withdrawn. Version 2 had made the archive's Lean folders complete Lake projects.
The role of complex quantities in quantum theory has been puzzling physicists since the beginnings. It is, thus, natural to ask whether, in order to describe our experiments, the mathematical structure of the complex Hilbert spaces it is built on is really necessary. Recently, it was shown that this structure is inevitable in network scenarios with independent sources. More precisely, Real Quantum Theory cannot explain the predictions of (Complex) Quantum Theory [Renou et al., Nature (London) 600, 625 (2021).NATUAS0028-083610.1038/s41586-021-04160-4]. Here, we revisit the independence assumption underlying this work. We show that assuming partial independence is sufficient for showing the inadequacy of Real Quantum Theory. We derive a tradeoff between source independence and the Bell value achievable in Real Quantum Theory, which also lower bounds the source correlations required to explain previous experiments by means of real quantum systems. We further show that 1 bit of entanglement is necessary and sufficient for recovering the complex quantum correlations by means of Real Quantum Theory in the scenario from [Renou et al., Nature (London) 600, 625 (2021).NATUAS0028-083610.1038/s41586-021-04160-4]. Finally, building on [McKague et al., Phys. Rev. Lett. 102, 2009PRLTAO0031-900710.1103/PhysRevLett.102.020505], we provide a construction to simulate any complex quantum setup with m independent sources by means of Real Quantum Theory by allowing the sources to share an m real-qubit entangled state in the first round of the experiment.
The question of whether complex numbers play a fundamental role in quantum theory has been debated since the inception of quantum mechanics. Recently, a feasible proposal to differentiate between real and complex quantum theories based on the technique of testing Bell nonlocalities has emerged [Renou et al., Nature (London) 600, 625 (2021)]. Based on this method, the real quantum theory has been falsified experimentally in both photonic and superconducting quantum systems [Li et al., Phys. Rev. Lett. 128, 040402 (2022); Chen, et al., Phys. Rev. Lett. 128, 040403 (2022)]. The quantum networks with multiple independent sources which are not causally connected have gained significant interest as they offer a new perspective on studying the nonlocalities. The independence of these sources imposes additional constraints on observable covariances and leads to new bounds for classical and quantum correlations. In this study, we examine the discrimination between the real and complex quantum theories with an entanglement swapping scenario under a stronger assumption that the two sources are causally independent, which was not made in previous works. Using a revised Navasc\'ues-Pironio-Ac\'{\i}n method and Bayesian optimization, we find a proposal with optimal coefficients of the correlation function which could give a larger discrimination between the real and quantum theories compared with the existing proposals. This work opens up avenues for further exploration of the discrimination between real and complex quantum theories within intricate quantum networks featuring causally independent parties.
Whether the complex numbers of standard quantum theory are experimentally indispensable has remained open for decades. Real quantum theory (RQT), obtained by replacing complex amplitudes with real ones while retaining the usual Kronecker-product composition rule, reproduces all single-party and bipartite Bell correlations of quantum theory (QT), but its lack of local tomography suggested that the two theories might diverge in more general local experiments. This possibility appeared to be confirmed by Renou et al., who argued that a bilocal network experiment can falsify RQT without falsifying QT. Here we show that this conclusion relies on an experimentally untestable assumption. The key distinction is between product-state independence, which constrains the mathematical form of source states, and operational independence, which is defined entirely by the absence of observable cross-source correlations. We prove that, once source independence is imposed operationally, every finite network correlation achievable in QT is also achievable in RQT with the same locality structure of the measurements. We then extend this equivalence to arbitrary finite sequential multipartite protocols involving channels and measurements with prescribed locality structure. Thus, as long as no violation of QT is observed, RQT cannot be experimentally falsified. Our results restore the empirical indistinguishability of QT and RQT, while showing that they support markedly different pictures of the correlation structure underlying the same observed world.
The best known lower bound for the minimum Kochen-Specker vector system in R3 -- 24 vectors -- rests on a computational proof whose combinatorial half emits DRAT proofs but whose geometric half does not: the non-embeddability of thousands of candidate graphs is established by Z3's nonlinear real arithmetic, which produces no checkable proof objects. We close this gap for the proof's blocking database. We introduce exact rational case-tree certificates of real non-embeddability, whose splits are polynomial factorizations and rational sum-of-squares decompositions and whose leaves are discharged by injectivity, ideal-membership, or Positivstellensatz-shaped positivity arguments, and we certify all 291 source lines (180 distinct graphs) of the published pipeline's order-10 to order-13 blocking lists. Certificates are replayed by two independent checkers that share no code with the generator: a pure-Python replay over exact fractions, and a total checker implemented and proved sound in Lean 4. The soundness theorem -- acceptance implies that no injective-on-rays, orthogonality-respecting assignment of nonzero real vectors realizes the graph -- is kernel-checked with axiom closure {propext, Classical.choice, Quot.sound}, and a gcd-free rational arithmetic layer makes the entire verdict computation kernel-reducible, so each per-graph non-embeddability result is a closed kernel theorem proved by decide. The formalization surfaced findings about the published pipeline, including a load-bearing injectivity side condition in its embeddability notion, hidden WLOG case obligations invisible to Z3-based workflows, and an unreproducible candidate count that we resolve against the published artifacts. All certificates, checkers, and proofs are available and replayable from a single build.
The 2022 superconducting-qubit experiment by USTC (Chen et al., PRL 128, 040403) reported a 43σ violation of the “real-number bound” in a three-party entanglement-swapping network, widely interpreted as decisive evidence that complex numbers are indispensable in quantum mechanics.Here we show that Real Geometric Quantum Mechanics (RGQM)—a formulation defined purely on real differential geometry (curvature, torsion, holonomy) of ℝ^{2𝑁} and containing no imaginary unit—reproduces the experimental result, T_exp = 8.09, with matching precision, 𝑇_RGQM = 8.08 without introducing any free parameters.The sole input is the independently measured Bell-state-measurement (BSM) fidelity 𝑓 = 0.952. In RGQM, each entanglement source creates an SO(2) torsion plane in ℝ^8.The BSM corresponds to a parallel-transport loop 𝛾 that couples these planes, and the observed nonlocal correlations arise from the resulting holonomy 𝑈(𝛾) ∈ SO(8).The two torsion planes contribute independent 2𝜋 holonomies, giving a total geometric phase of 4𝜋, which is the geometric origin of the theoretical maximum 𝑇_max = 8.485. The remarkable agreement between the experiment and the parameter-free RGQM prediction shows that complex numbers are not fundamental physical ingredients, but compact symbols for real geometric rotations. Version 3 description: Correction of numerical values. The values for the nonlocal correlation functional (T) and the Bell-state measurement fidelity (f) have been corrected to align with the experimental data reported by Chen et al. (Phys. Rev. Lett. 128, 040403). The previous version contained incorrect scaling factors (𝑇_max = 13.93 instead of 8.485). The theoretical conclusion remains unchanged.
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.