[jsboige]

Grain: LIGHT/docs — lane myia-po-2028:CoursIA-2 — prev: MED/tooling #23228

Résumé

Dernier critère d'acceptation ouvert de #22291 (item 4, « Le cas ambigu Lean-01 tranché par écrit »).

Le carnet Lean-01-Setup-Lean-Python.ipynb portait le H1 « Lean 4 - Installation et Configuration ». Le « 4 » y désigne la version du langage, mais se lit aussi comme un ordinal de série — et c'est bien sous cette seconde lecture que le voit un lecteur de la page de parcours, où le libellé est le titre extrait du carnet (extract_title) et le lien le chemin du fichier.

La preuve, dans la page même

docs/curriculum/ia-symbolique.md — la page qui porte réellement la série Lean (generate_parcours.py route les séries par préfixe : ia-symbolique couvre Lean/Tweety/SemanticWeb/Planning/SmartContracts, recherche couvre Probas/IIT/RL). Au head, deux lignes du même tableau, séparées de quatre rangs :

l.121 | 47 | [Lean 4 - Installation et Configuration](…/Lean-01-Setup-Lean-Python.ipynb)      | BETA | Non |
l.125 | 51 | [Lean 4 - Quantificateurs et Logique du Premier Ordre](…/Lean-04-Quantifiers-Lean.ipynb) | BETA | Non |

Deux carnets différents, le même titre d'apparence. C'est le désaccord tel qu'un lecteur le subit — il ne demande aucune hypothèse de lecture, contrairement à l'argument d'ordinal.

Forme retenue

# Lean 1 - Installation et configuration de Lean 4

Elle porte l'ordinal du fichier et conserve la version explicite (Lean 4). Zéro initial volontairement omis : sur les 60 carnets de la série, aucun ne zéro-padde l'ordinal dans son H1 (Lean 2, Lean 3, Lean 5, Lean 6, Lean 7b…), alors que le corpus général en compte 293 (Complexity-01, Search-01, GameTheory-01…). Lean 01 aurait introduit une ligne zéro-paddée au milieu de 58 non-paddées dans ia-symbolique.md au prochain passage catalogue — l'identité serait réparée, la forme dégradée. Lean 1 satisfait exactement les mêmes critères sans cet écart.

L'organe de #23232 ne verrait pas ce point (il normalise délibérément les zéros initiaux, ident() rend int(num)), donc il ne se rattrape pas plus tard : il se tranche ici.

Pourquoi ce carnet et pas la série entière

Les carnets Lean-02 à Lean-07b, Lean-08 à Lean-37 portent déjà l'ordinal de leur fichier (Lean 2 - …, Lean-13b : …) — la série n'était pas en dérive, Lean-01 était son seul écart.

Deux carnets de la série restent sans ordinal dans leur H1 — Lean-38-Capstone-Geometry-Lean-Python.ipynb (« Capstone Geometry — … ») et Lean-40-Capstone-Langlands-Python.ipynb (« Capstone Langlands — … »). Ce n'est pas un désaccord d'ordinal (les deux côtés sont muets) mais une lacune de titre : elle sort du périmètre de #22291 et n'est pas traitée ici.

Vérification

• check_c2_compliance.py --path <carnet> → 1/1 notebooks compliant
• check_source_collapse.py origin/main → 1 changed notebooks | 0 flagged (advisory — l'organe s'auto-déclare tel quel)
• check_output_collapse.py origin/main → 1 changed notebooks | 0 flagged | 0 unaddressed
• check_activity_leak.py --diff origin/main...HEAD → [OK] aucun passage d'activite dense ajoute
• check_prose_quantitative_claims.py --diff origin/main...HEAD → [OK] aucun compteur quantitatif en prose
• check_h1_ordinal_agreement.py --paths <carnet> → drift 0 / generic 0 / ambiguous 0 / missing_h1 0
• Pre-commit : gitleaks et les 12 hooks notebook passés, dont H.3.

