Lean-13b : la borne de Tsirelson — digestion formelle de la frontière classique/quantique

Navigation : << Lean-13 Kochen-Specker · Lean-16f Free-Will · Sommaire série

Le jeu de CHSH (Clauser, Horne, Shimony, Holt 1969) fait s’affronter deux joueurs qui ne communiquent plus : Alice reçoit un bit \(x\), Bob un bit \(y\), chacun rend un bit ; ils gagnent selon la règle \(a \oplus b = x \wedge y\). Le score le plus élevé qu’ils puissent atteindre en partageant seulement du hasard classique est \(2\). En partageant un état intrigué, ils atteignent \(2\sqrt{2}\) — c’est la borne de Tsirelson (1980), la première séparation quantique/classique prouvée de l’histoire de la physique.

Ce notebook est le compagnon natif du module conway_lean/Conway/CHSHQuantum.lean : il n’expose pas la théorie « en prose », il importe le module et exécute ses énoncés dans un kernel Lean 4 réel. Le lake est la source de vérité ; le notebook est le banc d’essai.

Ce que la tranche sépare, et que ce notebook prend soin de ne pas confondre :

Statut	Contenu
prouvé localement (ce lake)	la frontière classique déterministe (`\\|score\\| ≤ 2`) et randomisée (`\\|expectedScore\\| ≤ 2`), la réécriture `(√2)^3 = 2√2`, et la séparation stricte `2 < 2√2`
importé avec preuve noyau	la borne quantique elle-même : `Mathlib.Algebra.Star.CHSH.tsirelson_inequality`, dont `tsirelson_bound` est la forme usuelle
non établi ici	la saturation de \(2\sqrt{2}\) (aucune stratégie quantique explicite dans ce lake), la construction matricielle de Pauli, l’interprétation probabiliste complète d’un état quantique, et la borne bilatérale en norme d’opérateur

Provenance : J. F. Clauser, M. A. Horne, A. Shimony, R. A. Holt, Proposed experiment to test local hidden-variable theories, Phys. Rev. Lett. 23 (1969) ; B. S. Tsirelson (Cirel’son), Quantum generalizations of Bell’s inequality, Lett. Math. Phys. 4 (1980).

1. Vérification de l’environnement

L’import ci-dessous charge les modules du lake conway_lean (compilés en .olean). Il est résolu par le LEAN_PATH du kernel : le kernel doit tourner depuis un répertoire à l’intérieur du lake, sinon il retombe sur un lake-stub vide et tous les imports échouent en silence.

Kernel de ce notebook — une divergence assumée, et mesurée. Le body de #15700 nomme le kernel lean4-wsl, comme l’ensemble de la série. Ce notebook déclare lean4-wsl-conway, qui est le même kernel plus wsl.exe --cd vers le lake WSL, ~/conway-build. La raison est mécanique : Lean-13b vit dans MyIA.AI.Notebooks/SymbolicAI/Lean/, qui n’est pas un lake (aucun lakefile.lean en remontant l’arbre). Lancé depuis ce répertoire, le kernel lean4-wsl retombe donc sur le stub ~/lean-projects/notebook_context, qui ne contient ni Conway ni Mathlib — et un kernel dans cet état ne lève pas d’erreur d’import : il répond muet (#11874). Déclarer lean4-wsl ici produirait donc un notebook dont les sorties ne sont pas reproductibles par le kernel qu’il nomme. lean4-wsl-conway est la forme qui reproduit réellement les sorties committées.

import Conway.CHSHQuantum
import Conway.CHSH
import Conway.CHSHRandomized
open Conway

import Conway.CHSHQuantum

import Conway.CHSH

import Conway.CHSHRandomized

open Conway

--% env 0

Raw input

{"cmd": "import Conway.CHSHQuantum\nimport Conway.CHSH\nimport Conway.CHSHRandomized\nopen Conway\n"}

Raw output

{"env": 0}

Interprétation. Cette cellule ne prouve rien à elle seule, et c’est le point le plus important de cette section. Les commandes import du REPL sont paresseuses : importer un module inexistant ne produit pas de message, la réponse est {"env": 0} — indiscernable d’un succès. Une sonde sans contrôle positif lit donc un kernel mort comme un kernel silencieux. La preuve d’environnement est la cellule suivante, pas celle-ci.

2. Le contrôle positif — `#eval 2 + 2`

Si le kernel tournait sur le stub, il aurait perdu jusqu’à Init : la toute première évaluation échouerait sur Unknown identifier Nat. Ce contrôle est donc le discriminant entre « le lake est résolu » et « le kernel est muet ». Tout ce qui suit ne vaut que si cette cellule rend 4.

-- Controle positif : le kernel doit rendre 4.
-- S'il rend une erreur, le lake n'est pas resolu et le reste du notebook est sans valeur.
#eval (2 : Nat) + 2

