Lean-13c : la saturation de Tsirelson — le témoin de Pauli et le critère de Landau

Série : SymbolicAI/Lean | Précédent : Lean-13b — Tsirelson natif | Suivant : Lean-13d — Indéterminisme natif

Lean-13b a établi la frontière : la valeur classique \(2\), la borne quantique \(2\sqrt{2}\) importée de Mathlib, et le gap strict entre les deux. Mais elle nommait sa propre limite, et la première était la plus importante : la borne est un plafond, pas un maximum démontré. Rien ne prouvait qu’une stratégie quantique atteint \(2\sqrt{2}\).

Cette tranche exécute le module qui répond à cette question : Conway.CHSHLandau, quatrième tranche du pilote quantique de l’Epic #13106. Son résultat central, chsh_landau, exhibe un témoin explicite — quatre observables construites sur les matrices de Pauli \(\sigma_z\) et \(\sigma_x\) — dont l’opérateur CHSH vaut exactement \(2\sqrt{2} \cdot 1\) : la constante de Tsirelson est réalisée, pas seulement majorée.

Sur les quatre points que Lean-13b déclarait non établis, cette tranche en lève trois :

Point déclaré ouvert par Lean-13b	Ici
Saturation de \(2\sqrt{2}\)	prouvée — égalité exacte chsh_landau
Construction matricielle (Pauli, \(2\times 2\))	donnée — sigmaZ, sigmaX, B₀, B₁
Forme bilatérale en norme d’opérateur	livrée en forme spectrale — chsh_landau_diagonal
Interprétation probabiliste complète	reste ouverte (section 9)

1. Vérification de l’environnement

Ce notebook s’exécute sur le kernel Lean 4 (lean4-wsl), le lake conway_lean au pin leanprover/lean4:v4.33.0 — la même chaîne que Lean-13b. Le module importé, Conway.CHSHLandau, est le quatrième de la série CHSH du lake : après la frontière déterministe (Conway.CHSH), son enveloppe randomisée (Conway.CHSHRandomized) et la borne quantique importée (Conway.CHSHQuantum), il construit le témoin qui sature la borne.

import Conway.CHSHLandau

import Conway.CHSHLandau

--% env 0

Raw input

{"cmd": "import Conway.CHSHLandau"}

Raw output

{"env": 0}

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

Avant de lire quelque signature que ce soit, vérifier que le kernel répond.

-- Contrôle positif : le kernel doit rendre 4.
#eval 2 + 2

-- Contrôle positif : le kernel doit rendre 4.

#eval 2 + 2
 4

--% env 1

Raw input

{"cmd": "-- Contr\u00f4le positif : le kernel doit rendre 4.\n#eval 2 + 2", "env": 0}

Raw output

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

3. Le témoin — quatre observables explicites

Lean-13b écrivait : « aucun opérateur de Pauli, aucune matrice \(2 \times 2\) : IsCHSHTuple est une structure algébrique abstraite, pas une réalisation physique ». Les voici. Le témoin vit dans Matrix (Fin 2) (Fin 2) ℝ — le modèle réduit à un qubit :

Rôle	Observable	Définition	Propriétés
Alice \(A_0\)	\(\sigma_z\)	\(\mathrm{diag}(1, -1)\)	involutive, symétrique
Alice \(A_1\)	\(\sigma_x\)	antidiagonale	involutive, symétrique
Bob \(B_0\)	\((\sigma_z + \sigma_x)/\sqrt{2}\)	combinaison	involutive, symétrique
Bob \(B_1\)	\((\sigma_z - \sigma_x)/\sqrt{2}\)	combinaison	involutive, symétrique

-- Les quatre briques du témoin, telles que le lake les déclare
#check @Conway.CHSHLandau.sigmaZ
#check @Conway.CHSHLandau.sigmaX
#check @Conway.CHSHLandau.B₀
#check @Conway.CHSHLandau.B₁

-- Les quatre briques du témoin, telles que le lake les déclare

#check @Conway.CHSHLandau.sigmaZ
 Conway.CHSHLandau.sigmaZ : Matrix (Fin 2) (Fin 2) ℝ

#check @Conway.CHSHLandau.sigmaX
 Conway.CHSHLandau.sigmaX : Matrix (Fin 2) (Fin 2) ℝ

