Fix(lean,#19736): cellule d'audit -- un echec de verification n'est pas un verdict sur les axiomes

[jsboige]

Grain: MED/notebook-lean -- lane myia-po-2026:CoursIA -- prev: DEEP/research-code #19827

Verdict sur #19736 : la prémisse est réfutée par la mesure

L'issue lit l'échec de re-exécution comme « l'audit interne du carnet a détecté un axiome interdit ». Aucun axiome interdit n'a jamais été détecté :

1. Le AssertionError "audit incomplet" vient de la première assertion (assert code_retour == 0 and all(nom in ax ...)) — celle des axiomes interdits porte le message "axiome interdit" et n'a jamais parlé.
2. Cause réelle, mesurée en deux temps :
   • formal_logic_lean/.lake/build présent mais stub (1 seul olean, FormalLogic/Bridge.olean) et aucune épingle enregistrée → l'organe lean_exec refuse par doctrine (T3, Lean: organe canonique d'exécution avec budgets machine-wide et confinement des processus #15666), exit=125 ;
   • épingle native posée (registre WSL, explicit-first-writer), la vérification échoue ensuite sur error: object file '...FairBotLoeb.olean' does not exist — le cache était invalide pour la toolchain 4.33.1 (1225 jobs recompilés, 730 s).

Le fix

Le message d'assertion porte désormais le code de retour, la liste des symboles dont les axiomes n'ont pas été lus, et le journal de l'organe (qui porte la raison du refus). Les cellules 20 et 25 héritent du même diagnostic (rapport() partagé). Un échec d'environnement ne se lira plus comme un verdict d'audit.

Ré-exécution (C.2)

Papermill 40/40 cellules, kernel python313 (3.13, même major.minor que la base), 18 min 14 s :

• 0 erreur, 0 execution_count nul, 0 chemin machine dans le fichier ;
• les trois audits sont verts ; axiomes mesurés : propext, Classical.choice, Quot.sound — aucun des INTERDITS (sorryAx, Lean.ofReduceBool, Lean.trustCompiler) ;
• cellule [17] passe sans AssertionError → critère d'acceptance de l'issue satisfait ;
• les sorties committées étaient restées celles du 23/09 (metadata papermill), antérieures aux 5 lignes de source du commit 5dec50e74b — elles sont rafraîchies ici.

Ratchets sur la tête : output-failure 0 regressed (bloquant), output-collapse et source-collapse 0 flagged (advisory). Pre-commit H.3 passé.

Réparation d'environnement (non committable, consignée)

Épingle native posée pour formal_logic_lean dans le registre WSL de l'organe (origin explicit-first-writer). Effet de bord consigné : sonder l'organe en --backend auto écrit une épingle default-policy (mon contrôle négatif sur game_theory_lean l'a fait) — leçon rangée en mémoire machine.

Closes #19736

🤖 Generated with Claude Code

[github-actions]

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

[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]

Golden-Set Execution (H.7 P3)

✅ 9/9 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	3.9s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	3.8s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	4.4s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	4.1s
Search-01-StateSpace.ipynb	✅ SUCCESS	3.1s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	2.0s
RL-04-Bandits-Manchots-Python.ipynb	✅ SUCCESS	15.3s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	2.3s
GameTheory-13d-Optimistic-CFR-Python.ipynb	✅ SUCCESS	8.8s

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

[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 PR Validation: PASS

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

[Hermes] — review complète de la tête 7170a911 (notebook Lean-34b seul fichier, +208/−192).

VERDICT: LGTM — le fix tient sa promesse : un échec d'environnement ne se lit plus comme un verdict sur les axiomes.

Vérifié (full-read 40 cellules via vue structurelle + diff + outputs committés) :

• rapport() (cell. 17) porte désormais code de retour, symboles sans axiomes lus et journal de l'organe dans le message d'assertion — exactement le remède au mésusage diagnostiqué dans #19736 ; cellules 20 et 25 héritent du même diagnostic via la fonction partagée.
• Axiomes mesurés dans les outputs committés : propext, Classical.choice, Quot.sound sur les trois audits, aucun des INTERDITS — la claim du body est ancrée dans la sortie réelle.
• Cellule d'audit passée sans AssertionError (code de retour : 0) → critère d'acceptance de l'issue satisfait.
• Ré-exécution authentique : exec 1→14 consécutifs, 0 null, 0 erreur, papermill duration 1094,6 s = les « 18 min 14 s » du body à la seconde près, end_time 2026-10-08T04:29Z (sorties bien rafraîchies vs 23/09), 0 chemin machine.
• Gates #17040 : une lecture par output de code, placée immédiatement après ; exercices 1-3 non leakés (cellules « à compléter », indices sans solution).
• Sécurité : 0 match sur le diff. CI : 88 organes verts, seul PR gate pending (DWELL, non bloquant).

Approve sous clusterManager-Myia (reviewer ≠ auteur). La méthode est exemplaire : la cause racine (cache .lake/build stub sans épingle → refus d'organe exit=125, puis olean absent) est établie par la mesure avant le fix, et le correctif rend la classe d'échec auto-diagnostiquée.

[Hermes hermes-pr-review, cycle :06 08/10, host 1ed7af3074fb, sig=e0bda58b]

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 19874
head: 7170a91
complete: true
body: read
comments-reviewed: 7
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 9ebb58bb40281b6828005d5ecc6abd24e877646ba16ae5f59d67301f5728dca2
diff-files: 1
diff-additions: 208
diff-deletions: 192
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 19874
organ-rc: 0
[/ADJOINT PREFLIGHT]

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #19874 (Fix(lean,#19736): cellule d'audit -- un echec de verification n'est pas un verdict sur les axiomes) 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(lean,#19480): errors=replace sur subprocess utf-8 dans 5 carnets Lean #19564 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-34b-FairBot-Loeb.ipynb