-- Controle positif : le kernel doit rendre 4.

-- S'il rend une erreur, le lake n'est pas resolu et le reste du notebook est sans valeur.

#eval (2 : Nat) + 2 4

--% env 1

Raw input

{"cmd": "-- Controle positif : le kernel doit rendre 4.\n-- S'il rend une erreur, le lake n'est pas resolu et le reste du notebook est sans valeur.\n#eval (2 : Nat) + 2\n", "env": 0}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 5},
   "data": "4"}],
 "env": 1}

Interprétation. 4. Le kernel est vivant, sa toolchain est cohérente avec celle du lake (leanprover/lean4:v4.33.0, le pin de conway_lean), et la stdlib est résolue. Les imports de la cellule 1 peuvent maintenant être tenus pour acquis — ils ne l’étaient pas.

3. Les trois bornes — tableau comparatif

Régime	Objet mathématique	Borne	Déclaration Lean	Statut de la preuve
classique déterministe	`CHSH.score a₀ a₁ b₀ b₁ : ℤ`	\(\lvert \text{score} \rvert = 2\)	`Conway.CHSH.classical_abs_score`, `classical_bound`	prouvé dans ce lake
classique randomisé	`CHSHRandomized.expectedScore μ : ℚ`	\(\lvert \mathbb{E}[\text{score}] \rvert \le 2\) sous \(\mu \ge 0\) et \(\sum_p \mu_p = 1\)	`Conway.CHSHRandomized.randomized_bound`	prouvé dans ce lake
quantique	`CHSHQuantum.chshOperator A₀ A₁ B₀ B₁`	\(\le (2\sqrt{2}) \cdot 1\)	`Conway.CHSHQuantum.tsirelson_bound`	importé de `Mathlib.Algebra.Star.CHSH.tsirelson_inequality`
séparation	\(2\) vs \(2\sqrt{2}\)	\(2 < 2\sqrt{2}\)	`Conway.CHSHQuantum.classical_quantum_gap`	prouvé dans ce lake

Deux lignes disent « prouvé dans ce lake », une dit « importé » : c’est la distinction que la grille de #13106 demande de rendre visible. La borne quantique n’est pas redémontrée ici — la redériver artificiellement aurait été un exercice d’école, pas une digestion. Ce qui est local, c’est la carte d’hypothèses : le raccord entre le vocabulaire CoursIA et les hypothèses exactes de Mathlib, la réécriture de la forme brute \(\sqrt{2}^{\,3} \cdot 1\) vers la forme usuelle \(2\sqrt{2} \cdot 1\), et la preuve que l’écart est strict.

4. Exemple guidé 1 — la signature exacte du théorème quantique

Lire une signature, c’est lire la carte de ce qu’un théorème exige. Celle de tsirelson_bound est le cœur de la tranche : elle reprend celle de Mathlib — le sens « aucune hypothèse retirée » est épinglé par l’élaboration, le sens « aucune hypothèse ajoutée » n’est gardé par aucun instrument (une reprise, pas une égalité bidirectionnelle garantie ; cf. section 7).

#check @Conway.CHSHQuantum.chshOperator
#check @Conway.CHSHQuantum.tsirelson_bound
#check @Conway.CHSHQuantum.sqrt_two_cubed
#check @Conway.CHSHQuantum.classical_quantum_gap
#check @Conway.CHSHQuantum.classical_deterministic_bound_real
#check @Conway.CHSHQuantum.classical_randomized_bound_real
#check @Conway.CHSH.classical_bound
#check @Conway.CHSHRandomized.randomized_bound

#check @Conway.CHSHQuantum.chshOperator @CHSHQuantum.chshOperator : {R : Type u_1} → [Ring R] → R → R → R → R → R

#check @Conway.CHSHQuantum.tsirelson_bound @CHSHQuantum.tsirelson_bound : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
  [StarOrderedRing R] [inst_4 : Algebra ℝ R] [IsOrderedModule ℝ R] [StarModule ℝ R] (A₀ A₁ B₀ B₁ : R),
  IsCHSHTuple A₀ A₁ B₀ B₁ → CHSHQuantum.chshOperator A₀ A₁ B₀ B₁ ≤ (2 * √2) • 1

#check @Conway.CHSHQuantum.sqrt_two_cubed CHSHQuantum.sqrt_two_cubed : √2 ^ 3 = 2 * √2

#check @Conway.CHSHQuantum.classical_quantum_gap CHSHQuantum.classical_quantum_gap : 2 < 2 * √2

#check @Conway.CHSHQuantum.classical_deterministic_bound_real CHSHQuantum.classical_deterministic_bound_real : ∀ (a₀ a₁ b₀ b₁ : CHSH.Outcome), ↑|CHSH.score a₀ a₁ b₀ b₁| ≤ 2

