refactor(search,#17802): descente de 09d dans Discrepancy/ -- Discrepancy-02-Komlos-Lean

[jsboige]

Grain: MED/refactor -- lane myia-po-2027:CoursIA -- prev: MED/ledger #19085

Descente de 09d dans la sous-série Discrepancy/

Étape du plan de gradation Search (#17802), arbitrée en c.5832991722 : le compagnon formel du
lake discrepancy_lean descend dans la sous-série, avec son nom canonique dans le même
mouvement — un notebook ne se renomme qu'une fois.

Ancien chemin	Nouveau chemin
MyIA.AI.Notebooks/Search/Part1-Foundations/Search-09d-Lean-Discrepancy-Komlos.ipynb	MyIA.AI.Notebooks/Search/Discrepancy/Discrepancy-02-Komlos-Lean.ipynb

Le nom n'est pas choisi, il est mesuré contre deux sources :

• 02 — l'arbitrage fait du compagnon Beck-Fiala « la première marche de la sous-série »,
  livrée en Discrepancy-01-…. 09d est la deuxième.
• suffixe -Lean, et non -Lean-Python — la règle est écrite dans l'issue de la sous-série
  Search Discrepancy/ : notebook compagnon Beck-Fiala du lake discrepancy_lean (premiere marche de la sous-serie) #17816 : -Lean-Python s'applique « si le noyau est python3 et qu'il pilote le lake ». Le
  noyau réel de ce notebook est lean4-wsl (metadata.kernelspec.name, relevé sur origin/main).
  C'est le point où la lecture par le nom aurait donné le mauvais suffixe.

Comment le mouvement a été fait

Par l'organe canonique scripts/notebook_tools/rename_notebooks.py --mapping issue:17802#5984216914 --apply, en sa forme en deux commits :

1. git mv purs — le déplacement seul, aucun contenu touché ;
2. référents réécrits par surface — Part1-Foundations/README.md, Search/README.md,
   SymbolicAI/Lean/Lean-08-Agentic-Proving-Python.ipynb (cellule markdown),
   _quarto.yml, docs/curriculum/aima-walk.md, docs/curriculum/ia-classique.md,
   scripts/tests/baseline_nb_nav_chain.json.

Les deux commits sont ceux de l'outil : le second n'a pas été écrit à la main.

Réparation (tête 2d0ec03d) — la vague avait laissé des liens cassés

L'organe canonique réécrit le basename d'un lien relatif mais jamais son préfixe de
répertoire : après le déplacement, ../../Search/Part1-Foundations/<nom> pointait un dossier qui
ne contient plus le notebook. Le garde check-nav-chain a signalé un premier lien ; la lecture de
l'organe check_notebook_navlinks.py en a trouvé six, dont trois que la CI n'avait pas vus —
le notebook déplacé renvoie à Search-09c, qui était son voisin de dossier avant le mouvement.

Réparé sous garde structurelle I1/I2/I3 : aucune cellule de code, aucune sortie, aucun
execution_count n'est modifié — liens markdown, titre H1 et fil d'Ariane seulement, ce dernier
aligné sur la convention du pilote Discrepancy-01.

navlinks  : OK: 0 NEW broken navlink vs baseline (1472 notebooks scannes)
nav-chain : OK: 0 NEW finding vs baseline

Le défaut d'organe est signalé séparément (issue dédiée) : il devrait refuser en fail-closed un
lien relatif dont la cible change de répertoire, plutôt que produire un 404 silencieux — c'est la
doctrine I2/I3 que l'outil applique déjà aux cellules de code.

Vague de prose (tête d809ec0e) — fermée là où la descente rendait le texte faux

• arbre « Structure des fichiers » de Search/README.md — un nœud Discrepancy/ existe
  désormais (01 Beck–Fiala, 02 Komlós) ; la ligne du carnet a quitté le bloc Part1-Foundations/,
  dont le commentaire perd son compte de notebooks et la mention 09d ;
• table « Couverture actuelle » — ligne Discrepancy/ ajoutée, ligne Part1-Foundations
  corrigée : le compagnon Lean a changé de dossier, la ligne ne peut plus l'y compter ;
• Part1-Foundations/README.md — trois références de nom (prérequis, table des kernels,
  bibliographie) ;
• discrepancy_lean/FORMAL_STATUS.md (k5) et docs/curriculum/ia-classique.md (libellé) ;
• scripts/tests/baseline_nb_nav_chain.json — l'entrée unreachable de Discrepancy-02 est
  retirée : elle portait series: Part1-Foundations, une série devenue fausse, et le finding ne se
  produit plus (l'organe passe de 386 à 380 findings, zéro régression, --check rc=0). Les
  autres entrées caduques du fichier sont antérieures et sans rapport : elles ne sont pas absorbées
  dans ce diff.

Référents complétés (tête 13ffb217) — deux surfaces que l'organe ne liste pas

L'organe de renommage réécrit les liens qui citent le nom. Deux surfaces ne citent pas 09d et
déclaraient pourtant un état devenu faux ; elles ne pouvaient donc pas être vues par la vague :

• Search/LEAN_INVENTORY.md affirmait discrepancy_lean sans notebook câblé
  (« compagnon prévu : Search-15-CombinatorialDiscrepancy … Pas encore câblé »). C'est démenti par
  la mesure : Discrepancy-02-Komlos-Lean tourne sur lean4-wsl et porte 27 #check des
  énoncés du lake. La ligne passe de 0² à 1², le Total de 1 à 2.
  Le livrable A de Discrépance combinatoire — distiller Bansal–Jiang 2025 (arXiv:2508.03961) : notebook Search-15 + lake discrepancy_lean (noix Beck-Fiala 2k−1 grignotée par boutes, geste du découplage ancré ICT) #12823 est bien livré, mais en Discrepancy-01-BeckFiala-Lean-Python (kernel
  python3, zéro invocation du lake dans le code) : c'est un pont Python, et il ne compte donc
  pas dans une colonne qui mesure l'invocation effective du lake. Les distinguer était le point.
• Search/index.qmd ne documentait que search_lean sous « Companion formel — Lean 4 » : la
  section nomme désormais discrepancy_lean et ses deux carnets.

Correction d'un résidu mal motivé (même tête)

Le corps de cette PR a d'abord justifié le report de Lean-07b par « ni le kernel python3-wsl ni
les clés ne sont disponibles sur cette lane ». Les deux mesures étaient fausses : le kernel est
installé (jupyter kernelspec list) et .secrets/master.env existe. Re-mesuré avant d'agir, le
motif réel est autre — et il tient :

le correctif exige une ré-exécution, et l'exécuteur de cellule unique
(scripts/notebook_tools/exec_single_cell.py, l'organe C.2/C.3 pour ce cas précis) retire par
conception les blocs metadata.papermill hérités (#12722). Mesuré sur ce carnet : 387 lignes
supprimées, pour une chaîne de libellé. Or 1134 des 1485 carnets committés portent ces blocs —
c'est la convention dominante du dépôt, pas une dette à purger, et la suppression n'a aucun rapport
avec un renommage Search. Le sujet part donc en PR dédiée : c'est un arbitrage de périmètre, pas
un manque d'outillage.

Résidus déclarés, mesurés — hors de cette PR

• SymbolicAI/Lean/Lean-07b-Examples-Python.ipynb cellule 30 — l'ancien nom vit dans une
  cellule de code et dans ses sorties committées (libellé imprimé, pas un lien : le lien
  markdown de la cellule 28, lui, est réparé ici). Voir le paragraphe ci-dessus pour le motif exact
  du report. Une sortie committée ne se maquille pas (règle 6).
• Search/README.md — instantané daté « audit fichier-entier, 2026-09-16 » — deux lignes
  nomment encore Search-09d. Instantané daté, pas une couverture courante : mettre un total à
  jour à la main est interdit (fix(docs,#16904): audit README SemanticWeb — SW-13/14/15/16 absents, total 26→27, Python 14→15 #17029), et prose-counts est bloquant sur toute ligne ajoutée
  portant « N notebooks ».

DWELL

La tête a changé (d809ec0e → 13ffb217), donc le plancher de 120 min est ré-armé par ce
commit de contenu. Aucun impact sur l'attente : la candidate attend, la lane enchaîne.

Portée

Mouvement, référents mécaniques, réparation des liens, et deux surfaces documentaires qui
déclaraient un état faux. Aucune cellule source d'exercice, aucune sortie, aucun compteur de prose
n'est modifié ; COURSE_CATALOG.generated.* n'est pas touché (l'organe ne le réécrit pas, et la
règle interdit de le régénérer sur une branche feature).

Gardes rejouées sur la tête 13ffb217 : prose-counts --diff origin/main...HEAD --strict rc=0 ·
navlinks 0 lien cassé (1472 carnets) · nav-chain --check rc=0 (0 NEW vs baseline) ·
perimeter VERDICT OK, aucun workflow CI touché.

See #17802 · See #17816 · See #16231

🤖 Generated with Claude Code

[github-actions]

Golden-Set Execution (H.7 P3)

✅ 9/9 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	3.1s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	3.4s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	4.3s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	3.8s
Search-01-StateSpace.ipynb	✅ SUCCESS	3.8s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	14.4s
rl_4_multi_armed_bandits.ipynb	✅ SUCCESS	21.1s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	2.1s
GameTheory-13d-Optimistic-CFR-Python.ipynb	✅ SUCCESS	7.7s

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

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

⚠️ 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]

G-VAR-2/3 GENRE signals (advisory, non bloquant, #10020).
La lane `myia-po-2027:CoursIA` voit ces signaux actifs sur les mergees du jour (UTC 2026-10-04) :

• CAP-EXCEEDED-BY-GENRE : light_genre > cap partage G-VAR-2 (tally : declared=2 genre=3 cap=2)
• NOTE ([variation] Le label est lane-agregat mais PR-attache : le merge-gate peut HOLD le grain de CONTENU qui remedie au motif #10341) : la PR courante est de classe CONTENU (non LIGHT-genre) et ne contribue pas au motif ci-dessus -- les labels agregees ne sont PAS poses sur cette PR (le merge-gate ne doit pas la HOLD pour ce motif ; le coupable est parmi les grains META de la lane).

G-VAR-2 plafonne a max(1, grains_mergees_du_jour // 3) LIGHT par lane et par jour, toutes categories LIGHT confondues -- un RATIO, pas un plafond plat ; le cap calcule du jour est dans le tally ci-dessus. G-VAR-3 interdit deux genres LIGHT consecutifs. Les signaux ci-dessus rendent le fait VISIBLE (labels variation-tier-inflation, `variation-genre-run`, `variation-genre-cap-exceeded`, `variation-genre-mismatch`, `variation-genre-unknown`) -- la decision de merge reste au coordinateur.

[jsboige]

[REPAIR] Liens relatifs cassés par le mouvement — réparé en 2d0ec03d

Trois gardes étaient rouges sur la tête précédente (check-nav-chain, No enrich-quality regression, PR gate), et ils avaient la même cause unique : l'organe canonique
rename_notebooks.py réécrit le basename d'un lien relatif mais jamais son préfixe de
répertoire. Après le déplacement vers Search/Discrepancy/, ../../Search/Part1-Foundations/<nom>
pointait encore l'ancien dossier.

Le garde n'en avait vu qu'un. La lecture de l'organe check_notebook_navlinks.py en a trouvé
six — dont trois que la CI n'avait pas signalés, parce qu'ils vivent dans le notebook déplacé
lui-même (ses liens vers Search-09c, qui était son voisin de dossier avant le mouvement). C'est la
raison pour laquelle j'ai mesuré la classe entière plutôt que de réparer le seul finding signalé.

Réparé sous garde structurelle I1/I2/I3 : liens markdown, titre H1 et fil d'Ariane seulement —
aucune cellule de code, aucune sortie, aucun execution_count modifié.

navlinks  : OK: 0 NEW broken navlink vs baseline (1472 notebooks scannes)
nav-chain : OK: 0 NEW finding vs baseline -- 6 findings resolus depuis le baseline
perimeter : VERDICT: OK

Le Lean-07b markdown (cellule 28) est réparé ici. Son résidu restant est la cellule de code
30 et ses sorties, refusées en fail-closed par l'organe (I2/I3) : ce résidu exige une ré-exécution
C.2, il reste déclaré au body.

Le défaut de l'organe est un sujet séparé — il devrait refuser un lien relatif dont la cible
change de répertoire, au lieu de produire un 404 silencieux : issue dédiée.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2027:CoursIA-2
pr: 19151
head: 2d0ec03
complete: true
body: read
comments-reviewed: 8
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: de886d7f5e0b3fb897550745f9e33bef12e1b10102ebfb9830eeff1dcd70be12
diff-files: 10
diff-additions: 14
diff-deletions: 13
checks: BLOCKED
b0: clear
scope: pass
domain: not-applicable
verdict: BLOCKED
[/ADJOINT PREFLIGHT]

Motif BLOCKED -- un rouge propre a la PR, reparable par la lane :

• Audit README -> .ipynb links : failure @21:24:01Z. Cause lue au log du job : STALE_LINK NOUVELLES sur cette PR: 1 (base ddac1e1 : 1752 ; tete : 1752 ; 1 nouvelle) :
  MyIA.AI.Notebooks/Search/Part1-Foundations/README.md -> ../Discrepancy/Discrepancy-02-Komlos-Lean.ipynb
  Le renommage 09d -> Discrepancy-02-Komlos-Lean a laisse ce lien README pointant une cible perimee. La reparation de la lane @21:16Z (2d0ec03d) a traite check-nav-chain et No enrich-quality regression mais pas cette jambe README -- c'est la meme cause (mouvement de fichier) sur une troisieme surface. Geste : corriger le chemin du lien dans Search/Part1-Foundations/README.md, puis re-executer la garde.
• PR gate en cascade sur ce meme rouge.
• B.0 rc=0. Perimetre conforme : 10 fichiers, +14/-13 -- descente de 09d dans Discrepancy/ (Search(#5081): lecture de gradation de la serie — escalier, lettres greffees ICT, dette zero-pad et sous-series candidates #17802), volume de renommage + referents.

— dossier myia-po-2027:CoursIA-2, dispatch ai-01 dossiers tiers (04/10 23:17Z).

[github-actions]

Notebook PR Validation: PASS

• Notebooks checked: 2
• Code cells validated: 23
• 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 #19151 (refactor(search,#17802): descente de 09d dans Discrepancy/ -- Discrepancy-02-Komlos-Lean) 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 -- feat(lean,#18430): LeanDojo-v2 volet A -- install mesurée WSL + smoke 6/6 + carnet compagnon Lean-10b (DynamicDatabase + Pantograph) #19057 partage : _quarto.yml
• faible -- feat(lean,#17845): brique k1.5 -- Claim 3.2 (Delta(T_v P, (u,0)) <= Delta(P,u)) #19063 partage : MyIA.AI.Notebooks/Search/discrepancy_lean/FORMAL_STATUS.md
• faible -- feat(lean,#17845): brique k1.6 -- bit de scission (splitBit_eq) #19065 partage : MyIA.AI.Notebooks/Search/discrepancy_lean/FORMAL_STATUS.md
• faible -- feat(lean,#17845): brique k1.7 -- contention de support (correctif d'hypothese des briques k1) #19066 partage : MyIA.AI.Notebooks/Search/discrepancy_lean/FORMAL_STATUS.md
• faible -- feat(lean,#17845): brique k2.0 -- moments de la scission (mean_split) #19068 partage : MyIA.AI.Notebooks/Search/discrepancy_lean/FORMAL_STATUS.md
• faible -- feat(lean,#17845): brique k2.1 -- algebre du pas de pullback (sans convexite) #19070 partage : MyIA.AI.Notebooks/Search/discrepancy_lean/FORMAL_STATUS.md
• faible -- feat(qc,#18958): port du livre 06/02 -- preprocessing de facteurs et regimes (QC-Py-28c) #19071 partage : _quarto.yml
• faible -- feat(lean,#17845): brique k2.2 — surface de convexité (add_smul_mem_convexHull + sum_smul) #19078 partage : MyIA.AI.Notebooks/Search/discrepancy_lean/FORMAL_STATUS.md
• faible -- feat(lean,#17845): brique k2.3 -- transport de dimension (toReal + push + ponts barycentre/appartenance) #19081 partage : MyIA.AI.Notebooks/Search/discrepancy_lean/FORMAL_STATUS.md
• faible -- feat(lean,#17845): brique k2.4 -- pas complet de pullback (toRealProd + caracterisations de support + pullback) #19084 partage : MyIA.AI.Notebooks/Search/discrepancy_lean/FORMAL_STATUS.md
• faible -- feat(lean,#17845): brique k2.5 — cas de base mean_mem_convexHull (Distribution + jumeau _en) #19087 partage : MyIA.AI.Notebooks/Search/discrepancy_lean/FORMAL_STATUS.md
• faible -- feat(lean,#17845): brique k2.6a -- pont de niveau liftUp/pushUp (embedding produit vers Fin (d+1)) #19089 partage : MyIA.AI.Notebooks/Search/discrepancy_lean/FORMAL_STATUS.md
• faible -- fix(search,#12204): op 3 « Quotienter/Fibrer » loge dans Search-03b -- retire la lettre 03g (plafond §4) #19109 partage : MyIA.AI.Notebooks/Search/Part1-Foundations/README.md
• faible -- fix(search,#12204): op 5 « recoller » loge dans Search-03f -- retire la lettre 03h (plafond §4) #19112 partage : MyIA.AI.Notebooks/Search/Part1-Foundations/README.md
• faible -- Rename(#1650): Serre100 08 suffixe -Lean — audit de suffixe Serre100+Langlands #19128 partage : _quarto.yml
• fort -- rename(#16231): Tweety etape 1 -- suffixe de noyau (11 notebooks) + referents (47 fichiers) #19150 partage : _quarto.yml, docs/curriculum/aima-walk.md, docs/reference/rename-ledger.tsv, scripts/tests/baseline_nb_nav_chain.json (issues communes : Remise d'aplomb de la nomenclature des notebooks — suffixe noyau, sans-numero, profondeur d'accretion #16231)
• fort -- rename(#16231): ICT-45 -> ICT-42b -- accrétion de la famille InoculationBifurcation (chantier C) #19153 partage : _quarto.yml, docs/reference/rename-ledger.tsv (issues communes : Remise d'aplomb de la nomenclature des notebooks — suffixe noyau, sans-numero, profondeur d'accretion #16231)
• faible -- feat(translation,#1650): FT-02 QLoRA EN - couverture complete + rendu _en #19175 partage : scripts/tests/baseline_nb_nav_chain.json
• fort -- feat(search,#19189): partie 5 Frontieres -- 10 carnets d'audits sortent de Applications/Research #19189 partage : MyIA.AI.Notebooks/Search/README.md, _quarto.yml, docs/curriculum/ia-classique.md, docs/reference/rename-ledger.tsv, scripts/tests/baseline_nb_nav_chain.json (issues communes : Search(#5081): lecture de gradation de la serie — escalier, lettres greffees ICT, dette zero-pad et sous-series candidates #17802)

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-ai-01:CoursIA
pr: 19151
head: e99077f
complete: true
body: read
comments-reviewed: 11
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 041b3c65f1033aa7771ed48d6b284672af04f6d6b1239f6edcb78338463945df
diff-files: 12
diff-additions: 47
diff-deletions: 25
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 19151
organ-rc: 0
[/ADJOINT PREFLIGHT]

Note ai-01 (refactor Search, lecture firsthand) :

• Tête e99077f2ec : un merge de main dans la branche, sur lequel la CI s'est entièrement rejouée en vert. Le dossier BLOCKED précédent (tête 2d0ec03d) portait sur un lien périmé dans Part1-Foundations/README.md. Ce motif est réparé à cette tête : Audit README -> .ipynb links et readme-ipynb-links-guard sont verts.
• Carnet déplacé (Discrepancy/Discrepancy-02-Komlos-Lean.ipynb) : 39 cellules des deux côtés. Seules les cellules markdown 0 et 38 changent (titre, fil d'Ariane, deux liens relatifs). Aucune cellule code, sortie ou execution_count n'est modifiée. C'est la classe « markdown seul » de C.2. Les 3 carnets touchés ont 0 execution_count nul, 0 erreur, 0 motif interdit.
• Résidus de l'ancien nom (git grep Search-09d à la tête) : catalogue généré (jamais régénéré sur branche), note historique de LEAN_INVENTORY.md, cellule de Lean-07b (résidu déclaré, avec son motif), l'entrée du rename-ledger, et la section datée du README Search (déclarée). Un artefact daté arxiv_rescan_2026-09-03.json porte l'ancien chemin : c'est une mesure figée, à ne pas réécrire.
• Le seul rouge, PR gate (DWELL), a été rejoué après le plancher.