#check @Conway.CHSHLandau.B₀
 Conway.CHSHLandau.B₀ : Matrix (Fin 2) (Fin 2) ℝ

#check @Conway.CHSHLandau.B₁
 Conway.CHSHLandau.B₁ : Matrix (Fin 2) (Fin 2) ℝ

--% env 2

Raw input

{"cmd": "-- Les quatre briques du t\u00e9moin, telles que le lake les d\u00e9clare\n#check @Conway.CHSHLandau.sigmaZ\n#check @Conway.CHSHLandau.sigmaX\n#check @Conway.CHSHLandau.B\u2080\n#check @Conway.CHSHLandau.B\u2081", "env": 1}

Raw output

{"messages": [{"severity": "info", "pos": {"line": 2, "column": 0}, "endPos": {"line": 2, "column": 6}, "data": "Conway.CHSHLandau.sigmaZ : Matrix (Fin 2) (Fin 2) ℝ"}, {"severity": "info", "pos": {"line": 3, "column": 0}, "endPos": {"line": 3, "column": 6}, "data": "Conway.CHSHLandau.sigmaX : Matrix (Fin 2) (Fin 2) ℝ"}, {"severity": "info", "pos": {"line": 4, "column": 0}, "endPos": {"line": 4, "column": 6}, "data": "Conway.CHSHLandau.B₀ : Matrix (Fin 2) (Fin 2) ℝ"}, {"severity": "info", "pos": {"line": 5, "column": 0}, "endPos": {"line": 5, "column": 6}, "data": "Conway.CHSHLandau.B₁ : Matrix (Fin 2) (Fin 2) ℝ"}], "env": 2}

Lecture du résultat — la frontière computable / noncomputable

Les deux matrices de Pauli sont des définitions computables : leurs entrées sont des littéraux entiers. Les observables de Bob, elles, sont noncomputable — la marque de \(\sqrt{2}\) : un nombre réel dont aucune fonction ne calcule les décimales. C’est toute la différence entre écrire \(1/\sqrt{2}\) et le calculer : le lake choisit d’écrire, et de ne jamais approximer.

4. Exemple guidé 1 — la signature de l’égalité centrale

Le théorème central du module. Ce qu’il faut lire dans sa conclusion : un signe \(=\), pas un signe \(\le\).

#check @Conway.CHSHLandau.chsh_landau

#check @Conway.CHSHLandau.chsh_landau
 Conway.CHSHLandau.chsh_landau : Conway.CHSHQuantum.chshOperator Conway.CHSHLandau.A₀ Conway.CHSHLandau.A₁
    Conway.CHSHLandau.B₀ Conway.CHSHLandau.B₁ =
  (2 * √2) • 1

--% env 3

Raw input

{"cmd": "#check @Conway.CHSHLandau.chsh_landau", "env": 2}

Raw output

{"messages": [{"severity": "info", "pos": {"line": 1, "column": 0}, "endPos": {"line": 1, "column": 6}, "data": "Conway.CHSHLandau.chsh_landau : Conway.CHSHQuantum.chshOperator Conway.CHSHLandau.A₀ Conway.CHSHLandau.A₁\n Conway.CHSHLandau.B₀ Conway.CHSHLandau.B₁ =\n (2 * √2) • 1"}], "env": 3}

Lecture du résultat — l’opérateur vaut exactement \(2\sqrt 2\)

L’opérateur CHSH du quadruple \((\sigma_z,\ \sigma_x,\ (\sigma_z+\sigma_x)/\sqrt 2,\ (\sigma_z-\sigma_x)/\sqrt 2)\) vaut exactement \((2\sqrt 2) \cdot 1\) — l’identité matricielle scalée. Autrement dit : la constante que CHSHQuantum.tsirelson_bound majore en général est atteinte par ce témoin. La borne de Tsirelson n’était qu’un plafond ; elle devient un maximum, démontré par exhibition.

La preuve, côté lake, exécute un programme algébrique : les huit produits de l’opérateur développé se réordonnent en \(2\sigma_z^2 + 2\sigma_x^2\) plus quatre termes croisés \(\sigma_z\sigma_x + \sigma_x\sigma_z\) qui s’annulent deux à deux ; il reste \((4/\sqrt 2) \cdot 1\), et \(4/\sqrt 2 = 2\sqrt 2\).

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

