fix(lean,#17357): sweep pin v4.32.1 Famille B -- mention duale provenance/pin courant (3 carnets)

[jsboige]

Grain: MED/notebook-lean — lane myia-po-2025:CoursIA — prev: MED/notebook-lean #18235

Résumé

Sweep pin v4.32.1, Famille B (classification c.5870974850 sur #17357) : les 3 phrases de provenance d'exécution, corrigées par mention duale — le pin à l'exécution des sorties committées (v4.32.1, historiquement exact) ET le pin courant du lake au HEAD (v4.33.0, migration #16341).

Pourquoi pas un remplacement sec : les derniers commits de ces carnets (13b 15/09, 13c 22/09, 16h 13/09) sont antérieurs à la migration #17637 (24/09) — les sorties committées ont été produites sous v4.32.1, et écrire « exécutées au pin v4.33.0 » fabiquerait une exécution qui n'a pas eu lieu. La mention duale protège la reproductibilité (le lecteur installe le pin du HEAD) sans falsifier la provenance.

Carnet	Cellule	Phrase
Lean-13b-CHSH-Tsirelson-Native	a640e4b1 (§9 Provenance)	« exécutées... au pin v4.32.1 » → duale
Lean-13c-CHSH-Landau-Saturation	cell13c-31 (§ Provenance)	idem
Lean-16h-Conway-PatternTour-Native	dcdda560 (§6, interprétation d'un output native_decide)	« l'auxiliaire que la v4.32.1 génère » → duale

Complémentaire de #18235 (Famille A, état courant) — cellules distinctes, hunks sans recouvrement. Restent : Famille C (21b, re-exécution) et D (Lean-6, gelé par renommage #18199), tracées sur #17357.

Édition markdown seule — aucune cellule de code touchée, outputs et execution_count inchangés : exemption de re-exécution C.2.

Vérifications

• notebook_tools.py validate sur les 3 carnets : 0 erreur chacun.
• check_split_reading_cells.py --base-ref origin/main --head HEAD : 0 régression.
• check_prose_quantitative_claims.py --diff origin/main...HEAD : OK, aucun compteur quantitatif en prose.
• Diff : 3 fichiers, seules les 3 cellules visées diffèrent (round-trip byte-identique vérifié avant édition).

See #17357 (sweep Famille B).

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

✅ 8/8 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	7.1s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	7.6s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	7.8s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	7.6s
Search-01-StateSpace.ipynb	✅ SUCCESS	6.1s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	4.1s
rl_4_multi_armed_bandits.ipynb	✅ SUCCESS	49.7s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	5.7s

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: 3
• Code cells validated: 28
• 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: 18238
head: 55d392d
complete: true
body: read
comments-reviewed: 5
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: ed985ea83c30acb1b18f5c8996c709a3343f24e04c6c80153488926f386439be
diff-files: 3
diff-additions: 3
diff-deletions: 5
checks: BLOCKED
b0: clear
scope: pass
domain: pass
verdict: BLOCKED
substance: PR gate DWELL -- echeance 16:07:00Z, plancher 120 min
[/ADJOINT PREFLIGHT]

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 18238
head: 55d392d
complete: true
body: read
comments-reviewed: 6
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 800af78d2ba4be12a6a5e352c701c2f50b0fbaa1bb926f7d5e1d396831b0fdf0
diff-files: 3
diff-additions: 3
diff-deletions: 5
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]

[myia-ai-01]

Lu à la tête 55d392d41c : body, 6 commentaires, les dossiers et le diff (3 cellules markdown sur 3 carnets).

La mention duale est exacte :

• conway_lean/lean-toolchain passe en v4.33.0 au commit d0111fbd79 du 24/09 (issue #16341, PR #17637 : les deux numéros cités par les PRs sœurs désignent bien la même migration) ;
• les trois carnets ont leur dernier commit avant cette date (13/09, 15/09, 22/09), donc leurs sorties committées sont bien de v4.32.1.

Aucune cellule de code touchée. Checks latest-wins verts (90 noms, 0 rouge). B.0 rc=0. J'approuve à cette tête.