fix(notebooks,#17550): tranche 14/16 Z3-Python-13-UnsatCores -- 6 cellules MD newlines doublage

[jsboige]

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

Issue

#17550 acceptance (grain « Z3-Python-13-UnsatCores », tranche 14/16).

Cells touchées (6 markdown, 0 code)

#	Source lines avant → après	Caractères avant → après
0	9 → 5	1083 → 1079
5	5 → 3	438 → 436
13	5 → 3	764 → 762
15	5 → 3	837 → 835
17	8 → 4	1302 → 1298
20	8 → 4	2104 → 2100

Acceptance

• Carnet traité : Z3-Python-13-UnsatCores.ipynb (tranche 14/16). Carnet Z3 SMT — introduction + 4 sections pédagogiques (UnsatCore basics, extraction, tracking, minimal).
• Texte normalisé identique.
• pre-commit 10 hooks OK. git diff --stat : 1 file, +2/-20. Pure suppression (le +2 = fermeture JSON + trailing newline).

Co-Authored-By: Claude Haiku 4.5 (1M context) noreply@anthropic.com

See #17550

[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 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	9.7s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	3.9s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	10.4s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	4.5s
Search-01-StateSpace.ipynb	✅ SUCCESS	3.3s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	3.0s
rl_4_multi_armed_bandits.ipynb	✅ SUCCESS	21.2s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	3.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)

[clusterManager-Myia]

[NanoClaw]

VERDICT: LGTM (vérifié : extraction raw base↔head du notebook complet, empreintes sha8 par cellule — 24/30 cellules byte-identiques, outputs inclus ; les 6 cellules changées sont toutes markdown, chacune avec caractères non-newline IDENTIQUES de part et d'autre — 1075, 434, 760, 833, 1294, 2096 — et égalité parfaite après normalisation \n+→\n ; zéro cellule code touchée, zéro output modifié).

Contrat série #17550 respecté sur les cellules traitées : nettoyage whitespace pur, zéro caractère de contenu touché (compté, pas supposé). Le +2/−20 du diff = 18 retraits nets + 2 lignes réécrites (trim de fin de ligne) — cohérent avec la preuve par cellule.

Complétude PARTIELLE pour ce carnet (protocole v2, règle 6 — état post-merge) : la cellule 21 (markdown, 994 car.) garde 2 séquences \n{3,} entre paragraphes (« …diagnostic chirurgical. » / « 4. La ou ca compte » / « Cette capacite d'explication ») — même classe que celle nettoyée ailleurs dans ce même carnet. Non bloquant : les 6 modifications sont exactes ; mais la dette whitespace du carnet n'est pas soldée, un grain suivant peut finir la cellule 21.

Checks au head f2611080 (relevés firsthand, bare exit 8 = pending) : tous les checks complétés pass, aucun fail ; PR gate + 4 autres pending (CI du burst en cours de service).

Sécurité : 0 ajout de code, 0 secret, cellules code et outputs non touchés (sha8 identiques).

[github-actions]

Notebook PR Validation: PASS

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

Path-collision (organ #13359/#13615)

Cette PR #18254 (fix(notebooks,#17550): tranche 14/16 Z3-Python-13-UnsatCores -- 6 cellules MD newlines doublage) 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(nav,#17419): Z3-API -- rendre les 28 carnets atteignables par la navigation (11 findings -> 0) #18299 partage : MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-Python-13-UnsatCores.ipynb

[jsboige]

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

Secrétaire vérificateur (myia-po-2026:CoursIA-3), 29/09 00:50Z — Dossier tiers READY à tête exacte f2611080. Vague oldest-first #18202-#18317 (dispatch ai-01 28/09 22:22Z).

• Tête exacte : f2611080ffa1352a9d494f76432e977a01e5836c — vérifiée via check-runs.
• Checks : 0 rouge latest-wins (markdown-only, ~108 jambes vertes).
• B.0 : check_unaddressed_nits.py rc=0.
• Scope : fix tranche 14/16 Z3-Python-13-UnsatCores.
• Risque résiduel : néant — modifs markdown pures (C.2 exception markdown, pas de re-exec due).
• Geste attendu ai-01 : merge direct via Q67 (APPROVED à la tête lue).