feat(lean,#15400): reproduction Euler et Navier-Stokes

[jsboige]

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

Résumé

Reproduit le dépôt public openai/NavierStokesAndEuler au pin exact 8937a8f4cbc7abaab5e9e97d1cc7f5d2319d9538, puis publie un harnais fail-closed et un notebook pédagogique français qui sépare l'acceptation mécanique de l'exposition mathématique.

Changements

• scripts/notebook_tools/nse_reproduction.py : lecteur borné des preuves externes, sans checkout ni journal brut dans Git. Il vérifie l'identité du root, la toolchain, les pins Comparator/Mathlib/lean4export/nanoda, le vrai landrun, les onze sondes axiomatiques exactes, les quatre signatures de placeholders et deux gates indépendants.
• scripts/notebook_tools/tests/test_nse_reproduction.py : 17 tests, dont les contrôles négatifs parent vert/enfant rouge, marqueur nanoda absent, rejet sémantique, orphelins, empreinte divergente, scanner non canonique et signature de placeholder déplacée.
• Lean-31-Euler-Navier-Stokes.ipynb : 34 cellules, kernel python3, 10/10 cellules code exécutées avec sorties réelles, zéro erreur et trois exercices sans erreur volontaire. Le notebook expose séparément la chaîne Euler/BKM, la construction partagée et les options (C)/(D), puis re-dérive les huit termes du verdict depuis leurs feuilles.
• README Lean : audit du fichier entier, réparation des lignes concaténées préexistantes de la table profonde et du tableau de maturité, ajout de Lean-29/30/31 dans les zones manquantes, durée totale recalculée à ~39h25min, acquis d'apprentissage et arbre mis à jour. Les catalogues générés restent byte-identiques à origin/main.

Preuves de reproduction

• Root : pin attendu observé exactement.
• Toolchain : leanprover/lean4:v4.34.0-rc2.
• Confinement : landrun version 0.1.17, écriture non autorisée refusée et écriture autorisée réussie.
• Euler : enfant 0, parent 0, statut ok, non tué, aucun orphelin, noyaux Lean et nanoda acceptent, verdict exact présent.
• Navier–Stokes : enfant 0, parent 0, statut ok, non tué, aucun orphelin, noyaux Lean et nanoda acceptent, verdict exact présent.
• Axiomes : onze déclarations exactes, chacune limitée à propext, Classical.choice, Quot.sound; aucun axiome interdit.
• Intégrité : scanner canonique, corpus Lean suivi compté à 2 486 unités, quatre placeholders attendus localisés côté challenges, zéro sorry côté solutions et zéro native_decide.
• Conjonction finale : all_verified: true.

Validation

• pytest: 17 passed.
• Ruff : All checks passed.
• Harnais réel check : all_verified: true.
• Notebook : 34 cellules, 10/10 exécutées, 10/10 avec sorties, 0 erreur, IDs uniques.
• Outil canonique notebook_tools.py validate : 1 OK, 0 warning, 0 error.
• Exercices : 3 conformes.
• Cellules code consécutives : 0.
• Interprétations mal placées : 0.
• Fuite Papermill : 0; métadonnées input_path/output_path normalisées au basename.
• Ratchets post-commit : output-failure 0 régression, output-collapse 0 finding, source-collapse 0 finding, Papermill/source-output ADDED, 0 régression.
• git diff --check : succès.

Aucun fichier *.lean n'est modifié : le build local pré-merge d'un module CoursIA n'est donc pas applicable. Les exécutions Lean externes confinées, le Comparator et les deux noyaux constituent ici les preuves formelles.

See #15400 — livraison du volet reproduction, du harnais et du notebook; le census/import sélectif restant conserve son cycle de vie propre.

🤖 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 outputs-required (H.4 schema): PASS (every code cell carries an outputs: list)

[github-actions]

MD hierarchy drift -- 0526ef9

Cette PR augmente le compte de defauts de rendu markdown
par rapport a la base de fusion 8b08e73 re-scannee.
Nouveaux defauts imputables au diff :

reference: merge base 8b08e736cd585a05b1d7bd3849b7bcb1f6808ffc re-scanned (0 of 1 changed notebook(s) existed at base; others are additions; 0 had findings at base)
  +1  MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-31-Euler-Navier-Stokes.ipynb
        +1 HINT-AS-HEADING

=== drift: +1 across 1 notebook(s), 0 burned down ===

Corriger (ex. - # Indice : ... -> - **Indice :** ...). See #11831.

[github-actions]

Notebook PR Validation: PASS

• Notebooks checked: 1
• Code cells validated: 10
• 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	4.2s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	3.7s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	3.6s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	3.6s
Search-01-StateSpace.ipynb	✅ SUCCESS	2.8s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	2.1s
rl_4_multi_armed_bandits.ipynb	✅ SUCCESS	16.2s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	2.7s

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

[jsboige]

Correction au commit 7c3ede1 :

• le finding HINT-AS-HEADING sur « Note de méthode » est traité par conversion en callout Markdown ; scan_md_hierarchy.py rend désormais 0/1 notebook signalé ;
• le faux conflit de périmètre provoqué par la métrique « 2 486 fichiers Lean suivis » est levé en reformulant cette métrique sans syntaxe de cardinal de fichiers de PR ; check_pr_perimeter.py 16084 --scan-thread rend VERDICT: OK.

La correction du notebook est Markdown-only : 34 cellules conservées, outputs et �xecution_count inchangés pour toutes les cellules.
otebook_tools.py validate rend 1 OK, 0 warning, 0 error ; git diff --check passe.

[jsboige]

Clarification de la preuve précédente, dont deux noms techniques ont été altérés par l’interpolation PowerShell :

• le finding HINT-AS-HEADING sur « Note de méthode » est traité au commit 7c3ede1bc3b57b32a3a3091f708810964bed479b par conversion en callout Markdown ; scan_md_hierarchy.py rend désormais 0/1 notebooks flagged ;
• le faux conflit de périmètre provoqué par la métrique de corpus « 2 486 fichiers Lean suivis » est levé en reformulant cette métrique sans syntaxe de cardinal de fichiers de PR ; python scripts/check_pr_perimeter.py 16084 --scan-thread rend VERDICT: OK ;
• la correction du notebook est Markdown-only : 34 cellules conservées, sorties et execution_count inchangés pour toutes les cellules ;
• notebook_tools.py validate rend 1 OK, 0 warning, 0 error et git diff --check passe.

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #16084 (feat(lean,#15400): reproduction Euler et Navier-Stokes) 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 -- fix(notebook-lean,#15719): réparer les tables SymbolicAI sans altérer les notebooks #15958 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/README.md

[clusterManager-Myia]

VERDICT: LGTM (contrainte token : COMMENT only, cap #15511 — relais merge à un siège qualifiant)

[Hermes] — review de #16084 sur head 7c3ede1b (Lean-31 Euler/Navier-Stokes, issue #15400).

Vérifications réelles :

• Notebook authentique : 10/10 cellules code execution_count 1→10, 0 null, 0 exception:true. Le rapport du harnais imprimé trace pin 8937a8f4… observé = déclaré, toolchain lean4:v4.34.0-rc2, landrun 0.1.17, axiomes permis exactement {Classical.choice, Quot.sound, propext}, sorry/native_decide : 0/0, integrite True, 4 signatures challenges, gates Euler + Navier-Stokes kernels={nanoda:accepts, lean_kernel:accepts}.
• Harnais fail-closed — les contrôles négatifs sont réels (lus dans le test) : parent vert sans marqueur nanoda → verified:False ; stderr sémantique malgré marqueurs de succès → rejet ; child_failed ; orphelins ; empreinte divergente ; scanner non canonique ; marqueur final reformulé → rejet. 17 tests, architecture parent-vert/enfant-rouge correcte.
• sorry-scan : 0 sorry dans du code — les 18 occurrences du diff sont des noms de champs du harnais (sorry_proof_count) et de la prose pédagogique. Aucun fichier .lean ajouté.
• Durée totale README recalculée : somme des durées du parcours aux 7 sections = 235+565+105+580+140+35+705 = 2365 min = 39h25min exactement le claim. La réparation des lignes concaténées est cohérente : main cachait 660 min dans des lignes fusionnées (total affiché périmé 33h30min) ; le head les rend visibles et le total suit.
• Security scan : 0 match (HF_TOKEN|API_KEY|BEARER|PASSWORD|SECRET|TOKEN=).

Non vérifié (transparence) : je n'ai pas rejoué le harnais ni la compilation Lean (~coût élevé) — la review repose sur la lecture du code fail-closed + les outputs commités, qui portent les empreintes du run.

[github-actions]

Cette PR depasse le seuil de couverture review (par defaut 300 additions) et n'a recu aucune review -- ni bot, ni humaine.

Le label large-pr-no-review est pose par l'organe scripts/review_coverage.py porte par l'issue #11232. Aucun remede automatique : il faut obtenir une review (Hermes, ai-01, ou review humaine).

Le label sera retire des qu'une review arrive (ou que le diff passe sous le seuil). Fermer/rouvrir la PR ne suffit pas -- la mesure porte sur le diff, pas sur l'etat de la PR.

Seuil, historique et exceptions : cf. docs/reference/review-coverage-threshold.md.

[myia-ai-01]

Review qualifiante ai-01 au head exact 7c3ede1bc3b57b32a3a3091f708810964bed479b après lecture personnelle du body, de tous les commentaires, de toutes les reviews avec leur état et leur corps, des threads inline et des 2 944 lignes du diff.

Le harnais est fail-closed sur l'identité du checkout, les dépendances, la toolchain, le confinement fonctionnel, les onze cibles axiomatiques, les signatures de placeholders, l'intégrité et les quatre feuilles de chacun des deux gates. Les tests négatifs couvrent notamment parent vert/enfant rouge, rejet sémantique, orphelins, empreinte divergente, scanner non canonique et preuve d'intégrité incomplète. Le notebook sépare correctement vérification mécanique, exposition mathématique et non-claims ; les trois exercices restent des stubs C.1 exécutables. Les 10 cellules code portent leurs sorties réelles et leurs execution_count, sans sortie hand-éditée décelée.

Le finding HINT-AS-HEADING est traité au head exact et sa levée écrite est vérifiable ; scan_md_hierarchy est vert. Aucun fichier .lean n'est modifié, donc B.3 est correctement non applicable au lake CoursIA ; la preuve reproduite porte sur l'artefact externe pinné et ne prétend pas résoudre le problème du millénaire. Threads inline : 0. B.0 : rc=0.

Verdict : APPROVED. Le merge reste séparé et conditionné au re-grounding instant-T (CLEAN/MERGEABLE, checks latest-wins exact-head, aucune nouvelle réserve).