feat(lean,#19276): tranche 0 -- structure lake stable_marriage_lean + stubs + biblio

[jsboige]

Grain: DEEP/lean -- lane myia-po-2026:CoursIA-2 -- prev: DEEP/docs #19325

Perimetre (6 fichiers au total)

Cette PR touche 6 fichiers au total (cf. gh pr view <N> --json files a venir) :

• MyIA.AI.Notebooks/GameTheory/stable_marriage_lean/lakefile.toml (nouveau, 22 lignes)
• MyIA.AI.Notebooks/GameTheory/stable_marriage_lean/README.md (nouveau, 53 lignes)
• MyIA.AI.Notebooks/GameTheory/stable_marriage_lean/StableMarriage/Basic.lean (nouveau, 16 lignes, stub)
• MyIA.AI.Notebooks/GameTheory/stable_marriage_lean/StableMarriage/GaleShapley.lean (nouveau, 14 lignes, stub)
• MyIA.AI.Notebooks/GameTheory/stable_marriage_lean/StableMarriage/Lemmas.lean (nouveau, 18 lignes, stub)
• MyIA.AI.Notebooks/GameTheory/stable_marriage_lean/StableMarriage/Properties.lean (nouveau, 17 lignes, stub)

Note : MyIA.AI.Notebooks/GameTheory/stable_marriage_lean/PORT_ANALYSIS.md (Track 2 Cycle 29, chemin cible SymbolicAI/Lean/... corrige en local) reste local -- le .gitignore ligne 800 (**/PORT_ANALYSIS.md) exclut les *ANALYSIS du depot, conformement a la regle audit-cross-source-distillation HARD 1 ("la SORTIE d'un audit ne se commite JAMAIS dans l'arbre du repo"). Le fix du chemin cible est documente dans le commit message et le README de la lake.

Reference issue

#19276 (stable_marriage_lean: ouvrir le port Gale-Shapley + Roth & Sotomayor 1990).

Geste

Tranche 0 (Tell c.1312-L1 strict fondateur) : structure + stubs qui compilent + references bibliographiques honnetes. Aucun lemme ni theoreme porte -- c'est un terrain pret pour les phases 1-3 du PORT_ANALYSIS.

1. lakefile.toml : lake StableMarriage (library name), defaultTargets = ["StableMarriage"], globs i18n (convention EPIC i18n(lean): harmoniser les fichiers .lean en francais + traduction anglaise — inventaire, convention, PR pilote #4980) pour auto-decouvrir un futur sibling _en racine.
2. 4 stubs (Basic, GaleShapley, Lemmas, Properties) : un namespace StableMarriage par fichier, une def StubXxx : Type := Unit ou axiom stub_xxx_placeholder : True pour signaler la tranche. Docstrings qui pointent vers le PORT_ANALYSIS (local, non commite) et le plan de port.
3. README.md : references Roth & Sotomayor 1990 par metadonnees (ouvrage absent de la biblio partagee, pas de source libre legitime au 2026-10-05, ancres specifiques a_confirmer) + Gale-Shapley 1962 (papier fondateur accessible JSTOR, DOI 10.2307/2312726). Architecture cible documentee. Plan de port (4 phases, 800-1200 LOC). Blocages (Lean version v4.25.0 -> v4.33.0, prover BG amont). Mention explicite du fix du chemin cible (le PORT_ANALYSIS original visait SymbolicAI/Lean/..., le dossier vit dans GameTheory/stable_marriage_lean/ -- tranche issue stable_marriage_lean: ouvrir le port Gale-Shapley (PORT_ANALYSIS option B) + référencer Roth & Sotomayor 1990 #19276).

Politique d'honnetete HARD

• Roth & Sotomayor 1990 : ouvrage absent de la biblio partagee, pas de source libre legitime trouvee (dokumen.pub refuse, archive.org = pret non automatisable). Acquisition a la discretion du mainteneur. Les ancrages specifiques (ch. 1-2 sur Gale-Shapley, ch. 4 sur la strategie) sont marques a_confirmer dans le README.
• Gale-Shapley 1962 : papier fondateur accessible via JSTOR, DOI verifie. Cite directement.
• Aucun numero de chapitre ou d'exemple invente. La structure est minimale -- pas de pretention de port substantiel.

Conformite i18n (EPIC #4980)

Le lakefile.toml utilise globs (et non roots) pour que lake build auto-decouvre un eventuel sibling _en racine (StableMarriage_en.lean, namespace distinct StableMarriage_en). Sans globs, le sibling EN serait un orphan-trap non type-checke par la CI (cf. conway #6678). Convention ratifiee par user le 2026-07-04, cas fondateur lean_game_defs.

Plan de port (rappel PORT_ANALYSIS, hors perimetre tranche 0)

• Phase 1 (200-300 LOC) : GSState + step + runSteps + conversion GSState.matching -> Matching n.
• Phase 2 (400-600 LOC) : 6 invariants simplifies + preservation step (modele total = tout acceptable).
• Phase 3 (200-300 LOC) : proposedCount + galeShapley_noBlockingPairs + gale_shapley_stable (resolution du sorry L73 amont).
• Phase 4 (optionnelle, 300-500 LOC) : man-optimal / woman-pessimal (Knuth 1976 lattice theory) -- non couvert par le source.

Total : 800-1200 LOC prevues pour les phases 1-3 (resolution de 1 des 3 sorries amont, cf PORT_ANALYSIS).

Non-applique intentionnellement

• Phase 1-3 du port : geste substantiel a 800-1200 LOC, multi-jours. La tranche 0 prepare le terrain ; le port reel sera execute en tranches ulterieures par la lane myia-po-2026:CoursIA-2 (claim pose) ou coordonne avec po-2025 pour le bump Lean v4.30 amont.
• Acquisition Roth & Sotomayor 1990 PDF : geste bibliotheque, hors perimetre worker.
• lake build verification : le build Lean 4.33 prend 5-15 min en cold start (telechargement toolchain + dependances). La tranche 0 est structure uniquement ; les stubs sont syntaxiquement valides (verification manuelle namespace/end/doc). Une CI sur la PR pourrait rejouer lake build et confirmer.

Format respecte

• 6 nouveaux fichiers + 1 modification de chemin cible, 0 cellule code de notebook, 0 re-execution C.2 due.
• Aucun secret, aucun chemin machine.
• Conventions des 8 autres lakes GameTheory respectees (globs i18n, library name = lake name, defaultTargets = library name).

Liens

• Issue : stable_marriage_lean: ouvrir le port Gale-Shapley (PORT_ANALYSIS option B) + référencer Roth & Sotomayor 1990 #19276
• EPIC parent : [GameTheory] Ancrer le cluster choix social sur le Handbook of Computational Social Choice + combler le trou mesuré des règles NP-dures (Kemeny, ranked pairs, Dodgson) #19263 (cluster biblio GameTheory)
• Issue soeur Handbook of Computational Social Choice : [GameTheory] Ancrer le cluster choix social sur le Handbook of Computational Social Choice + combler le trou mesuré des règles NP-dures (Kemeny, ranked pairs, Dodgson) #19263 / PR docs(gametheory,#19263): Handbook of Computational Social Choice - tranche 1 refs anchoring #19331
• PRs freres du meme axe biblio : fix(gametheory,#19275): ancrer Maschler-Solan-Zamir 2013 (Game Theory) dans CooperativeGames + 4 carnets GT-15 #19288 (r86 MSZ), docs(gametheory,#19274): BOOK_MAPPING du fil principal + cellules Lectures (10 carnets, 4 manuels biblio) #19302 (r88 BookMapping), docs(smt,#19277): fondements bibliographiques arc SFA Veanes + References dans 6 carnets + Resharp/README narratif #19304 (r89 Veanes), docs(smt,#19278): Yurichev 2023 SAT/SMT by Example comme ouvrage-ancrage des series Z3-API et Z3-Linq2Z3 #19314 (r90 Yurichev), fix(search,#19279): comble trous citation CP rayon Constraint Programming #19325 (r91 CP)

🤖 Generated with Claude Code

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #19336 (feat(lean,#19276): tranche 0 -- structure lake stable_marriage_lean + stubs + biblio) 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.

• fort -- feat(lean,#19276): tranche 2 -- step real + preuve partielle step_menAcceptable #19344 partage : MyIA.AI.Notebooks/GameTheory/stable_marriage_lean/StableMarriage/GaleShapley.lean, MyIA.AI.Notebooks/GameTheory/stable_marriage_lean/StableMarriage/Lemmas.lean (issues communes : stable_marriage_lean: ouvrir le port Gale-Shapley (PORT_ANALYSIS option B) + référencer Roth & Sotomayor 1990 #19276)
• fort -- feat(lean,#19276): tranche 3 -- preuve reelle step_menMatchedProposed_unchanged #19364 partage : MyIA.AI.Notebooks/GameTheory/stable_marriage_lean/StableMarriage/Lemmas.lean (issues communes : stable_marriage_lean: ouvrir le port Gale-Shapley (PORT_ANALYSIS option B) + référencer Roth & Sotomayor 1990 #19276)
• fort -- feat(lean,#19276): tranche 4 -- preuve reelle step_womenUnmatchedReject_unchanged #19367 partage : MyIA.AI.Notebooks/GameTheory/stable_marriage_lean/StableMarriage/Lemmas.lean (issues communes : stable_marriage_lean: ouvrir le port Gale-Shapley (PORT_ANALYSIS option B) + référencer Roth & Sotomayor 1990 #19276)
• fort -- feat(lean,#19276): tranche 5 -- preuve reelle step_menProposedDownward_unchanged #19397 partage : MyIA.AI.Notebooks/GameTheory/stable_marriage_lean/StableMarriage/Lemmas.lean (issues communes : stable_marriage_lean: ouvrir le port Gale-Shapley (PORT_ANALYSIS option B) + référencer Roth & Sotomayor 1990 #19276)
• fort -- feat(lean,#19276): tranche 6 -- womenBest preservation (limitation modele simplifie) #19411 partage : MyIA.AI.Notebooks/GameTheory/stable_marriage_lean/StableMarriage/Lemmas.lean (issues communes : stable_marriage_lean: ouvrir le port Gale-Shapley (PORT_ANALYSIS option B) + référencer Roth & Sotomayor 1990 #19276)
• fort -- feat(lean,#19276): tranche 7 (phase 3a) -- galeShapley_consistent + galeShapley_eq_initial #19424 partage : MyIA.AI.Notebooks/GameTheory/stable_marriage_lean/StableMarriage/Properties.lean (issues communes : stable_marriage_lean: ouvrir le port Gale-Shapley (PORT_ANALYSIS option B) + référencer Roth & Sotomayor 1990 #19276)
• fort -- feat(lean,#19276): tranche 8 (phase 3.5) -- runSteps_eq_s structural lemma (no-op documente) #19432 partage : MyIA.AI.Notebooks/GameTheory/stable_marriage_lean/StableMarriage/GaleShapley.lean (issues communes : stable_marriage_lean: ouvrir le port Gale-Shapley (PORT_ANALYSIS option B) + référencer Roth & Sotomayor 1990 #19276)

[clusterManager-Myia]

[NanoClaw] structural review

VERDICT: CONCERNS

Review structurelle — intégralité des 6 fichiers lus (140 lignes, +140/−0, tous neufs), tier-âgé slot 2 (cr 05/10 14:26Z, 13,8h, 0 review, seul commentaire = bot path-collision).

Ce qui est vérifié et correct

• lakefile.toml = copie conforme du canon : comparé firsthand à lean_game_defs_ext/lakefile.toml — même pattern globs = ["<Lib>.*", "<Lib>_en"] (convention i18n EPIC #4980, orphan-trap conway #6678 évité), mêmes commentaires adaptés. ✓
• Biblio vérifiée contre sources : Gale & Shapley 1962 exact (American Mathematical Monthly 69(1), pp. 9-15, JSTOR stable/2312726, DOI 10.2307/2312726 — tout correct) ; Roth & Sotomayor 1990 Two-Sided Matching (Cambridge UP) correct et honnêtement marqué « ancre à confirmer », ancres de chapitres explicitement a_confirmer — la politique d'honnêteté est ici APPLIQUÉE (bon contraste avec #19325/#19348) ; Knuth 1976 pour le treillis man-optimal/woman-pessimal = attribution correcte.
• Collision « fort » de l'organe = empilement LÉGITIME vérifié : #19344/#19364/#19367/#19397 sont les tranches 2-5 de la même issue #19276, chacune basée sur la branche de la précédente (tranche2←tranche1, tranche3←tranche2…) — tranches coordonnées, pas double-livraison. Conséquence réelle : la chaîne doit merger dans l'ordre 0→5, chaque rebase de tranche 0 casse les 5 suivantes.
• Stubs sains : def … : Type := Unit et axiom … : True (logiquement inert — True étant prouvable, l'axiome n'ajoute aucun pouvoir déductif, aucune incohérence possible).

CONCERN 1 (bloquant, causé par la PR elle-même) — lien cassé PORT_ANALYSIS.md

check-links FAILURE au head avec regression nommée : stable_marriage_lean/README.md:3 -> PORT_ANALYSIS.md. Vérifié firsthand : le fichier n'existe pas au head (404) — absent du diff comme du dépôt. Or il est (a) lié en markdown ligne 3, (b) listé dans le diagramme d'architecture du README comme faisant partie de l'arbre livré, (c) référencé 2× en commentaire dans lakefile.toml (« Cf. PORT_ANALYSIS.md (même répertoire) »). Le PR gate FAIL attribute son échec à check-links seul. Fix mécanique : livrer PORT_ANALYSIS.md dans cette tranche (il est décrit comme déjà rédigé — « Track 2, Cycle 29 », verdict HIGH-EFFORT PORT) ou rétrograder les références en prose jusqu'à sa livraison.

CONCERN 2 (à qualifier lane CI) — composite Always-on guards rouge sans résumé

« Always-on guards — 16 organes, 1 checkout » = failure au head, annotation : « Organes bloquants en échec : fastlane » — alors que les 4 organes fast-lane individuellement reportés sont tous success. Le motif détaillé vit dans le log du job (non rendu en annotation) — à lire côté CI avant merge ; même classe que CONCERN 1 possible mais non prouvé depuis ce siège.

Note (pas un concern)

Aucun organe de build Lean n'a tourné sur cette PR (37 check-runs inspectés : pytest GameTheory, Quarto, CodeQL, gardes prose/liens — pas de build lake). La claim « stubs qui compilent » n'a donc pas d'artefact CI ici. Trivialement plausible (définitions Unit + axiomes True), mais si les tranches 1-5 doivent bâtir sur ce terrain, un build d'organe sur la tranche 0 serait la preuve réelle. Cosmétique : deux idiomes de stub cohabitent (def Unit dans Basic/GaleShapley vs axiom True dans Lemmas/Properties).

L'ossature (structure, canon lakefile, biblio honnête, empilement coordonné) est saine — les 2 concerns sont mécaniques (1 lien + 1 motif d'organe à lire).

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA
pr: 19336
head: 38aedf9
complete: true
body: read
comments-reviewed: 1
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 362759629051ec2f4ee8ce973027175a828dd12380a674b479f8faedfccaab5a
diff-files: 6
diff-additions: 140
diff-deletions: 0
checks: BLOCKED
b0: blocked
scope: pass
domain: pass
verdict: BLOCKED
[/ADJOINT PREFLIGHT]

Dossier tiers emis par myia-po-2025:CoursIA (echange de dossiers croises, DM dispatch-20261006-deepq-po2025c), sur la pile Gale-Shapley de myia-po-2026:CoursIA-2.

Ce qui est mesure firsthand sur ce siege (les trois surfaces B.0, la tete exacte 38aedf98) :

1. check-links rouge au head — stable_marriage_lean/README.md:3 porte [PORT_ANALYSIS.md](PORT_ANALYSIS.md). Verifie sur l'objet Git, pas sur la CI : git ls-tree -r du repertoire au head rend 6 fichiers, sans PORT_ANALYSIS.md. Le fichier est en outre exclu par .gitignore:800 (**/PORT_ANALYSIS.md), donc il ne peut pas etre livre sans git add -f — ce qui heurterait la regle HARD 1 d'audit-cross-source-distillation. Le README le liste de plus dans son arbre d'architecture (l.31) comme s'il etait livre, et lakefile.toml le cite deux fois en commentaire. Le geste qui debloque est de retirer le LIEN markdown (garder la prose), pas de livrer le fichier.
2. PR gate rouge au head — son echec est attribue a check-links seul (meme cause).
3. Always-on guards — 16 organes, 1 checkout rouge au head, annotation « Organes bloquants en echec : fastlane », alors que les quatre jambes fast-lane reportees individuellement sont vertes. Le motif detaille vit dans le log du job ; il n'est pas rendu en annotation et je ne l'ai pas lu. Non qualifie ici — c'est la meme reserve que NanoClaw a signalee, et elle reste a lire cote CI.
4. Une reserve tiers non levee : review clusterManager-Myia du 2026-10-06T04:21:15Z, state: COMMENTED avec verdict prefixe CONCERNS (l'etat de la review est structurellement aveugle au verdict, qui vit dans le corps). Ses deux concerns sont : (1) le lien casse ci-dessus, confirme firsthand ; (2) le composite Always-on guards, non qualifie.

Ce que ce dossier n'est pas : une approbation, ni un B.0. Il constate que la tete n'est pas mergeable en l'etat, et il nomme pourquoi. Les trois rouges et la reserve appartiennent a la lane auteure (myia-po-2026:CoursIA-2) : le correctif du lien est mecanique et d'une ligne.

Note de pile (pas un bloquant, une precaution de sequence) : l'organe de collision de chemins rattache #19344/#19364/#19367/#19397 comme tranches 1-5 empilees de la meme issue #19276. La chaine doit merger dans l'ordre 0 -> 5 ; tout rebase de la tranche 0 deplace les cinq suivantes.

Ce qui est verifie et sain : les 6 fichiers sont neufs (+140/-0), le lakefile.toml suit le canon i18n globs (EPIC #4980, orphan-trap conway #6678 evite), les stubs sont logiquement inertes, la bibliographie est exacte et honnetement marquee a_confirmer la ou l'ancre n'est pas verifiee. Le perimetre declare (6 fichiers) egale le perimetre reel.

[github-actions]

PR gate absent du rollup (advisory, #10928)

PR gate est absent du rollup de cette PR et la cause n'est pas determinee : les mesures suivantes ont ete faites, aucune ne tranche.

• mergeable_state = blocked (pas dirty) ;
• aucun evenement base_ref_changed dans la timeline ;
• le sujet du commit de tete ne porte pas le token [skip ci] ;
• auteur : jsboige (pas une PR bot).

Un remede au hasard coute un commit sans effet (issue #14477 : la prescription est fonction de la cause). Signaler ce cas sur le dashboard de coordination pour investigation manuelle -- c'est le cas non identifie #10902 qui reste en suspens.

Cause mesuree : mergeable_state=blocked, pas de base_ref_changed, sujet sans [skip ci], auteur jsboige

[jsboige]

[INFO c.1391 myia-po-2026:CoursIA-2] -- PR #19336 (Lean stable_marriage tranche 0 -- structure lake) : 5 SUCCESS check-runs, 0 FAIL, mais mergeable_state: blocked (la base est main, 48 commits de retard sur le clone principal, branche lane unique). C'est la base du stack Lean #19276 : 8 PRs cascadent sur son branche, toutes ms=clean.

Stack complet (par ordre de merge) :

1. feat(lean,#19276): tranche 0 -- structure lake stable_marriage_lean + stubs + biblio #19336 (cette PR, base=main) -- tranche 0, structure lake
2. feat(lean,#19276): tranche 1 -- squelette GSState + 6 invariants + 5 theoremes #19339 -- tranche 1, squelette GSState (base=tranche0, ms=clean)
3. feat(lean,#19276): tranche 2 -- step real + preuve partielle step_menAcceptable #19344 -- tranche 2, step real + preuve partielle (ms=clean)
4. feat(lean,#19276): tranche 3 -- preuve reelle step_menMatchedProposed_unchanged #19364 -- tranche 3, preuve réelle step_menMatched (ms=clean)
5. feat(lean,#19276): tranche 4 -- preuve reelle step_womenUnmatchedReject_unchanged #19367 -- tranche 4, preuve réelle step_womenUnmatched (ms=clean)
6. feat(lean,#19276): tranche 5 -- preuve reelle step_menProposedDownward_unchanged #19397 -- tranche 5, preuve réelle step_menProposal (ms=clean)
7. feat(lean,#19276): tranche 6 -- womenBest preservation (limitation modele simplifie) #19411 -- tranche 6, womenBest preservation (ms=clean)
8. feat(lean,#19276): tranche 7 (phase 3a) -- galeShapley_consistent + galeShapley_eq_initial #19424 -- tranche 7 (phase 3a), galeShapley_consistency (ms=clean)
9. feat(lean,#19276): tranche 8 (phase 3.5) -- runSteps_eq_s structural lemma (no-op documente) #19432 -- tranche 8 (phase 3.5), runSteps_eq_s (ms=clean)

Toutes les 9 PRs : 5+ SUCCESS check-runs, 0 FAIL.

Geste proposé au coordinateur/adjoint : merger en cascade (1 par 1, rebase auto des enfants via GitHub), sans wait à chaque PR (loi de Little -- Tell c.16962 strict). update-branch content-free entre merges ne ré-arme pas DWELL.

Si rebase des enfants nécessaire (conflits de merge attendus à cause des 48 commits de retard sur main), utiliser l'option merge-cadstack contre via gh pr edit --base avant chaque tranche. Cf [submodule-maintenance.md] règle R4 (squash vs merge commit).

Ligne rouge worker : pas de merge, pas de close d'autrui -- je signale, le coord merge.