Comme dans Lean-13b, la question n’est pas seulement « quel est l’énoncé ? » mais « sur quoi repose-t-il ? ». Un théorème peut reposer sur sorryAx — l’axiome du trou — et ne rien prouver du tout.

#print axioms Conway.CHSHLandau.chsh_landau

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

--% env 4

Raw input

{"cmd": "#print axioms Conway.CHSHLandau.chsh_landau", "env": 3}

Raw output

{"messages": [{"severity": "info", "pos": {"line": 1, "column": 0}, "endPos": {"line": 1, "column": 6}, "data": "'Conway.CHSHLandau.chsh_landau' depends on axioms: [propext, Classical.choice, Quot.sound]"}], "env": 4}

Lecture du résultat — les axiomes : trois, aucun sorryAx

Trois axiomes, tous standards de Mathlib (propext, Classical.choice, Quot.sound) — et pas de sorryAx. La chaîne est transparente : à aucun étage on n’admet ce qu’on prétend prouver. La saturation repose sur les mêmes fondements que la borne qu’elle sature.

6. Exemple guidé 3 — la forme spectrale bilatérale

L’égalité centrale dit S = 2√2 • 1 globalement. Le théorème suivant la précise entrée par entrée — et c’est la jambe bilatérale qui manquait à la série.

#check @Conway.CHSHLandau.chsh_landau_diagonal

#check @Conway.CHSHLandau.chsh_landau_diagonal
 Conway.CHSHLandau.chsh_landau_diagonal : ∀ (i j : Fin 2),
  Conway.CHSHQuantum.chshOperator Conway.CHSHLandau.A₀ Conway.CHSHLandau.A₁ Conway.CHSHLandau.B₀ Conway.CHSHLandau.B₁ i
      j =
    if i = j then 2 * √2 else 0

--% env 5

Raw input

{"cmd": "#check @Conway.CHSHLandau.chsh_landau_diagonal", "env": 4}

Raw output

{"messages": [{"severity": "info", "pos": {"line": 1, "column": 0}, "endPos": {"line": 1, "column": 6}, "data": "Conway.CHSHLandau.chsh_landau_diagonal : ∀ (i j : Fin 2),\n Conway.CHSHQuantum.chshOperator Conway.CHSHLandau.A₀ Conway.CHSHLandau.A₁ Conway.CHSHLandau.B₀ Conway.CHSHLandau.B₁ i\n j =\n if i = j then 2 * √2 else 0"}], "env": 5}

Lecture du résultat — un opérateur diagonal, tout vecteur propre

L’entrée \((i, j)\) de l’opérateur vaut \(2\sqrt 2\) si \(i = j\), \(0\) sinon : l’opérateur est diagonal, et chaque vecteur de base est vecteur propre pour la valeur propre \(2\sqrt 2\). CHSHQuantum.tsirelson_bound donnait \(\le 2\sqrt 2\) en général ; l’égalité centrale donnait l’atteinte ; cette forme spectrale montre qu’elle tient des deux côtés — la majoration est une égalité, entrée par entrée.

7. Le cœur algébrique — l’anticommutateur

Tout le module tient dans une identité de quatre entrées : \(\sigma_z\sigma_x + \sigma_x\sigma_z = 0\). C’est l’atome dont découlent l’involutivité des observables de Bob et l’égalité centrale.

#check @Conway.CHSHLandau.sigmaZ_anticomm_sigmaX
#check @Conway.CHSHLandau.sqrt_two_sq

#check @Conway.CHSHLandau.sigmaZ_anticomm_sigmaX
 Conway.CHSHLandau.sigmaZ_anticomm_sigmaX : Conway.CHSHLandau.sigmaZ * Conway.CHSHLandau.sigmaX +
    Conway.CHSHLandau.sigmaX * Conway.CHSHLandau.sigmaZ =
  0

#check @Conway.CHSHLandau.sqrt_two_sq
 Conway.CHSHLandau.sqrt_two_sq : √2 ^ 2 = 2

--% env 6

Raw input

{"cmd": "#check @Conway.CHSHLandau.sigmaZ_anticomm_sigmaX\n#check @Conway.CHSHLandau.sqrt_two_sq", "env": 5}

Raw output