#check @Conway.CHSHQuantum.classical_randomized_bound_real CHSHQuantum.classical_randomized_bound_real : ∀ (μ : CHSHRandomized.Strategy),
  (∀ (p : CHSHRandomized.Profile), 0 ≤ μ p) → ∑ p, μ p = 1 → ↑|CHSHRandomized.expectedScore μ| ≤ 2

#check @Conway.CHSH.classical_bound CHSH.classical_bound : ∀ (a₀ a₁ b₀ b₁ : CHSH.Outcome), |CHSH.score a₀ a₁ b₀ b₁| ≤ 2

#check @Conway.CHSHRandomized.randomized_bound CHSHRandomized.randomized_bound : ∀ (μ : CHSHRandomized.Strategy),
  (∀ (p : CHSHRandomized.Profile), 0 ≤ μ p) → ∑ p, μ p = 1 → |CHSHRandomized.expectedScore μ| ≤ 2

--% env 2

Raw input

{"cmd": "#check @Conway.CHSHQuantum.chshOperator\n#check @Conway.CHSHQuantum.tsirelson_bound\n#check @Conway.CHSHQuantum.sqrt_two_cubed\n#check @Conway.CHSHQuantum.classical_quantum_gap\n#check @Conway.CHSHQuantum.classical_deterministic_bound_real\n#check @Conway.CHSHQuantum.classical_randomized_bound_real\n#check @Conway.CHSH.classical_bound\n#check @Conway.CHSHRandomized.randomized_bound\n", "env": 1}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 6},
   "data":
   "@CHSHQuantum.chshOperator : {R : Type u_1} → [Ring R] → R → R → R → R → R"},
  {"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "@CHSHQuantum.tsirelson_bound : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]\n  [StarOrderedRing R] [inst_4 : Algebra ℝ R] [IsOrderedModule ℝ R] [StarModule ℝ R] (A₀ A₁ B₀ B₁ : R),\n  IsCHSHTuple A₀ A₁ B₀ B₁ → CHSHQuantum.chshOperator A₀ A₁ B₀ B₁ ≤ (2 * √2) • 1"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data": "CHSHQuantum.sqrt_two_cubed : √2 ^ 3 = 2 * √2"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data": "CHSHQuantum.classical_quantum_gap : 2 < 2 * √2"},
  {"severity": "info",
   "pos": {"line": 5, "column": 0},
   "endPos": {"line": 5, "column": 6},
   "data":
   "CHSHQuantum.classical_deterministic_bound_real : ∀ (a₀ a₁ b₀ b₁ : CHSH.Outcome), ↑|CHSH.score a₀ a₁ b₀ b₁| ≤ 2"},
  {"severity": "info",
   "pos": {"line": 6, "column": 0},
   "endPos": {"line": 6, "column": 6},
   "data":
   "CHSHQuantum.classical_randomized_bound_real : ∀ (μ : CHSHRandomized.Strategy),\n  (∀ (p : CHSHRandomized.Profile), 0 ≤ μ p) → ∑ p, μ p = 1 → ↑|CHSHRandomized.expectedScore μ| ≤ 2"},
  {"severity": "info",
   "pos": {"line": 7, "column": 0},
   "endPos": {"line": 7, "column": 6},
   "data":
   "CHSH.classical_bound : ∀ (a₀ a₁ b₀ b₁ : CHSH.Outcome), |CHSH.score a₀ a₁ b₀ b₁| ≤ 2"},
  {"severity": "info",
   "pos": {"line": 8, "column": 0},
   "endPos": {"line": 8, "column": 6},
   "data":
   "CHSHRandomized.randomized_bound : ∀ (μ : CHSHRandomized.Strategy),\n  (∀ (p : CHSHRandomized.Profile), 0 ≤ μ p) → ∑ p, μ p = 1 → |CHSHRandomized.expectedScore μ| ≤ 2"}],
 "env": 2}

Interprétation. La signature de tsirelson_bound énumère sept classes de types (Ring, PartialOrder, StarRing, StarOrderedRing, Algebra ℝ, IsOrderedModule ℝ, StarModule ℝ) avant l’hypothèse IsCHSHTuple A₀ A₁ B₀ B₁, et conclut ≤ (2 * √2) • 1. Deux choses s’y lisent d’un coup d’œil :

• (smul) et non un produit : la borne est un multiple scalaire de l’unité, ce qui est la seule écriture disponible dans une algèbre étoilée ordonnée quelconque — il n’y a pas de « 2√2 » comme élément de \(R\) avant d’avoir écrit \((2\sqrt{2}) \cdot 1_R\).
√2 ^ 3 chez Mathlib, 2 * √2 ici : la forme brute est la même quantité réécrite, et c’est exactement ce que sqrt_two_cubed établit formellement — pas une simplification « à l’œil » sur un symbole.

