Sixième tranche du pilote quantique de l’Epic #13106 (digestion et canonicalisation des mathématiques assistées). La série a établi jusqu’ici :
Lean-13 (Kochen-Specker) : aucune coloration {0,1} des 18 vecteurs de Cabello — la contradiction contextuelle ;
Lean-13b (Tsirelson) : la frontière classique |score| = 2 et la borne quantique 2√2 ;
Lean-13c (saturation) : un témoin de Pauli qui atteint2√2, et le critère de Landau vérifié dessus ;
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é.
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.
Prérequis : le score CHSH et la frontière classique (Lean-13b) ; le vocabulaire du libre arbitre (Lean-16f, lecture parallèle recommandée mais non exigée).
1. Vérification de l’environnement
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.
import Conway.CHSHFreeWill
import Conway.CHSH
import Conway.CHSHQuantum
import Conway.FreeWillTheorem
-- Conway.CHSHFreeWill : modele local deterministe + frontiere etat par etat + conclusion
-- Conway.CHSH : score CHSH et frontiere classique (|score| = 2)
-- Conway.CHSHQuantum : l'ecart de Tsirelson (2 < 2*sqrt(2))
-- Conway.FreeWillTheorem : HiddenState (le passe de l'univers) et le vocabulaire MIN
importConway.CHSHFreeWill
importConway.CHSH
importConway.CHSHQuantum
importConway.FreeWillTheorem
-- Conway.CHSHFreeWill : modele local deterministe + frontiere etat par etat + conclusion
-- Conway.CHSHQuantum : l'ecart de Tsirelson (2 < 2*sqrt(2))
-- Conway.FreeWillTheorem : HiddenState (le passe de l'univers) et le vocabulaire MIN
--% env 0
Raw input{"cmd": "import Conway.CHSHFreeWill\nimport Conway.CHSH\nimport Conway.CHSHQuantum\nimport Conway.FreeWillTheorem\n\n-- Conway.CHSHFreeWill : modele local deterministe + frontiere etat par etat + conclusion\n-- Conway.CHSH : score CHSH et frontiere classique (|score| = 2)\n-- Conway.CHSHQuantum : l'ecart de Tsirelson (2 < 2*sqrt(2))\n-- Conway.FreeWillTheorem : HiddenState (le passe de l'univers) et le vocabulaire MIN"}Raw output{"env": 0}
Interprétation. Cette cellule ne prouve rien à elle seule : elle rend les déclarations lisibles. Tout ce qui suit est soit une inspection (#check, #print axioms), soit un calcul (#eval), jamais une réimprovisation.
2. Le contrôle positif — #eval 2 + 2
Si le kernel tourne sans le lac résolu, tout le reste du notebook est sans valeur : ce contrôle atteste que la toolchain et les modules sont chargés.
-- Controle positif : le kernel doit rendre 4.
-- S'il rend une erreur, le lac n'est pas resolu et le reste du notebook est sans valeur.
#eval (2 : Nat) + 2
-- Controle positif : le kernel doit rendre 4.
-- S'il rend une erreur, le lac n'est pas resolu et le reste du notebook est sans valeur.
4
--% env 1
Raw input{"cmd": "-- Controle positif : le kernel doit rendre 4.\n-- S'il rend une erreur, le lac n'est pas resolu et le reste du notebook est sans valeur.\n#eval (2 : Nat) + 2", "env": 0}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 3, "column": 0},
"endPos": {"line": 3, "column": 5},
"data": "4"}],
"env": 1}
Interprétation.4. Le kernel est vivant, sa toolchain est celle du lac (v4.33.0).
3. Deux routes vers l’indéterminisme — tableau comparatif
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 reste du notebook parcourt la colonne droite.
4. Exemple guidé 1 — le modèle local déterministe
La définition centrale reprend le vocabulaire du libre arbitre : les réponses sont des fonctions de l’état cachéHiddenState (le « passé » de l’univers, chez Conway-Kochen). La localité — l’analogue de l’axiome MIN — vit dans la signature : la réponse d’Alice prend son propre réglage binaire (Bool : true = x, false = y) mais jamais celui de Bob.
Interprétation.AliceResponse = HiddenState → Bool → Outcome : pour chaque état caché et chacun de ses deux réglages, un résultat prédéterminé ±1. À rapprocher de Conway.FreeWillTheorem.TwoParticleResponse (HiddenState → Experimenter → VecIdx → Bool) : dans les deux cas, la localité/le MIN n’est pas une hypothèse — c’est une propriété du type, le réglage de l’autre parti n’apparaît nulle part. realizedScore injecte les quatre réponses prédéterminées dans le score de Conway.CHSH.
-- Le modele canonique : les deux partis repondent toujours +1.
-- Il realise le score +2 dans tout etat cache (borne atteinte).
example : Conway.CHSHFreeWill.realizedScore
Conway.CHSHFreeWill.canonicalAlice Conway.CHSHFreeWill.canonicalBob 0 = 2 :=
Conway.CHSHFreeWill.canonical_score 0
-- Le modele canonique : les deux partis repondent toujours +1.
-- Il realise le score +2 dans tout etat cache (borne atteinte).
Raw input{"cmd": "-- Le modele canonique : les deux partis repondent toujours +1.\n-- Il realise le score +2 dans tout etat cache (borne atteinte).\nexample : Conway.CHSHFreeWill.realizedScore\n Conway.CHSHFreeWill.canonicalAlice Conway.CHSHFreeWill.canonicalBob 0 = 2 :=\n Conway.CHSHFreeWill.canonical_score 0", "env": 2}Raw output{"env": 3}
Interprétation. La frontière locale n’est pas vacante : un modèle explicite la réalise. La borne que nous allons établir est donc serrée.
5. Exemple guidé 2 — la frontière locale, état par état
La frontière classique de Conway.CHSH était un fait sur quatre résultats isolés (16 assignations énumérées par decide). Ici elle devient un fait sur des familles entières de fonctions indexées par le passé.
Interprétation.local_abs_score : dans tout état caché, |realizedScore| = 2 exactement — la preuve délègue l’énumération à CHSH.classical_abs_score. no_state_beyond_classical est la forme qui servira à la conclusion : aucun état privilégié ne peut sauver un modèle — la borne n’est pas une moyenne, elle vaut état par état.
6. Exemple guidé 3 — l’écart de Tsirelson et la conclusion d’indéterminisme
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. Les deux faits mis côte à côte donnent la conclusion.
Interprétation.chsh_indeterminism est la conclusion de la tranche : aucun couple de réponses locales déterministes de l’état caché ne réalise un score CHSH strictement supérieur à 2 en réels — alors que la valeur quantique est 2√2 > 2 (écart 2√2 − 2 ≈ 0,83). C’est le même énoncé concluant que Conway.FreeWillTheorem.free_will_theorem — les réponses ne sont pas des fonctions du passé — obtenu par un argument statistique là où le FWT utilise un argument contextuel. Les hypothèses diffèrent, la conclusion est commune.
Interprétation. Chaque ligne se termine par un sous-ensemble des axiomes standard [propext, Classical.choice, Quot.sound] (les délégations pures à l’énumération n’exigent que propext) — jamais sorryAx, jamais Lean.ofReduceBool ni native_decide : « prouvé » veut dire vérifié par le noyau Lean, pas plausible.
7. Ce que cette tranche n’établit pas
L’équivalence des deux routes : seule la conclusion commune est formalisée ; SPIN + TWIN + MIN et « localité + statistiques quantiques » sont des jeux d’hypothèses distincts.
L’interprétation probabiliste complète (états, mesures, espérances sur le modèle tensoriel ℝ⁴) : déclarée ouverte, comme dans Conway.CHSHQuantum.
Les modèles stochastiques non locaux : la conclusion vise les modèles déterministes locaux ; l’enveloppe probabiliste classique est le sujet de Conway.CHSHRandomized.
8. Exercices
Trois exercices bornés pour manipuler les objets de la tranche. Aucun ne demande de poser un sorry : chaque amorce vérifie déjà un énoncé voisin.
Exercice 1 — le modèle « tout négatif »
Contre-intuitif : inverser toutes les réponses du modèle canonique (+1 → −1 chez Alice et Bob) ne change pas le score — chaque produit aᵢ·bⱼ conserve son signe. Définissez aliceNeg/bobNeg (constantes à .negative) et vérifiez que le score réalisé vaut encore 2, en instanciant canonical_score après avoir prouvé que vos fonctions sont égales aux canoniques.
-- Exercice 1 : le modele tout-negatif realize AUSSI +2.
-- TODO etudiant : definir aliceNeg / bobNeg, prouver l'egalite avec les canoniques,
-- puis instancier canonical_score. Indice : funext + rfl suffisent.
-- Amorce : le theoreme a instancier --
#check @Conway.CHSHFreeWill.canonical_score
-- Exercice 1 : le modele tout-negatif realize AUSSI +2.
-- TODO etudiant : definir aliceNeg / bobNeg, prouver l'egalite avec les canoniques,
-- puis instancier canonical_score. Indice : funext + rfl suffisent.
Raw input{"cmd": "-- Exercice 1 : le modele tout-negatif realize AUSSI +2.\n-- TODO etudiant : definir aliceNeg / bobNeg, prouver l'egalite avec les canoniques,\n-- puis instancier canonical_score. Indice : funext + rfl suffisent.\n-- Amorce : le theoreme a instancier --\n#check @Conway.CHSHFreeWill.canonical_score", "env": 6}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 5, "column": 0},
"endPos": {"line": 5, "column": 6},
"data":
"Conway.CHSHFreeWill.canonical_score : ∀ (state : Conway.FreeWillTheorem.HiddenState),\n Conway.CHSHFreeWill.realizedScore Conway.CHSHFreeWill.canonicalAlice Conway.CHSHFreeWill.canonicalBob state = 2"}],
"env": 7}
Exercice 2 — la borne inférieure
local_abs_score donne |s| = 2. Énoncez et prouvez la borne inférieure : pour tout modèle local et tout état, -2 ≤ realizedScore. Indice : le_abs_self appliqué à -s donne -s ≤ |s| ; réécrivez |s| = 2 avec local_abs_score, puis concluez — omega convient pour l’arithmétique de signe.
-- Exercice 2 : -2 <= realizedScore pour tout modele local, tout etat.
-- TODO etudiant : le theoreme (signature ci-dessous) et sa preuve.
-- Etape 1 : le_abs_self sur -realizedScore donne -s <= |s|
-- Etape 2 : reecrire |s| = 2 (local_abs_score), conclure (omega convient).
-- Amorce : les deux ingredients --
#check @Conway.CHSHFreeWill.local_abs_score
#check @le_abs_self
-- Exercice 2 : -2 <= realizedScore pour tout modele local, tout etat.
-- TODO etudiant : le theoreme (signature ci-dessous) et sa preuve.
-- Etape 1 : le_abs_self sur -realizedScore donne -s <= |s|
Raw input{"cmd": "-- Exercice 2 : -2 <= realizedScore pour tout modele local, tout etat.\n-- TODO etudiant : le theoreme (signature ci-dessous) et sa preuve.\n-- Etape 1 : le_abs_self sur -realizedScore donne -s <= |s|\n-- Etape 2 : reecrire |s| = 2 (local_abs_score), conclure (omega convient).\n-- Amorce : les deux ingredients --\n#check @Conway.CHSHFreeWill.local_abs_score\n#check @le_abs_self", "env": 7}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 6, "column": 0},
"endPos": {"line": 6, "column": 6},
"data":
"Conway.CHSHFreeWill.local_abs_score : ∀ (α : Conway.CHSHFreeWill.AliceResponse) (β : Conway.CHSHFreeWill.BobResponse)\n (state : Conway.FreeWillTheorem.HiddenState), |Conway.CHSHFreeWill.realizedScore α β state| = 2"},
{"severity": "info",
"pos": {"line": 7, "column": 0},
"endPos": {"line": 7, "column": 6},
"data":
"@le_abs_self : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] (a : α), a ≤ |a|"}],
"env": 8}
Exercice 3 — un modèle qui réalise −2
Tous les modèles locaux déterministes réalisent exactement ±2 — mais lequel donne −2 ? Définissez le modèle où Alice répond +1 sur x et −1 sur y, Bob pareil, et calculez le score réalisé au #eval : vous devez voir -2. Vérifiez ensuite la cohérence avec local_abs_score.
-- Exercice 3 : construire et calculer un modele a -2.
-- TODO etudiant : definir aliceM / bobM (true -> .positive, false -> .negative),
-- puis evaluer #eval Conway.CHSHFreeWill.realizedScore aliceM bobM 0
-- Resultat attendu : -2.
-- Amorce : les valeurs d'un resultat se calculent --
#eval Conway.CHSH.Outcome.positive.value
#eval Conway.CHSH.Outcome.negative.value
#check @Conway.CHSHFreeWill.local_abs_score
-- Exercice 3 : construire et calculer un modele a -2.
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.
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.
Raccords. Prolonge Lean-13b (score et frontière) et Lean-13c (saturation) ; fait le pont avec Lean-16f (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é ?