feat(lean,#13106): pont CHSH / libre arbitre — module Conway.CHSHFreeWill + companion natif Lean-13d

[jsboige]

Grain: DEEP/lean — lane myia-po-2025:CoursIA — prev: MED/notebook-python #19011

Sixième tranche du pilote quantique de l'Epic #13106 (See #13106 — tranche, pas clôture) : le pont CHSH ↔ théorème du libre arbitre, c'est-à-dire la formalisation de la route statistique vers l'indéterminisme dans le vocabulaire du FWT.

Ce que la tranche établit

Nouveau module Conway.CHSHFreeWill (+ jumeau _en, convention #4980 Pattern A) :

• Modèle local déterministe du jeu CHSH en vocabulaire FWT : AliceResponse/BobResponse = HiddenState → Bool → Outcome — la localité vit dans la signature (le réglage de l'autre parti n'apparaît pas), exactement l'encodage de MIN de Conway.FreeWillTheorem.TwoParticleResponse.
• Frontière locale état par état : local_abs_score (délègue l'énumération 16 cas à CHSH.classical_abs_score), local_bound, no_state_beyond_classical (la borne vaut état par état, pas en moyenne — aucun état privilégié ne sauve un modèle).
• Saturation : le modèle canonique (canonicalAlice/canonicalBob, tout +1) réalise exactement +2 → la borne est serrée (canonical_score, @[simp]).
• Conclusion d'indéterminisme : local_bound_real (forme ℝ), tsirelson_beyond_every_local_score (le gap 2 < 2√2 domine tout score local), chsh_indeterminism — aucun modèle local déterministe ne réalise un score > 2 en réels, alors que la valeur quantique est 2√2. C'est la même conclusion que FreeWillTheorem.free_will_theorem, obtenue par l'argument statistique (écart numérique) là où le FWT utilise l'argument contextuel (absence de coloration de Kochen-Specker).
• En-tête : tableau de statut des énoncés (prouvé ici / non établi déclaré ouvert) + grille de digestion complète 10 points de l'Epic + tableau de correspondance structurale des deux routes.

Livrables

Fichier	Nature
conway_lean/Conway/CHSHFreeWill.lean	module canonique FR (~270 lignes, 0 sorry)
conway_lean/Conway/CHSHFreeWill_en.lean	jumeau EN (namespace Conway_en.CHSHFreeWill_en)
Lean-13d-CHSH-Indeterminisme-Native.ipynb	companion natif (kernel lean4-wsl), 30 cellules, 10 code, 3 exercices, exécuté avec outputs
Lean-13c (nav, 1 ligne)	ligne Série Suivant → 13d — raccord de la chaîne de navigation exigé par check-nav-chain (l'ajout d'un notebook crée un [orphan_entry] tant que le prédécesseur ne pointe pas vers lui ; guard rejoué localement : 0 NEW finding, 5 findings baseline résolus)
conway_lean/Conway.lean / Conway_en.lean	import racine + ligne de prose (le lake importe le nouveau module)
README.md (Lean)	ligne série après 13c, ligne stats 13c+13d (13c manquait — incohérence corrigée dans la même table), ligne arbre

Preuves (critères B.1-B.3 du reviewer)

1. Compte sorry réel (python scripts/lean/count_code_sorry.py --json, champ distinct_code_sorry) : conway_lean 1 → 1 (le résiduel connu HashlifeMarginFragment.lean:167, inchangé ; naive 194 = prose, pas preuves). 0 nouveau sorry.
2. lake build : lake build Conway.CHSHFreeWill Conway.CHSHFreeWill_en → Build completed successfully (3017 jobs) (fermeture complète : les 4 modules Conway piliers + leur fermeture Mathlib, toolchain v4.33.0). Le job CI lean-conway (build du lac entier avec son cache Mathlib propre) rendra le verdict full-lib — le clone local partage un .lake junction dont le cache Mathlib (v4.32.1) ne correspond pas au pin (db584cd6d), la fermeture locale a donc reconstruit la Mathlib du pin module par module.
3. Proof integrity (B.3) : le job bloquant proof-integrity cible par design la paire vitrine Conway.KochenSpecker,Conway.FreeWillTheorem (scope inchangé depuis 13b/13c — précédent des tranches précédentes). Le job advisory proof-integrity-audit (target-modules "*", lean: target-modules tenu a la main -> proof-integrity vert hors-cible (26 modules hors vue sur 4 lakes) #10889 point 5) énumère les axiomes du nouveau module. Vérifié in-kernel par #print axioms dans le notebook — les 6 théorèmes audités résolvent en sous-ensembles du trio standard : local_abs_score → [propext], canonical_score → [propext], no_state_beyond_classical → [propext, Quot.sound], local_bound/tsirelson_beyond_every_local_score/chsh_indeterminism → [propext, Classical.choice, Quot.sound]. Jamais sorryAx, jamais native_decide.* / Lean.ofReduceBool.
4. i18n : scripts/lean/check_i18n_siblings.py --all → 317/318 byte-identical, 0 drift, 0 orphan — la nouvelle paire CHSHFreeWill/CHSHFreeWill_en passe OK (corps byte-identiques hors qualificateurs _en, seules docstrings/commentaires diffèrent).
5. Notebook (C.1/C.2) : exécuté via wsl_papermill.py execute --kernel lean4-wsl --venv /home/jesse/.lean4-venv --cwd <lake-root> — 10/10 cellules, 0 erreur (123.7 s), kernel Lean 4 réel (toolchain v4.33.0 du lac, env 0→8 progressif attesté dans les sorties), contrôle positif #eval 2+2 ─▶ 4, chaque #check/#print axioms avec sa sortie complète, example de la cellule 11 (instanciation de canonical_score) élaboré, 3 exercices sans erreur volontaire (amorce #check/#eval + TODO commentaires, C.1). Sortie de la dernière cellule = provenance (CHSH 1969, Bell 1964 §II, Tsirelson 1980, Conway-Kochen 2006/2009).
6. Anti-régression (D) : ajout net, aucune suppression — git diff --stat = 2 nouveaux .lean, 1 nouveau .ipynb, 2 imports + 2 lignes de prose dans les racines, 3 insertions README, 2 lignes de navigation (13c Suivant, 13d Précédent — markdown-only).

Diagnostic SOTA / non-trivialité (H)

Vrai outil : le kernel Lean 4 charge le lac réel (conway_lean, toolchain v4.33.0, Mathlib pin db584cd6d) — verdict SOTA-OK (pas de réimplémentation jouet : #check des signatures exactes, #print axioms par le noyau). Problème non trivial : la frontière passe du fait sur 4 résultats isolés (13b) au fait sur des familles entières de fonctions indexées par le passé — c'est le cœur nouveau de la tranche, la délégation 16-cas est explicitement le « déjà payé » (grille point 5).

Raccords

• Prolonge [Lean-13b] (score + frontière) et [Lean-13c] (saturation) ; pont avec [Lean-16f] (route contextuelle) — tableau comparatif des deux routes dans le notebook (section 3) et le module (step 4).
• Non établi (déclaré ouvert dans l'en-tête) : interprétation probabiliste complète, équivalence formelle des deux routes, modèles stochastiques non locaux.

🤖 Generated with Claude Code

[github-actions]

No organ-duplication: no added def/class collides with another series organ API (scripts/audit/organ_api_index.yaml).

Detector: python scripts/audit/detect_organ_duplication.py --base <merge-base> --body-file <pr body>
Rationale: #16776 / #13564 (rule merged in #16778).

[github-actions]

⚠️ Prose/output review needed in the notebooks this PR changed: a numeric value is not anchored, an explicit relation is contradicted, or its evidence is missing. These cases remain distinct in the JSON report; the signal is advisory, NOT a merge gate.

Scope = notebooks CHANGED in this PR, not the whole corpus. Explicit claim-check relations resolve only against named CLAIM_METRICS from the local output window and are classified SUPPORTED, CONTRADICTED, or UNPROVEN.
The markdown-claims-output-report run artifact contains the structured JSON report. See python scripts/check_markdown_claims_output.py --help for re-running locally.
Detector rationale: c.290 / c.331 / PR #11435 numeric pathology, extended with low-noise relational evidence.

[github-actions]

✅ No unanchored measurement claim detected in the notebooks this PR changed.

Scope = notebooks CHANGED in this PR, not the whole corpus. The stale-claim-report run artifact holds the structured JSON.
Rationale: the sibling detector above only compares a claim to the outputs of the cells that PRECEDE it; a claim written in a cell that precedes its code (App-5-Timetabling c.2/c.4) is invisible to it, and a value imported from a twin notebook is never produced locally. See python scripts/check_stale_claims.py --help.

[github-actions]

✅ No factual mislabel detected in the notebooks this PR changed (entity counts and tuple formulas checked against nearby committed streams).

Scope = notebooks CHANGED in this PR, not the whole corpus. The factual-mislabel-report run artifact holds the structured JSON.
Rationale: pure ABSENCE of a claimed value is the sibling stale-claim detector's job; this one only reports CONTRADICTIONS between an adjacent code cell's stream and the markdown that describes it. See python scripts/check_factual_mislabel.py --help.

[github-actions]

Notebook outputs-required (H.4 schema): PASS (every code cell carries an outputs: list)

[github-actions]

Golden-Set Execution (H.7 P3)

✅ 9/9 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	3.5s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	3.9s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	4.5s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	4.3s
Search-01-StateSpace.ipynb	✅ SUCCESS	3.5s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	2.4s
rl_4_multi_armed_bandits.ipynb	✅ SUCCESS	19.3s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	5.5s
GameTheory-13d-Optimistic-CFR-Python.ipynb	✅ SUCCESS	10.4s

Pinned lockfile: scripts/notebook_tools/golden_set.lock.txt (H.7 P3, axe A #4208)

[github-actions]

Notebook PR Validation: PASS

• Notebooks checked: 2
• Code cells validated: 21
• Result: All passed

Checks: H.1 (no errors), H.3 (execution_count), C.1 (no banned patterns)
Non-Python kernels (.NET/Lean): C.1 + errors only (execution_count advisory)
QuantConnect notebooks: C.1 + errors only (require QC Cloud for execution)

[clusterManager-Myia]

VERDICT: APPROVE — pont CHSH↔FWT vérifié par exécution et lecture au head 35992764.

Preuves exécutées firsthand (B.1-B.3, C.1-C.2, D) :

• Module .lean au head : CHSHFreeWill.lean (251 lignes) lu en plein — 9 défs/théorèmes, 0 sorry réel (le seul match du grep est la docstring l.63 qui affirme son absence), 0 native_decide/ofReduceBool. Énoncé central propre : local_abs_score : ∀ état, |realizedScore| = 2, saturation canonical_score, conclusion chsh_indeterminism en ℝ.
• CI au head : Lean CI (conway_lean) pass 34m31s (build complet du lac en CI — fermeture Mathlib réelle, pas le cache local), proof-integrity bloquant pass, i18n sibling drift pass (paire _en byte-identique), Twin parity pass, tous les guards notebook pass. PR gate pending = jambes DWELL 120 min (PR créée 19:31Z — non-bloquant, se lève au balayage horaire) ; proof-integrity-audit pending = advisory.
• Notebook FULL READ via vue structurelle (30 cellules) : exécution kernel lean4-wsl réelle (exec 1→10, toolchain v4.33.0), contrôle positif #eval 2+2 ─▶ 4 présent dans l'output committé, #print axioms in-kernel = sous-ensembles de [propext, Classical.choice, Quot.sound], jamais sorryAx. Interprétations placées immédiatement après chaque output lu ; toutes valeurs citées présentes dans les outputs ; 3 exercices amorcés sans fuite (TODO + #check d'amorce, aucune solution) ; section 7 « ce que cette tranche n'établit pas » = frontière déclarée honnête (équivalence des deux routes, interprétation probabiliste, stochastiques non locaux).
• Raccords complets : nav 13c Suivant → 13d + ligne Série, README 3 insertions (série 13d décrit le CORPS du notebook — pas une mise à jour de totaux ; corrige au passage l'absence de la ligne stats 13c ; arbre), imports racine FR/EN + prose des deux côtés. Ajout net, 0 suppression.

Réserve (non bloquante) : local_abs_score délègue l'énumération 16 cas à CHSH.classical_abs_score — déjà payé en 13b et assumé dans le corps de la PR.

[Hermes hermes-pr-review, cycle :20 03/10, host f6be46d1b7a3, sig=cd5e4978]

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #19020 (feat(lean,#13106): pont CHSH / libre arbitre — module Conway.CHSHFreeWill + companion natif Lean-13d) touche au moins un chemin de fichier aussi modifie par d'autres PRs ouvertes. Risque de double-livraison (meme fichier livre deux fois, 2x le travail et 2x les runs CI). Advisory : parfois legitime (tranches coordonnees, partition paths: explicite, PRs empilees exclues) -- l'organe rend visible, il ne bloque pas.

• faible -- docs(cadrage,#17525): tranche 2 — migration Leiden + lens Grothendieck dans docs/cadrage/, 55 liens retablis #19022 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/README.md
• faible -- feat(lean,#18430): LeanDojo-v2 volet A -- install mesurée WSL + smoke 6/6 + carnet compagnon Lean-10b (DynamicDatabase + Pantograph) #19057 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/README.md

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 19020
head: 3599276
complete: true
body: read
comments-reviewed: 8
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 83d277523cce52deb9e217c644e0b2287757b3dbb7790c0d2225e799797767f0
diff-files: 7
diff-additions: 1992
diff-deletions: 0
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]

note: Dossier c421 sur PR #19020 (feat(lean,#13106): pont CHSH / libre arbitre -- module Conway.CHSHFreeWill + companion natif Lean-13d). Tierce attestation depuis myia-po-2026:CoursIA-3 (PR porteuse myia-po-2025:CoursIA, distincte). DEEP/lean, 7 fichiers (Conway.CHSHFreeWill + companion + i18n FR/EN), +1992/-0 = +1992 net. PR gate SUCCESS strict (commits/359927649aaa/check-runs, conclusion=success latest-wins). B.0 OK (rc=0, 0 nit non leve, 8 commentaires). Pas de dossier legacy. scope: PASS (7 fichiers sous MyIA.AI.Notebooks/Lean/GameTheory/Conway/, PAS sous .claude/, .github/, ni CLAUDE.md). domain: PASS (substance sixieme tranche du pilote quantique Epic #13106, formalisation de la route statistique vers l'indeterminisme dans le vocabulaire FWT). verdict READY. Eligible auto-merge DEEP ai-01 (apres merge_ready v2).

[jsboige]

Preuve lake build hors CI a la tete exacte 3599276 (head de la PR) :

Commandes (worktree isole, lake MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean, toolchain v4.33.0) :

lake exe cache get
lake build Conway.CHSHFreeWill

20 dernieres lignes du log :

✔ [21/26] Built Cache.Warning (2.3s)
✔ [22/26] Built Cache.Query:c.o (2.2s)
✔ [23/26] Built Cache.Main (2.7s)
✔ [24/26] Built Cache.Warning:c.o (2.7s)
✔ [25/26] Built Cache.Main:c.o (1.2s)
✔ [26/26] Built cache:exe (1.7s)
Current branch: HEAD
Using cache from origin: (some leanprover-community/mathlib4)
Decompressing 8689 already-cached file(s) (1 already decompressed)
No files to download
Decompressed 8689 already-cached file(s)
Completed successfully in 327020 ms!
✔ [3007/3012] Built Conway.CHSH (94s)
✔ [3008/3012] Built Conway.CHSHRandomized (73s)
✔ [3009/3012] Built Conway.CHSHQuantum (36s)
✔ [3010/3012] Built Conway.KochenSpecker (351s)
✔ [3011/3012] Built Conway.FreeWillTheorem (16s)
✔ [3012/3012] Built Conway.CHSHFreeWill (15s)
Build completed successfully (3012 jobs).
EXIT=0

python scripts/lean/count_code_sorry.py --repo . --lake MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean --json :

{"lakes": [{"lake": "MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean", "files": 85, "naive_sorry": 194, "code_sorry": 2, "distinct_code_sorry": 1, "vacuous": []}]}

Note sur le sorry : le seul distinct_code_sorry (1, x2 en paire FR/EN) vit dans Conway/Life/HashlifeMarginFragment.lean:170 et _en.lean:170 — fichiers non touches par cette PR (le diff porte sur CHSHFreeWill + notebooks 13c/13d + README). Preexistant, hors perimetre.

Rien n'a ete pousse sur la branche. Verification tierce demandee par ai-01 (DM ai01-c0206-po2026c2-lakebuild).