{"messages": [{"severity": "info", "pos": {"line": 1, "column": 0}, "endPos": {"line": 1, "column": 6}, "data": "Conway.CHSHLandau.sigmaZ_anticomm_sigmaX : Conway.CHSHLandau.sigmaZ * Conway.CHSHLandau.sigmaX +\n Conway.CHSHLandau.sigmaX * Conway.CHSHLandau.sigmaZ =\n 0"}, {"severity": "info", "pos": {"line": 2, "column": 0}, "endPos": {"line": 2, "column": 6}, "data": "Conway.CHSHLandau.sqrt_two_sq : √2 ^ 2 = 2"}], "env": 6}

Lecture du résultat — l’anticommutateur des Pauli s’annule

Deux lectures. D’abord l’anticommutateur : les matrices de Pauli ne commutent pas, mais leur anticommutateur s’annule — et ce sont précisément les termes croisés de cette forme qui apparaissent dans le carré des \(B_j\) et dans l’opérateur CHSH développé.

Ensuite sqrt_two_sq : \((\sqrt 2)^2 = 2\). C’est le seul traitement que le module réserve à \(\sqrt 2\) — une quantité formelle, manipulée par son carré, jamais approchée numériquement. Aucune preuve du module ne contient de décimale.

8. Le critère de Landau, vérifié sur le témoin

Landau (1988) caractérise la valeur quantique maximale du score CHSH d’une matrice de corrélation \(C\) par les valeurs propres de sa partie symétrique. Le théorème général n’est pas formalisé dans le lake — ce qui l’est, c’est sa vérification sur le témoin.

#check @Conway.CHSHLandau.corrMatrix
#check @Conway.CHSHLandau.corrMatrix_symm
#check @Conway.CHSHLandau.corrMatrix_sq

#check @Conway.CHSHLandau.corrMatrix
 Conway.CHSHLandau.corrMatrix : Matrix (Fin 2) (Fin 2) ℝ

#check @Conway.CHSHLandau.corrMatrix_symm
 Conway.CHSHLandau.corrMatrix_symm : Conway.CHSHLandau.corrMatrix.transpose = Conway.CHSHLandau.corrMatrix

#check @Conway.CHSHLandau.corrMatrix_sq
 Conway.CHSHLandau.corrMatrix_sq : Conway.CHSHLandau.corrMatrix * Conway.CHSHLandau.corrMatrix = 1

--% env 7

Raw input

{"cmd": "#check @Conway.CHSHLandau.corrMatrix\n#check @Conway.CHSHLandau.corrMatrix_symm\n#check @Conway.CHSHLandau.corrMatrix_sq", "env": 6}

Raw output

{"messages": [{"severity": "info", "pos": {"line": 1, "column": 0}, "endPos": {"line": 1, "column": 6}, "data": "Conway.CHSHLandau.corrMatrix : Matrix (Fin 2) (Fin 2) ℝ"}, {"severity": "info", "pos": {"line": 2, "column": 0}, "endPos": {"line": 2, "column": 6}, "data": "Conway.CHSHLandau.corrMatrix_symm : Conway.CHSHLandau.corrMatrix.transpose = Conway.CHSHLandau.corrMatrix"}, {"severity": "info", "pos": {"line": 3, "column": 0}, "endPos": {"line": 3, "column": 6}, "data": "Conway.CHSHLandau.corrMatrix_sq : Conway.CHSHLandau.corrMatrix * Conway.CHSHLandau.corrMatrix = 1"}], "env": 7}

Lecture du résultat — le spectre du témoin : exactement \(\{-1, +1\}\)

La matrice de corrélation réduite du témoin est symétrique (corrMatrix_symm) et son carré vaut l’identité (corrMatrix_sq) : son spectre est exactement \(\{-1, +1\}\). Et le score du témoin vaut \(2\sqrt 2\) — la valeur que la caractérisation de Landau prédit pour ce spectre. La direction « suffisant » du critère est ainsi documentée par témoin explicite ; la caractérisation générale (les deux sens) reste déclarée ouverte.

9. Ce que cette tranche n’établit pas

Nommer les limites fait partie du livrable — comme dans Lean-13b, la table de statut est le résumé falsifiable du module :