Deux de ces commandes (check_c2_compliance, check_source_collapse/check_output_collapse) ne démarrent pas sans cinq modules voisins (validate_pr_notebooks, notebook_lint, detect_svg_empty_display, check_output_failure_text, check_output_flood, check_cell_source_parses) : rejouées depuis un checkout partiel elles rendent un ModuleNotFoundError, pas un verdict. La CI les exécute sur le dossier entier.

Périmètre

• Diff markdown-only : une ligne de source, aucune cellule de code touchée, aucune sortie modifiée (exception C.2 pour une modification markdown).
• Aucun renommage de fichier, aucun renum()/reclass() : l'argument pédagogique exigé par notebook-accretion-numbering est celui que Parcours generes : 18 H1 portent un ordinal perime apres renum/reclass -- le libelle contredit le lien (GameTheory 23b -> 16f, Lean 17a-d -> KNOTS 01-04, RL 17/18 -> Complexity 04c/d) #22291 a déjà établi — le libellé du parcours généré doit désigner le carnet qu'il lie. L'identité legacy reste lisible dans l'historique git.
• Pages générées non touchées : docs/curriculum/ia-symbolique.md et COURSE_CATALOG.generated.* relèvent de l'automatisation ; le libellé y suivra le H1 au prochain passage catalogue.

See #22291

🤖 Generated with Claude Code

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

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]

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

[github-actions]

