Navigation : << Lean-12 Sensitivity | Index | Lean-14 Finiteness-Derivatives >>
Kernel : Python 3 (illustrations + vérifications combinatoires) + Lean 4 (WSL) pour les sections 6-7
En 1967, Simon Kochen et Ernst Specker publient un théorème qui exclut une large classe d’interpretations de la mecanique quantique : les théories a variables cachees non-contextuelles. La preuve originale utilise 117 vecteurs de R^3. Plusieurs raffinements suivent (33 vecteurs par Peres 1991, 20 par Kernaghan 1994) jusqu’a la preuve la plus compacte connue avec 18 vecteurs de R^4 par Cabello, Estebaranz et Garcia-Alcaine en 1996. C’est cette dernière qui sert de noyau combinatoire au théorème de libre arbitre de Conway-Kochen (2006).
Ce notebook couvre les Piliers 1 et 3 de l’Epic #1651 (Théorème de Libre Arbitre Conway-Kochen). Il presente : 1. La question : peut-on attribuer une valeur 0/1 aux observables quantiques de maniere non-contextuelle ? 2. La structure : 18 vecteurs de R^4 en 9 bases orthogonales, chacun appartenant a exactement 2 bases 3. L’argument de parite : 9 (impair) vs 2k (pair) – contradiction 4. Vérification computationnelle : aucune coloration valide n’existe sur 2^18 essais 5. Le port Lean 4 : KochenSpecker.lean (Pilier 1, Prouvé) + FreeWillTheorem.lean (Pilier 2, Prouvé) 6. Vérification lake build : 0 sorry dans les 2 Piliers (KochenSpecker + FreeWillTheorem)
En mecanique quantique, mesurer une grandeur revient a projeter l’état du système sur une famille de vecteurs orthonormaux. Pour un système de spin-1, mesurer le carré du spin selon trois axes mutuellement orthogonaux (en 3D) ou quatre axes mutuellement orthogonaux (en 4D pour les paires entrelacees) donne toujours un seul résultat 1 et le reste 0.
Variable cachee non-contextuelle (NCHV) : une théorie qui attribue a chaque observable une valeur predeterminee, independante du contexte de mesure (i.e. des autres observables mesures simultanement).
Pour les observables associes a des directions vectorielles, cela revient a une fonction \(f : \text{vecteurs} \to \{0, 1\}\) telle que dans toute base orthogonale, exactement un vecteur recoit la valeur 1.
Théorème (Kochen-Specker 1967, version Cabello et al. 1996) : Il existe un ensemble fini de vecteurs de R^4 – précisément 18 vecteurs organises en 9 bases orthogonales – tel qu’aucune fonction \(f\) a valeurs dans \(\{0, 1\}\) ne peut satisfaire la contrainte “un seul 1 par base”.
Consequence : aucune théorie a variables cachees non-contextuelle ne peut reproduire les predictions de la mecanique quantique. Toute attribution de valeurs predeterminees doit dependre du contexte ou abandonner la realisme local.
import numpy as np
import matplotlib
matplotlib.use('Agg')
import matplotlib.pyplot as plt
from itertools import product
from collections import Counter
np.set_printoptions(suppress=True, precision=4)
print('Setup ok : numpy', np.__version__)Setup ok : numpy 2.4.2Les 18 vecteurs de la preuve Cabello et al. (1996) sont enumeres ci-dessous. Ils sont initialement donnes a normalisation pres – les coordonnees brutes (entières) suffisent pour les arguments combinatoires d’orthogonalite (le produit scalaire vaut 0 si et seulement si la version normalisee est orthogonale).
Source : Cabello, Estebaranz, Garcia-Alcaine, “Bell-Kochen-Specker theorem: A proof with 18 vectors”, Phys. Lett. A 212 (1996), 183-187. Table reproduite dans Wikipedia, section Overview.
# Les 18 vecteurs distincts (coordonnees brutes, R^4)
vectors = {
0: ( 0, 0, 0, 1), # v0
1: ( 0, 0, 1, 0), # v1
2: ( 1, 1, 0, 0), # v2
3: ( 1, -1, 0, 0), # v3
4: ( 0, 1, 0, 0), # v4
5: ( 1, 0, 1, 0), # v5
6: ( 1, 0, -1, 0), # v6
7: ( 1, -1, 1, -1), # v7
8: ( 1, -1, -1, 1), # v8
9: ( 0, 0, 1, 1), # v9
10: ( 1, 1, 1, 1), # v10
11: ( 0, 1, 0, -1), # v11
12: ( 1, 0, 0, 1), # v12
13: ( 1, 0, 0, -1), # v13
14: ( 0, 1, -1, 0), # v14
15: ( 1, 1, -1, 1), # v15
16: ( 1, 1, 1, -1), # v16
17: (-1, 1, 1, 1), # v17
}
# Vérifier l'unicite (18 vecteurs distincts apres deduplication)
unique_vecs = {v: k for k, v in vectors.items()}
assert len(unique_vecs) == 18, f'Doublons detectes : {18 - len(unique_vecs)}'
print(f'18 vecteurs distincts : OK')
print(f'Norme L2 (au carre) par vecteur : {sorted(set(sum(x*x for x in v) for v in vectors.values()))}')18 vecteurs distincts : OK
Norme L2 (au carre) par vecteur : [1, 2, 4]Les 18 vecteurs se groupent en 3 classes selon leur norme :
| Type | Exemple | Norme^2 | Nb vecteurs |
|---|---|---|---|
| Standards (1 coord) | (0,0,0,1) | 1 | 2 |
| Plans (2 coords +/-) | (1,1,0,0), (1,-1,0,0) | 2 | 8 |
| Quadruplets (4 coords +/-) | (1,1,1,1), (1,-1,1,-1) | 4 | 8 |
Tous deviennent unitaires après normalisation. L’orthogonalite (produit scalaire = 0) n’est pas affectee par la normalisation.
Les 18 vecteurs s’organisent en 9 bases orthogonales (“contextes”) de 4 vecteurs chacune. Chaque base correspond a une expérience de mesure simultanee compatible.
Notation : Ck = (i, j, k, l) signifie que la k-ieme base contient les vecteurs d’indices i, j, k, l (dans l’ordre du tableau Cabello original).
# Les 9 contextes (bases orthogonales) -- chaque entrée liste 4 indices de vecteurs
contexts = [
( 0, 1, 2, 3), # C0
( 0, 4, 5, 6), # C1
( 7, 8, 2, 9), # C2
( 7, 10, 6, 11), # C3
( 1, 4, 12, 13), # C4
( 8, 10, 13, 14), # C5
(15, 16, 3, 9), # C6
(15, 17, 5, 11), # C7
(16, 17, 12, 14), # C8
]
def dot(u, v):
return sum(a * b for a, b in zip(u, v))
# Vérifier que chaque contexte forme 4 vecteurs mutuellement orthogonaux
ortho_ok = True
for k, ctx in enumerate(contexts):
pairs = [(i, j) for idx_i, i in enumerate(ctx) for j in ctx[idx_i+1:]]
for i, j in pairs:
d = dot(vectors[i], vectors[j])
if d != 0:
print(f' C{k} : v{i} . v{j} = {d} (non-orthogonal !)')
ortho_ok = False
if ortho_ok:
pass
print(f'\n9 contextes, 6 paires par contexte = 54 paires verifiees')
print(f'Toutes orthogonales : {ortho_ok}')
9 contextes, 6 paires par contexte = 54 paires verifiees
Toutes orthogonales : TrueChaque base C0-C8 contient 4 vecteurs mutuellement orthogonaux. Cela donne 6 paires par base (C(4,2) = 6) et 54 paires au total a vérifier. La vérification renvoie True : la table Cabello respecte effectivement la contrainte geometrique d’orthogonalite, prerequis pour interpreter chaque base comme une mesure quantique compatible.
La section 3 a montre que les 9 bases de la table Cabello couvrent 54 paires orthogonales (intra-bases). Parmi les C(18,2) = 153 paires possibles, seules ces 54 sont garanties par les bases. Mais combien de paires supplémentaires sont accidentellement orthogonales ?
Objectif. Ecrire une fonction qui, etant donné un vecteur arbitraire de R^4, determine dans combien des 9 bases du KS il pourrait figurer (en verifiant l’orthogonalite avec les 3 autres vecteurs de chaque base). Vérifier experimentalement qu’aucun 19e vecteur ne peut s’integrer dans la structure sans briser l’invariant d’overlap.
# Indice : utilisez les variables vectors, contexts, dot déjà définies.# Indice : pour chaque base, tester si le nouveau vecteur est orthogonal a tous les 4 vecteurs de la base.# Étape 1 : définir une fonction bases_compatibles(vec, contexts, vectors) qui retourne la liste des indices de bases ou vec est orthogonal a tous les vecteurs de la base.# Étape 2 : generer quelques vecteurs aleatoires de R^4 et observer que le nombre de bases compatibles est toujours inférieur a 2 (donc l’invariant d’overlap est preserve).# Exercice 2 : vérifier la limite des 18 vecteurs
# TODO étudiant :
# Etape 1 : définir bases_compatibles(vec, contexts, vectors)
# Etape 2 : tester avec des vecteurs aleatoires de R^4
# Etape 3 : vérifier que l'invariant d'overlap est preserve
print("Exercice a completer")
result = None # TODO étudiant : determiner les bases compatibles pour un vecteur arbitraireExercice a completerLa cle combinatoire du théorème est que les 18 vecteurs et les 9 bases sont relies par une structure d’overlap : chaque vecteur appartient a exactement 2 des 9 bases.
Pourquoi ? Une base a 4 vecteurs, donc 9 bases x 4 = 36 “slots”. Si chaque vecteur etait dans une seule base, il faudrait 36 vecteurs distincts – on n’en a que 18. Donc le ratio est 36/18 = 2 en moyenne. La table Cabello realise ce ratio uniformement : exactement 2 pour chaque vecteur, ni 1, ni 3.
# Compter les occurrences de chaque vecteur dans les 9 contextes
occurrences = Counter()
for ctx in contexts:
for i in ctx:
occurrences[i] += 1
# Vérifier l'invariant : chaque vecteur apparait exactement 2 fois
print(f'{"Vec":<5} | {"#bases":<8} | {"Bases contenant ce vecteur"}')
print('-' * 65)
all_two = True
for v in range(18):
bases = [k for k, ctx in enumerate(contexts) if v in ctx]
print(f'v{v:<4} | {occurrences[v]:<8} | C{bases[0]} et C{bases[1]}' if len(bases)==2 else f'v{v:<4} | {occurrences[v]:<8} | {bases} (PROBLEME)')
if occurrences[v] != 2:
all_two = False
print(f'\nChaque vecteur dans exactement 2 bases : {all_two}')
print(f'Total slots = 36 = 9 bases x 4 = 18 vecteurs x 2 : {sum(occurrences.values()) == 36}')Vec | #bases | Bases contenant ce vecteur
-----------------------------------------------------------------
v0 | 2 | C0 et C1
v1 | 2 | C0 et C4
v2 | 2 | C0 et C2
v3 | 2 | C0 et C6
v4 | 2 | C1 et C4
v5 | 2 | C1 et C7
v6 | 2 | C1 et C3
v7 | 2 | C2 et C3
v8 | 2 | C2 et C5
v9 | 2 | C2 et C6
v10 | 2 | C3 et C5
v11 | 2 | C3 et C7
v12 | 2 | C4 et C8
v13 | 2 | C4 et C5
v14 | 2 | C5 et C8
v15 | 2 | C6 et C7
v16 | 2 | C6 et C8
v17 | 2 | C7 et C8
Chaque vecteur dans exactement 2 bases : True
Total slots = 36 = 9 bases x 4 = 18 vecteurs x 2 : TrueLe tableau confirme que les 18 vecteurs apparaissent chacun dans exactement 2 des 9 bases. C’est cette invariance qui rend l’argument de parite possible – si la repartition etait inegale (par exemple un vecteur dans 3 bases ou un autre dans 1 seule), l’argument echouerait et il pourrait exister une coloration valide.
Cette propriété est exactement ce que la lemme Lean each_vector_in_two_contexts enonce dans KochenSpecker.lean (cf section 5).
Une coloration \(c : \text{vecteurs} \to \{0, 1\}\) est dite valide si dans chaque base, exactement un vecteur recoit la valeur 1.
Si une telle coloration existe, le nombre total de 1 (compte avec multiplicite sur les bases) est : \[\sum_{k=0}^{8} (\text{ones dans } C_k) = 9 \cdot 1 = 9\]
puisque chaque base contribue exactement 1.
Reordonnons la somme en regroupant par vecteur. Chaque vecteur \(v\) contribue \(c(v) \cdot (\text{nb de bases contenant } v)\). Avec la propriété d’overlap (chaque vecteur dans 2 bases) : \[\sum_{k=0}^{8} (\text{ones dans } C_k) = \sum_{v=0}^{17} c(v) \cdot 2 = 2 \cdot \sum_{v=0}^{17} c(v)\]
Ce nombre est pair.
Une même somme vaut a la fois 9 (impair) et 2k (pair). Contradiction. Donc aucune coloration valide n’existe.
Verifions ce raisonnement par recherche exhaustive sur les \(2^{18} = 262\,144\) colorations possibles.
# Recherche exhaustive : enumerer les 2^18 colorations, compter combien sont valides
# (SOTA Prong-A #3801 : l'histogramme ASCII de distribution est remplace par un vrai
# graphique matplotlib ; l'enumeration exhaustive, elle, est inchangee.)
n_valid = 0
n_total = 2 ** 18
examples_per_count = {}
for bits in range(n_total):
c = [(bits >> v) & 1 for v in range(18)]
# Compter, pour chaque contexte, le nombre de 1
sums = [sum(c[i] for i in ctx) for ctx in contexts]
if all(s == 1 for s in sums):
n_valid += 1
# Distribution des nombres de contextes "OK" (= sum exactly 1)
k_ok = sum(1 for s in sums if s == 1)
examples_per_count[k_ok] = examples_per_count.get(k_ok, 0) + 1
print(f'Total colorations explorees : {n_total:,}')
print(f'Colorations valides (9/9 contextes OK) : {n_valid}')
print()
print(f'Distribution du nombre de contextes "exactement 1" :')
for k in range(10): # 0/9 a 9/9 inclus (9/9 = 0 = le théorème)
cnt = examples_per_count.get(k, 0)
pct = 100.0 * cnt / n_total
print(f' {k}/9 OK : {cnt:>7,} colorations ({pct:5.2f}%)')
# Visualisation : distribution des colorations (matplotlib, remplace l'histogramme ASCII)
import io
from IPython.display import Image, display
ks_all = list(range(10))
counts_all = [examples_per_count.get(k, 0) for k in ks_all]
colors = ['#2980b9'] * 9 + ['#c0392b'] # 9/9 = 0 mis en evidence (rouge = impossibilite)
fig, ax = plt.subplots(figsize=(7.5, 3.5))
ax.bar([f'{k}/9' for k in ks_all], counts_all, color=colors)
ax.set_xlabel("Nombre de contextes 'exactement 1' (sur 9)")
ax.set_ylabel('Nombre de colorations')
ax.set_title("Distribution des colorations (Kochen-Specker : 9/9 = 0 coloration valide)")
ax.annotate('0 (impossible)', xy=(9, 0), xytext=(7.0, 40000),
arrowprops=dict(arrowstyle='->', color='#c0392b'), color='#c0392b', fontweight='bold')
plt.tight_layout()
buf = io.BytesIO()
fig.savefig(buf, format='png', dpi=110, bbox_inches='tight')
buf.seek(0)
display(Image(data=buf.getvalue()))
plt.close(fig)Total colorations explorees : 262,144
Colorations valides (9/9 contextes OK) : 0
Distribution du nombre de contextes "exactement 1" :
0/9 OK : 30,550 colorations (11.65%)
1/9 OK : 59,760 colorations (22.80%)
2/9 OK : 66,780 colorations (25.47%)
3/9 OK : 51,768 colorations (19.75%)
4/9 OK : 33,264 colorations (12.69%)
5/9 OK : 13,248 colorations ( 5.05%)
6/9 OK : 5,748 colorations ( 2.19%)
7/9 OK : 792 colorations ( 0.30%)
8/9 OK : 234 colorations ( 0.09%)
9/9 OK : 0 colorations ( 0.00%)
La recherche exhaustive confirme : aucune coloration parmi les 262 144 ne satisfait simultanement les 9 contraintes. C’est la vérification “par force brute” du théorème de Kochen-Specker pour la table Cabello a 18 vecteurs.
On peut aussi observer la distribution : un nombre significatif de colorations satisfait 7 ou 8 contextes sur 9, mais aucune ne franchit la barre de 9/9 – ce qui aligne avec l’intuition que la contradiction est globale, pas locale.
Note pedagogique : la preuve formelle Lean (theorem kochen_specker dans KochenSpecker.lean) ne procede pas par enumeration mais par argument symbolique (parite), ce qui généralise immediatement a tout n’importe quel ensemble similaire et donne une preuve courte.
La recherche exhaustive de la section 5 montre que le maximum atteint est 8/9 contextes valides. L’argument de parite prouve que 9/9 est impossible. Mais quelles sont concretement ces colorations “presque valides” ?
Objectif. Implementer une recherche exhaustive qui trouve une coloration maximale (maximisant le nombre de contextes OK). Vérifier que le maximum atteint est bien 8/9 et que le 9e contexte echoue toujours, quel que soit le choix des 8 autres.
# Indice : enumerer les 2^18 colorations possibles ; pour chacune, vérifier chaque contexte et compter les OK.# Indice : parmi les colorations a 8/9, identifier celle(s) dont le contexte manquant est toujours le même (ou non).# Étape 1 : reprendre la boucle de la section 5 et stocker les colorations atteignant le maximum.# Étape 2 : pour chaque coloration a 8/9, afficher le contexte qui echoue et la repartition des 0/1.# Exercice 3 : construire la meilleure coloration partielle
# TODO étudiant :
# Etape 1 : enumerer les 2^18 colorations, stocker celles avec max contextes OK
# Etape 2 : pour chaque coloration a 8/9, afficher le contexte qui echoue
print("Exercice a completer")
best_coloring = None # TODO étudiant : trouver la coloration maximisant les contextes validesExercice a completerKochenSpecker.lean (Pilier 1)Le fichier conway_lean/Conway/KochenSpecker.lean formalise le théorème de Kochen-Specker pour la table Cabello. Il sert de Pilier 1 dans la construction du théorème de libre arbitre de Conway-Kochen (Epic #1651).
Plutot que de formaliser les coordonnees R^4 et la vérification d’orthogonalite (qui requiert des produits scalaires réels), le scaffold encode la structure combinatoire : - 18 indices de vecteurs : VecIdx := Fin 18 - 9 indices de contextes : ContextIdx := Fin 9 - La fonction contextMembers : ContextIdx -> Fin 4 -> VecIdx qui realise la table Cabello
L’orthogonalite de chaque contexte est implicite : vérifier les produits scalaires est une charge separee, reportee a Pilier 2 (FreeWillTheorem.lean).
contextMembers/-- An abstract index for the 18 distinct vectors. -/
abbrev VecIdx := Fin 18
/-- An abstract index for the 9 orthogonal bases (contexts). -/
abbrev ContextIdx := Fin 9
/-- Context membership: which 4 vector indices form each orthogonal basis. -/
def contextMembers : ContextIdx -> Fin 4 -> VecIdx
-- C0: {v0, v1, v2, v3}
| 0, 0 => 0 | 0, 1 => 1 | 0, 2 => 2 | 0, 3 => 3
-- C1: {v0, v4, v5, v6}
| 1, 0 => 0 | 1, 1 => 4 | 1, 2 => 5 | 1, 3 => 6
-- ... C2 a C8 sur le même modèleCette définition encode exactement la table vérifiée numeriquement en section 3. Le pattern matching sur (k : Fin 9, i : Fin 4) couvre les 36 slots de la table.
/-- A {0,1}-coloring of the 18 vectors. -/
def Coloring := VecIdx → Bool
/-- A coloring is valid iff every context has exactly one vector colored true. -/
def IsValidColoring (c : Coloring) : Prop :=
∀ k : ContextIdx,
(∑ i : Fin 4, if c (contextMembers k i) then (1 : ℕ) else 0) = 1
/-- Key property: each of the 18 vectors appears in exactly 2 contexts. -/
lemma each_vector_in_two_contexts (v : VecIdx) :
(∑ k : ContextIdx, ∑ i : Fin 4,
if contextMembers k i = v then (1 : ℕ) else 0) = 2 := by
fin_cases v <;> decideLe lemme each_vector_in_two_contexts est l’enonce formel de la propriété combinatoire vérifiée en section 4 (chaque vecteur dans exactement 2 bases). La preuve utilise fin_cases v pour generer 18 sous-buts (un par vecteur), chacun resolu par le décideur du noyau Lean.
/-- **Kochen-Specker Theorem (18-vector Cabello proof)**.
There is no valid {0,1}-coloring of the 18 vectors compatible
with the orthogonality constraint. -/
theorem kochen_specker : ¬ ∃ c : Coloring, IsValidColoring c := by
rintro ⟨c, hc⟩
set S : ℕ := ∑ k : ContextIdx, ∑ i : Fin 4,
if c (contextMembers k i) then (1 : ℕ) else 0 with hS_def
-- Step 1: S = 9 (each context has exactly one `1`)
have hS9 : S = 9 := by
have hsum : S = ∑ _k : ContextIdx, (1 : ℕ) := by
apply Finset.sum_congr rfl; intro k _; exact hc k
rw [hsum]; decide
-- Step 2: rewrite as sum over v, swap with Finset.sum_comm
have hS_even : S = 2 * (∑ v : VecIdx, if c v then (1 : ℕ) else 0) := by ...
-- Step 3: 2 | 9 contradiction
have h2div : 2 ∣ S := ⟨_, hS_even⟩
rw [hS9] at h2div; omegaLa preuve complète suit exactement l’argument de la section 5 :
c. Sommer sur les 9 contextes : S = 9 (par IsValidColoring).Finset.sum_comm : S = 2 * sum_v c(v) (par each_vector_in_two_contexts).omega).Statut : Prouvé. Les 2 sorrys ont ete elimines en juin 2026 (PR #2019). La cle : fin_cases v <;> decide pour le lemme d’overlap + preuve structurelle (pas brute-force native_decide qui timeout sur Fin 18).
lake build + grep sorryVerifions que le module compile avec 0 sorry (Pilier 1 Prouvé) et que le théorème de libre arbitre (Pilier 2) est également vérifié.
import sys
from pathlib import Path
# Cross-platform Lean utilities (Epic #2314)
sys.path.insert(0, str(Path.cwd()))
from lean_notebook_utils import (
find_lean_project, get_lean_project_path,
run_lake, count_sorry, is_native_platform,
)
# Backward-compatible aliases for cells later in this notebook
lean_project_win = find_lean_project('conway_lean')
wsl_path = get_lean_project_path('conway_lean')
build_timeout_s = 900 # 15 min
plat = "natif" if is_native_platform() else "WSL"
print(f'Chemin Windows : {lean_project_win}')
print(f'Chemin Lean : {wsl_path}')
print(f'Plateforme : {plat}')
print()
print('Verification du module Conway (lake build)...')
print('-' * 60)
rc, out, err = run_lake(wsl_path, 'build Conway', timeout=build_timeout_s)
if out:
print(out[-1800:] if len(out) > 1800 else out)
if err:
print('STDERR:', err[-300:])
print()
print(f'Exit code : {rc}')
print('0 = SUCCESS, autre = ECHEC')
if rc == -1:
print(f'TimeoutExpired apres {build_timeout_s}s (cache mathlib pas prechauffe).')Chemin Windows : <repo>MyIA.AI.Notebooks\SymbolicAI\Lean\conway_lean
Chemin Lean : <repo>MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean
Plateforme : WSL
Verification du module Conway (lake build)...
------------------------------------------------------------
simp only [← hn̵e̵_̵l̵v̵l̵,̵ ̵←̵ ̵h̵sw_lvl, ← hse_lvl] at hb
Note: Simp arguments with `←` have the additional effect of removing the other direction from the simp set, even if the simp argument itself is unused. If the hint above does not work, try replacing `←` with `-` to only get that effect and silence this warning.
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Conway/Life/JumpCapture.lean:511:28: This simp argument is unused:
← hsw_lvl
Hint: Omit it from the simp argument list.
simp only [← hne_lvl, ← hsw̵_̵l̵v̵l̵,̵ ̵←̵ ̵h̵s̵e_lvl] at hb
Note: Simp arguments with `←` have the additional effect of removing the other direction from the simp set, even if the simp argument itself is unused. If the hint above does not work, try replacing `←` with `-` to only get that effect and silence this warning.
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Conway/Life/JumpCapture.lean:534:36: Variable name `hT` 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`
Build completed successfully (8733 jobs).
Exit code : 0
0 = SUCCESS, autre = ECHECLe build Lean 4 compile les 3352 jobs du module Conway. Les seuls sorry residuels se situent dans Life/HashlifeCorrectness.lean (P4/P5, prover targets, Epic #2162). Le module KS lui-même est sans sorry – les preuves sont closes.
| Aspect | Résultat |
|---|---|
| Jobs compiles | 3352 |
| Exit code | 0 (SUCCESS) |
sorry residuels |
voir avertissements declaration uses 'sorry' dans stdout ci-dessus (HashlifeCorrectness, Epic #2162) | comptage exact en cellule suivante |
| Modules KS + FWT | 0 sorry |
Note technique : le build s’exécute via
wsl_papermillavec un timeout de 15 minutes. Le premier build après un clean necessite le prechauffage du cache Mathlib.
import os, glob, sys
from pathlib import Path
# Compter les sorrys dans les 2 Piliers de CE notebook : KochenSpecker + FreeWillTheorem
# Instrument canonique du depot (scripts/lean/count_code_sorry.py) : le comptage
# naif .count('sorry') attrape aussi la prose — KochenSpecker.lean l.107 porte
# « Tous les `sorry` ont ete elimines » dans un bloc /- -/, pas de preuve trouee.
_repo_root = Path.cwd().parents[2]
sys.path.insert(0, str(_repo_root / 'scripts' / 'lean'))
from count_code_sorry import strip_lean_comments, _SORRY_RE
conway_dir = os.path.join(str(lean_project_win), 'Conway')
for fname in ['KochenSpecker.lean', 'FreeWillTheorem.lean']:
fpath = os.path.join(conway_dir, fname)
if os.path.exists(fpath):
raw = Path(fpath).read_text(encoding='utf-8')
n = len(_SORRY_RE.findall(strip_lean_comments(raw)))
print(f' {fname}: {n}')
else:
print(f' {fname}: (fichier non trouve)')
print()
# Contexte honnete : lister les AUTRES modules Conway qui contiennent encore "sorry"
# (hors scope de ce notebook, qui ne traite que les Piliers 1+2)
autres = []
for fpath in glob.glob(os.path.join(conway_dir, '**', '*.lean'), recursive=True):
fname = os.path.relpath(fpath, str(lean_project_win))
if 'KochenSpecker' in fname or 'FreeWillTheorem' in fname:
continue
with open(fpath, 'r', encoding='utf-8') as f:
if 'sorry' in f.read():
autres.append(fname)
print('Autres modules Conway contenant encore "sorry" (HORS scope de ce notebook) :')
for f in sorted(autres):
print(f' - {f}')
print()
print('Lecture honnete :')
print(' * Piliers 1+2 (KochenSpecker + FreeWillTheorem) : 0 sorry -- formellement PROUVES.')
print(' * Angel.lean / DoomsdayLemmas.lean : "sorry" en commentaire/roadmap (pas de preuve trouee).')
print(' * Life/* (Game of Life, Hashlife) : sorrys de PRODUCTION en cours (Phase 2-3) --')
print(' objectifs P4/P5 intractables + lemmes bridge/scaffolding, documentes dans la roadmap Conway.')
print(' => Ce notebook (Piliers 1+2) ne depend PAS des modules Life/* : ses 2 piliers sont complets.') KochenSpecker.lean: 0
FreeWillTheorem.lean: 0
Autres modules Conway contenant encore "sorry" (HORS scope de ce notebook) :
- Conway\Angel.lean
- Conway\Angel_en.lean
- Conway\CHSHLandau.lean
- Conway\CHSHLandau_en.lean
- Conway\CHSHQuantum.lean
- Conway\CHSHQuantum_en.lean
- Conway\CollatzLike.lean
- Conway\CollatzLike_en.lean
- Conway\DoomsdayLemmas.lean
- Conway\DoomsdayLemmas_en.lean
- Conway\Life\AdversarialBattery.lean
- Conway\Life\AdversarialBatteryG2.lean
- Conway\Life\ConeGeometry.lean
- Conway\Life\DecideProbe.lean
- Conway\Life\DecideProbe_en.lean
- Conway\Life\GridCanonical.lean
- Conway\Life\GridCanonical_en.lean
- Conway\Life\HashlifeCorrectness.lean
- Conway\Life\HashlifeCorrectness\Foundation.lean
- Conway\Life\HashlifeCorrectness\Walls\NE.lean
- Conway\Life\HashlifeCorrectness\Walls\NW.lean
- Conway\Life\HashlifeCorrectness\Walls\SE.lean
- Conway\Life\HashlifeCorrectness\Walls\SW.lean
- Conway\Life\HashlifeMarginFragment.lean
- Conway\Life\HashlifeMarginFragment_en.lean
- Conway\Life\JumpCapture.lean
- Conway\Life\LightCone.lean
- Conway\Life\LightCone_en.lean
- Conway\Life\Novelty.lean
- Conway\Life\Novelty_en.lean
- Conway\Life\Pillars.lean
- Conway\Life\Pillars_en.lean
Lecture honnete :
* Piliers 1+2 (KochenSpecker + FreeWillTheorem) : 0 sorry -- formellement PROUVES.
* Angel.lean / DoomsdayLemmas.lean : "sorry" en commentaire/roadmap (pas de preuve trouee).
* Life/* (Game of Life, Hashlife) : sorrys de PRODUCTION en cours (Phase 2-3) --
objectifs P4/P5 intractables + lemmes bridge/scaffolding, documentes dans la roadmap Conway.
=> Ce notebook (Piliers 1+2) ne depend PAS des modules Life/* : ses 2 piliers sont complets.| Vérification | Résultat | Signification |
|---|---|---|
lake build Conway |
Exit code 0, 3352 jobs | Le workspace compile |
| Sorrys Piliers 1+2 | 0 dans KS + FWT | Les 2 piliers de ce notebook sont complets |
KochenSpecker.lean |
0 sorry | Parite formellement prouvée (PR #2019) |
FreeWillTheorem.lean |
0 sorry | FWT formellement prouve (PR #2026) |
Les 2 piliers mathematiques du théorème de libre arbitre sont maintenant entierement prouves en Lean 4. Le Pilier 1 (KS) via argument de parite (fin_cases v <;> decide + Finset.sum_comm + omega), et le Pilier 2 (FWT) via reduction au Pilier 1 (SatisfiesSPIN + SatisfiesTWIN + structure MIN).
Perimetre. Le seul module Conway contenant des
sorryde production estLife/HashlifeCorrectness.lean(comptage exact viagrep -c sorrysur la branche : voir avertissementsdeclaration uses 'sorry'dans stdout du build precedent ; objectifs P4/P5, Epic #2162). Les autres modules Conway (Angel, CollatzLike, DoomsdayLemmas, HashlifeMemo, Pillars, GridCanonical) peuvent contenir des commentaires textuels mentionnantsorry(roadmap), qui ne sont pas des preuves trouees –count_sorry(L532) strip les commentaires + skip.lakeet distingue les deux.
Le théorème de Kochen-Specker est le noyau combinatoire du théorème de libre arbitre (Free Will Theorem) de Conway et Kochen (2006, 2009). Ce théorème affirme :
Si la reponse d’un experimentateur a un choix de mesure n’est pas une fonction de tout ce qui s’est passe avant, alors la reponse de la particule mesuree non plus.
Attention pedagogique : “libre arbitre” chez Conway-Kochen est une définition mathematique (la reponse des particules n’est pas une fonction de l’état anterieur), et PAS une these philosophique. Le théorème démontre rigoureusement qu’un certain type de determinisme est mathematiquement incompatible avec trois axiomes physiques modestes.
Le théorème repose sur 3 axiomes formalises dans FreeWillTheorem.lean :
| Axiome | Enonce intuitif | Formalisation Lean |
|---|---|---|
| SPIN | Pour les particules de spin 1, mesurer le carré du spin selon des axes orthogonaux donne exactement un “1” par base | SatisfiesSPIN : DeterministicResponse → Prop |
| TWIN | Deux particules entrelacees donnent le même résultat sur des axes paralleles | SatisfiesTWIN : TwoParticleResponse → Prop |
| MIN | Les choix d’experimentateurs spatialement separes sont independants | Structural (type signature TwoParticleResponse) |
conway_lean/
Conway/
KochenSpecker.lean <-- Pilier 1 : Prouvé (0 sorry, PR #2019)
FreeWillTheorem.lean <-- Pilier 2 : Prouvé (0 sorry, PR #2026)
[Doomsday, LookAndSay, <-- Autres modules Conway
Fractran, Nim, Angel,
Life/* (Phase 2)]Théorème 1 (single-particle) : fwt_single_particle - Hypothese : une fonction de reponse déterministe satisfait SPIN - Preuve : reduction directe a kochen_specker (une telle fonction définit une coloration KS valide, qui n’existe pas)
Théorème 2 (two-particle) : free_will_theorem - Hypothese : un modèle déterministe a deux particules satisfait SPIN + TWIN + MIN - Preuve : par TWIN, Alice et Bob partagent la même fonction de reponse. Par SPIN(alice), cette fonction satisfait le théorème a une particule. Contradiction.
| Pilier | Module | Statut |
|---|---|---|
| 1 | KochenSpecker.lean |
Prouvé (PR #2019 merge) |
| 2 | FreeWillTheorem.lean |
Prouvé (PR #2026) |
| 3 | Notebook companion | Ce fichier (Lean-13), mis a jour |
Les concepts vus plus haut (orthogonalite des bases, structure d’overlap, argument de parite) se pretent a une mise en pratique directe sur les mêmes objets vectors, contexts, occurrences et la fonction dot déjà définis dans ce notebook. Les trois exercices ci-dessous suivent la progression des sections 3, 4 et 5 : ils reconstruisent pas a pas le coeur de la preuve de Kochen-Specker. Completez chaque fonction (les cellules s’executent sans erreur tant qu’elles ne sont pas completees, elles renvoient simplement None).
Resolu par le groupe Matteo Atkinson & Paul Witkowski (contribution PR #2288).
Objectif. Ecrire une fonction qui vérifie qu’un contexte (4 indices de vecteurs) forme bien une base orthogonale de R^4, c’est-a-dire que les 4 vecteurs sont deux a deux orthogonaux.
# Indice : reutilisez dot(u, v) ; un contexte de 4 vecteurs comporte 6 paires a tester.# Indice : deux vecteurs sont orthogonaux quand leur produit scalaire est nul.def base_est_orthogonale(ctx, vectors):
# Indice : generer les 6 paires (i, j) avec i < j parmi les 4 indices de ctx
# Etape 1 : pour chaque paire, calculer dot(vectors[i], vectors[j])
# Etape 2 : retourner True si tous ces produits scalaires sont nuls, False sinon
for idx_i in range(len(ctx)):
for idx_j in range(idx_i + 1, len(ctx)):
i, j = ctx[idx_i], ctx[idx_j]
if dot(vectors[i], vectors[j]) != 0:
return False
return True
# Test (une fois complète, attendu : True pour chaque base) :
resultat = base_est_orthogonale(contexts[0], vectors)
print(f"base_est_orthogonale(C0) = {resultat} (attendu : True)")
print(f"Verification sur les 9 bases : {all(base_est_orthogonale(ctx, vectors) for ctx in contexts)}")base_est_orthogonale(C0) = True (attendu : True)
Verification sur les 9 bases : TrueResolu par le groupe Matteo Atkinson & Paul Witkowski (contribution PR #2288).
Objectif. L’argument de parite repose sur le decompte des “slots” (paires vecteur-base). Ecrire une fonction qui calcule le nombre total de slots sur les 9 bases et renvoie aussi sa parite.
# Indice : chaque base contient 4 vecteurs et il y a 9 bases.# Indice : chaque vecteur apparait dans exactement 2 bases (cf. section 4) ; le total est donc pair.def slots_totaux_et_parite(contexts):
# Indice : un "slot" est une occurrence (vecteur, base) ; sommez len(ctx) sur les 9 contextes
# Etape 1 : total = somme des tailles des 9 contextes
total = sum(len(ctx) for ctx in contexts)
# Etape 2 : retourner (total, total % 2) # parite : 0 = pair, 1 = impair
return (total, total % 2)
# Test (une fois complète, attendu : (36, 0) -> PAIR) :
res = slots_totaux_et_parite(contexts)
print(f"(total_slots, parite) = {res} (attendu : (36, 0), soit PAIR)")
print(f"Interpretation : 9 bases x 4 vecteurs = {res[0]} slots, {'PAIR' if res[1] == 0 else 'IMPAIR'}")(total_slots, parite) = (36, 0) (attendu : (36, 0), soit PAIR)
Interpretation : 9 bases x 4 vecteurs = 36 slots, PAIRResolu par le groupe Matteo Atkinson & Paul Witkowski (contribution PR #2288).
Objectif. Sous l’hypothese (fausse, c’est tout l’enjeu) qu’une coloration {0, 1} valide existe – exactement un vecteur “vrai” par base – exhiber la contradiction de parite : le decompte “cote bases” est impair (9) alors que le decompte “cote vecteurs” est forcement pair.
# Indice : cote bases, une coloration valide met exactement un 1 par base -> somme = 9 (impair).# Indice : cote vecteurs, la même somme vaut sum(color[v] * occurrences[v]) ; comme chaque occurrences[v] vaut 2, cette somme est paire quelles que soient les valeurs color[v].# Indice : 9 (impair) ne peut pas etre egal a un nombre pair -> aucune coloration valide.def argument_de_parite(contexts, occurrences):
# Indice : somme_cote_bases = nombre de bases (un 1 par base dans une coloration valide)
# Etape 1 : somme_cote_bases = len(contexts) # = 9, impair
somme_cote_bases = len(contexts)
# Etape 2 : la somme cote vecteurs vaut sum(color[v] * occurrences[v]) ; chaque occurrences[v] = 2
# donc elle est PAIRE quelle que soit la coloration -> parite_cote_vecteurs = "pair"
parite_cote_vecteurs = "pair"
# Etape 3 : retourner (somme_cote_bases, parite_cote_vecteurs)
return (somme_cote_bases, parite_cote_vecteurs)
# Test (une fois complète, attendu : (9, 'pair') -> 9 impair contredit une somme paire) :
verdict = argument_de_parite(contexts, occurrences)
print(f"(cote_bases, cote_vecteurs) = {verdict}")
print(f"Contradiction : {verdict[0]} est {'impair' if verdict[0] % 2 == 1 else 'pair'} "
f"(cote bases) mais la somme cote vecteurs est toujours {verdict[1]}.")
print("=> Aucune coloration valide ne peut exister (QED).")(cote_bases, cote_vecteurs) = (9, 'pair')
Contradiction : 9 est impair (cote bases) mais la somme cote vecteurs est toujours pair.
=> Aucune coloration valide ne peut exister (QED).Les exemples guides ci-dessus verifient l’orthogonalite a l’interieur de chaque base. A votre tour : comptez le nombre total de paires orthogonales parmi les 18 vecteurs (toutes paires confondues, pas seulement intra-bases), et comparez-le aux 9 x 6 = 54 paires garanties par les bases.
dot(u, v) et parcourez les paires (i, j) avec i < j parmi les 18 vecteurs.(i, j), i < j.# Exercice : compter toutes les paires orthogonales parmi les 18 vecteurs
# TODO étudiant :
# Etape 1 : parcourir toutes les paires (i, j) avec i < j parmi les 18 vecteurs
# Etape 2 : compter celles dont dot(vectors[i], vectors[j]) == 0
# Etape 3 : comparer ce total aux 9 x 6 = 54 paires intra-bases
print("Exercice a completer")Exercice a completer| Concept | Définition | Importance |
|---|---|---|
| Variables cachees non-contextuelles | Théorie attribuant des valeurs predeterminees independantes du contexte | Ce que KS exclut |
| Table Cabello (18 vecteurs) | 18 vecteurs de R^4 en 9 bases orthogonales, chaque vecteur dans exactement 2 bases | Structure combinatoire minimale |
| Coloration valide | Fonction vecteurs -> {0,1} avec exactement un 1 par base | Objet dont on prouve l’inexistence |
| Argument de parite | Somme des 1 = 9 (impair) via les bases, mais = 2k (pair) via l’overlap | Contradiction |
| Théorème de libre arbitre | Si experimentateurs libres, alors particules libres | Generalisation de KS via SPIN+TWIN+MIN |
| Module | Statut | Sorry | Rôle |
|---|---|---|---|
KochenSpecker.lean |
Prouvé | 0 | Parite formelle sur la table Cabello |
FreeWillTheorem.lean |
Prouvé | 0 | Reduction FWT -> KS (SPIN+TWIN+MIN) |
Conway (workspace) |
Compile | 2 (HashlifeCorrectness P4/P5) | 3352 jobs, lake build SUCCESS |
Pour explorer d’autres résultats de John Conway formalises en Lean, voir Lean-16b-Conway-Game-of-Life-Lean. Pour la robustesse des reseaux de neurones, voir Lean-11-TorchLean.
S. Kochen, E. P. Specker, “The Problem of Hidden Variables in Quantum Mechanics”, J. Math. Mech. 17 (1967), 59-87. La preuve originale a 117 vecteurs en R^3.
A. Peres, “Two simple proofs of the Kochen-Specker theorem”, J. Phys. A 24 (1991), L175-L178. Preuve a 33 vecteurs.
M. Kernaghan, “Bell-Kochen-Specker theorem for 20 vectors”, J. Phys. A 27 (1994), L829-L830.
A. Cabello, J. M. Estebaranz, G. Garcia-Alcaine, “Bell-Kochen-Specker theorem: A proof with 18 vectors”, Phys. Lett. A 212 (1996), 183-187. La table utilisee dans ce notebook.
J. H. Conway, S. Kochen, “The Free Will Theorem”, Found. Phys. 36 (2006), 1441-1473. arXiv:quant-ph/0604079.
J. H. Conway, S. Kochen, “The Strong Free Will Theorem”, Notices AMS 56 (2009), 226-232.
Le théorème KS et sa generalisation au théorème de libre arbitre demolissent une classe entière d’interpretations realistes locales de la mecanique quantique :
conway_lean/Conway/FreeWillTheorem.lean et tracer la chaîne de reduction : free_will_theorem -> fwt_single_particle -> kochen_specker. Combien d’étapes ?FreeWillTheorem.lean avec des coordonnees R^4 explicites et une preuve d’orthogonalite pour chaque contexte (actuellement implicite dans contextMembers).Navigation : << Lean-12 Sensitivity | Index | Lean-14 Finiteness-Derivatives >>