Fix(lean,#15629): Lean-03b formalized logic -- encoding=utf-8 sur les 4 appels subprocess text=True

[jsboige]

Grain: MED/notebook-python -- lane myia-po-2026:CoursIA -- prev: MED/notebook-python #19415

Summary — tapis #15629 (7/9)

Lean-03b-Formalized-Formal-Logic-Lean-Python.ipynb : les 4 appels subprocess.run(..., text=True) sans encoding= décodent leurs pipes en cp1252 (locale Windows) — crash silencieux du thread lecteur ou mojibake selon l'environnement. Ajout de encoding="utf-8" sur les 4 appels (résolution du lake formal_logic_lean ×2, lake build timeout=1800, timeout=900).

Diagnostic dérive

• Cause (a) env/kernel : text=True sans encoding= décode en cp1252 sous locale Windows ; l'exécution précédente dépendait de PYTHONUTF8=1 dans l'environnement du lanceur — invisible dans le notebook.
• Verdict : CAUSE_FIXED — l'encodage est désormais explicite dans la source.

Preuve A/B (outputs inchangés par le fix)

Run	Commande	Résultat
A (commité)	env -u PYTHONUTF8 papermill ... -k python313	9 cellules, 0 erreur
B (témoin)	PYTHONUTF8=1 papermill ... -k python313	9 cellules, 0 erreur

Comparaison par cellule (streams concaténés + execute_result text/plain, normalisée pour la segmentation de flush stdout) : 0 cellule avec outputs différents.

Validation

• Lake formal_logic_lean préchauffé avant exécution (cache oleans natif : 8360 archives d'oleans décompressées, build 878 jobs FormalLogic.Bridge — pas de compilation mathlib depuis la source).
• Papermill end-to-end sous py -3.13 -m papermill, kernel python313 (base language_info 3.13.7 — drift guard major.minor OK).
• H.3 : chaque cellule code porte execution_count + outputs ; 0 erreur volontaire.

See #15629

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

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

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

Golden-Set Execution (H.7 P3)

✅ 9/9 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	7.0s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	4.1s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	5.7s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	7.1s
Search-01-StateSpace.ipynb	✅ SUCCESS	5.3s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	3.6s
rl_4_multi_armed_bandits.ipynb	✅ SUCCESS	61.4s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	10.3s
GameTheory-13d-Optimistic-CFR-Python.ipynb	✅ SUCCESS	24.4s

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)

[github-actions]

Notebook PR Validation: PASS

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

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 19417
head: 3225a04
complete: true
body: read
comments-reviewed: 7
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 7e50a3676282ae610f37413f6456b018a62f3fd965bf1dd69231b252da66a7a7
diff-files: 1
diff-additions: 112
diff-deletions: 112
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 19417
organ-rc: 0
[/ADJOINT PREFLIGHT]