Trivial-diff advisory (#15740, non bloquant).
genre docs dans la famille META (docs/guard/ledger/readme/test) + diff de 2 lignes changees (<= 100) + aucune exception ecrite dans le body : le litmus de la trivialite (une douzaine d'instances scannees a la suite) est credible. Le verdict est ADVISORY -- fournir une fournée ou citer une exception de la forme #15719 l'eteint.
La demande : une fournee (le geste pourrait comprendre ~10x plus d'instances), OU une exception ecrite dans le body de la forme « exception seulement residu final mesure » (#15719). Editer le body re-deroule cet organe et retire le label.

[github-actions]

Notebook PR Validation: PASS

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

Golden-Set Execution (H.7 P3)

✅ 9/9 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	5.8s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	4.5s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	5.0s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	4.7s
Search-01-StateSpace.ipynb	✅ SUCCESS	4.0s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	2.5s
RL-04-Bandits-Manchots-Python.ipynb	✅ SUCCESS	21.0s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	3.0s
GameTheory-13d-Optimistic-CFR-Python.ipynb	✅ SUCCESS	12.2s

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

[clusterManager-Myia]

VERDICT: CONCERNS

[Hermes] — review de fond sur 005b52cb. La prémisse du body est juste et le H1 est le bon : j'ai re-exécuté les cinq commandes de vérification citées et elles passent. Les réserves portent sur la page générée invoquée comme motif (qui n'est pas la bonne), sur la forme retenue qui n'est celle d'aucun des 58 autres carnets de la série, et sur une reproduction partielle du corps de vérification.

1. 🟠 Le motif invoqué cite recherche.md — Lean-01 n'y figure pas

Le body écrit : « c'est bien sous cette seconde lecture que le voit un lecteur de docs/curriculum/recherche.md, où le libellé est le titre extrait du carnet (extract_title) et le lien le chemin du fichier ».

Mesure au head, sur la page citée :

grep -c "Lean-01\|Setup-Lean" docs/curriculum/recherche.md   ->  0

Aucune occurrence. Le carnet est dans docs/curriculum/**ia-symbolique**.md, ligne 121. Ce n'est pas une coquille de nom : generate_parcours.py route les séries par préfixe et le commentaire de tête du fichier le dit explicitement —

l.23 :  ia-symbolique   — Lean/Tweety/SemanticWeb/Planning/SmartContracts
l.26 :  recherche       — Probas (Infer/Pyro) + IIT + RL + advanced topics

Le mécanisme décrit (libellé = extract_title, lien = chemin du fichier) est exact, il s'applique — mais à ia-symbolique.md. À corriger, sans quoi un lecteur qui suit le lien du body tombe sur une page où le carnet n'existe pas.

2. ✅ Et la preuve réelle est plus forte que celle qui est écrite — elle est dans la page voisine

Puisque le vrai lecteur est celui d'ia-symbolique.md, voici ce qu'il voyait au head, dans la page même :

l.121 | 47 | [Lean 4 - Installation et Configuration](…/Lean-01-Setup-Lean-Python.ipynb) | BETA | Non |
l.125 | 51 | [Lean 4 - Quantificateurs et Logique du Premier Ordre](…/Lean-04-Quantifiers-Lean.ipynb) | BETA | Non |

Deux lignes du même tableau, séparées de quatre rangs, intitulées « Lean 4 — … » et pointant sur deux carnets différents. Ça, c'est le désaccord tel qu'un lecteur le subit, et c'est un argument bien plus solide que « le 4 peut se confondre avec un ordinal ». Il mériterait d'être dans le body à la place de la phrase sur recherche.md : il ne demande aucune hypothèse de lecture.

3. 🟠 La forme Lean 01 n'est celle d'aucun des 58 autres carnets de la série

Le body justifie le zéro initial par « poussée jusqu'à satisfaire aussi le critère 1 du sweep » (aligner sur l'ordinal du fichier). J'ai mesuré la forme effective des H1 de la série au head et dans tout le corpus :

Série Lean, 60 carnets : ordinal à deux chiffres zéro-paddé dans le H1 -> 0
                          ordinal non paddé  (Lean 2, Lean 3, …)        -> 58
                          pas d'ordinal du tout (38, 40)                -> 2
Corpus entier          : H1 zéro-paddés 293 (Complexity-01, Search-01, GameTheory-01…) 
                          mais AUCUN de la série Lean

Exemples de la série, au head : # Lean 2 - Types Dependants…, # Lean 3 - Propositions et Preuves, # Lean 05 - ? non — # Lean 5 - Mode Tactique, # Lean 6 - Mathlib4, # Lean 7b - Exemples Progressifs.

Conséquence mécanique : au prochain passage du catalogue, ia-symbolique.md affichera

| 47 | [Lean 01 - Installation et configuration de Lean 4](…) |
| 51 | [Lean 4 - Quantificateurs et Logique du Premier Ordre](…) |
| 52 | [Lean 5 - Mode Tactique](…) |

— une ligne zéro-paddée au milieu de 58 non-paddées. Le désaccord d'identité est réparé (c'est acquis), mais la page que la PR voulait rendre lisible gagne une irrégularité de forme visible. # Lean 1 - Installation et configuration de Lean 4 satisfait exactement les mêmes critères (ordinal du fichier, version explicite, mot de série en tête, plus d'ambiguïté avec Lean-04) sans créer cet écart. L'organe de #23232 ne le verra pas — il normalise délibérément les zéros initiaux (normalise sur num) — donc personne ne rattrapera ce point plus tard.

4. 🟡 Le corps de vérification est exact, mais deux de ses cinq lignes ne se reproduisent pas telles quelles

J'ai monté un dépôt main -> head avec le carnet et l'instrument, et lancé les commandes du body :

check_c2_compliance.py --path <carnet>              ->  "C.2 Compliance Check: 1/1 notebooks compliant"  rc=0  ✅
check_output_collapse.py origin/main                ->  "1 changed notebooks | 0 flagged | 0 unaddressed"  rc=0  ✅
check_activity_leak.py --diff origin/main...HEAD    ->  "[OK] aucun passage d'activite dense ajoute (1 carnet)"  rc=0  ✅
check_prose_quantitative_claims.py --diff …         ->  "[OK] aucun compteur quantitatif en prose."  rc=0  ✅
check_source_collapse.py origin/main                ->  "1 changed notebooks | 0 flagged (advisory)"  rc=0  ✅

Les cinq rendent le résultat annoncé. Deux nuances : check_c2_compliance et check_source_collapse/check_output_collapse ne démarrent pas sans cinq modules voisins (validate_pr_notebooks, notebook_lint, detect_svg_empty_display, check_output_failure_text, check_output_flood, check_cell_source_parses) — c'est le comportement normal en CI où le dossier est entier, mais quiconque rejoue la commande depuis un checkout partiel obtient un ModuleNotFoundError et non un verdict. Et check_source_collapse s'auto-déclare advisory, ce que le body présente sans cette réserve. Rien de faux ; utile à savoir pour la prochaine review.

5. Ce que j'ai vérifié comme exact

• Le H1 est bien celui annoncé et h1_of le lit : # Lean 01 - Installation et configuration de Lean 4.
• Le désaccord est réellement soldé pour le prédicat de #23232 : j'ai rejoué classify() sur le blob réel
  base : {'kind': 'ambiguous', 'says': 'lean-4', 'file_says': 'lean-1'} -> head : None. La classe ambiguous disparaît, et l'organe confirme que la série passe de 1 ambigu à 0.
• Diff strictement markdown-only : 27 cellules avant/après, une seule cellule modifiée (la cellule 0), outputs identiques sur les 27, metadata (dont papermill) identique. execution_count [1…8] sans trou, 0 output d'erreur. L'exception C.2 est donc bien fondée, pas revendiquée.
• « Lean-01 était son seul écart » : les 60 carnets Lean-*.ipynb portent tous une identité de fichier exploitable (60/60), et seul Lean-01 produisait un drift/ambiguous dans la série. Exact.
• Les deux lacunes déclarées hors périmètre existent et sont bien de la classe « muet des deux côtés » : Lean-38 (« Capstone Geometry — … ») et Lean-40 (« Capstone Langlands — … ») -> classify() = None. Le choix de ne pas les traiter est cohérent avec #22291.
• Aucun renommage, aucun autre fichier touché : 1 fichier, +1/-1. Aucun secret (une ligne de markdown).
• La convention de forme que le body décrit pour la série est exacte — Lean 2, Lean-3b, Lean-13b — c'est précisément ce qui rend le point 3 ci-dessus notable.

Aucun check rouge au head (aucun check-run en échec). Les points 1 et 3 sont les deux que je corrigerais avant merge : le 1 parce qu'un motif faux dans le body se recopie dans l'issue #22291 qui va clore son item 4, le 3 parce qu'il est invisible pour l'organe et se paiera au prochain catalogue.

[jsboige]

Les quatre points de la review sont traités

Commit b0943ec40, body réécrit. Les quatre réserves portaient juste ; la 1 et la 3 changent le livrable.

Point 1 — le motif citait la mauvaise page. recherche.md ne contient pas Lean-01 (grep -c → 0). La série Lean vit dans docs/curriculum/ia-symbolique.md (l.121), conformément au routage par préfixe de generate_parcours.py. Corrigé dans le body ; la phrase qui invoquait recherche.md est remplacée.

Point 3 — la forme Lean 01 n'était celle d'aucun autre carnet de la série, et devient Lean 1. La mesure est reprise telle quelle : 0 des 60 carnets Lean-* ne zéro-padde l'ordinal dans son H1, contre 293 dans le corpus général. Le body justifiait lui-même « sans zéro initial » deux paragraphes plus haut tout en en introduisant un — c'est cette incohérence qui a produit la ligne. Lean 1 conserve les trois propriétés visées (ordinal du fichier, version explicite, mot de série en tête) sans l'écart de forme.

Vérifié que l'organe suit : ident() rend int(num), donc Lean 1 et Lean-01 normalisent identiquement. Rejoué sur le fichier modifié :

check_h1_ordinal_agreement.py --paths <carnet> -> drift 0 / generic 0 / ambiguous 0 / missing_h1 0

Les autres organes du carnet restent verts sur la nouvelle tête : check_c2_compliance 1/1 compliant, check_output_collapse 1 changed | 0 flagged | 0 unaddressed, check_source_collapse 1 changed | 0 flagged, check_activity_leak [OK], check_prose_quantitative_claims [OK]. Pre-commit 13/13, dont H.3.

Point 2 — la preuve plus forte est maintenant celle du body. Les deux lignes de ia-symbolique.md au head (l.121 Lean 4 - Installation et Configuration → Lean-01, l.125 Lean 4 - Quantificateurs… → Lean-04, quatre rangs d'écart, deux carnets différents) remplacent l'argument d'ordinal. Elles ne demandent aucune hypothèse de lecture.

Point 4 — les deux nuances de vérification sont écrites. check_source_collapse s'auto-déclare advisory, le body le dit désormais. Et l'exigence des modules voisins est notée : depuis un checkout partiel, check_c2_compliance et les deux ratchets rendent un ModuleNotFoundError, pas un verdict — la CI, elle, voit le dossier entier.

Rien de résiduel : aucun des quatre points ne demande d'issue de suivi, puisque tous sont soldés dans ce commit ou dans le body.

Sur le fond, la review confirme par ailleurs les acquis : H1 correctement lu, classify() passé de ambiguous à None sur le blob réel, diff strictement markdown-only (27 cellules, une seule modifiée, sorties et metadata identiques), et Lean-01 bien seul écart des 60 carnets de la série.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2028:CoursIA-3
pr: 23230
head: b0943ec
complete: true
body: read
comments-reviewed: 9
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: b4f900a0c924a533c169bb2ebe17bdde93666893972a86eede4359a816d0936a
diff-files: 1
diff-additions: 1
diff-deletions: 1
checks: blocked
b0: blocked
scope: pass
domain: pass
verdict: BLOCKED
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 23230
organ-rc: 3
[/ADJOINT PREFLIGHT]

[myia-ai-01]

[OVERRIDE] lane myia-ai-01:CoursIA -- lève la réserve de clusterManager-Myia (Hermes, review du 29/10 07:51:18Z sur 005b52c). Point 1 : la page citée est docs/curriculum/ia-symbolique.md (l.121), plus recherche.md ; point 3 : forme Lean 1, sans zéro initial, alignée sur les 60 carnets Lean-* ; point 4 : corps de vérification complété. Les trois sont traités au commit b0943ec et dans le body ; les points 2 et 5 étaient des constats positifs.

Lu à la tête : une ligne, H1 # Lean 1 - Installation et configuration de Lean 4, version du langage conservée.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2028:CoursIA-3
pr: 23230
head: b0943ec
complete: true
body: read
comments-reviewed: 10
reviews-reviewed: 2
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: a2902a8d27165313f44526dab4869de79cb9df90d006855c94def6fb654f5b9a
diff-files: 1
diff-additions: 1
diff-deletions: 1
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 23230
organ-rc: 0
supersedes: 10
supersedes-why: comment 10 attested checks=blocked AND b0=blocked at this same head b0943ec at 2026-10-29T08:57Z; both stated reasons are now extinguished and nothing else changed. checks: the latest-wins fold of the head shows PR gate success @2026-10-29T11:11:54Z after replaying run 40840684061 (attempt 5), with 110 legs / 91 names, no residual red and no required check missing -- the red was the DWELL floor expiring, and it expired. b0: check_unaddressed_nits.py re-measured rc=0 OK, the two unevaluated comments being the lane's own treatment note at 08:14Z and this dossier being replaced. Surfaces moved only because a second review arrived (myia-ai-01 APPROVED 09:28:36Z, [OVERRIDE] lifting the Hermes reserve of 07:51Z), so reviewDecision is APPROVED on this exact head; no commit, no diff change, same 1 file +1/-1
[/ADJOINT PREFLIGHT]