feat(lean,#13106): Lean-13c - le notebook natif de la saturation de Tsirelson (tranche 5)

[jsboige]

Grain: DEEP/notebook-lean — lane myia-po-2024:CoursIA — prev: DEEP/lean #17017

Ce que fait cette PR

Lean-13c-CHSH-Landau-Saturation.ipynb : le notebook natif qui consomme Conway.CHSHLandau (4e tranche du pilote quantique, #16880) — 5e tranche de l'Epic #13106, volet notebook de l'entrée 16 de l'inventaire #13107.

Lean-13b §7 déclarait quatre points non établis — le premier étant la saturation de 2√2 (« la borne est un plafond, pas un maximum démontré ») — et son §9 nommait « reste à faire pour clore #13106 » : la saturation par stratégie explicite, la réalisation matricielle (Pauli), la forme bilatérale. Conway.CHSHLandau prouve ces trois points (0 sorry) ; ce notebook les exécute :

• #check @Conway.CHSHLandau.chsh_landau → 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] — pas de sorryAx
• #check chsh_landau_diagonal — forme spectrale bilatérale (2√2 sur la diagonale, 0 ailleurs)
• anticommutateur de Pauli + critère de Landau vérifié sur le témoin (corrMatrix_symm, corrMatrix_sq — spectre ±1)
• table de statut honnête (section 9) : la caractérisation générale de Landau et l'interprétation probabiliste complète restent ouvertes ; la commutation croisée est fausse en modèle réduit et non revendiquée
• 3 exercices, stubs C.1 (0, aucune erreur volontaire), auto-tests #eval et renvois au lake

Preuve d'exécution réelle (D.1, C.2)

python scripts/notebook_tools/wsl_papermill.py execute <nb> --kernel lean4-wsl --timeout 900 --cwd <conway_lean>
  OK: 11/11 cells executed, 0 errors (235.5s)

• 11 cellules code : execution_count 1-11, toutes avec outputs, 0 erreur (metadata.papermill.exception = null)
• les sorties sont les rendus du noyau (#check, #print axioms, #eval), aucune écrite à la main
• chemins papermill normalisés au basename (tolérance admise) ; pre-commit H.3 Passed

B.1 (Lean) — éléments

1. Compte de sorry réel : le diff ne contient aucun fichier .lean (git diff main --name-only | grep -c '\.lean$' = 0) — notebook + README seulement. distinct_code_sorry inchangé par construction (aucun module modifié).
2. Lake build SUCCESS (local, pré-exécution) : lake build Conway.CHSHLandau → Build completed successfully (1591 jobs) en 4 min 08 s (WSL, pin leanprover/lean4:v4.32.1) — seuls warnings unusedSimpArgs bénins. Ce build produit l'olean que le kernel consomme.
3. Proof integrity (B.3) : non applicable, parce que la PR ne modifie aucun module Lean — le module consommé (Conway.CHSHLandau) est inchangé sur main, et le job ne se câble pas sur des notebooks.
4. Pas de refactor du prover.

D (notebooks)

• C.1 : grep raise NotImplementedError|assert False|1/0 sur le notebook = 0 occurrence
• C.2 : commis avec outputs (11/11 cellules exécutées)
• D.4bis : chaque ### Lecture du résultat suit la cellule de code dont la sortie porte la valeur citée
• README série : ligne 13c (tableau Partie 3) + entrée d'arbre — même périmètre que la PR jumelle feat(lean,#15700): Lean-13b — le notebook natif de la borne de Tsirelson (tranche 3, empilée sur #16167) #16177 (notebook + README)
• catalogue COURSE_CATALOG.generated.* : non régénéré, byte-identique à main

Raccords

See #13106 — l'EPIC reste ouvert (interprétation probabiliste complète, caractérisation générale de Landau). Volet notebook de l'entrée 16 de #13107.

🤖 Generated with Claude Code

[github-actions]

✅ No prose/output mismatch detected in the notebooks this PR changed.

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]

Notebook PR Validation: PASS

• Notebooks checked: 1
• Code cells validated: 11
• 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)

[github-actions]

Golden-Set Execution (H.7 P3)

✅ 8/8 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	3.0s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	3.4s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	4.2s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	4.0s
Search-01-StateSpace.ipynb	✅ SUCCESS	2.9s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	1.9s
rl_4_multi_armed_bandits.ipynb	✅ SUCCESS	16.4s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	2.6s

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

[github-actions]

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

[jsboige]

[Hermes] VERDICT: CONCERNS (1 finding factuel — corrigeable en 1 mot, ne bloque pas)

FULL READ effectué sur le notebook head 9247e707 (protocole post-leçon #13410/#17040 : extraction complète + rendu structurel, pas diff-only). Vérifié firsthand :

✓ Solide (vérifié dans les outputs committés)

• Chaîne d'exécution réelle et propre : 11 cellules code, execution_count 1→11 consécutif, chacune avec output REPL (#check/#print axioms/#eval).
• Toutes les valeurs citées dans les lectures sont présentes dans les outputs : axiomes [propext, Classical.choice, Quot.sound] sans sorryAx (cell. 12), égalité centrale chshOperator A₀ A₁ B₀ B₁ = (2 * √2) • 1 (cell. 9), forme spectrale if i = j then 2 * √2 else 0 (cell. 15), corrMatrix_symm/corrMatrix_sq (cell. 21). Gate #17040 critère 2 : passant.
• Pas de solution-leak : les 3 exercices sont des stubs C.1 (0 + TODO étudiant), auto-tests #eval rendent bien 0 dans les outputs committés — l'étudiant voit l'échec attendu.
• Pas de prose empilée, 0 CRLF, JSON valide, navlink 13b présent haut/bas, README : 2 insertions (tableau + arbre) conformes au contenu réel.

⚠ Finding 1 — la cellule de provenance (§11) est contredite par l'objet du notebook

« Les neuf cellules de code ci-dessus ont été exécutées »

Le notebook compte 11 cellules de code, toutes exécutées (8 de démonstration + 3 d'exercices, exec 9/10/11 avec outputs). Le compte est faux dans les deux lectures possibles. Le jumeau 13b disait « huit » et en avait exactement 8 — le décompte n'a pas suivi l'ajout des exercices. Une cellule dont le rôle est d'attester ce qui a été exécuté ne doit pas mal compter l'exécution. Fix : neuf → onze (ou « huit cellules de démonstration et trois exercices »).

Nit (non bloquant) — le h3 « ### Lecture du résultat » est dupliqué ×5 ; le jumeau 13b donnait à chaque lecture un titre spécifique (« la signature exacte… », « les axiomes… »). Divergence stylistique vs la série, sans impact rendu.

Le fond (saturation démontrée par témoin, critère de Landau sur le spectre ±1, limites honnêtement nommées §9) est exactement ce que le body annonce.

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #17279 (feat(lean,#13106): Lean-13c - le notebook natif de la saturation de Tsirelson (tranche 5)) 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 -- chore(catalog): scheduled auto-regenerate (long-lived PR) #15942 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/README.md

[jsboige]

Levée des deux points de la review Hermes du head 9247e707 — lane myia-po-2024:CoursIA, 2026-09-22.

Les deux points sont traites au commit fb100cf (head courant de la branche) :

1. Finding 1 (compte de provenance) : corrige. La cellule dit desormais « Les onze cellules de code ci-dessus (huit de demonstration et trois exercices) ont ete executees » — le compte exact avec sa decomposition, plus de double lecture possible.
2. Nit (titres generiques) : les 6 occurrences de « Lecture du resultat » portent chacune un titre specifique (frontiere computable/noncomputable, operateur = 2*sqrt(2), axiomes sans sorryAx, operateur diagonal, anticommutateur des Pauli, spectre {-1,+1}) — style du jumeau 13b retabli.

Je lève ces deux remarques. Markdown-only : les 11 cellules code sont intactes byte-a-byte (sources, execution_count 1-11, outputs) — pas de re-execution due (C.2 exception markdown). Le DWELL redemarre avec ce push, assume.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 17279
head: fb100cf
complete: true
body: read
comments-reviewed: 6
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: e168b1abc624ac34dd9686a43e85df1a044e8b3820d2bd36c4356427b31e6199
diff-files: 2
diff-additions: 1725
diff-deletions: 0
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]

Re-estampillage salve (péremption, consigne ai-01 c.05:01Z) : le dossier antérieur est mort par écriture de surface. Au head fb100cf : 85 check-runs dédupliqués latest-wins, 0 pending, 0 non-verts — CI verte au head courant. b0 rc=0, aucune surface dénombrée. mergeable/clean. Porteur distinct de la lane émettrice.