diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-13c-CHSH-Landau-Saturation.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-13c-CHSH-Landau-Saturation.ipynb
index 3c92fe3b8b..e75dc92596 100644
--- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-13c-CHSH-Landau-Saturation.ipynb
+++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-13c-CHSH-Landau-Saturation.ipynb
@@ -16,6 +16,8 @@
"source": [
"# Lean-13c : la saturation de Tsirelson — le témoin de Pauli et le critère de Landau\n",
"\n",
+ "**Série** : [SymbolicAI/Lean](README.md) | Précédent : [Lean-13b — Tsirelson natif](Lean-13b-CHSH-Tsirelson-Native.ipynb) | Suivant : [Lean-13d — Indéterminisme natif](Lean-13d-CHSH-Indeterminisme-Native.ipynb)\n",
+ "\n",
"[Lean-13b](Lean-13b-CHSH-Tsirelson-Native.ipynb) a établi la **frontière** : la valeur classique $2$,\n",
"la borne quantique $2\\sqrt{2}$ importée de Mathlib, et le gap strict entre les deux. Mais elle\n",
"nommait sa propre limite, et la première était la plus importante : *la borne est un plafond, pas\n",
diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-13d-CHSH-Indeterminisme-Native.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-13d-CHSH-Indeterminisme-Native.ipynb
new file mode 100644
index 0000000000..1922a3696d
--- /dev/null
+++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-13d-CHSH-Indeterminisme-Native.ipynb
@@ -0,0 +1,1466 @@
+{
+ "cells": [
+ {
+ "cell_type": "markdown",
+ "id": "cell-13d-00",
+ "metadata": {
+ "papermill": {
+ "duration": 0.002843,
+ "end_time": "2026-10-03T19:27:46.593280+00:00",
+ "exception": false,
+ "start_time": "2026-10-03T19:27:46.590437+00:00",
+ "status": "completed"
+ },
+ "tags": []
+ },
+ "source": [
+ "# Lean-13d : du CHSH au libre arbitre — la route statistique\n",
+ "\n",
+ "**Série** : [SymbolicAI/Lean](README.md) | Précédent : [Lean-13c — Saturation de Tsirelson](Lean-13c-CHSH-Landau-Saturation.ipynb)\n",
+ "\n",
+ "Sixième tranche du **pilote quantique** de l'Epic [#13106](https://github.com/jsboige/CoursIA/issues/13106) (digestion et canonicalisation des mathématiques assistées). La série a établi jusqu'ici :\n",
+ "\n",
+ "- **Lean-13** (Kochen-Specker) : aucune coloration `{0,1}` des 18 vecteurs de Cabello — la contradiction *contextuelle* ;\n",
+ "- **Lean-13b** (Tsirelson) : la frontière classique `|score| = 2` et la borne quantique `2√2` ;\n",
+ "- **Lean-13c** (saturation) : un témoin de Pauli qui *atteint* `2√2`, et le critère de Landau vérifié dessus ;\n",
+ "- **Lean-16f** (libre arbitre) : le théorème de Conway-Kochen — sous SPIN + TWIN + MIN, les réponses ne sont pas des fonctions du passé.\n",
+ "\n",
+ "Cette tranche ferme la boucle annoncée par l'Epic : elle formalise la **route statistique** vers la même conclusion d'indéterminisme. Le nouveau module `Conway.CHSHFreeWill` définit un *modèle local déterministe* du jeu CHSH — des fonctions de réponse de l'état caché, une par parti, chacune aveugle au réglage de l'autre (l'analogue structurel de MIN) — et démontre qu'aucun tel modèle ne peut réaliser un score au-delà de la frontière classique, alors que la mécanique quantique atteint `2√2`.\n",
+ "\n",
+ "**Prérequis** : le score CHSH et la frontière classique ([Lean-13b](Lean-13b-CHSH-Tsirelson-Native.ipynb)) ; le vocabulaire du libre arbitre ([Lean-16f](Lean-16f-Conway-Free-Will-Theorem.ipynb), lecture parallèle recommandée mais non exigée)."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "cell-13d-01",
+ "metadata": {
+ "papermill": {
+ "duration": 0.002177,
+ "end_time": "2026-10-03T19:27:46.597994+00:00",
+ "exception": false,
+ "start_time": "2026-10-03T19:27:46.595817+00:00",
+ "status": "completed"
+ },
+ "tags": []
+ },
+ "source": [
+ "## 1. Vérification de l'environnement\n",
+ "\n",
+ "L'import ci-dessous charge le module de cette tranche (`Conway.CHSHFreeWill`) ainsi que ses trois piliers : `Conway.CHSH` (score et frontière), `Conway.CHSHQuantum` (l'écart `2 < 2√2`), `Conway.FreeWillTheorem` (l'état caché et le vocabulaire MIN). Il ne prouve rien : il expose."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 1,
+ "id": "cell-13d-02",
+ "metadata": {
+ "execution": {
+ "iopub.execute_input": "2026-10-03T19:27:46.603849Z",
+ "iopub.status.busy": "2026-10-03T19:27:46.603648Z",
+ "iopub.status.idle": "2026-10-03T19:29:30.166975Z",
+ "shell.execute_reply": "2026-10-03T19:29:30.165384Z"
+ },
+ "papermill": {
+ "duration": 103.570546,
+ "end_time": "2026-10-03T19:29:30.170956+00:00",
+ "exception": false,
+ "start_time": "2026-10-03T19:27:46.600410+00:00",
+ "status": "completed"
+ },
+ "tags": []
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/html": [
+ "\n",
+ " \n",
+ " \n",
+ " \n",
+ " \n",
+ " \n",
+ " \n",
+ " \n",
+ "
\n",
+ "
importConway.CHSHFreeWill
\n",
+ "
importConway.CHSH
\n",
+ "
importConway.CHSHQuantum
\n",
+ "
importConway.FreeWillTheorem
\n",
+ "
\n",
+ "
-- Conway.CHSHFreeWill : modele local deterministe + frontiere etat par etat + conclusion
\n",
+ " \n",
+ " Raw input\n",
+ " {\"cmd\": \"-- Exercice 3 : construire et calculer un modele a -2.\\n-- TODO etudiant : definir aliceM / bobM (true -> .positive, false -> .negative),\\n-- puis evaluer #eval Conway.CHSHFreeWill.realizedScore aliceM bobM 0\\n-- Resultat attendu : -2.\\n-- Amorce : les valeurs d'un resultat se calculent --\\n#eval Conway.CHSH.Outcome.positive.value\\n#eval Conway.CHSH.Outcome.negative.value\\n#check @Conway.CHSHFreeWill.local_abs_score\", \"env\": 8}\n",
+ " \n",
+ " \n",
+ " Raw output\n",
+ " {\"messages\":\r\n",
+ " [{\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 6, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 6, \"column\": 5},\r\n",
+ " \"data\": \"1\"},\r\n",
+ " {\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 7, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 7, \"column\": 5},\r\n",
+ " \"data\": \"-1\"},\r\n",
+ " {\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 8, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 8, \"column\": 6},\r\n",
+ " \"data\":\r\n",
+ " \"Conway.CHSHFreeWill.local_abs_score : ∀ (α : Conway.CHSHFreeWill.AliceResponse) (β : Conway.CHSHFreeWill.BobResponse)\\n (state : Conway.FreeWillTheorem.HiddenState), |Conway.CHSHFreeWill.realizedScore α β state| = 2\"}],\r\n",
+ " \"env\": 9}\n",
+ " \n",
+ " "
+ ],
+ "text/plain": [
+ "-- Exercice 3 : construire et calculer un modele a -2.\n",
+ "-- TODO etudiant : definir aliceM / bobM (true -> .positive, false -> .negative),\n",
+ "-- puis evaluer #eval Conway.CHSHFreeWill.realizedScore aliceM bobM 0\n",
+ "-- Resultat attendu : -2.\n",
+ "-- Amorce : les valeurs d'un resultat se calculent --\n",
+ "#eval Conway.CHSH.Outcome.positive.value\n",
+ "─────▶ 1\n",
+ "#eval Conway.CHSH.Outcome.negative.value\n",
+ "─────▶ -1\n",
+ "#check @Conway.CHSHFreeWill.local_abs_score\n",
+ "──────▶ Conway.CHSHFreeWill.local_abs_score : ∀ (α : Conway.CHSHFreeWill.AliceResponse) (β : Conway.CHSHFreeWill.BobResponse)\n",
+ " (state : Conway.FreeWillTheorem.HiddenState), |Conway.CHSHFreeWill.realizedScore α β state| = 2\n",
+ "--% env 9\n",
+ "\n",
+ "Raw input:\n",
+ "{\"cmd\": \"-- Exercice 3 : construire et calculer un modele a -2.\\n-- TODO etudiant : definir aliceM / bobM (true -> .positive, false -> .negative),\\n-- puis evaluer #eval Conway.CHSHFreeWill.realizedScore aliceM bobM 0\\n-- Resultat attendu : -2.\\n-- Amorce : les valeurs d'un resultat se calculent --\\n#eval Conway.CHSH.Outcome.positive.value\\n#eval Conway.CHSH.Outcome.negative.value\\n#check @Conway.CHSHFreeWill.local_abs_score\", \"env\": 8}\n",
+ "Raw output:\n",
+ "{\"messages\":\r\n",
+ " [{\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 6, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 6, \"column\": 5},\r\n",
+ " \"data\": \"1\"},\r\n",
+ " {\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 7, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 7, \"column\": 5},\r\n",
+ " \"data\": \"-1\"},\r\n",
+ " {\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 8, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 8, \"column\": 6},\r\n",
+ " \"data\":\r\n",
+ " \"Conway.CHSHFreeWill.local_abs_score : ∀ (α : Conway.CHSHFreeWill.AliceResponse) (β : Conway.CHSHFreeWill.BobResponse)\\n (state : Conway.FreeWillTheorem.HiddenState), |Conway.CHSHFreeWill.realizedScore α β state| = 2\"}],\r\n",
+ " \"env\": 9}"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "-- Exercice 3 : construire et calculer un modele a -2.\n",
+ "-- TODO etudiant : definir aliceM / bobM (true -> .positive, false -> .negative),\n",
+ "-- puis evaluer #eval Conway.CHSHFreeWill.realizedScore aliceM bobM 0\n",
+ "-- Resultat attendu : -2.\n",
+ "-- Amorce : les valeurs d'un resultat se calculent --\n",
+ "#eval Conway.CHSH.Outcome.positive.value\n",
+ "#eval Conway.CHSH.Outcome.negative.value\n",
+ "#check @Conway.CHSHFreeWill.local_abs_score"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "cell-13d-29",
+ "metadata": {
+ "papermill": {
+ "duration": 0.003705,
+ "end_time": "2026-10-03T19:29:32.147537+00:00",
+ "exception": false,
+ "start_time": "2026-10-03T19:29:32.143832+00:00",
+ "status": "completed"
+ },
+ "tags": []
+ },
+ "source": [
+ "## 9. Provenance, raccords et conclusion\n",
+ "\n",
+ "**Ce qui a été exécuté.** Le module `Conway.CHSHFreeWill` (sixième tranche du pilote quantique, siblings FR/EN, zéro `sorry`), ses six déclarations (`local_abs_score`, `local_bound`, `no_state_beyond_classical`, `canonical_score`, `local_bound_real`, `tsirelson_beyond_every_local_score`, `chsh_indeterminism`) chargées, vérifiées et passées aux axiomes dans un kernel Lean 4 réel.\n",
+ "\n",
+ "**Provenance.** Clauser, Horne, Shimony, Holt (1969), *Proposed experiment to test local hidden-variable theories* ; Bell (1964) pour l'inégalité mère et sa lecture indéterministe (§II) ; Tsirelson (1980) pour la borne quantique ; Conway-Kochen (2006/2009) pour le vocabulaire des fonctions de réponse du passé. La grille de digestion complète (10 points) vit dans l'en-tête du module.\n",
+ "\n",
+ "**Raccords.** Prolonge [Lean-13b](Lean-13b-CHSH-Tsirelson-Native.ipynb) (score et frontière) et [Lean-13c](Lean-13c-CHSH-Landau-Saturation.ipynb) (saturation) ; fait le pont avec [Lean-16f](Lean-16f-Conway-Free-Will-Theorem.ipynb) (route contextuelle) — les deux colonnes du tableau de la section 3 se lisent comme les deux réponses du corpus à la même question : *pourquoi les réponses quantiques ne sont-elles pas des fonctions du passé ?*"
+ ]
+ }
+ ],
+ "metadata": {
+ "kernelspec": {
+ "display_name": "Lean 4 (WSL)",
+ "language": "lean4",
+ "name": "lean4-wsl"
+ },
+ "language_info": {
+ "codemirror_mode": "lean4",
+ "file_extension": ".lean",
+ "mimetype": "text/x-lean4",
+ "name": "lean4"
+ },
+ "papermill": {
+ "default_parameters": {},
+ "duration": 122.572181,
+ "end_time": "2026-10-03T19:29:32.766864+00:00",
+ "environment_variables": {},
+ "exception": null,
+ "input_path": "/mnt/d/dev/CoursIA-chshfw/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-13d-CHSH-Indeterminisme-Native.ipynb",
+ "output_path": "/tmp/Lean-13d-CHSH-Indeterminisme-Native_wsl_output.ipynb",
+ "parameters": {},
+ "start_time": "2026-10-03T19:27:30.194683+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 be73ba46ad..ef387f49aa 100644
--- a/MyIA.AI.Notebooks/SymbolicAI/Lean/README.md
+++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/README.md
@@ -103,6 +103,7 @@ Tous les notebooks incluent une **barre de navigation** en haut et en bas permet
| 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 |
| 13c | [Lean-13c-CHSH-Landau-Saturation](Lean-13c-CHSH-Landau-Saturation.ipynb) | Companion **natif** du lake `conway_lean` : la saturation de Tsirelson exécutée in-kernel — `#check` de l'égalité centrale `chshOperator A₀ A₁ B₀ B₁ = (2 * √2) • 1` (égalité exacte, pas un majorant : la borne de Lean-13b devient un maximum démontré), `#print axioms` = `[propext, Classical.choice, Quot.sound]` sans `sorryAx`, témoin de Pauli (`sigmaZ`, `sigmaX`, `B₀`, `B₁` en `Matrix (Fin 2) (Fin 2) ℝ`), forme spectrale bilatérale (`2√2` sur la diagonale), anticommutateur, critère de Landau vérifié sur le témoin (spectre ±1) et 3 exercices - Epic #13106 | 25 min |
+| 13d | [Lean-13d-CHSH-Indeterminisme-Native](Lean-13d-CHSH-Indeterminisme-Native.ipynb) | Companion **natif** du lake `conway_lean` : la route statistique vers l'indéterminisme exécutée in-kernel — modèle local déterministe du jeu CHSH en vocabulaire FWT (`AliceResponse`/`BobResponse` : fonctions de l'état caché, localité par signature, l'analogue structurel de MIN), frontière locale état par état (`|realizedScore| = 2`, délégué à `classical_abs_score`), écart de Tsirelson `2 < 2√2` et conclusion `chsh_indeterminism` (aucun modèle local déterministe ne réalise un score `> 2` en réels — la même conclusion que le théorème du libre arbitre, obtenue par l'argument statistique), tableau comparatif des deux routes (contextuelle vs statistique) et 3 exercices - Epic #13106 | 25 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 |
@@ -233,6 +234,8 @@ Pour l'état formel détaillé des modules support (preuves résolues vs `sorry`
| 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`) |
+| 13c | CHSH-Landau-Saturation | ~11 | 3 | 0 | **NOUVEAU** (kernel `lean4-wsl-conway`) |
+| 13d | CHSH-Indeterminisme-Native | ~10 | 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) |
@@ -460,6 +463,7 @@ Lean/
├── 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-13c-CHSH-Landau-Saturation.ipynb # Lean4 (WSL) kernel - saturation de Tsirelson : témoin de Pauli, égalité centrale 2√2, forme spectrale (Epic #13106)
+├── Lean-13d-CHSH-Indeterminisme-Native.ipynb # Lean4 (WSL) kernel - pont CHSH <-> libre arbitre : modèle local déterministe, frontière état par état, conclusion d'indéterminisme (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)
diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway.lean b/MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway.lean
index 88bea2e023..6214510a97 100644
--- a/MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway.lean
+++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway.lean
@@ -45,6 +45,12 @@ Substance réelle :
- `Conway.CHSH` : frontière classique de l’inégalité de Bell CHSH
(Clauser-Horne-Shimony-Holt 1969) — toute stratégie locale déterministe
à réponses binaires a un score de valeur absolue exactement égal à 2.
+- `Conway.CHSHFreeWill` : pont entre la série CHSH et le théorème du libre
+ arbitre — un modèle local déterministe du jeu CHSH en fonctions de
+ l’état caché (localité par signature, analogue de MIN) ne peut réaliser
+ un score au-delà de 2 dans aucun état, alors que la mécanique quantique
+ atteint 2√2 : la même conclusion d’indéterminisme que le FWT, par la
+ route statistique.
- `Conway.CollatzLike` : généralisations de type Collatz (3n+1) — la
conjecture de Syracuse reformalisée en Lean.
- `Conway.Angel` : problème de l'Ange de Conway (J. Conway 1996 / 2002
@@ -91,5 +97,6 @@ import Conway.Life.Novelty
import Conway.KochenSpecker
import Conway.FreeWillTheorem
import Conway.CHSH
+import Conway.CHSHFreeWill
import Conway.MathlibMap
import Conway.CollatzLike
diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/CHSHFreeWill.lean b/MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/CHSHFreeWill.lean
new file mode 100644
index 0000000000..3bb0c14644
--- /dev/null
+++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/CHSHFreeWill.lean
@@ -0,0 +1,251 @@
+/-
+ `Conway.CHSHFreeWill` — Du CHSH au libre arbitre : la route statistique
+ =====================================================================
+ Sixième tranche du pilote quantique de l'Epic #13106. Les tranches
+ précédentes ont borné la frontière classique déterministe
+ (`Conway.CHSH`), son enveloppe randomisée (`Conway.CHSHRandomized`),
+ importé la borne quantique `2√2` de Mathlib (`Conway.CHSHQuantum`), puis
+ saturé Tsirelson par un témoin explicite et vérifié le critère de Landau
+ (`Conway.CHSHLandau`, consommé par le notebook `Lean-13c`).
+
+ Il manquait au pilote le pont annoncé par l'Epic : la série CHSH et le
+ théorème du libre arbitre (`Conway.FreeWillTheorem`, notebook
+ `Lean-16f`) concluent **tous deux** à l'indéterminisme des réponses
+ quantiques, mais par deux routes formellement déconnectées :
+
+ - la **route contextuelle** (Free Will Theorem) : trois directions de
+ mesure, axiomes SPIN + TWIN + MIN, contradiction par l'absence de
+ coloration de Kochen-Specker (`kochen_specker`) ;
+ - la **route statistique** (CHSH) : deux réglages par parti, localité
+ des réponses, contradiction par l'écart numérique `2 < 2√2`.
+
+ Ce module formalise la route statistique dans le vocabulaire du FWT —
+ un « modèle local déterministe » est une famille de fonctions de réponse
+ de l'état caché, une par parti, chacune aveugle au réglage de l'autre
+ (l'analogue structurel de MIN) — et démontre la conclusion
+ d'indéterminisme : **aucun modèle local déterministe ne peut réaliser un
+ score CHSH au-delà de la frontière classique, dans aucun état caché**,
+ alors que la mécanique quantique atteint `2√2`. Les réponses ne peuvent
+ donc pas être des fonctions du passé — la même conclusion que le FWT,
+ obtenue sans coloration.
+
+ ### Table d'état des énoncés
+
+ | Énoncé | Statut |
+ |---|---|
+ | Frontière locale déterministe état-par-état : `|realizedScore| = 2` | **prouvé ici** (délégué à `CHSH.classical_abs_score`) |
+ | Saturation par un modèle local explicite (`canonical`) | **prouvé ici** |
+ | Aucun état où un modèle local dépasse `2` (entier) | **prouvé ici** |
+ | La valeur de Tsirelson `2√2` majore strictement tout score local (réel) | **prouvé ici** |
+ | Conclusion d'indéterminisme : aucun modèle local ne réalise `> 2` en réels | **prouvé ici** |
+ | Interprétation probabiliste complète (états, mesures, espérances sur ℝ⁴) | **non établie** — déclarée ouverte, comme dans `Conway.CHSHQuantum` |
+ | Équivalence des deux routes (FWT ⟷ CHSH) | **non établie** — les hypothèses diffèrent ; seule la conclusion commune est formalisée |
+
+ ### Grille de digestion (10 points, Epic #13106)
+
+ 1. **Énoncés et niveau de garantie** : bornes et égalités exactes sur `ℤ`
+ puis `ℝ`, sans analyse fonctionnelle ; la constante `2√2` est celle de
+ `Conway.CHSHQuantum.classical_quantum_gap`.
+ 2. **Provenance** : Clauser, Horne, Shimony, Holt (1969), « Proposed
+ experiment to test local hidden-variable theories » ; Bell (1964) pour
+ l'inégalité mère ; Tsirelson (1980) pour la borne quantique. Le lien
+ « violation de Bell ⟹ indéterminisme » est la lecture standard (Bell
+ 1964, §II) ; la formulation en « fonctions de réponse du passé » suit
+ le vocabulaire de Conway-Kochen (2006/2009).
+ 3. **Nouveauté réelle** : le dépôt avait les deux ingrédients séparés
+ (borne `CHSH.classical_abs_score`, écart `classical_quantum_gap`) ; le
+ modèle local déterministe comme famille de fonctions de l'état caché,
+ la borne état-par-état et la conclusion d'indéterminisme sont nouveaux
+ dans le dépôt.
+ 4. **Carte des dépendances** : `Conway.CHSH` (score, frontière),
+ `Conway.CHSHQuantum` (écart), `Conway.FreeWillTheorem` (`HiddenState`,
+ vocabulaire) ; Mathlib restreinte à `Mathlib.Tactic.Ring` et aux
+ `omega` sur `|s| = 2` / coercions `ℤ → ℝ`. Aucun `sorry`,
+ aucun axiome au-delà des trois standard.
+ 5. **Trivial condensé / nouveau développé** : la frontière elle-même est
+ déléguée (énumération 16 cas déjà payée par `Conway.CHSH`) ; le cœur
+ nouveau est le passage **pour tout état** : la borne classique était un
+ fait sur quatre résultats, elle devient un fait sur des familles
+ entières de fonctions de réponse.
+ 6. **Friction** : la tentation d'un énoncé d'espérance (score moyen sous
+ une distribution d'états cachés) a été écartée : la machinerie
+ d'espérance n'apporte rien à la conclusion (la borne état-par-état est
+ plus forte pour un modèle déterministe) et alourdirait le module.
+ 7. **Chemin de découverte** : la correspondance structurelle MIN ⟷
+ localité-par-signature a été trouvée en relisant la signature de
+ `TwoParticleResponse` de `Conway.FreeWillTheorem` — la localité n'y
+ est pas une hypothèse mais une propriété du type. Le même encodage est
+ repris ici à l'identique.
+ 8. **Limites** : la conclusion porte sur les modèles **déterministes
+ locaux** ; elle ne dit rien des modèles stochastiques non locaux ni de
+ la borne randomisée (voir `Conway.CHSHRandomized` pour l'enveloppe
+ probabiliste classique).
+ 9. **Raccord au corpus** : consommé par le notebook
+ `Lean-13d-CHSH-Indeterminisme-Native.ipynb` (pont croisé avec
+ `Lean-16f`), prolongement de la série 13b/13c ; prérequis : score CHSH
+ et frontière classique (`Lean-13b`).
+ 10. **Transmission** : notebook natif avec témoin calculé, tableau de
+ correspondance des deux routes, et relecture croisée à la revue.
+
+ ### i18n — convention #4980 (ratifiée 2026-07-04)
+
+ Ce fichier est le **canonique français**. Le miroir anglais est le fichier
+ frère `Conway/CHSHFreeWill_en.lean` (`namespace Conway_en` >
+ `namespace CHSHFreeWill_en`, imports suffixés `_en`) — modèle sibling pair
+ Pattern A, comme `Conway/CHSHLandau` c.240. Docstrings en français ici ;
+ le corps (signatures, defs, preuves) reste byte-identique entre les deux
+ fichiers, aux qualifieurs `_en` près. Pas de bloc bilingue inline.
+-/
+
+import Conway.CHSH
+import Conway.CHSHQuantum
+import Conway.FreeWillTheorem
+
+namespace Conway
+
+namespace CHSHFreeWill
+
+open CHSH CHSHQuantum FreeWillTheorem
+
+/-!
+## Étape 1 : modèle local déterministe du jeu CHSH
+
+Le vocabulaire est celui du théorème du libre arbitre : les réponses sont
+des fonctions de l'état caché (le « passé » de l'univers). La **localité**
+est encodée par la signature, exactement comme MIN dans
+`Conway.FreeWillTheorem.TwoParticleResponse` : la réponse d'Alice ne voit
+jamais le réglage de Bob, et réciproquement — ce n'est pas une hypothèse
+à prouver, c'est une propriété du type.
+-/
+
+/-- Réponse locale d'Alice : pour chaque état caché et chacun de ses deux
+réglages (`true` = x, `false` = y), un résultat prédéterminé `±1`.
+
+C'est l'analogue à deux réglages de `Conway.FreeWillTheorem.DeterministicResponse`
+(qui en portait trois, directions de spin). La localité (MIN) vit dans la
+signature : le réglage de Bob n'apparaît pas. -/
+abbrev AliceResponse := HiddenState → Bool → Outcome
+
+/-- Réponse locale de Bob : même encodage, symétrique de celui d'Alice. -/
+abbrev BobResponse := HiddenState → Bool → Outcome
+
+/-- Score CHSH réalisé par le modèle `(α, β)` dans l'état caché `state` :
+les quatre réponses prédéterminées sont injectées dans le score de
+`Conway.CHSH`. -/
+def realizedScore (α : AliceResponse) (β : BobResponse) (state : HiddenState) : ℤ :=
+ score (α state true) (α state false) (β state true) (β state false)
+
+/-!
+## Étape 2 : la frontière locale, état par état
+
+La frontière classique de `Conway.CHSH` était un fait sur quatre résultats
+isolés. Pour un modèle local déterministe, elle vaut **dans chaque état
+caché** — c'est le pont du particulier (une stratégie) au général (une
+famille entière de stratégies indexée par le passé).
+-/
+
+/-- **Frontière locale déterministe, forme exacte.** Dans tout état caché,
+le score réalisé par un modèle local déterministe vaut exactement `±2`.
+
+La preuve délègue l'énumération des 16 assignations à
+`Conway.CHSH.classical_abs_score` : chaque état caché instancie quatre
+réponses, et la frontière s'applique. -/
+theorem local_abs_score (α : AliceResponse) (β : BobResponse) (state : HiddenState) :
+ |realizedScore α β state| = 2 :=
+ classical_abs_score _ _ _ _
+
+/-- Forme usuelle de la frontière locale. -/
+theorem local_bound (α : AliceResponse) (β : BobResponse) (state : HiddenState) :
+ |realizedScore α β state| ≤ 2 :=
+ local_abs_score α β state ▸ le_refl _
+
+/-- **Aucun modèle local déterministe ne dépasse la frontière classique,
+dans aucun état caché.** La borne n'est pas une moyenne : elle vaut
+état par état, donc aucun état privilégié ne peut sauver le modèle. -/
+theorem no_state_beyond_classical :
+ ¬ ∃ (α : AliceResponse) (β : BobResponse) (state : HiddenState),
+ (2 : ℤ) < realizedScore α β state := by
+ rintro ⟨α, β, state, h⟩
+ have habs : |realizedScore α β state| = 2 := local_abs_score α β state
+ have hle : realizedScore α β state ≤ |realizedScore α β state| := le_abs_self _
+ omega
+
+/-- La frontière locale est **atteinte** : le modèle canonique — les deux
+partis répondent toujours `+1` — réalise le score `+2` dans tout état.
+La borne de `local_bound` est donc serrée pour les modèles locaux. -/
+def canonicalAlice : AliceResponse := fun _ _ => .positive
+
+def canonicalBob : BobResponse := fun _ _ => .positive
+
+@[simp]
+theorem canonical_score (state : HiddenState) :
+ realizedScore canonicalAlice canonicalBob state = 2 := by
+ simp [realizedScore, canonicalAlice, canonicalBob, score, Outcome.value]
+
+/-!
+## Étape 3 : l'écart de Tsirelson exclut les modèles locaux déterministes
+
+La mécanique quantique prédit (et l'expérience confirme) des corrélations
+CHSH de valeur `2√2` — strictement au-dessus de la frontière locale
+(`Conway.CHSHQuantum.classical_quantum_gap`). Puisque tout modèle local
+déterministe est plafonné à `2` dans chaque état, aucun ne peut reproduire
+la prédiction quantique.
+-/
+
+/-- Version réelle de la frontière locale : le score réalisé, vu comme
+réel, reste sous la frontière classique. -/
+theorem local_bound_real (α : AliceResponse) (β : BobResponse) (state : HiddenState) :
+ (realizedScore α β state : ℝ) ≤ 2 := by
+ have h : realizedScore α β state ≤ 2 := by
+ have habs : |realizedScore α β state| = 2 := local_abs_score α β state
+ have hle : realizedScore α β state ≤ |realizedScore α β state| := le_abs_self _
+ omega
+ exact_mod_cast h
+
+/-- **L'écart de Tsirelson domine tous les scores locaux.** La valeur
+quantique `2√2` est strictement supérieure à la frontière classique, et
+tout modèle local déterministe réalise au plus `2` : l'écart est incompressible
+pour ces modèles. -/
+theorem tsirelson_beyond_every_local_score :
+ (2 : ℝ) < 2 * √2 ∧
+ ∀ (α : AliceResponse) (β : BobResponse) (state : HiddenState),
+ (realizedScore α β state : ℝ) ≤ 2 :=
+ ⟨classical_quantum_gap, local_bound_real⟩
+
+/-- **Conclusion d'indéterminisme par la route CHSH.** Aucun modèle où les
+réponses des deux partis sont des fonctions déterministes de l'état caché
+(localité par signature) ne peut réaliser un score CHSH strictement
+supérieur à la frontière classique — alors que la valeur quantique est
+`2√2 > 2`.
+
+C'est la même conclusion que `Conway.FreeWillTheorem.free_will_theorem`
+(les réponses ne sont pas des fonctions du passé), obtenue par un argument
+**statistique** (l'écart numérique de Tsirelson) là où le FWT utilise un
+argument **contextuel** (l'absence de coloration de Kochen-Specker). Les
+hypothèses diffèrent — deux réglages contre trois directions, écart
+numérique contre coloration impossible —, la conclusion est commune. -/
+theorem chsh_indeterminism :
+ ¬ ∃ (α : AliceResponse) (β : BobResponse) (state : HiddenState),
+ (2 : ℝ) < realizedScore α β state := by
+ rintro ⟨α, β, state, h⟩
+ exact no_state_beyond_classical ⟨α, β, state, by exact_mod_cast h⟩
+
+/-!
+## Étape 4 : correspondance structurelle des deux routes
+
+ | | Route contextuelle (FWT, `Lean-16f`) | Route statistique (CHSH, `Lean-13b/13c/13d`) |
+ |---|---|---|
+ | Réglages par parti | 3 directions orthogonales | 2 réglages binaires |
+ | Axiomes | SPIN + TWIN + MIN | localité (par signature) + statistiques quantiques |
+ | Moteur de contradiction | `kochen_specker` : aucune coloration valide | `classical_quantum_gap` : `2 < 2√2` |
+ | Ce qui est nié | toute réponse fonction du passé (déterminisme) | tout modèle local déterministe reproduisant `2√2` |
+ | Force de la conclusion | exacte, sans hypothèse statistique | numérique : quantifie l'écart (`2√2 − 2`) |
+
+ Les deux routes sont **complémentaires** : le FWT ne dit rien de l'écart
+ numérique, la route CHSH ne dit rien des corrélations parfaites TWIN.
+ Le notebook `Lean-13d` parcourt les deux colonnes sur le même témoin.
+-/
+
+end CHSHFreeWill
+
+end Conway
diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/CHSHFreeWill_en.lean b/MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/CHSHFreeWill_en.lean
new file mode 100644
index 0000000000..9606dda52a
--- /dev/null
+++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/CHSHFreeWill_en.lean
@@ -0,0 +1,255 @@
+/-
+Copyright (c) 2026 CoursIA. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+## From CHSH to free will: the statistical route
+
+This module is the sixth tranche of the quantum pilot of Epic #13106. The
+previous tranches bounded the deterministic classical frontier
+(`Conway.CHSH`), its randomized envelope (`Conway.CHSHRandomized`),
+imported Mathlib's quantum bound `2√2` (`Conway.CHSHQuantum`), then
+saturated Tsirelson with an explicit witness and checked Landau's criterion
+(`Conway.CHSHLandau`, consumed by the notebook `Lean-13c`).
+
+What the pilot was still missing is the bridge its Epic announced: the CHSH
+series and the Free Will Theorem (`Conway.FreeWillTheorem`, notebook
+`Lean-16f`) **both** conclude that quantum responses are indeterministic,
+yet through two formally disconnected routes:
+
+- the **contextual route** (Free Will Theorem): three measurement
+ directions, axioms SPIN + TWIN + MIN, contradiction by the absence of a
+ Kochen-Specker coloring (`kochen_specker`);
+- the **statistical route** (CHSH): two settings per party, locality of the
+ responses, contradiction by the numerical gap `2 < 2√2`.
+
+This module formalizes the statistical route in the vocabulary of the FWT —
+a "local deterministic model" is a family of response functions of the
+hidden state, one per party, each blind to the other party's setting (the
+structural analogue of MIN) — and proves the indeterminism conclusion:
+**no local deterministic model can realize a CHSH score beyond the
+classical frontier, in no hidden state**, while quantum mechanics reaches
+`2√2`. The responses therefore cannot be functions of the past — the same
+conclusion as the FWT, obtained without any coloring.
+
+### Statement status
+
+| Statement | Status |
+|---|---|
+| Local deterministic frontier state-by-state: `|realizedScore| = 2` | **proved here** (delegated to `CHSH.classical_abs_score`) |
+| Saturation by an explicit local model (`canonical`) | **proved here** |
+| No state where a local model exceeds `2` (integer) | **proved here** |
+| Tsirelson's value `2√2` strictly dominates every local score (real) | **proved here** |
+| Indeterminism conclusion: no local model realizes `> 2` in reals | **proved here** |
+| Full probabilistic interpretation (states, measurements, expectations on ℝ⁴) | **not established** — declared open, as in `Conway.CHSHQuantum` |
+| Equivalence of the two routes (FWT ⟷ CHSH) | **not established** — the hypotheses differ; only the shared conclusion is formalized |
+
+### Digestion grid (10 points, Epic #13106)
+
+1. **Statements and guarantee level**: exact bounds and equalities over `ℤ`
+ then `ℝ`, no functional analysis; the constant `2√2` is the one of
+ `CHSHQuantum_en.classical_quantum_gap`.
+2. **Provenance**: Clauser, Horne, Shimony, Holt (1969), "Proposed
+ experiment to test local hidden-variable theories"; Bell (1964) for the
+ parent inequality; Tsirelson (1980) for the quantum bound. The link
+ "Bell violation ⟹ indeterminism" is the standard reading (Bell 1964,
+ §II); the phrasing in "response functions of the past" follows the
+ vocabulary of Conway-Kochen (2006/2009).
+3. **Novelty**: the repository had the two ingredients separately (bound
+ `CHSH.classical_abs_score`, gap `classical_quantum_gap`); the local
+ deterministic model as a family of functions of the hidden state, the
+ state-by-state frontier and the indeterminism conclusion are new to the
+ repository.
+4. **Dependencies**: `Conway.CHSH` (score, frontier),
+ `Conway.CHSHQuantum` (gap), `Conway.FreeWillTheorem` (`HiddenState`,
+ vocabulary); Mathlib restricted to `Mathlib.Tactic.Ring` and the
+ `omega` on `|s| = 2` / coercions `ℤ → ℝ`. No `sorry`, no
+ axioms beyond the three standard ones.
+5. **Trivial condensed / new developed**: the frontier itself is delegated
+ (16-case enumeration already paid by `Conway.CHSH`); the new heart is
+ the **for every state** step: the classical frontier was a fact about
+ four outcomes, it becomes a fact about entire families of response
+ functions.
+6. **Friction**: the temptation of an expectation statement (average score
+ under a distribution of hidden states) was set aside: expectation
+ machinery adds nothing to the conclusion (the state-by-state bound is
+ stronger for a deterministic model) and would weigh the module down.
+7. **Discovery path**: the structural correspondence MIN ⟷
+ locality-by-signature was found by rereading the signature of
+ `TwoParticleResponse` in `Conway.FreeWillTheorem` — locality there is
+ not a hypothesis but a property of the type. The same encoding is
+ reused here verbatim.
+8. **Limits**: the conclusion covers **deterministic local** models; it
+ says nothing about stochastic non-local models nor about the randomized
+ bound (see `Conway.CHSHRandomized` for the classical probabilistic
+ envelope).
+9. **Corpus connection**: consumed by the notebook
+ `Lean-13d-CHSH-Indeterminisme-Native.ipynb` (cross bridge with
+ `Lean-16f`), prolongation of the 13b/13c series; prerequisites: CHSH
+ score and classical frontier (`Lean-13b`).
+10. **Transmission**: native notebook with a computed witness,
+ correspondence table of the two routes, and cross-review at review
+ time.
+
+### i18n — convention #4980 (ratified 2026-07-04)
+
+This file is the **English mirror** of `Conway/CHSHFreeWill.lean`
+(`namespace Conway_en` > `namespace CHSHFreeWill_en`, `_en`-suffixed
+imports) — sibling pair Pattern A, like `Conway/CHSHLandau_en`. The body
+(signatures, defs, proofs) is byte-identical between the two files, up to
+the `_en` qualifiers; only the docstrings and comments differ. No inline
+bilingual block.
+-/
+
+import Conway.CHSH_en
+import Conway.CHSHQuantum_en
+import Conway.FreeWillTheorem_en
+
+namespace Conway_en
+
+namespace CHSHFreeWill_en
+
+open CHSH_en CHSHQuantum_en FreeWillTheorem_en
+
+/-!
+## Step 1: local deterministic model of the CHSH game
+
+The vocabulary is the Free Will Theorem's: responses are functions of the
+hidden state (the "past" of the universe). **Locality** is encoded by the
+signature, exactly like MIN in
+`Conway.FreeWillTheorem.TwoParticleResponse`: Alice's response never sees
+Bob's setting, and conversely — not a hypothesis to prove, a property of
+the type.
+-/
+
+/-- Alice's local response: for each hidden state and each of her two
+settings (`true` = x, `false` = y), a predetermined outcome `±1`.
+
+This is the two-setting analogue of
+`Conway.FreeWillTheorem.DeterministicResponse`
+(which carried three, spin directions). Locality (MIN) lives in the
+signature: Bob's setting does not appear. -/
+abbrev AliceResponse := HiddenState → Bool → Outcome
+
+/-- Bob's local response: same encoding, Alice's mirror. -/
+abbrev BobResponse := HiddenState → Bool → Outcome
+
+/-- CHSH score realized by the model `(α, β)` in the hidden state `state`:
+the four predetermined responses are injected into the score of
+`Conway.CHSH`. -/
+def realizedScore (α : AliceResponse) (β : BobResponse) (state : HiddenState) : ℤ :=
+ score (α state true) (α state false) (β state true) (β state false)
+
+/-!
+## Step 2: the local frontier, state by state
+
+The classical frontier of `Conway.CHSH` was a fact about four isolated
+outcomes. For a local deterministic model it holds **in every hidden
+state** — this is the bridge from the particular (one strategy) to the
+general (an entire family of strategies indexed by the past).
+-/
+
+/-- **Local deterministic frontier, exact form.** In every hidden state,
+the score realized by a local deterministic model is exactly `±2`.
+
+The proof delegates the 16-assignment enumeration to
+`Conway.CHSH.classical_abs_score`: each hidden state instantiates four
+responses, and the frontier applies. -/
+theorem local_abs_score (α : AliceResponse) (β : BobResponse) (state : HiddenState) :
+ |realizedScore α β state| = 2 :=
+ classical_abs_score _ _ _ _
+
+/-- Usual form of the local frontier. -/
+theorem local_bound (α : AliceResponse) (β : BobResponse) (state : HiddenState) :
+ |realizedScore α β state| ≤ 2 :=
+ local_abs_score α β state ▸ le_refl _
+
+/-- **No local deterministic model exceeds the classical frontier, in no
+hidden state.** The bound is not an average: it holds state by state, so
+no privileged state can save the model. -/
+theorem no_state_beyond_classical :
+ ¬ ∃ (α : AliceResponse) (β : BobResponse) (state : HiddenState),
+ (2 : ℤ) < realizedScore α β state := by
+ rintro ⟨α, β, state, h⟩
+ have habs : |realizedScore α β state| = 2 := local_abs_score α β state
+ have hle : realizedScore α β state ≤ |realizedScore α β state| := le_abs_self _
+ omega
+
+/-- The local frontier is **attained**: the canonical model — both parties
+always answer `+1` — realizes the score `+2` in every state.
+The bound of `local_bound` is therefore tight for local models. -/
+def canonicalAlice : AliceResponse := fun _ _ => .positive
+
+def canonicalBob : BobResponse := fun _ _ => .positive
+
+@[simp]
+theorem canonical_score (state : HiddenState) :
+ realizedScore canonicalAlice canonicalBob state = 2 := by
+ simp [realizedScore, canonicalAlice, canonicalBob, score, Outcome.value]
+
+/-!
+## Step 3: the Tsirelson gap excludes local deterministic models
+
+Quantum mechanics predicts (and experiment confirms) CHSH correlations of
+value `2√2` — strictly above the local frontier
+(`Conway.CHSHQuantum.classical_quantum_gap`). Since every local
+deterministic model is capped at `2` in each state, none can reproduce the
+quantum prediction.
+-/
+
+/-- Real form of the local frontier: the realized score, seen as a real,
+stays under the classical frontier. -/
+theorem local_bound_real (α : AliceResponse) (β : BobResponse) (state : HiddenState) :
+ (realizedScore α β state : ℝ) ≤ 2 := by
+ have h : realizedScore α β state ≤ 2 := by
+ have habs : |realizedScore α β state| = 2 := local_abs_score α β state
+ have hle : realizedScore α β state ≤ |realizedScore α β state| := le_abs_self _
+ omega
+ exact_mod_cast h
+
+/-- **Tsirelson's gap dominates every local score.** The quantum value
+`2√2` is strictly above the classical frontier, and every local
+deterministic model realizes at most `2`: the gap is incompressible for
+these models. -/
+theorem tsirelson_beyond_every_local_score :
+ (2 : ℝ) < 2 * √2 ∧
+ ∀ (α : AliceResponse) (β : BobResponse) (state : HiddenState),
+ (realizedScore α β state : ℝ) ≤ 2 :=
+ ⟨classical_quantum_gap, local_bound_real⟩
+
+/-- **Indeterminism conclusion via the CHSH route.** No model where the
+two parties' responses are deterministic functions of the hidden state
+(locality by signature) can realize a CHSH score strictly above the
+classical frontier — while the quantum value is `2√2 > 2`.
+
+This is the same conclusion as `Conway.FreeWillTheorem.free_will_theorem`
+(the responses are not functions of the past), obtained through a
+**statistical** argument (Tsirelson's numerical gap) where the FWT uses a
+**contextual** argument (the absence of a Kochen-Specker coloring). The
+hypotheses differ — two settings versus three directions, numerical gap
+versus impossible coloring — the conclusion is shared. -/
+theorem chsh_indeterminism :
+ ¬ ∃ (α : AliceResponse) (β : BobResponse) (state : HiddenState),
+ (2 : ℝ) < realizedScore α β state := by
+ rintro ⟨α, β, state, h⟩
+ exact no_state_beyond_classical ⟨α, β, state, by exact_mod_cast h⟩
+
+/-!
+## Step 4: structural correspondence of the two routes
+
+ | | Contextual route (FWT, `Lean-16f`) | Statistical route (CHSH, `Lean-13b/13c/13d`) |
+ |---|---|---|
+ | Settings per party | 3 orthogonal directions | 2 binary settings |
+ | Axioms | SPIN + TWIN + MIN | locality (by signature) + quantum statistics |
+ | Contradiction engine | `kochen_specker`: no valid coloring | `classical_quantum_gap`: `2 < 2√2` |
+ | What is denied | any response function of the past (determinism) | any local deterministic model reproducing `2√2` |
+ | Strength of the conclusion | exact, no statistical hypothesis | numerical: quantifies the gap (`2√2 − 2`) |
+
+ The two routes are **complementary**: the FWT says nothing about the
+ numerical gap, the CHSH route says nothing about the perfect TWIN
+ correlations. The notebook `Lean-13d` walks both columns on the same
+ witness.
+-/
+
+end CHSHFreeWill_en
+
+end Conway_en
diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway_en.lean b/MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway_en.lean
index 4fd7918935..97050cfb8e 100644
--- a/MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway_en.lean
+++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway_en.lean
@@ -34,6 +34,12 @@
- `Conway.CHSH` — classical boundary of the CHSH Bell inequality
(Clauser-Horne-Shimony-Holt 1969): every deterministic local strategy
with binary outcomes has a score of absolute value exactly 2.
+ - `Conway.CHSHFreeWill` — bridge between the CHSH series and the Free
+ Will Theorem: a local deterministic model of the CHSH game as response
+ functions of the hidden state (locality by signature, the structural
+ analogue of MIN) cannot realize a score beyond 2 in any state, while
+ quantum mechanics reaches 2√2 — the same indeterminism conclusion as
+ the FWT, through the statistical route.
- `Conway.CollatzLike` — Collatz-type generalizations (3n+1),
Syracuse conjecture reformalized in Lean.
- `Conway.Angel` — Conway's Angel problem (1996 / 2002 *Angel
@@ -63,6 +69,7 @@ import Conway.Life_en
import Conway.KochenSpecker_en
import Conway.FreeWillTheorem_en
import Conway.CHSH_en
+import Conway.CHSHFreeWill_en
import Conway.MathlibMap_en
import Conway.CollatzLike_en
import Conway.FractranLemmas_en