fix(lean,#18053): tranche Lean -- DANGLING_INTRO Lean-01-Setup cell[3] + INTERP_BEFORE_CODE Lean-7b-Examples cell[21]

[jsboige]

Grain: MED/notebook-python -- lane myia-po-2026:CoursIA-2 -- prev: DEEP/notebook-python #19773

fix(#18053): tranche Lean -- DANGLING_INTRO Lean-01-Setup + INTERP_BEFORE_CODE Lean-7b-Examples

See #18053 (audit du 27/09, ordre code/interpretation). Tranche 2/9 du dispatch ai-01 tapis central 06/10 (apres la tranche GameTheory PR #19773).

2 constats CONFIRMED firsthand (G.9, re-verification sur main vif avant edition)

• Lean-01-Setup-Lean-Python cell[3] (DANGLING_INTRO, 3/3) : la cellule se terminait par « Executez la cellule suivante pour diagnostiquer votre environnement : » mais la cellule suivante [4] est le markdown « Plateformes supportees » ; le bloc de code de diagnostic est en cell[5]. Fix = reformulation (pattern fix(notebooks,#18053): Argumentation-08b -- la note technique pointe sa vraie cible #18535) : la phrase nomme la position reelle du bloc « Diagnostic complet de l'environnement Lean 4 », la promesse d'une cellule suivante code disparait.

• Lean-7b-Examples-Python cell[21] (INTERP_BEFORE_CODE, 3/3) : « ### Interpretation de la solution » decrivait la fonction correction_loop_solution -- qui n'est definie NULLE PART avant elle (grep du dossier Lean : 0 definition, seules 2 references, cell[21] et les consignes de l'Exercice 2 en cell[32]). L'exercice qui la vise vient 11 cellules plus bas. Fix = reformulation titre + chapeau : « Architecture de la boucle de correction », presentation prospective de la cible de l'Exercice 2, plus lecture d'une sortie inexistante. Le corps (tableau, note pedagogique) est conserve tel quel.

Perimetre

• 2 fichiers, 4 insertions, 4 suppressions (markdown-only).
• Lean-17b-Knots-Invariants-Companion (3e constat Lean vivant) reste hors perimetre : 2 PRs ouvertes d'autres lanes touchent ce carnet (L898 collision guard, recherche par chemin exact) : Fix(lean,#19653): section 6.1 SnapPy 3.3.2 -- 5/5 PD-codes + float(vol) + is_achievable retrait + 3 contre-verites #19666 + feat(lean,#19644): Lean-17 Conway-Bridge-to-Knots - portail escalier #19669.

Verifications pre-commit

• scan_cell_ordering.py post-edition : Lean-01-Setup 1 clean, 0 findings ; Lean-7b-Examples le finding MED INTERP_BEFORE_CODE elimine, residuel LOW SECTION_GAP 7.7 (numerotation de sections) hors scope de l'issue.
• detect_md_content_loss.py --base origin/main --head HEAD : findings=0 sur les 2 carnets (normalized_chars identiques).
• Cellules code byte-identiques (8 + 11), ids de cellules preserves : pas de re-execution due (C.3, pattern fix(notebooks,#18053): Sudoku -- l'interpretation suit sa source #18533/fix(notebooks,#18053): Argumentation-08b -- la note technique pointe sa vraie cible #18535).
• Pre-commit H.3 : hooks PASSED (sortie du commit).

Conformite

• C.1 : pas d'erreur volontaire (aucune cellule code touchee).
• C.2 : outputs non touches, markdown seul.
• G.1 : constats re-verifies firsthand sur main avant edition (audit-reassessment Step 1-2).

Suite de la file dispatch (ai-01 tapis central 06/10)

• audit(notebooks): 46 constats d'ordre code / interprétation confirmés par 3 sceptiques, 17 séries (audit du 27/09) #18053 : restent 4 constats vivants hors Lean (GenAI/Texte 09b_Prompt_Security_RedTeam, Vibe-Coding 01-Claude-CLI-Bases, SemanticWeb RDF.Net-Legacy, Tweety-5) + Lean-17b (gelle sur PRs d'autres lanes).
• [Audit #17073] Série Complexity — partition Hermes #17151 : PR fix(complexity,#17151): 4 findings Complexity -- cross-links RL, stale-claims, banniere, preface 06b #19781 ouverte (ripe CLEAN).
• audit(readme): 55 écarts README / notebooks — Autres séries, 33 README (audit du 27/09) #18064 : READMEs GameTheory/Tweety/Geometry -- pas encore servi.
• densite pedagogique : 430 notebooks sous le plancher 1200 — surface majoritairement non suivie #13410 : densite queue du body -- pas encore servi.

---

🤖 Generated with Claude Code

[github-actions]

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

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

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	2.9s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	3.0s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	3.6s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	4.6s
Search-01-StateSpace.ipynb	✅ SUCCESS	3.9s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	2.6s
RL-04-Bandits-Manchots-Python.ipynb	✅ SUCCESS	15.8s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	2.6s
GameTheory-13d-Optimistic-CFR-Python.ipynb	✅ SUCCESS	10.4s

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

[github-actions]

Notebook PR Validation: PASS

• Notebooks checked: 2
• Code cells validated: 19
• 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-2025:CoursIA-2
pr: 19878
head: 258f5b6
complete: true
body: read
comments-reviewed: 7
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 5e7a5776f7f0550ce90a930a4eb6bdf4e77af1f105b2853602c11fd90e0a409a
diff-files: 2
diff-additions: 4
diff-deletions: 4
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 19878
organ-rc: 0
[/ADJOINT PREFLIGHT]