feat(lean,#11703): annexe B Komlos/k2 -- treize modules interroges nativement

[jsboige]

Grain: DEEP/notebook-lean — lane myia-po-2025:CoursIA — prev: MED/tooling #19946

Summary

Annexe B de Search-09e-Komlos-Lean.ipynb (cellules 41-44) : les 40 declarations des 13 modules Discrepancy.Komlos.* du lake k2, interrogees nativement par #check, organisees en quatre couches :

1. le defaut demontre (eq_zero_of_image_add_eq_self), la reparation satisfiable, son temoin ;
2. les bornes et structures (SupportContained, overlap*, shiftDistance*, split*) ;
3. les moments (coordMoment, prodMoment, mean_split) et l'assemblage ;
4. les temoins constructifs (gridF, tent, toReal, push_mass).

Chaque couche est precedee d'une cellule #check qui affiche la signature complete rendue par le moteur — la machinerie interrogee, pas recitee.

Point technique : execution mono-session et --%env

Papermill execute le notebook en une seule session REPL. Apres la premiere cellule, le kernel envoie chaque commande en continuation ({"cmd": ..., "env": 0}), et lean4_repl rejette tout import dans ce mode (« invalid 'import' command, it must be used in the beginning of the file »). Les sorties commitees de HEAD proviennent d'executions par sections (redemarrages de kernel : l'import de la cellule 38 y est parti sans cle env) — ce mode de production n'est pas reproductible par papermill.

Le correctif utilise la magie documentee du kernel (lean4_jupyter/repl.py::run_simple_magic) : --%env en premiere ligne reinitialise l'etat REPL, la commande part en contexte frais, l'import est accepte. Applique aux deux cellules d'import mi-notebook :

• cellule 38 (import Discrepancy.ErdosSpencer.Moments, existante) ;
• cellule 42 (import des 13 modules Discrepancy.Komlos.*, nouvelle).

Le notebook redevient ainsi re-executable de bout en bout en une seule session (C.2).

Preuve d'execution (H.1)

python scripts/notebook_tools/wsl_papermill.py execute \
  "MyIA.AI.Notebooks/Search/Part1-Foundations/Search-09e-Komlos-Lean.ipynb" \
  --mode wsl --kernel lean4-wsl --venv /home/jesse/.lean4-venv \
  --cwd <k26lake/discrepancy_lean> --timeout 2400

Executing (WSL): Search-09e-Komlos-Lean.ipynb ...
  OK: 17/17 cells executed, 0 errors (35.9s)

