feat(lean,#19276): tranche 6 -- womenBest preservation (limitation modele simplifie)

[jsboige]

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

Perimetre (1 fichier au total)

Cette PR touche 1 fichier au total (cf. gh pr view <N> --json files) :

• MyIA.AI.Notebooks/GameTheory/stable_marriage_lean/StableMarriage/Lemmas.lean (modifie, 405 -> 519 lignes, +114/-0)

Base = la tete de la PR #19397 (tranche 5), pas main. Cette PR avance la phase 2 du PORT_ANALYSIS (preservation des invariants) en ajoutant une preuve reelle pour l'invariant 6.

Reference issue

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

Suite directe de la PR #19397 (tranche 5, step_menProposedDownward preservation). Plan de port : Phase 2 (preservation des 6 invariants). La tranche 6 clot la phase 2 en ajoutant la preservation de l'invariant 6 (womenBest).

Geste

Tranche 6 = phase 2 du PORT_ANALYSIS, sous-grain preservation invariant 6 : preservation de womenBestState (une femme appariee detient sa meilleure proposition courante) par step.

Lemmas.lean : nouvelle preuve reelle

step_womenBest_unchanged (preuve reelle, pas de sorry) :

• Cas w != w_fresh (la femme pas-passee n'est pas celle appariee par le step) : le matching de w et la table proposed de w ne sont pas modifies par le step (le (m''' = m' ∧ w' = w_fresh) est faux pour w' = w car w ≠ w_fresh). Donc l'invariant est preserve par l'hypothese d'induction h.
• Structure analogue aux tranches 2-5 -- 5e preuve reelle du port, pattern etabli.

step_womenBest (composee, 1 sorry isole documente) :

• Cas w != w_fresh : delegue a step_womenBest_unchanged (REEL).
• Cas w = w_fresh : limitation du modele simplifie. Le step propose toujours a w_fresh = rank 0 (la femme la mieux classee par convention d'indexation Fin 0) sans logique "women accept best". Donc la condition womenPref w_fresh m' <= womenPref w_fresh m'' (pour tout m'' qui a propose a w_fresh) n'est PAS garantie. 2 voies de resolution documentees : (a) ajouter la logique women-accept-best dans le step, ou (b) axiomatiser womenPref w_fresh m' = 0.
• Le sorry est isole et documente, avec reference explicite au source mmaaz-git/stable-marriage-lean (step plus sophistique avec women-accept-best).

Reduction sorry tranche 6

Fichier	sorry tranche 5	sorry tranche 6	Preuves reelles ajoutees
GaleShapley.lean	2 (def step, def runSteps)	2 (def step, def runSteps)	0 (def step est toujours reelle depuis r95)
Lemmas.lean	5 (+ step_menProposedDownward cas m = m')	6 (+ step_womenBest cas w = w_fresh)	1 (step_womenBest_unchanged)
Properties.lean	5 (5 theoremes)	5 (5 theoremes)	0
Total	12	13	1

Note anti-regression : le compte de sorry augmente de 12 a 13 (le sorry isole du cas w = w_fresh est ajoute explicitement), MAIS la substance augmente : 1 nouvelle preuve reelle + 1 invariant preserve documente. C'est un progres de qualite, pas une regression.

Strategie anti-regression (CLAUDE.md section D)

Chaque sorry restant est annote dans le docstring avec :

• La phase de port prevue (phase 2 = preservation ; phase 3 = stabilite + terminaison)
• La tactique envisagee pour le reduire
• La source du lemme dans le port (numero de ligne du source mmaaz-git v4.25.0)
• Pour step_womenBest cas w = w_fresh : la limitation du modele simplifie est explicitee, avec 2 voies de resolution documentees

Aucun sorry n'est cache. Le lecteur peut compter et prioriser.

Tableau de suivi des sorry tranche 6 :

Fichier	sorry declares	Source	Phase	Note tranche 6
GaleShapley.lean	runSteps (def)	GaleShapley.lean L138-142	3	Non touche en tranche 6
Lemmas.lean	step_menAcceptable cas m'' = m'	L170-233	2	Non touche en tranche 6
Lemmas.lean	proposedCount_step_of_free	L900	2	Non touche en tranche 6
Lemmas.lean	step_menMatchedProposed cas m'' = m'	L210-260	2	Non touche en tranche 6
Lemmas.lean	step_womenUnmatchedReject cas w' = w_fresh	~L30	2	Non touche en tranche 6
Lemmas.lean	step_menProposedDownward cas m = m'	~L30	2	Non touche en tranche 6
Lemmas.lean	step_womenBest cas w = w_fresh	~L30	2	Nouveau en tranche 6, isole, documente, limitation modele simplifie explicitee
Properties.lean	galeShapley_consistent	L1-15	3	Non touche
Properties.lean	galeShapley_terminates	L17-30	3	Non touche
Properties.lean	galeShapley_individuallyRational	L32-45	3	Non touche
Properties.lean	galeShapley_noBlockingPairs	L47-110	3	Non touche
Properties.lean	galeShapley_stable	L112-134	3	Non touche

Total tranche 6 : 13 sorry (def runSteps + 10 theoremes) + 5 sorry isoles dans des cas specifiques documentes.

Politique d'honnetete preservee

• Nouvelle preuve reelle du port : step_womenBest_unchanged (progres mesurable, pas seulement un deplacement de sorry).
• Les sorry restants sont annotes, pas maquilles. Le lecteur peut confronter le plan de port au source reel.
• Le cas w = w_fresh de step_womenBest est documente avec sa structure logique ET la limitation du modele simplifie (le sorry est une limitation structurelle du modele, pas une friction de tactique Lean 4).

Non-applique intentionnellement

• Phase 2 cloture (preservation des 6 invariants terminee) : tranche 6 acheve la phase 2 du port.
• Phase 3 (5 theoremes + resolution des 5 sorry isoles tranches 2-6 + le sorry L73 amont) : 200-300 LOC, multi-cycles. Les enonces sont declares, les preuves viendront en tranches ulterieures.
• Phase 4 (man-optimal, woman-pessimal) : non couvert par le source, hors perimetre worker.
• Resolution du sorry w = w_fresh : necessite soit (a) modifier la definition de step pour inclure women-accept-best, soit (b) axiomatiser womenPref w_fresh m' = 0. Ces deux options sont documentees dans le commentaire du theoreme, et reservees a un futur lake refinement.
• lake build verification : le build Lean 4.33 prend 5-15 min en cold start. Le squelette est syntaxiquement valide (namespace + structure + def + theorem, avec sorry la ou necessaire). Une CI sur la PR pourrait rejouer lake build et confirmer.

Format respecte

• 1 fichier de lean modifie, 0 cellule code de notebook, 0 re-execution C.2 due.
• Aucun secret, aucun chemin machine.
• Style : docstrings en francais (CLAUDE.md section E + EPIC i18n(lean): harmoniser les fichiers .lean en francais + traduction anglaise — inventaire, convention, PR pilote #4980 i18n), noms de theoremes/lemmes en anglais (compat Mathlib 4).
• Conventions des autres lakes respectees (globs i18n, library name canonique).

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)
• PR tranche 0 : feat(lean,#19276): tranche 0 -- structure lake stable_marriage_lean + stubs + biblio #19336
• PR tranche 1 : feat(lean,#19276): tranche 1 -- squelette GSState + 6 invariants + 5 theoremes #19339
• PR tranche 2 : feat(lean,#19276): tranche 2 -- step real + preuve partielle step_menAcceptable #19344
• PR tranche 3 : feat(lean,#19276): tranche 3 -- preuve reelle step_menMatchedProposed_unchanged #19364
• PR tranche 4 : feat(lean,#19276): tranche 4 -- preuve reelle step_womenUnmatchedReject_unchanged #19367
• PR tranche 5 : feat(lean,#19276): tranche 5 -- preuve reelle step_menProposedDownward_unchanged #19397
• Source : mmaaz-git/stable-marriage-lean v4.25.0 (46 lemmes, 5 theoremes)
• Ouvrages : Roth & Sotomayor 1990 (a_confirmer), Gale-Shapley 1962 (JSTOR DOI 10.2307/2312726)

🤖 Generated with Claude Code

[github-actions]

Base != main (advisory, #10918)

Cette PR ne livre pas sur main : son contenu attend le merge de feat/19276-stable-marriage-tranche5. Aucune PR ouverte de feat/19276-stable-marriage-tranche5 vers main a cet instant -- si la base n'est jamais mergee, le livrable (feat(lean,#19276): tranche 6 -- womenBest preservation (limitation modele simplifie)) devient un orphelin (personne ne le verra jamais, cf. #10918). Remede : ouvrir une PR de feat/19276-stable-marriage-tranche5 vers main, ou rebaser cette PR sur main.

Couverture CI perdue sur cette base (mesure, #16194)

6 workflow(s) se declencheraient si cette PR visait main, et ne se declenchent pas ici : leur filtre de branche cible les eteint, alors que leur filtre de chemins est satisfait par les fichiers de cette PR.

• always-on-guards.yml
• gametheory-tests.yml
• lean-visibility-advisory.yml
• notebook-plan-loss-gate.yml
• pr-gate.yml
• secret-scan.yml

Un check absent n'est pas un check vert. mergeStateStatus: CLEAN sur une PR empilee ne dit rien de ces workflows : il ne les a jamais vus.

[jsboige]

[BLOCKED] Alerte chemin obsolete -- ne PAS merger cette PR avant arbitrage user sur EPIC #19276

Constat first-hand (git log + GitHub) :

Cette PR reintroduit le chemin MyIA.AI.Notebooks/GameTheory/stable_marriage_lean/ qui a ete supprime de main par cc5c0fa8dd (2026-07-11, PR #5971, chore(lean): #4365 remove stable_marriage_lean duplicate (absorbed into game_theory_lean)).

Le port Gale-Shapley existe deja dans MyIA.AI.Notebooks/GameTheory/game_theory_lean/StableMarriage/ (6 modules, ~10k+ LOC, port complet par po-2026 en 6 PRs MERGED : #5902/#5904/#5905/#5910/#5911/#5913). La representation est Matching bijection totale + Knuth lattice duality (anti-crossing lemma #1287/#1233/#1188), pas Option B du PORT_ANALYSIS.

Stack affectee (toutes les 9 PRs de la lane myia-po-2026:CoursIA-2 sur l'EPIC #19276) :

• feat(lean,#19276): tranche 0 -- structure lake stable_marriage_lean + stubs + biblio #19336 (tranche 0, structure + stubs) -- check-links FAIL collision
• feat(lean,#19276): tranche 2 -- step real + preuve partielle step_menAcceptable #19344 (tranche 2, step real) -- CLEAN MERGEABLE
• feat(lean,#19276): tranche 3 -- preuve reelle step_menMatchedProposed_unchanged #19364 (tranche 3, step_menMatche) -- CLEAN MERGEABLE
• feat(lean,#19276): tranche 4 -- preuve reelle step_womenUnmatchedReject_unchanged #19367 (tranche 4, step_womenUnmatch) -- CLEAN MERGEABLE
• feat(lean,#19276): tranche 5 -- preuve reelle step_menProposedDownward_unchanged #19397 (tranche 5, step_menPropose) -- CLEAN MERGEABLE
• • tranches 6, 7, 8 (Phase 2 + 3.5 effective + 3.5 structurel) livrees en r107-r114

Risque immediate : merge_ready.py (organe coordinateur) pourrait merger les 4 PRs CLEAN MERGEABLE automatiquement, re-ajoutant le chemin obsolete. L'EPIC #19276 elle-meme est en etat OPEN et n'a pas de mention de l'absorption game_theory_lean.

Position du worker :

• La lane myia-po-2026:CoursIA-2 ne peut pas trancher la question strategique (re-orienter le port vers game_theory_lean vs clore la stack vs re-ouvrir stable_marriage_lean).
• Documentation sur l'EPIC parent stable_marriage_lean: ouvrir le port Gale-Shapley (PORT_ANALYSIS option B) + référencer Roth & Sotomayor 1990 #19276 (commentaire 6009545545) avec 3 options de portee et recommandation.
• Geste minimal : cette alerte sur la PR CLEAN MERGEABLE pour eviter un merge accidentel avant arbitrage.

Action attendue :

• Coordinateur (myia-ai-01) ou mainteneur (jsboige) -- avant tout passage de merge_ready.py sur cette PR.
• Soit : pivoter le travail de la stack vers game_theory_lean/StableMarriage/ (lieu canonique), soit : clore la stack en closed-unmerged avec reference au port canonique deja merge, soit : re-ouvrir le chemin stable_marriage_lean/ par amendement explicite de chore(lean): #4365 remove stable_marriage_lean duplicate (absorbed into game_theory_lean) #5971 (et reintegrer le port existant comme base).
• Cf commentaire EPIC pour la matrice complete.

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #19411 (feat(lean,#19276): tranche 6 -- womenBest preservation (limitation modele simplifie)) 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 1 -- squelette GSState + 6 invariants + 5 theoremes #19339 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 2 -- step real + preuve partielle step_menAcceptable #19344 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 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)

[jsboige]

Substance déjà portée par game_theory_lean/StableMarriage/Lemmas.lean (901 lignes FR+EN). Tranche 6 = preservation womenBest (114 lignes). Le canonique porte womenBestState.step + initial + lemmes associés (Lemmas.lean:148-200). Apport propre = nul. Voir arbitrage ai-01 #arb-20261006-19276-stack-9prs. Branche feat/19276-stable-marriage-tranche6 conservée.