classical_deterministic_bound_real et classical_randomized_bound_real sont les deux bornes classiques transportées dans \(\mathbb{R}\) : c’est ce transport qui rend les imports de Conway.CHSH et Conway.CHSHRandomized porteurs plutôt que décoratifs.

5. Exemple guidé 2 — les axiomes : ce que « prouvé » veut dire

Un théorème qui compile peut encore dépendre d’un axiome ajouté (sorryAx). #print axioms est la seule façon de le voir ; c’est aussi l’instrument qui permet d’affirmer « pas de sorry » sans se contenter d’un grep.

#print axioms Conway.CHSHQuantum.tsirelson_bound
#print axioms Conway.CHSHQuantum.sqrt_two_cubed
#print axioms Conway.CHSHQuantum.classical_quantum_gap
#print axioms Conway.CHSHQuantum.classical_deterministic_bound_real
#print axioms Conway.CHSHQuantum.classical_randomized_bound_real

#print axioms Conway.CHSHQuantum.tsirelson_bound 'Conway.CHSHQuantum.tsirelson_bound' depends on axioms: [propext, Classical.choice, Quot.sound]

#print axioms Conway.CHSHQuantum.sqrt_two_cubed 'Conway.CHSHQuantum.sqrt_two_cubed' depends on axioms: [propext, Classical.choice, Quot.sound]

#print axioms Conway.CHSHQuantum.classical_quantum_gap 'Conway.CHSHQuantum.classical_quantum_gap' depends on axioms: [propext, Classical.choice, Quot.sound]

#print axioms Conway.CHSHQuantum.classical_deterministic_bound_real 'Conway.CHSHQuantum.classical_deterministic_bound_real' depends on axioms: [propext, Classical.choice, Quot.sound]

#print axioms Conway.CHSHQuantum.classical_randomized_bound_real 'Conway.CHSHQuantum.classical_randomized_bound_real' depends on axioms: [propext, Classical.choice, Quot.sound]

--% env 3

Raw input

{"cmd": "#print axioms Conway.CHSHQuantum.tsirelson_bound\n#print axioms Conway.CHSHQuantum.sqrt_two_cubed\n#print axioms Conway.CHSHQuantum.classical_quantum_gap\n#print axioms Conway.CHSHQuantum.classical_deterministic_bound_real\n#print axioms Conway.CHSHQuantum.classical_randomized_bound_real\n", "env": 2}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 6},
   "data":
   "'Conway.CHSHQuantum.tsirelson_bound' depends on axioms: [propext, Classical.choice, Quot.sound]"},
  {"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "'Conway.CHSHQuantum.sqrt_two_cubed' depends on axioms: [propext, Classical.choice, Quot.sound]"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "'Conway.CHSHQuantum.classical_quantum_gap' depends on axioms: [propext, Classical.choice, Quot.sound]"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data":
   "'Conway.CHSHQuantum.classical_deterministic_bound_real' depends on axioms: [propext, Classical.choice, Quot.sound]"},
  {"severity": "info",
   "pos": {"line": 5, "column": 0},
   "endPos": {"line": 5, "column": 6},
   "data":
   "'Conway.CHSHQuantum.classical_randomized_bound_real' depends on axioms: [propext, Classical.choice, Quot.sound]"}],
 "env": 3}

Interprétation. Les cinq déclarations dépendent de [propext, Classical.choice, Quot.sound] — les trois axiomes standard de Lean et de Mathlib, et pas de sorryAx. C’est la mesure qui autorise la phrase « aucune preuve admise » : un théorème dont le corps contiendrait sorry afficherait sorryAx dans cette liste.

Une réserve d’instrument, qu’il faut connaître : #print axioms est contaminé par une erreur d’élaboration. Si le module ne compile pas, Lean admet l’énoncé et l’instrument affiche sorryAx — un théorème parfaitement prouvé peut donc paraître dépendre de sorry. La mesure n’est valide que sur un module qui compile sans erreur ; lake build Conway.CHSHQuantum doit être vert avant qu’on lise cette sortie.

6. Exemple guidé 3 — la frontière classique, mesurée sur les valeurs

La borne classique est atteinte, et c’est ce qui en fait une frontière et non une simple majoration lâche. Les valeurs ci-dessous sont calculées par le noyau, pas recopiées.

#eval Conway.CHSH.Outcome.positive.value
#eval Conway.CHSH.Outcome.negative.value
#eval Conway.CHSH.score .positive .positive .positive .positive
#eval Conway.CHSH.score .positive .negative .positive .negative
#eval Conway.CHSHRandomized.expectedScore (Conway.CHSHRandomized.dirac Conway.CHSHRandomized.pPos)
#eval Conway.CHSHRandomized.expectedScore Conway.CHSHRandomized.balancedMix

