A formalization of the CHSH inequality and Tsirelson's upper-bound in Isabelle/HOL

• URL: http://arxiv.org/abs/2306.12535v1
• Date: Wed, 21 Jun 2023 19:49:42 GMT
• Title: A formalization of the CHSH inequality and Tsirelson's upper-bound in Isabelle/HOL
• Authors: Mnacho Echenim and Mehdi Mhalla
• Abstract summary: We present a formalization of several fundamental notions and results from Quantum Information theory. The proof of the latter result is based on the so-called CHSH inequality, and it is the violation of this inequality that was experimentally evidenced by Aspect. We also formalize various results related to the violation of the CHSH inequality, such as Tsirelson's bound which permits to obtain the maximum violation of this inequality in a quantum setting.
• Score: 2.817412580574242
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We present a formalization of several fundamental notions and results from Quantum Information theory, including density matrices and projective measurements, along with the proof that the local hidden-variable hypothesis advocated by Einstein to model quantum mechanics cannot hold. The proof of the latter result is based on the so-called CHSH inequality, and it is the violation of this inequality that was experimentally evidenced by Aspect who earned the Nobel Prize in 2022 for his work. We also formalize various results related to the violation of the CHSH inequality, such as Tsirelson's bound which permits to obtain the maximum violation of this inequality in a quantum setting.

Related papers

• An inconsistency in the CHSH inequality [0.0]
  Violation of the CHSH inequality supposedly demonstrates an irreconcilable conflict between quantum mechanics and local, realistic hidden variable theories. We show that the mathematical assumptions underlying the proof of the CHSH inequality are, in fact, incompatible with the physics of the experiments testing such inequality.
  arXiv  Detail & Related papers  (2024-09-02T14:12:26Z)
• Testing trajectory-based determinism via time probability distributions [44.99833362998488]
  Bohmian mechanics (BM) has inherited more predictive power than quantum mechanics (QM) We introduce a prescription for constructing a flight-time probability distribution within generic trajectory-equipped theories. We derive probability distributions that are unreachable by QM.
  arXiv  Detail & Related papers  (2024-04-15T11:36:38Z)
• Coherence generation with Hamiltonians [44.99833362998488]
  We explore methods to generate quantum coherence through unitary evolutions. This quantity is defined as the maximum derivative of coherence that can be achieved by a Hamiltonian. We identify the quantum states that lead to the largest coherence derivative induced by the Hamiltonian.
  arXiv  Detail & Related papers  (2024-02-27T15:06:40Z)
• What in fact proves the violation of the Bell-type inequalities? [0.0]
  In a measurement in which some variables are tested, other variables, not tested, have no defined value. It is proved that the correct conclusion of the violation of the CHSH inequality is different.
  arXiv  Detail & Related papers  (2023-03-15T10:36:32Z)
• Work statistics, quantum signatures and enhanced work extraction in quadratic fermionic models [62.997667081978825]
  In quadratic fermionic models we determine a quantum correction to the work statistics after a sudden and a time-dependent driving. Such a correction lies in the non-commutativity of the initial quantum state and the time-dependent Hamiltonian. Thanks to the latter, one can assess the onset of non-classical signatures in the KDQ distribution of work.
  arXiv  Detail & Related papers  (2023-02-27T13:42:40Z)
• Quantum Fluctuation-Response Inequality and Its Application in Quantum Hypothesis Testing [6.245537312562826]
  We find a bound for the mean difference of an observable at two different quantum states. When the spectrum of the observable is bounded, the sub-Gaussian property is used to link the bound with the sub-Gaussian norm of the observable. We show the versatility of our results by their applications in problems like thermodynamic inference and speed limit.
  arXiv  Detail & Related papers  (2022-03-20T09:10:54Z)
• Leggett-Garg inequalities in the quantum field theory of neutrino oscillations [0.0]
  This finding relates temporal nonclassicality to quantum uncertainty. We show that Leggett-Garg inequalities are violated more strongly in quantum field theory than in quantum mechanics.
  arXiv  Detail & Related papers  (2021-11-18T23:47:07Z)
• Non-equilibrium stationary states of quantum non-Hermitian lattice models [68.8204255655161]
  We show how generic non-Hermitian tight-binding lattice models can be realized in an unconditional, quantum-mechanically consistent manner. We focus on the quantum steady states of such models for both fermionic and bosonic systems.
  arXiv  Detail & Related papers  (2021-03-02T18:56:44Z)
• Entanglement in Cognition violating Bell Inequalities Beyond Cirel'son's Bound [0.0]
  We present the results of two tests where a sample of human participants were asked to make judgements about conceptual combinations. Both tests significantly violate the Clauser-Horne-Shimony-Holt version of Bell inequalities (CHSH inequality') We show that the observed violations of the CHSH inequality can be explained as a consequence of a strong form of quantum entanglement' between the component conceptual entities.
  arXiv  Detail & Related papers  (2021-02-07T16:57:59Z)
• Quantum Mechanical description of Bell's experiment assumes Locality [91.3755431537592]
  Bell's experiment description assumes the (Quantum Mechanics-language equivalent of the classical) condition of Locality. This result is complementary to a recently published one demonstrating that non-Locality is necessary to describe said experiment. It is concluded that, within the framework of Quantum Mechanics, there is absolutely no reason to believe in the existence of non-Local effects.
  arXiv  Detail & Related papers  (2020-02-27T15:04:08Z)
• Bell's theorem for trajectories [62.997667081978825]
  A trajectory is not an outcome of a quantum measurement, in the sense that there is no observable associated with it. We show how to overcome this problem by considering a special case of our generic inequality that can be experimentally tested point-by-point in time.
  arXiv  Detail & Related papers  (2020-01-03T01:40:44Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.