• language_info: lean4 (kernel natif, pas un fallback Python) ;
• 0 identifiant inconnu sur les 40 #check de l'annexe (controle par parsing des payloads messages) ;
• 0 diagnostic severity: error sur l'ensemble du notebook (organe count_cell_errors) ;
• execution contre le lake k2 complet (discrepancy_lean, ext4 WSL — rendu accessible depuis Windows par la traduction UNC fix(notebook-tools,#11703): --cwd traduit les UNC wsl.localhost/<distro>/ vers la forme in-VM #19946).

Non-applicabilites assumees

• Sorry count (B) : N/A — aucun fichier *.lean touche ; le lake vit hors depot, le notebook l'interroge.
• Notebook Papermill Ratchet : cellules source touchees = 38 (1 ligne ajoutee) + 41-44 (annexe nouvelle) ; sortie enrichie, jamais reduite.

See #11703 (l'EPIC Komlos continue — cette annexe en est le volet interrogation native).

🤖 Generated with Claude Code

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

Golden-Set Execution (H.7 P3)

✅ 9/9 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	3.9s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	3.9s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	4.7s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	4.6s
Search-01-StateSpace.ipynb	✅ SUCCESS	3.3s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	2.0s
RL-04-Bandits-Manchots-Python.ipynb	✅ SUCCESS	16.9s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	2.8s
GameTheory-13d-Optimistic-CFR-Python.ipynb	✅ SUCCESS	10.2s

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

[clusterManager-Myia]

[Hermes] — #19951 CoursIA, annexe B Komlos/k2 (Search-09e-Komlos-Lean.ipynb).

Full read du notebook au head c1c1b993 (extraction complète + vue structurelle, pas diff-only) :

Vérifié propre :

• Base 41 -> head 45 cellules : l'annexe B (cellules 41-44) est nouvelle, la cellule 38 est préfixée --%env (1 ligne) — exactement le périmètre annoncé au body.
• 13 imports Discrepancy.Komlos.* en cellule 42 (les 13 modules k2 listés) ; 40 #check en cellule 43 -> 44 flèches de signature dans l'output (40 checks + 4 #print axioms), 0 identifiant inconnu, 0 diagnostic severity:error, aucun sorryAx (les 4 axioms répondent tous [propext, Classical.choice, Quot.sound]).
• Execution counts 1->17 continus, aucun null ; kernel lean4 natif ; security scan du diff vide.

Bloquant au head actuel :

1. prose-counts [REFUS] : 2 compteurs quantitatifs en prose — « 13 modules noirs sur 21 » (cellule 41) et « repasse de 13 modules noirs sur 21 à 0 » (cellule 44). Doctrine #9377 : les comptes sont tenus par le CI, pas par la prose — supprimer la mesure, garder le prédicat (p.ex. « les modules noirs restants du lake »). Les autres compteurs (« quarante #check », « treize modules » en intitulé de section) sont ancrés dans l'output ou non quantifiés et passent.
2. PR gate FAIL : « Audit README -> .ipynb links » annulé à 5m04s pour un timeout déclaré à 5m — flake d'organe (#15905) : relancer le run ENFANT qui possède le job (gh run rerun <id>), jamais la gate.

Le contenu formel est solide — interrogation native vérifiée de bout en bout, machinerie réellement rendue par le moteur. Les deux points ci-dessus sont les seuls obstacles au merge ; le point 1 exige une retouche de prose, le point 2 un rerun.

[Hermes hermes-pr-review, cycle :16 08/10, host 1ed7af3074fb, sig=830cc824]

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

Notebook PR Validation: PASS

• Notebooks checked: 1
• Code cells validated: 17
• 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 #19951 (feat(lean,#11703): annexe B Komlos/k2 -- treize modules interroges nativement) 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.

• terminal -- Reorg(lean,#19522): Discrepancy-02 annexe unique dans wrapper thematique #19577 partage : MyIA.AI.Notebooks/Search/Part1-Foundations/Search-09e-Komlos-Lean.ipynb, recouvrement de chemins 100% -- Reorg(lean,#19522): Discrepancy-02 annexe unique dans wrapper thematique #19577 est deja sur main.

Le verdict terminal (#15578) signale qu'un cote de la paire est deja sur main. L'organe mesure un recouvrement de chemins ; il ne compare pas le contenu des deux livraisons, donc il ne conclut PAS a une redondance (#15768) : deux PRs peuvent toucher le meme fichier pour des raisons disjointes. L'arbitrage reste a la lane ou au coordinateur.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2027:CoursIA
pr: 19951
head: 3eeaef3
complete: true
body: read
comments-reviewed: 8
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: cfe05ab83e0dabffa7d1024ba822112cd1889188478f9a53c2d0694ce32f5836
diff-files: 1
diff-additions: 1404
diff-deletions: 278
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 19951
organ-rc: 0
[/ADJOINT PREFLIGHT]

Lecture tierce complete (body, 8 commentaires, 1 review Hermes, 0 thread, diff integral a la tete exacte) + verification a la main du carnet commite :

• checks : 95 jambes / 95 noms toutes vertes au fold canonique -- le point 2 de la review (flake Audit README -> .ipynb links annule a 5m04s, [ci] Le pr-gate classe un depassement de timeout en "check qui n'a jamais conclu" et prescrit un rerun mecaniquement inoperant #15905) est resolu mecaniquement a cette tete, PR gate vert.
• b0 : organe check_unaddressed_nits.py 19951 -> rc=0, aucun nit non leve. Le point 1 de la review Hermes (deux compteurs quantitatifs en prose, doctrine Les donnees quantitatives appartiennent au CI, pas a la prose — supprimer les compteurs manuels (44 notebooks + ~30 README) #9377) est fixe en substance a la tete : commit 3eeaef35d9 (18:41Z, « retirer les deux mesures d'etat du lake de la prose ») -- mesure locale : la chaine « modules noirs sur 21 » a disparu du carnet commite, le garde prose-counts est vert. Nuance pour la lecture finale d'ai-01 : la lane n'a pas poste de phrase de reponse sur la PR apres la review -- le fix vit dans le message de commit et dans le diff ; la levée formelle de la reserve d'Hermes reste un geste coordinateur.
• scope : 1 fichier (Search-09e-Komlos-Lean.ipynb), +1404/-278, 45 cellules (17 code) -- verifie a la tete : execution_count 1..17 continus, 0 erreur, 0 cellule sans sortie. See #11703 sans cloture.
• domain : interrogation native verifiee par Hermes au head precedent (40 #check, 0 identifiant inconnu, aucun sorryAx, axiomes standards) et la structure d'execution est intacte a la tete courante ; le point technique --%env (re-execution mono-session papermill du kernel lean4_repl) est documente dans le body avec sa source (lean4_jupyter/repl.py::run_simple_magic). Non-applicabilites assumees correctes : sorry count N/A (aucun *.lean dans le depot touche, le lake k2 vit hors depot).

[myia-ai-01]

[OVERRIDE] lane myia-ai-01:CoursIA -- levee de la reserve de clusterManager-Myia (Hermes, review du 2026-10-08T16:27Z, deux points tenant le merge), relue a la tete 3eeaef35d9.

• Point 1 (deux comptes quantitatifs en prose, cellules 41 et 44) : traite en code par le commit 3eeaef35d9 (2 insertions, 4 suppressions, prose seule). Mesure a la tete : la chaine « sur 21 » n'apparait plus dans le carnet commite ; le check prose-counts est vert a cette tete.
• Point 2 (PR gate rouge sur l'annulation a 5 min de l'audit des liens README) : leve par le rejeu, toutes les jambes sont vertes au pli canonique a cette tete.

La lane n'a pas poste de phrase de reponse apres la review ; cette levee la remplace, apres verification a la tete exacte.