#eval Conway.CHSH.Outcome.positive.value 1

#eval Conway.CHSH.Outcome.negative.value -1

#eval Conway.CHSH.score .positive .positive .positive .positive 2

#eval Conway.CHSH.score .positive .negative .positive .negative -2

#eval Conway.CHSHRandomized.expectedScore (Conway.CHSHRandomized.dirac Conway.CHSHRandomized.pPos) 2

#eval Conway.CHSHRandomized.expectedScore Conway.CHSHRandomized.balancedMix 0

--% env 4

Raw input

{"cmd": "#eval Conway.CHSH.Outcome.positive.value\n#eval Conway.CHSH.Outcome.negative.value\n#eval Conway.CHSH.score .positive .positive .positive .positive\n#eval Conway.CHSH.score .positive .negative .positive .negative\n#eval Conway.CHSHRandomized.expectedScore (Conway.CHSHRandomized.dirac Conway.CHSHRandomized.pPos)\n#eval Conway.CHSHRandomized.expectedScore Conway.CHSHRandomized.balancedMix\n", "env": 3}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 5},
   "data": "1"},
  {"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 5},
   "data": "-1"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 5},
   "data": "2"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 5},
   "data": "-2"},
  {"severity": "info",
   "pos": {"line": 5, "column": 0},
   "endPos": {"line": 5, "column": 5},
   "data": "2"},
  {"severity": "info",
   "pos": {"line": 6, "column": 0},
   "endPos": {"line": 6, "column": 5},
   "data": "0"}],
 "env": 4}

Interprétation. Les deux valeurs d’un résultat sont \(\pm 1\) (Outcome.value), et le score du profil tout-positif vaut \(2\) : la borne \(|\text{score}| \le 2\) est donc saturée par une stratégie déterministe — impossible de faire mieux sans intrication, et c’est précisément ce que la borne quantique contredit. Le profil mixte rend \(-2\) : la symétrie \(\text{score}(a, \bar a, b, \bar b) = -\text{score}(a,a,b,b)\) est visible à l’écran.

Le mélange équilibré balancedMix (moitié pPos, moitié pNeg) rend une espérance de \(0\) : mélanger deux stratégies déterministes de scores opposés annule le score sans jamais le pousser au-delà de \(2\) en valeur absolue. C’est le sens du théorème randomized_bound : le hasard classique ne fait pas sortir de l’intervalle \([-2, 2]\).

7. Ce que cette tranche n’établit pas

Nommer les limites fait partie du livrable. Rien de ce qui suit n’est prouvé dans ce lake :

La saturation de \(2\sqrt{2}\). Le lake prouve la borne \(\le 2\sqrt{2}\), jamais son atteinte : il n’expose aucune stratégie quantique, aucun état intrigué et aucun observable qui réaliseraient \(2\sqrt{2}\) sur le jeu de CHSH. La borne est un plafond, pas un maximum démontré.
La construction matricielle. Aucun opérateur de Pauli, aucune matrice \(2 \times 2\) : IsCHSHTuple est une structure algébrique abstraite, pas une réalisation physique.
L’interprétation probabiliste complète. Le lien entre un état quantique, des observables et une distribution de réponses mesurées n’est pas formalisé ici.
La borne bilatérale en norme d’opérateur. L’énoncé est une inégalité dans un ordre partiel d’algèbre étoilée ordonnée, pas un énoncé de norme.
La carte d’hypothèses n’est pas une égalité garantie. Le module reprend les hypothèses de Mathlib. Le sens « aucune hypothèse retirée » est épinglé par l’élaboration (durcir la signature amont ferait échouer la preuve, donc rouge) ; le sens « aucune hypothèse ajoutée » n’est gardé par aucun instrument — un affaiblissement amont laisserait le théorème compiler avec une hypothèse devenue superflue, en silence. La liste est énoncée comme une reprise, jamais comme une égalité vérifiée.

La difficulté réelle de la preuve amont mérite d’être dite : la démonstration de Tsirelson dans Mathlib n’est pas une manipulation d’inégalités triangulaires, c’est une somme de carrés (SOS) — on exhibe une décomposition positive de \(2\sqrt{2} \cdot 1 - \text{chshOperator}\). C’est cette structure qui explique pourquoi l’énoncé a besoin d’un anneau étoilé ordonné (StarOrderedRing) : sans ordre compatible avec l’involution, il n’y a pas de positivité à invoquer. Reconstruire cette preuve est un travail de formalisation à part entière ; ce notebook en consomme le résultat, il ne le refait pas.

8. Exercices

