diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-13b-CHSH-Tsirelson-Native.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-13b-CHSH-Tsirelson-Native.ipynb new file mode 100644 index 0000000000..932da45153 --- /dev/null +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-13b-CHSH-Tsirelson-Native.ipynb @@ -0,0 +1,1696 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "id": "3666be08", + "metadata": { + "papermill": { + "duration": 0.006226, + "end_time": "2026-09-14T15:05:42.748408+00:00", + "exception": false, + "start_time": "2026-09-14T15:05:42.742182+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "# Lean-13b : la borne de Tsirelson — digestion formelle de la frontière classique/quantique\n", + "\n", + "**Navigation** : [<< Lean-13 Kochen-Specker](Lean-13-Kochen-Specker.ipynb) · [Lean-16f Free-Will](Lean-16f-Conway-Free-Will-Theorem.ipynb) · [Sommaire série](README.md)\n", + "\n", + "Le **jeu de CHSH** (Clauser, Horne, Shimony, Holt 1969) fait s'affronter deux joueurs qui ne\n", + "communiquent plus : Alice reçoit un bit $x$, Bob un bit $y$, chacun rend un bit ; ils gagnent\n", + "selon la règle $a \\oplus b = x \\wedge y$. Le score le plus élevé qu'ils puissent atteindre en\n", + "partageant seulement du hasard **classique** est $2$. En partageant un état **intrigué**, ils\n", + "atteignent $2\\sqrt{2}$ — c'est la **borne de Tsirelson** (1980), la première séparation\n", + "quantique/classique prouvée de l'histoire de la physique.\n", + "\n", + "Ce notebook est le **compagnon natif** du module `conway_lean/Conway/CHSHQuantum.lean` : il\n", + "n'expose pas la théorie « en prose », il **importe le module et exécute ses énoncés** dans un\n", + "kernel Lean 4 réel. Le lake est la source de vérité ; le notebook est le banc d'essai.\n", + "\n", + "Ce que la tranche sépare, et que ce notebook prend soin de ne pas confondre :\n", + "\n", + "| Statut | Contenu |\n", + "|---|---|\n", + "| **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` |\n", + "| **importé avec preuve noyau** | la borne quantique elle-même : `Mathlib.Algebra.Star.CHSH.tsirelson_inequality`, dont `tsirelson_bound` est la forme usuelle |\n", + "| **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 |\n", + "\n", + "Provenance : J. F. Clauser, M. A. Horne, A. Shimony, R. A. Holt, *Proposed experiment to test\n", + "local hidden-variable theories*, Phys. Rev. Lett. **23** (1969) ; B. S. Tsirelson (Cirel'son),\n", + "*Quantum generalizations of Bell's inequality*, Lett. Math. Phys. **4** (1980).\n" + ] + }, + { + "cell_type": "markdown", + "id": "8b25373a", + "metadata": { + "papermill": { + "duration": 0.004788, + "end_time": "2026-09-14T15:05:42.760250+00:00", + "exception": false, + "start_time": "2026-09-14T15:05:42.755462+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 1. Vérification de l'environnement\n", + "\n", + "L'import ci-dessous charge les modules du lake `conway_lean` (compilés en `.olean`). Il est\n", + "résolu par le `LEAN_PATH` du kernel : le kernel doit tourner **depuis un répertoire à\n", + "l'intérieur du lake**, sinon il retombe sur un lake-stub vide et tous les imports échouent\n", + "en silence.\n", + "\n", + "**Kernel de ce notebook — une divergence assumée, et mesurée.** Le body de #15700 nomme le\n", + "kernel `lean4-wsl`, comme l'ensemble de la série. Ce notebook déclare `lean4-wsl-conway`, qui\n", + "est le même kernel plus `wsl.exe --cd` vers le lake WSL, `~/conway-build`. La raison est mécanique :\n", + "`Lean-13b` vit dans `MyIA.AI.Notebooks/SymbolicAI/Lean/`, qui **n'est pas** un lake (aucun\n", + "`lakefile.lean` en remontant l'arbre). Lancé depuis ce répertoire, le kernel `lean4-wsl`\n", + "retombe donc sur le stub `~/lean-projects/notebook_context`, qui ne contient **ni Conway ni\n", + "Mathlib** — et un kernel dans cet état ne lève pas d'erreur d'import : il **répond muet**\n", + "(#11874). Déclarer `lean4-wsl` ici produirait donc un notebook dont les sorties ne sont pas\n", + "reproductibles par le kernel qu'il nomme. `lean4-wsl-conway` est la forme qui reproduit\n", + "réellement les sorties committées.\n" + ] + }, + { + "cell_type": "code", + "execution_count": 1, + "id": "5089dc43", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-14T15:05:42.771461Z", + "iopub.status.busy": "2026-09-14T15:05:42.771178Z", + "iopub.status.idle": "2026-09-14T15:05:43.766730Z", + "shell.execute_reply": "2026-09-14T15:05:43.766004Z" + }, + "papermill": { + "duration": 1.003345, + "end_time": "2026-09-14T15:05:43.768662+00:00", + "exception": false, + "start_time": "2026-09-14T15:05:42.765317+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "data": { + "text/html": [ + "\n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + "
\n", + " 
import Conway.CHSHQuantum
\n", + "
import Conway.CHSH
\n", + "
import Conway.CHSHRandomized
\n", + "
open Conway
\n", + "
\n", + "
--% env 0
\n", + "
\n", + "
\n", + " Raw input\n", + " {\"cmd\": \"import Conway.CHSHQuantum\\nimport Conway.CHSH\\nimport Conway.CHSHRandomized\\nopen Conway\\n\"}\n", + "
\n", + "
\n", + " Raw output\n", + " {\"env\": 0}\n", + "
\n", + " " + ], + "text/plain": [ + "import Conway.CHSHQuantum\n", + "import Conway.CHSH\n", + "import Conway.CHSHRandomized\n", + "open Conway\n", + "\n", + "--% env 0\n", + "\n", + "Raw input:\n", + "{\"cmd\": \"import Conway.CHSHQuantum\\nimport Conway.CHSH\\nimport Conway.CHSHRandomized\\nopen Conway\\n\"}\n", + "Raw output:\n", + "{\"env\": 0}" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "import Conway.CHSHQuantum\n", + "import Conway.CHSH\n", + "import Conway.CHSHRandomized\n", + "open Conway\n" + ] + }, + { + "cell_type": "markdown", + "id": "76544e27", + "metadata": { + "papermill": { + "duration": 0.003522, + "end_time": "2026-09-14T15:05:43.776600+00:00", + "exception": false, + "start_time": "2026-09-14T15:05:43.773078+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "**Interprétation.** Cette cellule ne prouve **rien** à elle seule, et c'est le point le plus\n", + "important de cette section. Les commandes `import` du REPL sont **paresseuses** : importer un\n", + "module inexistant ne produit pas de message, la réponse est `{\"env\": 0}` — indiscernable d'un\n", + "succès. Une sonde sans contrôle positif lit donc un kernel mort comme un kernel silencieux.\n", + "La preuve d'environnement est la cellule suivante, pas celle-ci.\n" + ] + }, + { + "cell_type": "markdown", + "id": "0b8fb102", + "metadata": { + "papermill": { + "duration": 0.006662, + "end_time": "2026-09-14T15:05:43.787958+00:00", + "exception": false, + "start_time": "2026-09-14T15:05:43.781296+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 2. Le contrôle positif — `#eval 2 + 2`\n", + "\n", + "Si le kernel tournait sur le stub, il aurait perdu jusqu'à `Init` : la toute première\n", + "évaluation échouerait sur `Unknown identifier Nat`. Ce contrôle est donc **le discriminant**\n", + "entre « le lake est résolu » et « le kernel est muet ». Tout ce qui suit ne vaut que si\n", + "cette cellule rend `4`.\n" + ] + }, + { + "cell_type": "code", + "execution_count": 2, + "id": "a2cd73e5", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-14T15:05:43.802886Z", + "iopub.status.busy": "2026-09-14T15:05:43.802504Z", + "iopub.status.idle": "2026-09-14T15:05:43.959324Z", + "shell.execute_reply": "2026-09-14T15:05:43.958522Z" + }, + "papermill": { + "duration": 0.166995, + "end_time": "2026-09-14T15:05:43.960517+00:00", + "exception": false, + "start_time": "2026-09-14T15:05:43.793522+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "data": { + "text/html": [ + "\n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + "
\n", + " 
-- 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", + "
 4
\n", + "
\n", + "
--% env 1
\n", + "
\n", + "
\n", + " Raw input\n", + " {\"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}\n", + "
\n", + "
\n", + " Raw output\n", + " {\"messages\":\r\n", + " [{\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 3, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 3, \"column\": 5},\r\n", + " \"data\": \"4\"}],\r\n", + " \"env\": 1}\n", + "
\n", + " " + ], + "text/plain": [ + "-- 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", + "─────▶ 4\n", + "\n", + "--% env 1\n", + "\n", + "Raw input:\n", + "{\"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}\n", + "Raw output:\n", + "{\"messages\":\r\n", + " [{\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 3, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 3, \"column\": 5},\r\n", + " \"data\": \"4\"}],\r\n", + " \"env\": 1}" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "-- 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" + ] + }, + { + "cell_type": "markdown", + "id": "dc212dc0", + "metadata": { + "papermill": { + "duration": 0.004387, + "end_time": "2026-09-14T15:05:43.967918+00:00", + "exception": false, + "start_time": "2026-09-14T15:05:43.963531+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "**Interprétation.** `4`. Le kernel est vivant, sa toolchain est cohérente avec celle du lake\n", + "(`leanprover/lean4:v4.32.1`, le pin de `conway_lean`), et la stdlib est résolue. Les imports\n", + "de la cellule 1 peuvent maintenant être **tenus pour acquis** — ils ne l'étaient pas.\n" + ] + }, + { + "cell_type": "markdown", + "id": "ae99c202", + "metadata": { + "papermill": { + "duration": 0.004363, + "end_time": "2026-09-14T15:05:43.975508+00:00", + "exception": false, + "start_time": "2026-09-14T15:05:43.971145+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 3. Les trois bornes — tableau comparatif\n", + "\n", + "| Régime | Objet mathématique | Borne | Déclaration Lean | Statut de la preuve |\n", + "|---|---|---|---|---|\n", + "| **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 |\n", + "| **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 |\n", + "| **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` |\n", + "| **séparation** | $2$ vs $2\\sqrt{2}$ | $2 < 2\\sqrt{2}$ | `Conway.CHSHQuantum.classical_quantum_gap` | prouvé dans ce lake |\n", + "\n", + "Deux lignes disent « prouvé dans ce lake », une dit « importé » : c'est la distinction que la\n", + "grille de #13106 demande de rendre visible. La borne quantique n'est **pas** redémontrée ici —\n", + "la redériver artificiellement aurait été un exercice d'école, pas une digestion. Ce qui est\n", + "local, c'est la **carte d'hypothèses** : le raccord entre le vocabulaire CoursIA et les\n", + "hypothèses exactes de Mathlib, la réécriture de la forme brute $\\sqrt{2}^{\\,3} \\cdot 1$ vers\n", + "la forme usuelle $2\\sqrt{2} \\cdot 1$, et la preuve que l'écart est **strict**.\n" + ] + }, + { + "cell_type": "markdown", + "id": "74f81683", + "metadata": { + "papermill": { + "duration": 0.002276, + "end_time": "2026-09-14T15:05:43.980188+00:00", + "exception": false, + "start_time": "2026-09-14T15:05:43.977912+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 4. Exemple guidé 1 — la signature exacte du théorème quantique\n", + "\n", + "Lire une signature, c'est lire la carte de ce qu'un théorème exige. Celle de `tsirelson_bound`\n", + "est le cœur de la tranche : elle reprend celle de Mathlib — le sens « aucune hypothèse\n", + "retirée » est épinglé par l'élaboration, le sens « aucune hypothèse ajoutée » n'est gardé\n", + "par aucun instrument (une reprise, pas une égalité bidirectionnelle garantie ; cf. section 7).\n" + ] + }, + { + "cell_type": "code", + "execution_count": 3, + "id": "1bc55db2", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-14T15:05:43.988998Z", + "iopub.status.busy": "2026-09-14T15:05:43.988528Z", + "iopub.status.idle": "2026-09-14T15:05:44.186035Z", + "shell.execute_reply": "2026-09-14T15:05:44.184999Z" + }, + "papermill": { + "duration": 0.204457, + "end_time": "2026-09-14T15:05:44.187197+00:00", + "exception": false, + "start_time": "2026-09-14T15:05:43.982740+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "data": { + "text/html": [ + "\n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + "
\n", + " 
 @CHSHQuantum.chshOperator : {R : Type u_1} → [Ring R] → R → R → R → R → R
\n", + "
 @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
\n", + "
 CHSHQuantum.sqrt_two_cubed : √2 ^ 3 = 2 * √2
\n", + "
 CHSHQuantum.classical_quantum_gap : 2 < 2 * √2
\n", + "
 CHSHQuantum.classical_deterministic_bound_real : ∀ (a₀ a₁ b₀ b₁ : CHSH.Outcome), ↑|CHSH.score a₀ a₁ b₀ b₁| ≤ 2
\n", + "
 CHSHQuantum.classical_randomized_bound_real : ∀ (μ : CHSHRandomized.Strategy),\n",
+       "  (∀ (p : CHSHRandomized.Profile), 0 ≤ μ p) → ∑ p, μ p = 1 → ↑|CHSHRandomized.expectedScore μ| ≤ 2
\n", + "
 CHSH.classical_bound : ∀ (a₀ a₁ b₀ b₁ : CHSH.Outcome), |CHSH.score a₀ a₁ b₀ b₁| ≤ 2
\n", + "
 CHSHRandomized.randomized_bound : ∀ (μ : CHSHRandomized.Strategy),\n",
+       "  (∀ (p : CHSHRandomized.Profile), 0 ≤ μ p) → ∑ p, μ p = 1 → |CHSHRandomized.expectedScore μ| ≤ 2
\n", + "
\n", + "
--% env 2
\n", + "
\n", + "
\n", + " Raw input\n", + " {\"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}\n", + "
\n", + "
\n", + " Raw output\n", + " {\"messages\":\r\n", + " [{\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 1, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 1, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"@CHSHQuantum.chshOperator : {R : Type u_1} → [Ring R] → R → R → R → R → R\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 2, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 2, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"@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\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 3, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 3, \"column\": 6},\r\n", + " \"data\": \"CHSHQuantum.sqrt_two_cubed : √2 ^ 3 = 2 * √2\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 4, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 4, \"column\": 6},\r\n", + " \"data\": \"CHSHQuantum.classical_quantum_gap : 2 < 2 * √2\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 5, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 5, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"CHSHQuantum.classical_deterministic_bound_real : ∀ (a₀ a₁ b₀ b₁ : CHSH.Outcome), ↑|CHSH.score a₀ a₁ b₀ b₁| ≤ 2\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 6, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 6, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"CHSHQuantum.classical_randomized_bound_real : ∀ (μ : CHSHRandomized.Strategy),\\n (∀ (p : CHSHRandomized.Profile), 0 ≤ μ p) → ∑ p, μ p = 1 → ↑|CHSHRandomized.expectedScore μ| ≤ 2\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 7, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 7, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"CHSH.classical_bound : ∀ (a₀ a₁ b₀ b₁ : CHSH.Outcome), |CHSH.score a₀ a₁ b₀ b₁| ≤ 2\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 8, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 8, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"CHSHRandomized.randomized_bound : ∀ (μ : CHSHRandomized.Strategy),\\n (∀ (p : CHSHRandomized.Profile), 0 ≤ μ p) → ∑ p, μ p = 1 → |CHSHRandomized.expectedScore μ| ≤ 2\"}],\r\n", + " \"env\": 2}\n", + "
\n", + " " + ], + "text/plain": [ + "#check @Conway.CHSHQuantum.chshOperator\n", + "──────▶ @CHSHQuantum.chshOperator : {R : Type u_1} → [Ring R] → R → R → R → R → R\n", + "#check @Conway.CHSHQuantum.tsirelson_bound\n", + "──────▶ @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\n", + "#check @Conway.CHSHQuantum.sqrt_two_cubed\n", + "──────▶ CHSHQuantum.sqrt_two_cubed : √2 ^ 3 = 2 * √2\n", + "#check @Conway.CHSHQuantum.classical_quantum_gap\n", + "──────▶ CHSHQuantum.classical_quantum_gap : 2 < 2 * √2\n", + "#check @Conway.CHSHQuantum.classical_deterministic_bound_real\n", + "──────▶ CHSHQuantum.classical_deterministic_bound_real : ∀ (a₀ a₁ b₀ b₁ : CHSH.Outcome), ↑|CHSH.score a₀ a₁ b₀ b₁| ≤ 2\n", + "#check @Conway.CHSHQuantum.classical_randomized_bound_real\n", + "──────▶ CHSHQuantum.classical_randomized_bound_real : ∀ (μ : CHSHRandomized.Strategy),\n", + " (∀ (p : CHSHRandomized.Profile), 0 ≤ μ p) → ∑ p, μ p = 1 → ↑|CHSHRandomized.expectedScore μ| ≤ 2\n", + "#check @Conway.CHSH.classical_bound\n", + "──────▶ CHSH.classical_bound : ∀ (a₀ a₁ b₀ b₁ : CHSH.Outcome), |CHSH.score a₀ a₁ b₀ b₁| ≤ 2\n", + "#check @Conway.CHSHRandomized.randomized_bound\n", + "──────▶ CHSHRandomized.randomized_bound : ∀ (μ : CHSHRandomized.Strategy),\n", + " (∀ (p : CHSHRandomized.Profile), 0 ≤ μ p) → ∑ p, μ p = 1 → |CHSHRandomized.expectedScore μ| ≤ 2\n", + "\n", + "--% env 2\n", + "\n", + "Raw input:\n", + "{\"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}\n", + "Raw output:\n", + "{\"messages\":\r\n", + " [{\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 1, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 1, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"@CHSHQuantum.chshOperator : {R : Type u_1} → [Ring R] → R → R → R → R → R\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 2, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 2, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"@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\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 3, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 3, \"column\": 6},\r\n", + " \"data\": \"CHSHQuantum.sqrt_two_cubed : √2 ^ 3 = 2 * √2\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 4, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 4, \"column\": 6},\r\n", + " \"data\": \"CHSHQuantum.classical_quantum_gap : 2 < 2 * √2\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 5, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 5, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"CHSHQuantum.classical_deterministic_bound_real : ∀ (a₀ a₁ b₀ b₁ : CHSH.Outcome), ↑|CHSH.score a₀ a₁ b₀ b₁| ≤ 2\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 6, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 6, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"CHSHQuantum.classical_randomized_bound_real : ∀ (μ : CHSHRandomized.Strategy),\\n (∀ (p : CHSHRandomized.Profile), 0 ≤ μ p) → ∑ p, μ p = 1 → ↑|CHSHRandomized.expectedScore μ| ≤ 2\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 7, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 7, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"CHSH.classical_bound : ∀ (a₀ a₁ b₀ b₁ : CHSH.Outcome), |CHSH.score a₀ a₁ b₀ b₁| ≤ 2\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 8, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 8, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"CHSHRandomized.randomized_bound : ∀ (μ : CHSHRandomized.Strategy),\\n (∀ (p : CHSHRandomized.Profile), 0 ≤ μ p) → ∑ p, μ p = 1 → |CHSHRandomized.expectedScore μ| ≤ 2\"}],\r\n", + " \"env\": 2}" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "#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" + ] + }, + { + "cell_type": "markdown", + "id": "96f59fc6", + "metadata": { + "papermill": { + "duration": 0.003459, + "end_time": "2026-09-14T15:05:44.193864+00:00", + "exception": false, + "start_time": "2026-09-14T15:05:44.190405+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "**Interprétation.** La signature de `tsirelson_bound` énumère sept classes de types\n", + "(`Ring`, `PartialOrder`, `StarRing`, `StarOrderedRing`, `Algebra ℝ`, `IsOrderedModule ℝ`,\n", + "`StarModule ℝ`) avant l'hypothèse `IsCHSHTuple A₀ A₁ B₀ B₁`, et conclut\n", + "`≤ (2 * √2) • 1`. Deux choses s'y lisent d'un coup d'œil :\n", + "\n", + "- **`•` (smul) et non un produit** : la borne est un multiple scalaire de l'unité, ce qui est\n", + " la seule écriture disponible dans une algèbre étoilée ordonnée quelconque — il n'y a pas de\n", + " « 2√2 » comme élément de $R$ avant d'avoir écrit $(2\\sqrt{2}) \\cdot 1_R$.\n", + "- **`√2 ^ 3` chez Mathlib, `2 * √2` ici** : la forme brute est la même quantité réécrite, et\n", + " c'est exactement ce que `sqrt_two_cubed` établit formellement — pas une simplification\n", + " « à l'œil » sur un symbole.\n", + "\n", + "`classical_deterministic_bound_real` et `classical_randomized_bound_real` sont les deux bornes\n", + "classiques **transportées dans $\\mathbb{R}$** : c'est ce transport qui rend les imports de\n", + "`Conway.CHSH` et `Conway.CHSHRandomized` porteurs plutôt que décoratifs.\n" + ] + }, + { + "cell_type": "markdown", + "id": "6aaf49b1", + "metadata": { + "papermill": { + "duration": 0.003123, + "end_time": "2026-09-14T15:05:44.200456+00:00", + "exception": false, + "start_time": "2026-09-14T15:05:44.197333+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 5. Exemple guidé 2 — les axiomes : ce que « prouvé » veut dire\n", + "\n", + "Un théorème qui compile peut encore dépendre d'un axiome ajouté (`sorryAx`). `#print axioms`\n", + "est la seule façon de le voir ; c'est aussi l'instrument qui permet d'affirmer « pas de\n", + "`sorry` » sans se contenter d'un `grep`.\n" + ] + }, + { + "cell_type": "code", + "execution_count": 4, + "id": "5e624f01", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-14T15:05:44.208497Z", + "iopub.status.busy": "2026-09-14T15:05:44.208330Z", + "iopub.status.idle": "2026-09-14T15:05:44.376557Z", + "shell.execute_reply": "2026-09-14T15:05:44.375762Z" + }, + "papermill": { + "duration": 0.174155, + "end_time": "2026-09-14T15:05:44.377555+00:00", + "exception": false, + "start_time": "2026-09-14T15:05:44.203400+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "data": { + "text/html": [ + "\n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + "
\n", + " 
 'Conway.CHSHQuantum.tsirelson_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
\n", + "
 'Conway.CHSHQuantum.sqrt_two_cubed' depends on axioms: [propext, Classical.choice, Quot.sound]
\n", + "
 'Conway.CHSHQuantum.classical_quantum_gap' depends on axioms: [propext, Classical.choice, Quot.sound]
\n", + "
 'Conway.CHSHQuantum.classical_deterministic_bound_real' depends on axioms: [propext, Classical.choice, Quot.sound]
\n", + "
 'Conway.CHSHQuantum.classical_randomized_bound_real' depends on axioms: [propext, Classical.choice, Quot.sound]
\n", + "
\n", + "
--% env 3
\n", + "
\n", + "
\n", + " Raw input\n", + " {\"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}\n", + "
\n", + "
\n", + " Raw output\n", + " {\"messages\":\r\n", + " [{\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 1, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 1, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"'Conway.CHSHQuantum.tsirelson_bound' depends on axioms: [propext, Classical.choice, Quot.sound]\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 2, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 2, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"'Conway.CHSHQuantum.sqrt_two_cubed' depends on axioms: [propext, Classical.choice, Quot.sound]\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 3, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 3, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"'Conway.CHSHQuantum.classical_quantum_gap' depends on axioms: [propext, Classical.choice, Quot.sound]\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 4, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 4, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"'Conway.CHSHQuantum.classical_deterministic_bound_real' depends on axioms: [propext, Classical.choice, Quot.sound]\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 5, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 5, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"'Conway.CHSHQuantum.classical_randomized_bound_real' depends on axioms: [propext, Classical.choice, Quot.sound]\"}],\r\n", + " \"env\": 3}\n", + "
\n", + " " + ], + "text/plain": [ + "#print axioms Conway.CHSHQuantum.tsirelson_bound\n", + "──────▶ 'Conway.CHSHQuantum.tsirelson_bound' depends on axioms: [propext, Classical.choice, Quot.sound]\n", + "#print axioms Conway.CHSHQuantum.sqrt_two_cubed\n", + "──────▶ 'Conway.CHSHQuantum.sqrt_two_cubed' depends on axioms: [propext, Classical.choice, Quot.sound]\n", + "#print axioms Conway.CHSHQuantum.classical_quantum_gap\n", + "──────▶ 'Conway.CHSHQuantum.classical_quantum_gap' depends on axioms: [propext, Classical.choice, Quot.sound]\n", + "#print axioms Conway.CHSHQuantum.classical_deterministic_bound_real\n", + "──────▶ 'Conway.CHSHQuantum.classical_deterministic_bound_real' depends on axioms: [propext, Classical.choice, Quot.sound]\n", + "#print axioms Conway.CHSHQuantum.classical_randomized_bound_real\n", + "──────▶ 'Conway.CHSHQuantum.classical_randomized_bound_real' depends on axioms: [propext, Classical.choice, Quot.sound]\n", + "\n", + "--% env 3\n", + "\n", + "Raw input:\n", + "{\"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}\n", + "Raw output:\n", + "{\"messages\":\r\n", + " [{\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 1, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 1, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"'Conway.CHSHQuantum.tsirelson_bound' depends on axioms: [propext, Classical.choice, Quot.sound]\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 2, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 2, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"'Conway.CHSHQuantum.sqrt_two_cubed' depends on axioms: [propext, Classical.choice, Quot.sound]\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 3, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 3, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"'Conway.CHSHQuantum.classical_quantum_gap' depends on axioms: [propext, Classical.choice, Quot.sound]\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 4, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 4, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"'Conway.CHSHQuantum.classical_deterministic_bound_real' depends on axioms: [propext, Classical.choice, Quot.sound]\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 5, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 5, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"'Conway.CHSHQuantum.classical_randomized_bound_real' depends on axioms: [propext, Classical.choice, Quot.sound]\"}],\r\n", + " \"env\": 3}" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "#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" + ] + }, + { + "cell_type": "markdown", + "id": "569ae6e2", + "metadata": { + "papermill": { + "duration": 0.003889, + "end_time": "2026-09-14T15:05:44.385924+00:00", + "exception": false, + "start_time": "2026-09-14T15:05:44.382035+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "**Interprétation.** Les cinq déclarations dépendent de\n", + "`[propext, Classical.choice, Quot.sound]` — les trois axiomes standard de Lean et de Mathlib,\n", + "et **pas** de `sorryAx`. C'est la mesure qui autorise la phrase « aucune preuve admise » : un\n", + "théorème dont le corps contiendrait `sorry` afficherait `sorryAx` dans cette liste.\n", + "\n", + "Une réserve d'instrument, qu'il faut connaître : `#print axioms` est **contaminé par une erreur\n", + "d'élaboration**. Si le module ne compile pas, Lean admet l'énoncé et l'instrument affiche\n", + "`sorryAx` — un théorème parfaitement prouvé peut donc *paraître* dépendre de `sorry`. La mesure\n", + "n'est valide que sur un module qui compile **sans erreur** ; `lake build Conway.CHSHQuantum`\n", + "doit être vert avant qu'on lise cette sortie.\n" + ] + }, + { + "cell_type": "markdown", + "id": "8dfe7dff", + "metadata": { + "papermill": { + "duration": 0.006205, + "end_time": "2026-09-14T15:05:44.398074+00:00", + "exception": false, + "start_time": "2026-09-14T15:05:44.391869+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 6. Exemple guidé 3 — la frontière classique, mesurée sur les valeurs\n", + "\n", + "La borne classique est **atteinte**, et c'est ce qui en fait une frontière et non une simple\n", + "majoration lâche. Les valeurs ci-dessous sont calculées par le noyau, pas recopiées.\n" + ] + }, + { + "cell_type": "code", + "execution_count": 5, + "id": "2cf94049", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-14T15:05:44.413642Z", + "iopub.status.busy": "2026-09-14T15:05:44.413302Z", + "iopub.status.idle": "2026-09-14T15:05:44.592601Z", + "shell.execute_reply": "2026-09-14T15:05:44.591942Z" + }, + "papermill": { + "duration": 0.189849, + "end_time": "2026-09-14T15:05:44.594630+00:00", + "exception": false, + "start_time": "2026-09-14T15:05:44.404781+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "data": { + "text/html": [ + "\n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + "
\n", + " 
 1
\n", + "
 -1
\n", + "
 2
\n", + "
 -2
\n", + "
 2
\n", + "
 0
\n", + "
\n", + "
--% env 4
\n", + "
\n", + "
\n", + " Raw input\n", + " {\"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}\n", + "
\n", + "
\n", + " Raw output\n", + " {\"messages\":\r\n", + " [{\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 1, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 1, \"column\": 5},\r\n", + " \"data\": \"1\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 2, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 2, \"column\": 5},\r\n", + " \"data\": \"-1\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 3, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 3, \"column\": 5},\r\n", + " \"data\": \"2\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 4, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 4, \"column\": 5},\r\n", + " \"data\": \"-2\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 5, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 5, \"column\": 5},\r\n", + " \"data\": \"2\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 6, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 6, \"column\": 5},\r\n", + " \"data\": \"0\"}],\r\n", + " \"env\": 4}\n", + "
\n", + " " + ], + "text/plain": [ + "#eval Conway.CHSH.Outcome.positive.value\n", + "─────▶ 1\n", + "#eval Conway.CHSH.Outcome.negative.value\n", + "─────▶ -1\n", + "#eval Conway.CHSH.score .positive .positive .positive .positive\n", + "─────▶ 2\n", + "#eval Conway.CHSH.score .positive .negative .positive .negative\n", + "─────▶ -2\n", + "#eval Conway.CHSHRandomized.expectedScore (Conway.CHSHRandomized.dirac Conway.CHSHRandomized.pPos)\n", + "─────▶ 2\n", + "#eval Conway.CHSHRandomized.expectedScore Conway.CHSHRandomized.balancedMix\n", + "─────▶ 0\n", + "\n", + "--% env 4\n", + "\n", + "Raw input:\n", + "{\"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}\n", + "Raw output:\n", + "{\"messages\":\r\n", + " [{\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 1, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 1, \"column\": 5},\r\n", + " \"data\": \"1\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 2, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 2, \"column\": 5},\r\n", + " \"data\": \"-1\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 3, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 3, \"column\": 5},\r\n", + " \"data\": \"2\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 4, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 4, \"column\": 5},\r\n", + " \"data\": \"-2\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 5, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 5, \"column\": 5},\r\n", + " \"data\": \"2\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 6, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 6, \"column\": 5},\r\n", + " \"data\": \"0\"}],\r\n", + " \"env\": 4}" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "#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" + ] + }, + { + "cell_type": "markdown", + "id": "2de89b43", + "metadata": { + "papermill": { + "duration": 0.006076, + "end_time": "2026-09-14T15:05:44.607780+00:00", + "exception": false, + "start_time": "2026-09-14T15:05:44.601704+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "**Interprétation.** Les deux valeurs d'un résultat sont $\\pm 1$ (`Outcome.value`), et le score\n", + "du profil tout-positif vaut $2$ : la borne $|\\text{score}| \\le 2$ est donc **saturée** par une\n", + "stratégie déterministe — impossible de faire mieux sans intrication, et c'est précisément ce\n", + "que la borne quantique contredit. Le profil mixte rend $-2$ : la symétrie\n", + "$\\text{score}(a, \\bar a, b, \\bar b) = -\\text{score}(a,a,b,b)$ est visible à l'écran.\n", + "\n", + "Le mélange équilibré `balancedMix` (moitié `pPos`, moitié `pNeg`) rend une espérance de $0$ :\n", + "mélanger deux stratégies déterministes de scores opposés **annule** le score sans jamais le\n", + "pousser au-delà de $2$ en valeur absolue. C'est le sens du théorème `randomized_bound` : le\n", + "hasard classique ne fait pas sortir de l'intervalle $[-2, 2]$.\n" + ] + }, + { + "cell_type": "markdown", + "id": "8adf74a9", + "metadata": { + "papermill": { + "duration": 0.006094, + "end_time": "2026-09-14T15:05:44.617866+00:00", + "exception": false, + "start_time": "2026-09-14T15:05:44.611772+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 7. Ce que cette tranche n'établit pas\n", + "\n", + "Nommer les limites fait partie du livrable. Rien de ce qui suit n'est prouvé dans ce lake :\n", + "\n", + "- **La saturation de $2\\sqrt{2}$.** Le lake prouve la **borne** $\\le 2\\sqrt{2}$, jamais son\n", + " atteinte : il n'expose aucune stratégie quantique, aucun état intrigué et aucun observable\n", + " qui réaliseraient $2\\sqrt{2}$ sur le jeu de CHSH. La borne est un plafond, pas un maximum\n", + " démontré.\n", + "- **La construction matricielle.** Aucun opérateur de Pauli, aucune matrice $2 \\times 2$ :\n", + " `IsCHSHTuple` est une structure algébrique abstraite, pas une réalisation physique.\n", + "- **L'interprétation probabiliste complète.** Le lien entre un état quantique, des observables\n", + " et une distribution de réponses mesurées n'est pas formalisé ici.\n", + "- **La borne bilatérale en norme d'opérateur.** L'énoncé est une inégalité dans un ordre\n", + " partiel d'algèbre étoilée ordonnée, pas un énoncé de norme.\n", + "- **La carte d'hypothèses n'est pas une égalité garantie.** Le module reprend les hypothèses de\n", + " Mathlib. Le sens « aucune hypothèse retirée » est épinglé par l'élaboration (durcir la\n", + " signature amont ferait échouer la preuve, donc rouge) ; le sens « aucune hypothèse ajoutée »\n", + " n'est gardé par **aucun instrument** — un affaiblissement amont laisserait le théorème\n", + " compiler avec une hypothèse devenue superflue, en silence. La liste est énoncée comme une\n", + " **reprise**, jamais comme une égalité vérifiée.\n", + "\n", + "La difficulté réelle de la preuve amont mérite d'être dite : la démonstration de Tsirelson dans\n", + "Mathlib n'est pas une manipulation d'inégalités triangulaires, c'est une **somme de carrés**\n", + "(SOS) — on exhibe une décomposition positive de $2\\sqrt{2} \\cdot 1 - \\text{chshOperator}$.\n", + "C'est cette structure qui explique pourquoi l'énoncé a besoin d'un anneau étoilé **ordonné**\n", + "(`StarOrderedRing`) : sans ordre compatible avec l'involution, il n'y a pas de positivité à\n", + "invoquer. Reconstruire cette preuve est un travail de formalisation à part entière ; ce\n", + "notebook en **consomme** le résultat, il ne le refait pas.\n" + ] + }, + { + "cell_type": "markdown", + "id": "52895c98", + "metadata": { + "papermill": { + "duration": 0.003531, + "end_time": "2026-09-14T15:05:44.625734+00:00", + "exception": false, + "start_time": "2026-09-14T15:05:44.622203+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 8. Exercices\n", + "\n", + "Trois exercices bornés pour manipuler les objets du lake. Chaque cellule **s'exécute telle\n", + "quelle** (corps trivial) : à vous de remplacer le corps par la bonne définition. Les `#eval`\n", + "de contrôle affichent côte à côte votre valeur et celle du lake.\n" + ] + }, + { + "cell_type": "markdown", + "id": "72b4abe4", + "metadata": { + "papermill": { + "duration": 0.002927, + "end_time": "2026-09-14T15:05:44.632414+00:00", + "exception": false, + "start_time": "2026-09-14T15:05:44.629487+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Exercice 1 — le profile est-il maximal ?\n", + "\n", + "Définissez `estMaximal` renvoyant `true` si et seulement si le score du profil vaut exactement\n", + "$2$ (le maximum classique). Le corps actuel renvoie `true` en toutes circonstances : sur les\n", + "profils de score négatif, votre valeur et celle du lake divergeront — c'est le test.\n" + ] + }, + { + "cell_type": "code", + "execution_count": 6, + "id": "4bc6a064", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-14T15:05:44.641633Z", + "iopub.status.busy": "2026-09-14T15:05:44.641303Z", + "iopub.status.idle": "2026-09-14T15:05:44.837509Z", + "shell.execute_reply": "2026-09-14T15:05:44.836724Z" + }, + "papermill": { + "duration": 0.202971, + "end_time": "2026-09-14T15:05:44.838937+00:00", + "exception": false, + "start_time": "2026-09-14T15:05:44.635966+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "data": { + "text/html": [ + "\n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + "
\n", + " 
-- Exercice 1 : le profil atteint-il le maximum classique (score = 2) ?
\n", + "
-- TODO etudiant : remplacer le corps ci-dessous
\n", + "
🟨 Variable name `a₀` is not explicitly referenced.\n",
+       "\n",
+       "The binding can be removed (if unused) or named `_` (if used implicitly).\n",
+       "\n",
+       "Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 Variable name `a₁` is not explicitly referenced.\n",
+       "\n",
+       "The binding can be removed (if unused) or named `_` (if used implicitly).\n",
+       "\n",
+       "Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 Variable name `b₀` is not explicitly referenced.\n",
+       "\n",
+       "The binding can be removed (if unused) or named `_` (if used implicitly).\n",
+       "\n",
+       "Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 Variable name `b₁` is not explicitly referenced.\n",
+       "\n",
+       "The binding can be removed (if unused) or named `_` (if used implicitly).\n",
+       "\n",
+       "Note: This linter can be disabled with `set_option linter.unusedVariables false`
\n", + "
  true
\n", + "
\n", + "
-- Doivent valoir true, true, false (le lake rend 2, 2, -2)
\n", + "
 true
\n", + "
 true
\n", + "
 true
\n", + "
-- Les scores correspondants, calcules par le lake
\n", + "
 2
\n", + "
 2
\n", + "
 -2
\n", + "
\n", + "
--% env 5
\n", + "
\n", + "
\n", + " Raw input\n", + " {\"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}\n", + "
\n", + "
\n", + " Raw output\n", + " {\"messages\":\r\n", + " [{\"severity\": \"warning\",\r\n", + " \"pos\": {\"line\": 3, \"column\": 16},\r\n", + " \"endPos\": {\"line\": 3, \"column\": 18},\r\n", + " \"data\":\r\n", + " \"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`\"},\r\n", + " {\"severity\": \"warning\",\r\n", + " \"pos\": {\"line\": 3, \"column\": 19},\r\n", + " \"endPos\": {\"line\": 3, \"column\": 21},\r\n", + " \"data\":\r\n", + " \"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`\"},\r\n", + " {\"severity\": \"warning\",\r\n", + " \"pos\": {\"line\": 3, \"column\": 22},\r\n", + " \"endPos\": {\"line\": 3, \"column\": 24},\r\n", + " \"data\":\r\n", + " \"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`\"},\r\n", + " {\"severity\": \"warning\",\r\n", + " \"pos\": {\"line\": 3, \"column\": 25},\r\n", + " \"endPos\": {\"line\": 3, \"column\": 27},\r\n", + " \"data\":\r\n", + " \"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`\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 7, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 7, \"column\": 5},\r\n", + " \"data\": \"true\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 8, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 8, \"column\": 5},\r\n", + " \"data\": \"true\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 9, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 9, \"column\": 5},\r\n", + " \"data\": \"true\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 11, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 11, \"column\": 5},\r\n", + " \"data\": \"2\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 12, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 12, \"column\": 5},\r\n", + " \"data\": \"2\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 13, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 13, \"column\": 5},\r\n", + " \"data\": \"-2\"}],\r\n", + " \"env\": 5}\n", + "
\n", + " " + ], + "text/plain": [ + "-- Exercice 1 : le profil atteint-il le maximum classique (score = 2) ?\n", + "-- TODO etudiant : remplacer le corps ci-dessous\n", + "def estMaximal (a₀ a₁ b₀ b₁ : Conway.CHSH.Outcome) : Bool :=\n", + " ──▶ 🟨 Variable name `a₀` is not explicitly referenced.\n", + "\n", + "The binding can be removed (if unused) or named `_` (if used implicitly).\n", + "\n", + "Note: This linter can be disabled with `set_option linter.unusedVariables false`\n", + " ──▶ 🟨 Variable name `a₁` is not explicitly referenced.\n", + "\n", + "The binding can be removed (if unused) or named `_` (if used implicitly).\n", + "\n", + "Note: This linter can be disabled with `set_option linter.unusedVariables false`\n", + " ──▶ 🟨 Variable name `b₀` is not explicitly referenced.\n", + "\n", + "The binding can be removed (if unused) or named `_` (if used implicitly).\n", + "\n", + "Note: This linter can be disabled with `set_option linter.unusedVariables false`\n", + " ──▶ 🟨 Variable name `b₁` is not explicitly referenced.\n", + "\n", + "The binding can be removed (if unused) or named `_` (if used implicitly).\n", + "\n", + "Note: This linter can be disabled with `set_option linter.unusedVariables false`\n", + " true\n", + "\n", + "-- Doivent valoir true, true, false (le lake rend 2, 2, -2)\n", + "#eval estMaximal .positive .positive .positive .positive\n", + "─────▶ true\n", + "#eval estMaximal .positive .negative .negative .positive\n", + "─────▶ true\n", + "#eval estMaximal .positive .negative .positive .negative\n", + "─────▶ true\n", + "-- Les scores correspondants, calcules par le lake\n", + "#eval Conway.CHSH.score .positive .positive .positive .positive\n", + "─────▶ 2\n", + "#eval Conway.CHSH.score .positive .negative .negative .positive\n", + "─────▶ 2\n", + "#eval Conway.CHSH.score .positive .negative .positive .negative\n", + "─────▶ -2\n", + "\n", + "--% env 5\n", + "\n", + "Raw input:\n", + "{\"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}\n", + "Raw output:\n", + "{\"messages\":\r\n", + " [{\"severity\": \"warning\",\r\n", + " \"pos\": {\"line\": 3, \"column\": 16},\r\n", + " \"endPos\": {\"line\": 3, \"column\": 18},\r\n", + " \"data\":\r\n", + " \"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`\"},\r\n", + " {\"severity\": \"warning\",\r\n", + " \"pos\": {\"line\": 3, \"column\": 19},\r\n", + " \"endPos\": {\"line\": 3, \"column\": 21},\r\n", + " \"data\":\r\n", + " \"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`\"},\r\n", + " {\"severity\": \"warning\",\r\n", + " \"pos\": {\"line\": 3, \"column\": 22},\r\n", + " \"endPos\": {\"line\": 3, \"column\": 24},\r\n", + " \"data\":\r\n", + " \"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`\"},\r\n", + " {\"severity\": \"warning\",\r\n", + " \"pos\": {\"line\": 3, \"column\": 25},\r\n", + " \"endPos\": {\"line\": 3, \"column\": 27},\r\n", + " \"data\":\r\n", + " \"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`\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 7, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 7, \"column\": 5},\r\n", + " \"data\": \"true\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 8, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 8, \"column\": 5},\r\n", + " \"data\": \"true\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 9, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 9, \"column\": 5},\r\n", + " \"data\": \"true\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 11, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 11, \"column\": 5},\r\n", + " \"data\": \"2\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 12, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 12, \"column\": 5},\r\n", + " \"data\": \"2\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 13, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 13, \"column\": 5},\r\n", + " \"data\": \"-2\"}],\r\n", + " \"env\": 5}" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "-- Exercice 1 : le profil atteint-il le maximum classique (score = 2) ?\n", + "-- TODO etudiant : remplacer le corps ci-dessous\n", + "def estMaximal (a₀ a₁ b₀ b₁ : 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" + ] + }, + { + "cell_type": "markdown", + "id": "0bbda90d", + "metadata": { + "papermill": { + "duration": 0.004199, + "end_time": "2026-09-14T15:05:44.847861+00:00", + "exception": false, + "start_time": "2026-09-14T15:05:44.843662+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Exercice 2 — reconstruire le score à la main\n", + "\n", + "Le score de CHSH s'obtient par `A₀·B₀ + A₀·B₁ + A₁·B₀ - A₁·B₁`, où chaque résultat vaut\n", + "$\\pm 1$ (`Conway.CHSH.Outcome.value`). Réimplémentez-le **sans** appeler `CHSH.score`.\n" + ] + }, + { + "cell_type": "code", + "execution_count": 7, + "id": "71f168d0", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-14T15:05:44.862578Z", + "iopub.status.busy": "2026-09-14T15:05:44.862348Z", + "iopub.status.idle": "2026-09-14T15:05:45.053220Z", + "shell.execute_reply": "2026-09-14T15:05:45.052585Z" + }, + "papermill": { + "duration": 0.199359, + "end_time": "2026-09-14T15:05:45.055163+00:00", + "exception": false, + "start_time": "2026-09-14T15:05:44.855804+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "data": { + "text/html": [ + "\n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + "
\n", + " 
-- Exercice 2 : score de CHSH reconstruit depuis Outcome.value
\n", + "
-- TODO etudiant : remplacer le corps ci-dessous
\n", + "
🟨 Variable name `a₀` is not explicitly referenced.\n",
+       "\n",
+       "The binding can be removed (if unused) or named `_` (if used implicitly).\n",
+       "\n",
+       "Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 Variable name `a₁` is not explicitly referenced.\n",
+       "\n",
+       "The binding can be removed (if unused) or named `_` (if used implicitly).\n",
+       "\n",
+       "Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 Variable name `b₀` is not explicitly referenced.\n",
+       "\n",
+       "The binding can be removed (if unused) or named `_` (if used implicitly).\n",
+       "\n",
+       "Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 Variable name `b₁` is not explicitly referenced.\n",
+       "\n",
+       "The binding can be removed (if unused) or named `_` (if used implicitly).\n",
+       "\n",
+       "Note: This linter can be disabled with `set_option linter.unusedVariables false`
\n", + "
  0
\n", + "
\n", + "
-- Doivent donner les memes valeurs que CHSH.score
\n", + "
 0
\n", + "
 2
\n", + "
 0
\n", + "
 -2
\n", + "
 0
\n", + "
 -2
\n", + "
\n", + "
--% env 6
\n", + "
\n", + "
\n", + " Raw input\n", + " {\"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}\n", + "
\n", + "
\n", + " Raw output\n", + " {\"messages\":\r\n", + " [{\"severity\": \"warning\",\r\n", + " \"pos\": {\"line\": 3, \"column\": 17},\r\n", + " \"endPos\": {\"line\": 3, \"column\": 19},\r\n", + " \"data\":\r\n", + " \"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`\"},\r\n", + " {\"severity\": \"warning\",\r\n", + " \"pos\": {\"line\": 3, \"column\": 20},\r\n", + " \"endPos\": {\"line\": 3, \"column\": 22},\r\n", + " \"data\":\r\n", + " \"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`\"},\r\n", + " {\"severity\": \"warning\",\r\n", + " \"pos\": {\"line\": 3, \"column\": 23},\r\n", + " \"endPos\": {\"line\": 3, \"column\": 25},\r\n", + " \"data\":\r\n", + " \"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`\"},\r\n", + " {\"severity\": \"warning\",\r\n", + " \"pos\": {\"line\": 3, \"column\": 26},\r\n", + " \"endPos\": {\"line\": 3, \"column\": 28},\r\n", + " \"data\":\r\n", + " \"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`\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 7, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 7, \"column\": 5},\r\n", + " \"data\": \"0\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 8, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 8, \"column\": 5},\r\n", + " \"data\": \"2\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 9, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 9, \"column\": 5},\r\n", + " \"data\": \"0\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 10, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 10, \"column\": 5},\r\n", + " \"data\": \"-2\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 11, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 11, \"column\": 5},\r\n", + " \"data\": \"0\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 12, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 12, \"column\": 5},\r\n", + " \"data\": \"-2\"}],\r\n", + " \"env\": 6}\n", + "
\n", + " " + ], + "text/plain": [ + "-- Exercice 2 : score de CHSH reconstruit depuis Outcome.value\n", + "-- TODO etudiant : remplacer le corps ci-dessous\n", + "def scoreManuel (a₀ a₁ b₀ b₁ : Conway.CHSH.Outcome) : Int :=\n", + " ──▶ 🟨 Variable name `a₀` is not explicitly referenced.\n", + "\n", + "The binding can be removed (if unused) or named `_` (if used implicitly).\n", + "\n", + "Note: This linter can be disabled with `set_option linter.unusedVariables false`\n", + " ──▶ 🟨 Variable name `a₁` is not explicitly referenced.\n", + "\n", + "The binding can be removed (if unused) or named `_` (if used implicitly).\n", + "\n", + "Note: This linter can be disabled with `set_option linter.unusedVariables false`\n", + " ──▶ 🟨 Variable name `b₀` is not explicitly referenced.\n", + "\n", + "The binding can be removed (if unused) or named `_` (if used implicitly).\n", + "\n", + "Note: This linter can be disabled with `set_option linter.unusedVariables false`\n", + " ──▶ 🟨 Variable name `b₁` is not explicitly referenced.\n", + "\n", + "The binding can be removed (if unused) or named `_` (if used implicitly).\n", + "\n", + "Note: This linter can be disabled with `set_option linter.unusedVariables false`\n", + " 0\n", + "\n", + "-- Doivent donner les memes valeurs que CHSH.score\n", + "#eval scoreManuel .positive .positive .positive .positive\n", + "─────▶ 0\n", + "#eval Conway.CHSH.score .positive .positive .positive .positive\n", + "─────▶ 2\n", + "#eval scoreManuel .positive .negative .positive .negative\n", + "─────▶ 0\n", + "#eval Conway.CHSH.score .positive .negative .positive .negative\n", + "─────▶ -2\n", + "#eval scoreManuel .negative .negative .positive .positive\n", + "─────▶ 0\n", + "#eval Conway.CHSH.score .negative .negative .positive .positive\n", + "─────▶ -2\n", + "\n", + "--% env 6\n", + "\n", + "Raw input:\n", + "{\"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}\n", + "Raw output:\n", + "{\"messages\":\r\n", + " [{\"severity\": \"warning\",\r\n", + " \"pos\": {\"line\": 3, \"column\": 17},\r\n", + " \"endPos\": {\"line\": 3, \"column\": 19},\r\n", + " \"data\":\r\n", + " \"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`\"},\r\n", + " {\"severity\": \"warning\",\r\n", + " \"pos\": {\"line\": 3, \"column\": 20},\r\n", + " \"endPos\": {\"line\": 3, \"column\": 22},\r\n", + " \"data\":\r\n", + " \"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`\"},\r\n", + " {\"severity\": \"warning\",\r\n", + " \"pos\": {\"line\": 3, \"column\": 23},\r\n", + " \"endPos\": {\"line\": 3, \"column\": 25},\r\n", + " \"data\":\r\n", + " \"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`\"},\r\n", + " {\"severity\": \"warning\",\r\n", + " \"pos\": {\"line\": 3, \"column\": 26},\r\n", + " \"endPos\": {\"line\": 3, \"column\": 28},\r\n", + " \"data\":\r\n", + " \"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`\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 7, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 7, \"column\": 5},\r\n", + " \"data\": \"0\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 8, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 8, \"column\": 5},\r\n", + " \"data\": \"2\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 9, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 9, \"column\": 5},\r\n", + " \"data\": \"0\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 10, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 10, \"column\": 5},\r\n", + " \"data\": \"-2\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 11, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 11, \"column\": 5},\r\n", + " \"data\": \"0\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 12, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 12, \"column\": 5},\r\n", + " \"data\": \"-2\"}],\r\n", + " \"env\": 6}" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "-- Exercice 2 : score de CHSH reconstruit depuis Outcome.value\n", + "-- TODO etudiant : remplacer le corps ci-dessous\n", + "def scoreManuel (a₀ a₁ b₀ b₁ : 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" + ] + }, + { + "cell_type": "markdown", + "id": "d636fee5", + "metadata": { + "papermill": { + "duration": 0.004498, + "end_time": "2026-09-14T15:05:45.068440+00:00", + "exception": false, + "start_time": "2026-09-14T15:05:45.063942+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Exercice 3 — lire la borne dans le théorème\n", + "\n", + "Lisez `Conway.CHSH.classical_bound`, puis déclarez l'entier $B$ tel que\n", + "$\\lvert \\text{score} \\rvert \\le B$ pour **tout** profil — la borne que le théorème garantit,\n", + "en valeur absolue. Expliquez ensuite en commentaire pourquoi la borne quantique, elle, ne peut\n", + "pas s'écrire comme un entier de cette façon.\n" + ] + }, + { + "cell_type": "code", + "execution_count": 8, + "id": "f2f69b73", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-14T15:05:45.082955Z", + "iopub.status.busy": "2026-09-14T15:05:45.082626Z", + "iopub.status.idle": "2026-09-14T15:05:45.250941Z", + "shell.execute_reply": "2026-09-14T15:05:45.250126Z" + }, + "papermill": { + "duration": 0.179865, + "end_time": "2026-09-14T15:05:45.252757+00:00", + "exception": false, + "start_time": "2026-09-14T15:05:45.072892+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "data": { + "text/html": [ + "\n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + "
\n", + " 
-- Exercice 3 : la borne absolue garantie par Conway.CHSH.classical_bound
\n", + "
-- TODO etudiant : remplacer le corps ci-dessous
\n", + "
def borneAbsolueClassique : Int :=
\n", + "
  0
\n", + "
\n", + "
-- Doit valoir 2
\n", + "
 0
\n", + "
\n", + "
-- TODO etudiant (commentaire) : pourquoi 2*sqrt(2) n'a pas d'equivalent entier ici ?
\n", + "
\n", + "
--% env 7
\n", + "
\n", + "
\n", + " Raw input\n", + " {\"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}\n", + "
\n", + "
\n", + " Raw output\n", + " {\"messages\":\r\n", + " [{\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 7, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 7, \"column\": 5},\r\n", + " \"data\": \"0\"}],\r\n", + " \"env\": 7}\n", + "
\n", + " " + ], + "text/plain": [ + "-- Exercice 3 : la borne absolue garantie par Conway.CHSH.classical_bound\n", + "-- TODO etudiant : remplacer le corps ci-dessous\n", + "def borneAbsolueClassique : Int :=\n", + " 0\n", + "\n", + "-- Doit valoir 2\n", + "#eval borneAbsolueClassique\n", + "─────▶ 0\n", + "\n", + "-- TODO etudiant (commentaire) : pourquoi 2*sqrt(2) n'a pas d'equivalent entier ici ?\n", + "\n", + "--% env 7\n", + "\n", + "Raw input:\n", + "{\"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}\n", + "Raw output:\n", + "{\"messages\":\r\n", + " [{\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 7, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 7, \"column\": 5},\r\n", + " \"data\": \"0\"}],\r\n", + " \"env\": 7}" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "-- Exercice 3 : la borne absolue garantie par Conway.CHSH.classical_bound\n", + "-- TODO etudiant : remplacer le corps ci-dessous\n", + "def 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" + ] + }, + { + "cell_type": "markdown", + "id": "a640e4b1", + "metadata": { + "papermill": { + "duration": 0.004249, + "end_time": "2026-09-14T15:05:45.264514+00:00", + "exception": false, + "start_time": "2026-09-14T15:05:45.260265+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 9. Provenance, raccords et conclusion\n", + "\n", + "**Ce qui a été exécuté.** Les huit cellules de code ci-dessus ont été exécutées par le kernel\n", + "Lean 4 (`lean4-wsl-conway`, `--cd ~/conway-build`) sur le lake `conway_lean` au pin\n", + "`leanprover/lean4:v4.32.1`. Les sorties sont celles du noyau : `#check`, `#print axioms` et\n", + "`#eval` sont rendus par le REPL, aucune sortie n'a été écrite à la main.\n", + "\n", + "**Chaîne de dépendance, telle qu'elle se lit dans les sorties.** `tsirelson_bound` n'est pas une\n", + "redémonstration : elle applique `Mathlib.Algebra.Star.CHSH.tsirelson_inequality`, réécrit\n", + "`√2 ^ 3` en `2 * √2` par `sqrt_two_cubed`, et change l'écriture de l'opérateur CHSH par\n", + "`chshOperator`. Les trois axiomes affichés (`propext`, `Classical.choice`, `Quot.sound`) sont\n", + "ceux de Mathlib — la chaîne est donc *transparente* : à aucun étage on n'admet ce qu'on prétend\n", + "prouver.\n", + "\n", + "**Raccords dans la série.**\n", + "\n", + "- **[Lean-13 Kochen-Specker](Lean-13-Kochen-Specker.ipynb)** — la contextualité : KS montre\n", + " qu'aucune valuation non contextuelle ne reproduit les prédictions quantiques. CHSH en est le\n", + " pendant *statistique*, sous forme d'inégalité testable entre deux joueurs séparés.\n", + "- **[Lean-16f Free-Will](Lean-16f-Conway-Free-Will-Theorem.ipynb)** — la liberté : le théorème\n", + " de Conway–Kochen (2006) montre que le déterminisme et la liberté du choix des mesures sont\n", + " incompatibles avec l'accord quantique. C'est l'hypothèse même que le jeu de CHSH met à\n", + " l'épreuve expérimentale.\n", + "- **`Conway/CHSH.lean` et `Conway/CHSHRandomized.lean`** — les bornes classiques que la borne\n", + " quantique contredit, prouvées dans ce même lake.\n", + "\n", + "**Ce que la tranche laisse ouvert**, et qui reste à faire pour clore #13106 : la saturation de\n", + "$2\\sqrt{2}$ par une stratégie quantique explicite, la réalisation matricielle (Pauli), et la\n", + "borne bilatérale en norme d'opérateur. Aucune de ces trois n'est prouvée ici, et aucune n'est\n", + "simulée par un exemple scalaire de remplacement.\n" + ] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Lean 4 (WSL, conway-build)", + "language": "lean4", + "name": "lean4-wsl-conway" + }, + "language_info": { + "codemirror_mode": "python", + "file_extension": ".lean", + "mimetype": "text/x-lean4", + "name": "lean4" + }, + "papermill": { + "default_parameters": {}, + "duration": 4.427208, + "end_time": "2026-09-14T15:05:45.510546+00:00", + "environment_variables": {}, + "exception": null, + "input_path": "Lean-13b-CHSH-Tsirelson-Native.ipynb", + "output_path": "Lean-13b-CHSH-Tsirelson-Native.ipynb", + "parameters": {}, + "start_time": "2026-09-14T15:05:41.083338+00:00", + "version": "2.7.0" + } + }, + "nbformat": 4, + "nbformat_minor": 5 +} diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/README.md b/MyIA.AI.Notebooks/SymbolicAI/Lean/README.md index c1f88d5dc3..4483036c9b 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/README.md +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/README.md @@ -100,6 +100,7 @@ Tous les notebooks incluent une **barre de navigation** en haut et en bas permet | # | Notebook | Contenu | Durée | |---|----------|---------|-------| | 13 | [Lean-13-Kochen-Specker](Lean-13-Kochen-Specker.ipynb) | théorème de Kochen-Specker (1967), preuve Cabello 18 vecteurs, parité, contextuality quantique - Pilier 1.B Epic #1651 | 60 min | +| 13b | [Lean-13b-CHSH-Tsirelson-Native](Lean-13b-CHSH-Tsirelson-Native.ipynb) | Companion **natif** du lake `conway_lean` : la borne de Tsirelson exécutée in-kernel — `#check` de la signature exacte (7 classes de types + `IsCHSHTuple`, conclusion `≤ (2 * √2) • 1`), `#print axioms` = `[propext, Classical.choice, Quot.sound]` sans `sorryAx`, frontière classique mesurée (score `2` atteint, mélange équilibré → `0`), contrôle positif de kernel contre le REPL muet (#11874) et 3 exercices - Epic #13106 | 30 min | | 14 | [Lean-14-Finiteness-Derivatives](Lean-14-Finiteness-Derivatives.ipynb) | Dérivées symboliques de Brzozowski : la finitude des dérivées qui garantit le matching linéaire (langages rationnels, automates) | 25 min | | 14b | [Lean-14b-Finiteness-Lean-Companion](Lean-14b-Finiteness-Lean-Companion.ipynb) | Companion **natif** (kernel Lean) : les 7 déclarations du lake `finiteness_lean` (`Regex`, `nullable`, `deriv`, `derivWord`, `accepts`, `aStar`, `abWord`) re-déclarées fidèlement (kernel sans oleans), vérifiées et exécutées in-kernel, finitude observée sur une regex à union (6 préfixes → 4 dérivées distinctes) | 20 min | @@ -195,6 +196,7 @@ Pour l'état formel détaillé des modules support (preuves résolues vs `sorry` | 12 | Sensitivity-Theorem | ~31 | 4 | Non | **NOUVEAU** | | 12b | Lean-Sensitivity-Theorem (natif) | ~19 | 3 | 0 | **NOUVEAU** (kernel `lean4-wsl`) | | 13 | Kochen-Specker | ~25 | 1 | 0 | **NOUVEAU** | +| 13b | CHSH-Tsirelson-Native | ~8 | 3 | 0 | **NOUVEAU** (kernel `lean4-wsl-conway`) | | 14 | Finiteness-Derivatives | ~12 | 1 | - | **NOUVEAU** | | 14b | Finiteness-Lean-Companion | ~19 | 3 | 0 | **NOUVEAU** (kernel `lean4-wsl`) | | 15 | Grothendieck-Tribute | ~23 | 0 | - | **NOUVEAU** (hommage) | @@ -395,6 +397,7 @@ Lean/ ├── Lean-16i-Translateur-Life.ipynb # Python kernel - synthèse d'un translateur minuscule (SAT borné, Loi II, Chantier 2 #12205) ├── Lean-16j-Conway-Hashlife-Correctness-Native.ipynb # Lean4 (WSL) kernel - compagnon Hashlife correctness (cône, MacroCell, 4 murs, marge, batterie adverse, Epic #11703) ├── Lean-13-Kochen-Specker.ipynb # Lean4 kernel - théorème de Kochen-Specker (Pilier 1.B) +├── Lean-13b-CHSH-Tsirelson-Native.ipynb # Lean4 (WSL, conway-build) kernel - borne de Tsirelson : signature, axiomes, frontière classique (Epic #13106) ├── Lean-14-Finiteness-Derivatives.ipynb # Python kernel - dérivées symboliques de Brzozowski (finitude, matching linéaire) ├── Lean-14b-Finiteness-Lean-Companion.ipynb # Lean kernel - companion natif du lake finiteness_lean (7 déclarations citées) ├── Lean-16f-Conway-Free-Will-Theorem.ipynb # Python kernel - hommage Conway (théorème du libre arbitre, adossé à FreeWillTheorem.lean)