From 7180077df5548ea740303038392a2dcd33c0bfda Mon Sep 17 00:00:00 2001 From: jsboige Date: Mon, 14 Sep 2026 17:08:12 +0200 Subject: [PATCH 1/2] =?UTF-8?q?feat(lean,#15700):=20notebook=20natif=20Lea?= =?UTF-8?q?n-13b=20=E2=80=94=20la=20borne=20de=20Tsirelson=20ex=C3=A9cut?= =?UTF-8?q?=C3=A9e=20in-kernel?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Grain: DEEP/lean — lane myia-po-2027:CoursIA — prev: DEEP/lean #16047 Tranche 3 de #15700 : le 3e fichier du périmètre, le notebook compagnon natif des deux modules livrés par #16167. Empilée sur cette branche, dont elle importe Conway.CHSHQuantum. Contenu — 26 cellules dont 8 de code, exécutées par un kernel Lean 4 réel (lean4-wsl-conway, --cd vers le lake conway_lean au pin leanprover/lean4:v4.32.1) : - navigation vers Lean-13 (contextualité) et Lean-16f (libre arbitre) ; - tableau comparatif déterministe / randomisé / quantique, chaque ligne portant le statut de sa preuve — « prouvé dans ce lake » vs « importé de Mathlib » ; - 3 exemples guidés compilés : #check de la signature exacte de tsirelson_bound, #print axioms des 5 déclarations ([propext, Classical.choice, Quot.sound], aucun sorryAx), #eval de la frontière classique (score 2 atteint, mélange équilibré -> 0) ; - un contrôle positif de kernel (#eval 2+2 -> 4) : les imports du REPL sont paresseux, un kernel retombé sur le lake-stub répond muet (#11874) ; - 3 exercices bornés, stubs à corps trivial, aucun raise/assert False (C.1) ; - une section de limites nommées : saturation de 2*sqrt(2) non établie, aucune construction de Pauli, pas de borne en norme d'opérateur. Le kernelspec déclaré est lean4-wsl-conway et non lean4-wsl comme le nomme le body de l'issue : mesuré, lean4-wsl lancé depuis MyIA.AI.Notebooks/SymbolicAI/Lean (qui n'est pas un lake) retombe sur le stub et ne résout ni Conway ni Mathlib. Raisonnement complet et mesures au body de PR. Les deux organes de validation de ces notebooks sont par ailleurs aveugles au rouge Lean — signalé séparément en #16176, non traité ici. Co-Authored-By: Claude Sonnet 5 --- .../Lean/Lean-13b-CHSH-Tsirelson-Native.ipynb | 1694 +++++++++++++++++ MyIA.AI.Notebooks/SymbolicAI/Lean/README.md | 3 + 2 files changed, 1697 insertions(+) create mode 100644 MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-13b-CHSH-Tsirelson-Native.ipynb 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..588ec8135e --- /dev/null +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-13b-CHSH-Tsirelson-Native.ipynb @@ -0,0 +1,1694 @@ +{ + "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 doit être celle de Mathlib, sans élargissement ni restriction.\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 huit 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 six 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..fc83736838 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 (8 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) From 888c5c158e6bfaf7952b227802088311447dfc22 Mon Sep 17 00:00:00 2001 From: jsboige Date: Mon, 14 Sep 2026 18:51:15 +0200 Subject: [PATCH 2/2] =?UTF-8?q?fix(#16177):=20reparations=20markdown=20du?= =?UTF-8?q?=20preflight=20adjoint=20=E2=80=94=20pipes=20de=20tableau,=20fo?= =?UTF-8?q?rmulation=20hypotheses,=20comptes?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Trois points de la review 5200122665 (exact-head d760ccead2aa), tous markdown-only (exception C.2, aucune re-execution due) : 1. Tableau d'intro : les pipes des inline-code `|score|` et `|expectedScore|` sont echappes en \| — GitHub les parsing comme delimiteurs de colonnes et rendait la table en un seul paragraphe. 2. Section 4 : « doit etre celle de Mathlib, sans elargissement ni restriction » remplacee par la formulation honnete alignee sur la base reparee (#16167) : reprise dont le sens « aucune hypothese retiree » est epingle par l'elaboration, le sens « aucune hypothese ajoutee » n'etant garde par aucun instrument (renvoi section 7). 3. Comptes : « huit classes » -> « sept » (Ring, PartialOrder, StarRing, StarOrderedRing, Algebra R, IsOrderedModule R, StarModule R ; IsCHSHTuple est un argument propositionnel, pas une 8e classe) dans le notebook et le README ; « six cellules de code » -> « huit » (execution_count 1..8) en conclusion. Sorties byte-identiques : seules 4 lignes source markdown du notebook et 1 ligne README changent. Co-Authored-By: Claude Sonnet 5 --- .../Lean/Lean-13b-CHSH-Tsirelson-Native.ipynb | 10 ++++++---- MyIA.AI.Notebooks/SymbolicAI/Lean/README.md | 2 +- 2 files changed, 7 insertions(+), 5 deletions(-) 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 index 588ec8135e..932da45153 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-13b-CHSH-Tsirelson-Native.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-13b-CHSH-Tsirelson-Native.ipynb @@ -33,7 +33,7 @@ "\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", + "| **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", @@ -343,7 +343,9 @@ "## 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 doit être celle de Mathlib, sans élargissement ni restriction.\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" ] }, { @@ -541,7 +543,7 @@ "tags": [] }, "source": [ - "**Interprétation.** La signature de `tsirelson_bound` énumère huit classes de types\n", + "**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", @@ -1633,7 +1635,7 @@ "source": [ "## 9. Provenance, raccords et conclusion\n", "\n", - "**Ce qui a été exécuté.** Les six cellules de code ci-dessus ont été exécutées par le kernel\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", diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/README.md b/MyIA.AI.Notebooks/SymbolicAI/Lean/README.md index fc83736838..4483036c9b 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/README.md +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/README.md @@ -100,7 +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 (8 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 | +| 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 |