Trois exercices bornés pour manipuler les objets du lake. Chaque cellule s’exécute telle quelle (corps trivial) : à vous de remplacer le corps par la bonne définition. Les #eval de contrôle affichent côte à côte votre valeur et celle du lake.

Exercice 1 — le profile est-il maximal ?

Définissez estMaximal renvoyant true si et seulement si le score du profil vaut exactement \(2\) (le maximum classique). Le corps actuel renvoie true en toutes circonstances : sur les profils de score négatif, votre valeur et celle du lake divergeront — c’est le test.

-- Exercice 1 : le profil atteint-il le maximum classique (score = 2) ?
-- TODO etudiant : remplacer le corps ci-dessous
def estMaximal (a₀ a₁ b₀ b₁ : Conway.CHSH.Outcome) : Bool :=
  true

-- Doivent valoir true, true, false (le lake rend 2, 2, -2)
#eval estMaximal .positive .positive .positive .positive
#eval estMaximal .positive .negative .negative .positive
#eval estMaximal .positive .negative .positive .negative
-- Les scores correspondants, calcules par le lake
#eval Conway.CHSH.score .positive .positive .positive .positive
#eval Conway.CHSH.score .positive .negative .negative .positive
#eval Conway.CHSH.score .positive .negative .positive .negative

-- Exercice 1 : le profil atteint-il le maximum classique (score = 2) ?

-- TODO etudiant : remplacer le corps ci-dessous

def estMaximal (a₀ a₁ b₀ b₁ : Conway.CHSH.Outcome) : Bool :=🟨 Variable name `a₀` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 Variable name `a₁` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 Variable name `b₀` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 Variable name `b₁` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`

  true

-- Doivent valoir true, true, false (le lake rend 2, 2, -2)

#eval estMaximal .positive .positive .positive .positive true

#eval estMaximal .positive .negative .negative .positive true

#eval estMaximal .positive .negative .positive .negative true

-- Les scores correspondants, calcules par le lake

#eval Conway.CHSH.score .positive .positive .positive .positive 2

#eval Conway.CHSH.score .positive .negative .negative .positive 2

#eval Conway.CHSH.score .positive .negative .positive .negative -2

--% env 5

Raw input

{"cmd": "-- Exercice 1 : le profil atteint-il le maximum classique (score = 2) ?\n-- TODO etudiant : remplacer le corps ci-dessous\ndef estMaximal (a\u2080 a\u2081 b\u2080 b\u2081 : Conway.CHSH.Outcome) : Bool :=\n  true\n\n-- Doivent valoir true, true, false (le lake rend 2, 2, -2)\n#eval estMaximal .positive .positive .positive .positive\n#eval estMaximal .positive .negative .negative .positive\n#eval estMaximal .positive .negative .positive .negative\n-- Les scores correspondants, calcules par le lake\n#eval Conway.CHSH.score .positive .positive .positive .positive\n#eval Conway.CHSH.score .positive .negative .negative .positive\n#eval Conway.CHSH.score .positive .negative .positive .negative\n", "env": 4}

Raw output

{"messages":
 [{"severity": "warning",
   "pos": {"line": 3, "column": 16},
   "endPos": {"line": 3, "column": 18},
   "data":
   "Variable name `a₀` is not explicitly referenced.\n\nThe binding can be removed (if unused) or named `_` (if used implicitly).\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"},
  {"severity": "warning",
   "pos": {"line": 3, "column": 19},
   "endPos": {"line": 3, "column": 21},
   "data":
   "Variable name `a₁` is not explicitly referenced.\n\nThe binding can be removed (if unused) or named `_` (if used implicitly).\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"},
  {"severity": "warning",
   "pos": {"line": 3, "column": 22},
   "endPos": {"line": 3, "column": 24},
   "data":
   "Variable name `b₀` is not explicitly referenced.\n\nThe binding can be removed (if unused) or named `_` (if used implicitly).\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"},
  {"severity": "warning",
   "pos": {"line": 3, "column": 25},
   "endPos": {"line": 3, "column": 27},
   "data":
   "Variable name `b₁` is not explicitly referenced.\n\nThe binding can be removed (if unused) or named `_` (if used implicitly).\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"},
  {"severity": "info",
   "pos": {"line": 7, "column": 0},
   "endPos": {"line": 7, "column": 5},
   "data": "true"},
  {"severity": "info",
   "pos": {"line": 8, "column": 0},
   "endPos": {"line": 8, "column": 5},
   "data": "true"},
  {"severity": "info",
   "pos": {"line": 9, "column": 0},
   "endPos": {"line": 9, "column": 5},
   "data": "true"},
  {"severity": "info",
   "pos": {"line": 11, "column": 0},
   "endPos": {"line": 11, "column": 5},
   "data": "2"},
  {"severity": "info",
   "pos": {"line": 12, "column": 0},
   "endPos": {"line": 12, "column": 5},
   "data": "2"},
  {"severity": "info",
   "pos": {"line": 13, "column": 0},
   "endPos": {"line": 13, "column": 5},
   "data": "-2"}],
 "env": 5}

Exercice 2 — reconstruire le score à la main

Le score de CHSH s’obtient par A₀·B₀ + A₀·B₁ + A₁·B₀ - A₁·B₁, où chaque résultat vaut \(\pm 1\) (Conway.CHSH.Outcome.value). Réimplémentez-le sans appeler CHSH.score.

-- Exercice 2 : score de CHSH reconstruit depuis Outcome.value
-- TODO etudiant : remplacer le corps ci-dessous
def scoreManuel (a₀ a₁ b₀ b₁ : Conway.CHSH.Outcome) : Int :=
  0

-- Doivent donner les memes valeurs que CHSH.score
#eval scoreManuel .positive .positive .positive .positive
#eval Conway.CHSH.score .positive .positive .positive .positive
#eval scoreManuel .positive .negative .positive .negative
#eval Conway.CHSH.score .positive .negative .positive .negative
#eval scoreManuel .negative .negative .positive .positive
#eval Conway.CHSH.score .negative .negative .positive .positive

-- Exercice 2 : score de CHSH reconstruit depuis Outcome.value

-- TODO etudiant : remplacer le corps ci-dessous

def scoreManuel (a₀ a₁ b₀ b₁ : Conway.CHSH.Outcome) : Int :=🟨 Variable name `a₀` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 Variable name `a₁` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 Variable name `b₀` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 Variable name `b₁` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`