Énoncé	Statut
Opérateur CHSH du témoin \(= 2\sqrt 2 \cdot 1\) (égalité exacte)	prouvé
Involutivité des quatre observables (\(M^2 = 1\))	prouvé
Auto-adjointude (symétrie des matrices réelles)	prouvé
Forme spectrale : \(S\) diagonal, \(2\sqrt 2\) sur la diagonale	prouvé
Corrélation symétrique, de carré \(1\) (spectre \(\pm 1\))	prouvé
Caractérisation générale de Landau (les deux sens)	non établi — vérifié sur témoin seulement
Interprétation probabiliste complète (états, mesures)	non établi — déclaré ouvert
Commutation croisée \(A_i B_j = B_j A_i\) dans le modèle réduit	fausse, et non revendiquée

Le dernier point mérite d’être dit : les observables vivent dans le modèle réduit à un qubit, où la commutation croisée — hypothèse structurelle du IsCHSHTuple abstrait, vraie dans le modèle tensoriel \(A \otimes 1\), \(1 \otimes B\) sur \(\mathbb{R}^4\) — est fausse : \([\sigma_z,\ \sigma_z + \sigma_x] = [\sigma_z, \sigma_x] \neq 0\). Ce que le module établit est plus modeste et exact : la valeur de l’opérateur CHSH du témoin — la constante que la borne abstraite majore — est réalisée par une construction concrète. L’interprétation probabiliste complète (états, mesures, espérances) reste ouverte, comme dans Conway.CHSHQuantum.

10. Exercices

Exercice 1 — le carré de \(\sigma_x\), à la main

L’entrée \((i, j)\) du carré \(\sigma_x \cdot \sigma_x\) s’obtient en sommant, sur l’indice intermédiaire \(k\), les produits d’entrées \(\sigma_x(i,k) \cdot \sigma_x(k,j)\). Complétez carreSigmaX — le lake prouve que le résultat est l’identité, donc la diagonale vaut \(1\) et l’anti-diagonale \(0\). Le corps actuel rend \(0\) partout : sur la diagonale, votre valeur et l’identité divergeront — c’est le test.

-- Exercice 1 : l'entree (i, j) du carre de sigmaX, calculee a la main
-- TODO etudiant : remplacer le corps ci-dessous
def carreSigmaX (i j : Fin 2) : Int :=
  0

