docs(lean,#15892): exposer le chemin de découverte prover de StableMarriage (sans changement mathématique)

[jsboige]

Grain: MED/notebook-lean — lane myia-po-2024:CoursIA — prev: DEEP/genai #15872

Sujet

Cas d'exposition de l'EPIC #13105 (Axe A) : le chemin de découverte du prover pour StableMarriage, conservé depuis les traces réelles — sans changer une ligne de preuve. Sous-grain #15892 (ouvert ce cycle, groundé firsthand).

Livrable

1. Section README « Chemin de découverte (traces prover) » (game_theory_lean/README.md, dans la section StableMarriage) :
   • le verdict INTRACTABLE_UNTIL_GS_IMPL sur gale_shapley_stable / _man_optimal / _woman_pessimal (stagnations reproductibles 138 s / 83 s, condition déblocante nommée = port GS ~1000 lignes, livré par [Cycle 29 / Track 2] mmaaz-git stable-marriage-lean port (GS algorithm) #997) ;
   • le résiduel gsChooseMax_maximal (partial_progress : objectif résiduel + closure_hint = trichotomie) et le piège Finset.exists_maximal (maximalité conditionnelle seulement).
2. Docstrings FR + siblings EN : gsChooseMax (nouvelle), gsChooseMax_maximal (l'ancienne était inexacte — « directement depuis la maximalité » — remplacée par le schéma de fermeture réel), gale_shapley_stable (complétée du chemin prover).
3. Table README : comptes de lignes réconciliés (GSState 168/177 → 178/187, GaleShapley 181/171 → 191/184 — la table était déjà stale sur ces deux lignes).

Preuves

• Byte-identity preuves/signatures : les 3 seules lignes supprimées du diff sont les 2 anciennes docstrings de gsChooseMax_maximal (FR + EN) ; toutes les additions sont des lignes de docstring. Diff inspecté ligne à ligne.
• Sorry : python scripts/lean/count_code_sorry.py --json → game_theory_lean distinct_code_sorry 1 avant / 1 après (naive 35/35, code 2/2) — inchangé.
• i18n siblings : python scripts/lean/check_i18n_siblings.py MyIA.AI.Notebooks/GameTheory/game_theory_lean → 22/23 byte-identical | 1 consumer-pattern | 0 drift | 0 orphan.
• Lake build + proof-integrity : portés par la CI (lean-game-theory.yml → lean-axiom) ; diff docstring-only, attendus identiques à main — checks visibles sur la PR.
• Traçabilité des faits : chaque fait de la section découverte est cité depuis un artefact tracé — agent_tests/prover/session_state/lessons_learned.json (stable_marriage.partial_progress[0], .failure_patterns : c'est la trace elle-même qui nomme [Cycle 29 / Track 2] mmaaz-git stable-marriage-lean port (GS algorithm) #997 comme condition déblocante), proof_knowledge.json (failed_approaches, proved_theorems_inventory). Les traces ne couvrent PAS le module Lattice (0 hit mesuré) — dit explicitement dans le README, aucune attribution fabriquée.

Frontières #13105 respectées

Pas d'ingestion Palomar, pas de rapport d'audit committé (la sortie est de la prose pédagogique dans le README existant), pas de rollout sur les autres lakes — un cas, pas un genre.

See #15892 (sous-grain), #13105 (EPIC)

🤖 Generated with Claude Code

[jsboige]

PR gate rouge sur cette PR : c'est un DWELL, pas un defaut. Rien a reparer.

Le verdict est dans l'annotation du check-run PR gate (son output.title / output.summary sont nuls — l'interroger fait conclure a tort « organe illisible »). Recopie tel quel, check-run 103660046654 sur la tete b29047ab600d :

[pr-gate] DWELL -- tete du 2026-09-13T02:32:00Z, 8 min -- plancher 120 min,
reste 112 min, leve au premier balayage suivant 2026-09-13T04:32:00Z.
Le balayage horaire (pr-gate-stale-sweep.yml, cron '7 * * * *') re-agrege
cette jambe des que le plancher est ecoule ; aucun geste manuel n'est requis.

Tous les autres checks sont verts — 30 check-runs sur cette tete, PR gate est le seul non-vert. Zero rouge de substance : c'est le plancher anti-flapping de 120 min qui, seul, tient le gate au rouge.

Aucun geste de ma part, et c'est delibere :

• gh pr update-branch remet le plancher a zero — un nouveau head repart pour 120 min au lieu de les ecourter (mesure du 2026-09-11 sur test(#14730): consolidate 3rd live duplicated test pair - legacy extract_titles into canons #15543 : head 27 min apres l'update-branch, 93 min restantes) ;
• un rerun avant l'echeance ne produirait qu'un DWELL identique, et pire, poserait un verdict neuf que le sweep lit comme immature (il mesure l'age du verdict, pas du head) ;
• le dernier passage du sweep est de 03:08:16Z, soit avant l'echeance de 04:32:00Z : son « aucun geste manuel » etait donc litteralement vrai, pas un defaut d'organe.

Echeance de ce plancher : 2026-09-13T04:32:00Z. La PR est mergeable des que la jambe est re-agregee.

Justification ecrite au titre du --ignore-red du picker (le DWELL declenche a lui seul son P0 « reparer ses propres PRs », qui compte PR gate comme check requis en echec sans lire le verdict).

Mesure faite au 2026-09-13T04:01Z.