-- Doivent donner les memes valeurs que CHSH.score

#eval scoreManuel .positive .positive .positive .positive 0

#eval Conway.CHSH.score .positive .positive .positive .positive 2

#eval scoreManuel .positive .negative .positive .negative 0

#eval Conway.CHSH.score .positive .negative .positive .negative -2

#eval scoreManuel .negative .negative .positive .positive 0

#eval Conway.CHSH.score .negative .negative .positive .positive -2

--% env 6

Raw input

{"cmd": "-- Exercice 2 : score de CHSH reconstruit depuis Outcome.value\n-- TODO etudiant : remplacer le corps ci-dessous\ndef scoreManuel (a\u2080 a\u2081 b\u2080 b\u2081 : Conway.CHSH.Outcome) : Int :=\n  0\n\n-- Doivent donner les memes valeurs que CHSH.score\n#eval scoreManuel .positive .positive .positive .positive\n#eval Conway.CHSH.score .positive .positive .positive .positive\n#eval scoreManuel .positive .negative .positive .negative\n#eval Conway.CHSH.score .positive .negative .positive .negative\n#eval scoreManuel .negative .negative .positive .positive\n#eval Conway.CHSH.score .negative .negative .positive .positive\n", "env": 5}

Raw output

{"messages":
 [{"severity": "warning",
   "pos": {"line": 3, "column": 17},
   "endPos": {"line": 3, "column": 19},
   "data":
   "Variable name `a₀` is not explicitly referenced.\n\nThe binding can be removed (if unused) or named `_` (if used implicitly).\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"},
  {"severity": "warning",
   "pos": {"line": 3, "column": 20},
   "endPos": {"line": 3, "column": 22},
   "data":
   "Variable name `a₁` is not explicitly referenced.\n\nThe binding can be removed (if unused) or named `_` (if used implicitly).\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"},
  {"severity": "warning",
   "pos": {"line": 3, "column": 23},
   "endPos": {"line": 3, "column": 25},
   "data":
   "Variable name `b₀` is not explicitly referenced.\n\nThe binding can be removed (if unused) or named `_` (if used implicitly).\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"},
  {"severity": "warning",
   "pos": {"line": 3, "column": 26},
   "endPos": {"line": 3, "column": 28},
   "data":
   "Variable name `b₁` is not explicitly referenced.\n\nThe binding can be removed (if unused) or named `_` (if used implicitly).\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"},
  {"severity": "info",
   "pos": {"line": 7, "column": 0},
   "endPos": {"line": 7, "column": 5},
   "data": "0"},
  {"severity": "info",
   "pos": {"line": 8, "column": 0},
   "endPos": {"line": 8, "column": 5},
   "data": "2"},
  {"severity": "info",
   "pos": {"line": 9, "column": 0},
   "endPos": {"line": 9, "column": 5},
   "data": "0"},
  {"severity": "info",
   "pos": {"line": 10, "column": 0},
   "endPos": {"line": 10, "column": 5},
   "data": "-2"},
  {"severity": "info",
   "pos": {"line": 11, "column": 0},
   "endPos": {"line": 11, "column": 5},
   "data": "0"},
  {"severity": "info",
   "pos": {"line": 12, "column": 0},
   "endPos": {"line": 12, "column": 5},
   "data": "-2"}],
 "env": 6}