-- Doivent valoir 1, 1, 0 (le carre de sigmaX est l'identite)
#eval carreSigmaX 0 0
#eval carreSigmaX 1 1
#eval carreSigmaX 0 1
-- La preuve du lake, pour comparaison
#check @Conway.CHSHLandau.sigmaX_sq

-- Exercice 1 : l'entree (i, j) du carre de sigmaX, calculee a la main

-- TODO etudiant : remplacer le corps ci-dessous

def carreSigmaX (i j : Fin 2) : Int :=
🟨 Variable name `i` is not explicitly referenced.

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

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

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

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

  0

-- Doivent valoir 1, 1, 0 (le carre de sigmaX est l'identite)

#eval carreSigmaX 0 0
 0

#eval carreSigmaX 1 1
 0

#eval carreSigmaX 0 1
 0

-- La preuve du lake, pour comparaison

#check @Conway.CHSHLandau.sigmaX_sq
 Conway.CHSHLandau.sigmaX_sq : Conway.CHSHLandau.sigmaX * Conway.CHSHLandau.sigmaX = 1

--% env 8

Raw input

{"cmd": "-- Exercice 1 : l'entree (i, j) du carre de sigmaX, calculee a la main\n-- TODO etudiant : remplacer le corps ci-dessous\ndef carreSigmaX (i j : Fin 2) : Int :=\n 0\n\n-- Doivent valoir 1, 1, 0 (le carre de sigmaX est l'identite)\n#eval carreSigmaX 0 0\n#eval carreSigmaX 1 1\n#eval carreSigmaX 0 1\n-- La preuve du lake, pour comparaison\n#check @Conway.CHSHLandau.sigmaX_sq", "env": 7}

Raw output

{"messages": [{"severity": "warning", "pos": {"line": 3, "column": 17}, "endPos": {"line": 3, "column": 18}, "data": "Variable name `i` is not explicitly referenced.\n\nThe binding can be removed (if unused) or named `_` (if used implicitly).\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 3, "column": 19}, "endPos": {"line": 3, "column": 20}, "data": "Variable name `j` is not explicitly referenced.\n\nThe binding can be removed (if unused) or named `_` (if used implicitly).\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "info", "pos": {"line": 7, "column": 0}, "endPos": {"line": 7, "column": 5}, "data": "0"}, {"severity": "info", "pos": {"line": 8, "column": 0}, "endPos": {"line": 8, "column": 5}, "data": "0"}, {"severity": "info", "pos": {"line": 9, "column": 0}, "endPos": {"line": 9, "column": 5}, "data": "0"}, {"severity": "info", "pos": {"line": 11, "column": 0}, "endPos": {"line": 11, "column": 6}, "data": "Conway.CHSHLandau.sigmaX_sq : Conway.CHSHLandau.sigmaX * Conway.CHSHLandau.sigmaX = 1"}], "env": 8}

Exercice 2 — le carré de la constante de saturation

chsh_landau établit \(S = 2\sqrt 2 \cdot 1\). La constante \(2\sqrt 2\) est irrationnelle : aucun littéral entier ne la représente. Son carré, lui, est un entier — et c’est le certificat que le module manipule en interne (\(\sqrt 2\) n’apparaît jamais qu’à travers son carré, sqrt_two_sq). Déclarez cet entier.

-- Exercice 2 : le carre de la constante de saturation (2 * sqrt 2)^2
-- TODO etudiant : remplacer le corps ci-dessous
def carreConstanteSaturation : Int :=
  0

-- Doit valoir 8
#eval carreConstanteSaturation

-- TODO etudiant (commentaire) : pourquoi le carre est-il le bon certificat ici,
-- et pas une approximation decimale de sqrt(2) ?

-- Exercice 2 : le carre de la constante de saturation (2 * sqrt 2)^2

-- TODO etudiant : remplacer le corps ci-dessous

def carreConstanteSaturation : Int :=

  0

-- Doit valoir 8

#eval carreConstanteSaturation
 0

-- TODO etudiant (commentaire) : pourquoi le carre est-il le bon certificat ici,

-- et pas une approximation decimale de sqrt(2) ?

--% env 9

Raw input

{"cmd": "-- Exercice 2 : le carre de la constante de saturation (2 * sqrt 2)^2\n-- TODO etudiant : remplacer le corps ci-dessous\ndef carreConstanteSaturation : Int :=\n 0\n\n-- Doit valoir 8\n#eval carreConstanteSaturation\n\n-- TODO etudiant (commentaire) : pourquoi le carre est-il le bon certificat ici,\n-- et pas une approximation decimale de sqrt(2) ?", "env": 8}

Raw output

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

Exercice 3 — le signe qui distingue \(B_1\)

La matrice de corrélation du témoin a toutes ses entrées égales à \(\pm 1/\sqrt 2\) en valeur absolue — trois positives, une négative. Complétez signeCorrelation pour qu’elle rende le signe (\(+1\) ou \(-1\)) de l’entrée \((i, j)\). Le corps actuel rend \(0\) : le test révèle quelle entrée porte le signe \(-\).

-- Exercice 3 : le signe de l'entree (i, j) de la matrice de correlation du temoin
-- TODO etudiant : remplacer le corps ci-dessous
def signeCorrelation (i j : Fin 2) : Int :=
  0

-- Doivent valoir 1, 1, 1, -1
#eval signeCorrelation 0 0
#eval signeCorrelation 0 1
#eval signeCorrelation 1 0
#eval signeCorrelation 1 1
-- La matrice du lake et ses proprietes, pour comparaison
#check @Conway.CHSHLandau.corrMatrix_symm
#check @Conway.CHSHLandau.corrMatrix_sq

-- Exercice 3 : le signe de l'entree (i, j) de la matrice de correlation du temoin

-- TODO etudiant : remplacer le corps ci-dessous

def signeCorrelation (i j : Fin 2) : Int :=
🟨 Variable name `i` is not explicitly referenced.

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

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

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

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

  0

-- Doivent valoir 1, 1, 1, -1

#eval signeCorrelation 0 0
 0

#eval signeCorrelation 0 1
 0

#eval signeCorrelation 1 0
 0

#eval signeCorrelation 1 1
 0

-- La matrice du lake et ses proprietes, pour comparaison

#check @Conway.CHSHLandau.corrMatrix_symm
 Conway.CHSHLandau.corrMatrix_symm : Conway.CHSHLandau.corrMatrix.transpose = Conway.CHSHLandau.corrMatrix

#check @Conway.CHSHLandau.corrMatrix_sq
 Conway.CHSHLandau.corrMatrix_sq : Conway.CHSHLandau.corrMatrix * Conway.CHSHLandau.corrMatrix = 1

--% env 10

Raw input

{"cmd": "-- Exercice 3 : le signe de l'entree (i, j) de la matrice de correlation du temoin\n-- TODO etudiant : remplacer le corps ci-dessous\ndef signeCorrelation (i j : Fin 2) : Int :=\n 0\n\n-- Doivent valoir 1, 1, 1, -1\n#eval signeCorrelation 0 0\n#eval signeCorrelation 0 1\n#eval signeCorrelation 1 0\n#eval signeCorrelation 1 1\n-- La matrice du lake et ses proprietes, pour comparaison\n#check @Conway.CHSHLandau.corrMatrix_symm\n#check @Conway.CHSHLandau.corrMatrix_sq", "env": 9}

Raw output

{"messages": [{"severity": "warning", "pos": {"line": 3, "column": 22}, "endPos": {"line": 3, "column": 23}, "data": "Variable name `i` is not explicitly referenced.\n\nThe binding can be removed (if unused) or named `_` (if used implicitly).\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 3, "column": 24}, "endPos": {"line": 3, "column": 25}, "data": "Variable name `j` is not explicitly referenced.\n\nThe binding can be removed (if unused) or named `_` (if used implicitly).\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "info", "pos": {"line": 7, "column": 0}, "endPos": {"line": 7, "column": 5}, "data": "0"}, {"severity": "info", "pos": {"line": 8, "column": 0}, "endPos": {"line": 8, "column": 5}, "data": "0"}, {"severity": "info", "pos": {"line": 9, "column": 0}, "endPos": {"line": 9, "column": 5}, "data": "0"}, {"severity": "info", "pos": {"line": 10, "column": 0}, "endPos": {"line": 10, "column": 5}, "data": "0"}, {"severity": "info", "pos": {"line": 12, "column": 0}, "endPos": {"line": 12, "column": 6}, "data": "Conway.CHSHLandau.corrMatrix_symm : Conway.CHSHLandau.corrMatrix.transpose = Conway.CHSHLandau.corrMatrix"}, {"severity": "info", "pos": {"line": 13, "column": 0}, "endPos": {"line": 13, "column": 6}, "data": "Conway.CHSHLandau.corrMatrix_sq : Conway.CHSHLandau.corrMatrix * Conway.CHSHLandau.corrMatrix = 1"}], "env": 10}

11. Provenance, raccords et conclusion

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

Chaîne de dépendance, telle qu’elle se lit dans les sorties. chsh_landau n’est pas une redémonstration : elle réutilise CHSHQuantum.chshOperator sans le redéfinir, et s’appuie sur l’anticommutateur sigmaZ_anticomm_sigmaX et sur l’atome sqrt_two_sq. Les trois axiomes affichés (propext, Classical.choice, Quot.sound) sont ceux de Mathlib — la chaîne est transparente.

Raccords dans la série.

• Lean-13b — la borne que cette tranche sature : ensemble, les deux notebooks couvrent \(\le 2\sqrt 2\) et \(= 2\sqrt 2\) atteint.
• Lean-13 Kochen-Specker — la contextualité, dont CHSH est le pendant statistique.
• Lean-16f Free-Will — l’hypothèse que le jeu de CHSH met à l’épreuve expérimentale.
• Modules du lake — Conway.CHSH (frontière déterministe), Conway.CHSHRandomized (enveloppe randomisée), Conway.CHSHQuantum (borne importée), Conway.CHSHLandau (le témoin, exécuté ici).

Ce qui reste ouvert pour clore l’Epic #13106 : l’interprétation probabiliste complète (états, mesures, modèle tensoriel sur \(\mathbb{R}^4\)) et la caractérisation générale de Landau (les deux sens, preuve SDP complète). Aucune des deux n’est simulée ici par un exemple scalaire de remplacement.

Sources. L. J. Landau, « On the violation of Bell inequalities in quantum theory », Physics Letters A 120 (1988), 54-56 ; B. S. Cirel’son (Tsirelson), « Quantum generalizations of Bell’s inequality », Letters in Mathematical Physics 4 (1980), 93-100 ; M. Nielsen, I. Chuang, Quantum Computation and Quantum Information, Cambridge University Press (2000), §2.4-2.5.