Exercice 3 — lire la borne dans le théorème

Lisez Conway.CHSH.classical_bound, puis déclarez l’entier \(B\) tel que \(\lvert \text{score} \rvert \le B\) pour tout profil — la borne que le théorème garantit, en valeur absolue. Expliquez ensuite en commentaire pourquoi la borne quantique, elle, ne peut pas s’écrire comme un entier de cette façon.

-- Exercice 3 : la borne absolue garantie par Conway.CHSH.classical_bound
-- TODO etudiant : remplacer le corps ci-dessous
def borneAbsolueClassique : Int :=
  0

-- Doit valoir 2
#eval borneAbsolueClassique

-- TODO etudiant (commentaire) : pourquoi 2*sqrt(2) n'a pas d'equivalent entier ici ?

-- Exercice 3 : la borne absolue garantie par Conway.CHSH.classical_bound

-- TODO etudiant : remplacer le corps ci-dessous

def borneAbsolueClassique : Int :=

-- Doit valoir 2

#eval borneAbsolueClassique 0

-- TODO etudiant (commentaire) : pourquoi 2*sqrt(2) n'a pas d'equivalent entier ici ?

--% env 7

Raw input

{"cmd": "-- Exercice 3 : la borne absolue garantie par Conway.CHSH.classical_bound\n-- TODO etudiant : remplacer le corps ci-dessous\ndef borneAbsolueClassique : Int :=\n  0\n\n-- Doit valoir 2\n#eval borneAbsolueClassique\n\n-- TODO etudiant (commentaire) : pourquoi 2*sqrt(2) n'a pas d'equivalent entier ici ?\n", "env": 6}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 7, "column": 0},
   "endPos": {"line": 7, "column": 5},
   "data": "0"}],
 "env": 7}

9. Provenance, raccords et conclusion

Ce qui a été exécuté. Les huit cellules de code ci-dessus ont été exécutées par le kernel Lean 4 (lean4-wsl-conway, --cd ~/conway-build) sur le lake conway_lean, au pin leanprover/lean4:v4.32.1 à l’exécution de ces sorties (le lake au HEAD pinne v4.33.0 depuis la migration #16341). Les sorties sont celles du noyau : #check, #print axioms et #eval sont rendus par le REPL, aucune sortie n’a été écrite à la main.

Chaîne de dépendance, telle qu’elle se lit dans les sorties. tsirelson_bound n’est pas une redémonstration : elle applique Mathlib.Algebra.Star.CHSH.tsirelson_inequality, réécrit √2 ^ 3 en 2 * √2 par sqrt_two_cubed, et change l’écriture de l’opérateur CHSH par chshOperator. Les trois axiomes affichés (propext, Classical.choice, Quot.sound) sont ceux de Mathlib — la chaîne est donc transparente : à aucun étage on n’admet ce qu’on prétend prouver.

Raccords dans la série.

Lean-13 Kochen-Specker — la contextualité : KS montre qu’aucune valuation non contextuelle ne reproduit les prédictions quantiques. CHSH en est le pendant statistique, sous forme d’inégalité testable entre deux joueurs séparés.
Lean-16f Free-Will — la liberté : le théorème de Conway–Kochen (2006) montre que le déterminisme et la liberté du choix des mesures sont incompatibles avec l’accord quantique. C’est l’hypothèse même que le jeu de CHSH met à l’épreuve expérimentale.
Conway/CHSH.lean et Conway/CHSHRandomized.lean — les bornes classiques que la borne quantique contredit, prouvées dans ce même lake.

Ce que la tranche laisse ouvert, et qui reste à faire pour clore #13106 : la saturation de \(2\sqrt{2}\) par une stratégie quantique explicite, la réalisation matricielle (Pauli), et la borne bilatérale en norme d’opérateur. Aucune de ces trois n’est prouvée ici, et aucune n’est simulée par un exemple scalaire de remplacement.

Retour au sommet

1. Vérification de l’environnement

2. Le contrôle positif — #eval 2 + 2

3. Les trois bornes — tableau comparatif

4. Exemple guidé 1 — la signature exacte du théorème quantique

5. Exemple guidé 2 — les axiomes : ce que « prouvé » veut dire

6. Exemple guidé 3 — la frontière classique, mesurée sur les valeurs

7. Ce que cette tranche n’établit pas

8. Exercices

Exercice 1 — le profile est-il maximal ?

Exercice 2 — reconstruire le score à la main

Exercice 3 — lire la borne dans le théorème

9. Provenance, raccords et conclusion

2. Le contrôle positif — `#eval 2 + 2`