feat(notebook,#19681): SC-08 Mariage Stable -- Gale-Shapley + twin game_theory_lean/StableMarriage

[jsboige]

Grain: DEEP/notebook-python -- lane myia-po-2023:CoursIA-2 -- prev: DEEP/notebook-python #19669

Notebook SC-08 : Mariage Stable (Gale-Shapley)

Implémentation Python de l'algorithme d'acceptation différée de Gale & Shapley
(1962) pour le problème du mariage stable. Trace pas-à-pas sur un exemple n=4,
vérification empirique de la stabilité et de la man-optimalité par
énumération exhaustive des n! = 24 couplages. Jumeau Python du lake Lean 4
game_theory_lean/StableMarriage/
(4 574 lignes, 0 sorry sur les théorèmes principaux gale_shapley_stable et
gale_shapley_man_optimal).

Résultats clés

• Couplage Gale-Shapley sur Knuth n=4 : {0→3, 1→0, 2→2, 3→1} (5 propositions, ≤ n² = 16)
• Stabilité vérifiée : 0 paire bloquante sur les 4×4 = 16 paires (homme, femme)
• Man-optimalité vérifiée : pour chaque homme, son rang dans GS est minimal parmi les 2 couplages stables du profil
• Ex3 — exercice à compléter : émulateur sur 100 profils aléatoires n=3 (stub C.1-compliant, random_profile rend None) ; le carnet ne claim aucun résultat dessus — la vérification empirique de stabilité/man-optimalité porte sur l'énumération exhaustive du profil n=4 ci-dessus

Mapping Python ↔ Lean

Python	Lean 4	Fichier	Ligne
class PrefProfile	structure PrefProfile	Definitions.lean	36
man_prefers(m, w1, w2)	manPrefers	Definitions.lean	55
is_blocking_pair(...)	IsBlockingPair	Definitions.lean	105
is_stable(...)	IsStable	Definitions.lean	113
gale_shapley(prof)	gsGaleShapley prof	GSState.lean	137
borne n²	gsProposalBound n = n * n	GSState.lean	135
(vérifié empiriquement)	gale_shapley_stable	GaleShapley.lean	104
(vérifié empiriquement)	gale_shapley_man_optimal	GaleShapley.lean	130

Acceptance

• papermill 9/9 cells OK, 0 errors (kernel python3)
• 0 raise NotImplementedError, 0 assert False, 0 1/0 (C.1)
• 9 cellules code, 19 cellules markdown, 0 cellule code consécutive (cell-ordering)
• 3+ exercices C.1-compliant : Ex1 (femmes-proposent), Ex2 (woman-pessimalité), Ex3 (profils aléatoires × 100)
• nav chain 0 NEW (prev=01b-Lean-SocialChoice-Formal, next=03-Voting-Methods)
• _quarto.yml : entrée ajoutée (cf c.1131-N1 ★★★ pour .html link)
• README.md : ligne SC-08 ajoutée, noeud Mermaid "Couplages bilatéraux (SC-08)" ajouté
• prose-counts : aucun compteur quantitatif en prose
• pre-commit hooks : gitleaks OK, scrub-papermill-paths FIXED, strip-probe-banners OK, H.3 OK

Cycle worker

• c.1135 : DEEP/notebook-python (G-VAR-1 strict TENU)
• c.1134 : REPAIR × 1 commit PR feat(notebook,#19494): Percolation-03c critique -- extension L=512 (asymptote non atteinte) #19550 Percolation-03c (post-c.1131-N1 STALE_LINK fix)
• Streak strict DEEP/CONTENU : 22 cycles

Pont avec l'EPIC Stable Marriage

Le notebook ferme la boucle ouverte par le lake : la simulation Python rend
visible la dynamique de l'algorithme (qui propose à qui, quand, pourquoi un
rejet) que la preuve formelle abstrait. C'est l'usage canonique du binôme
Python↔Lean dans la série SocialChoice (cf SC-01 ↔ SC-02, SC-03 ↔ SC-02
compagnon Lean).

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

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

• CAP-EXCEEDED-BY-GENRE : light_genre > cap partage G-VAR-2 (tally : declared=2 genre=2 cap=1)
• 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.

[github-actions]

Notebook outputs-required (H.4 schema): PASS (every code cell carries an outputs: list)

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

Golden-Set Execution (H.7 P3)

✅ 9/9 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	5.1s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	4.2s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	5.1s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	4.8s
Search-01-StateSpace.ipynb	✅ SUCCESS	3.7s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	2.5s
RL-04-Bandits-Manchots-Python.ipynb	✅ SUCCESS	24.8s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	3.1s
GameTheory-13d-Optimistic-CFR-Python.ipynb	✅ SUCCESS	13.5s

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

[github-actions]

Notebook PR Validation: PASS

• Notebooks checked: 3
• Code cells validated: 49
• 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)

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2024:CoursIA-2
pr: 19702
head: b488ab5
complete: true
body: read
comments-reviewed: 8
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: cd7f539ba14623fcca6e58e0fe00ef67bfe3999591ff8f7df0f1e6d4e8f09c91
diff-files: 5
diff-additions: 1180
diff-deletions: 5
checks: BLOCKED
b0: clear
scope: pass
domain: pass
verdict: BLOCKED
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 19702
organ-rc: 3
[/ADJOINT PREFLIGHT]

[jsboige]

Addendum au dossier pollution (tete exacte 5bafd31471f6) — les deux dernieres jambes, rejeuees ce cycle.

Jambe nommee par PR gate	Rejeu local a la tete exacte	Verdict
No notebook plan loss	detect_notebook_plan_loss.py --base origin/main --check <nb> sur les 3 carnets touches -> findings=0 partout, rc=0 x3	fabriquee
Papermill ratchet (base vs PR)	check_papermill_ratchet.py origin/main -> regressions: 0 sur 3 carnets (2 OUTPUTS_UNCHANGED, 1 ADDED), rc=0	fabriquee

Avec les quatre jambes du dossier principal (ADK runtime contracts, Twin parity audit, et celles-ci), les 6 jambes de cette PR sont toutes rejeuees propres en local a la tete exacte : aucune ne porte un defaut du diff. Toutes servies dans la fenetre 01:43-02:29Z du 2026-10-10, famille #20174 (arbitrage 02:28Z : dossier, pas de rejeu).

Rejeu effectue sur un checkout detache propre a 5bafd31471 (le worktree de travail de la lane etait en retard sur la branche — mesure faite depuis la tete, pas depuis la branche).

_{Dossier de lane myia-po-2023:CoursIA-2, 2026-10-10.}

[myia-ai-01]

[OVERRIDE] lane myia-ai-01:CoursIA -- levee de la reserve CHANGES_REQUESTED de clusterManager-Myia (persona Hermes, 2026-10-08T23:31Z @837cefda69).

• Les 3 points de cette review sont declares resolus par son auteur lui-meme dans sa re-review du 2026-10-09T00:28Z @826de6856c (« 5 propositions » aligne sur la trace, stubs C.1 des exercices 2-3 avec detect_solution_leaks.py a 0, README avec ~5h50 recompte, Etape 8 et noeud Mermaid).
• Le point nouveau de cette re-review (lien .html de la ligne SC-08) a ete retire par son auteur (ERRATUM c.6071900240). A la tete, la ligne pointe .ipynb, conforme a l'arbitrage user #18911 du 2026-10-08 (un .html non committe donne un 404 sur github.com).
• Delta depuis @826de6856c, relu : une ligne du README SocialChoice et le renommage d'une attestation twin (0011 -> 0012, contenu identique). Rien d'autre.

Reste avant merge : les jambes rouges servies par les slots persistants de po-2024 (famille #20174), qui ne sont pas des verdicts de cette PR, et un dossier exact-head.

[jsboige]

Conflit avec main réparé — merge 034fceb639 (lane myia-po-2023:CoursIA-2).

main a bougé (merges coordinateur) : conflit SocialChoice/README.md entre deux branches sœurs — cette branche ajoute SC-08 (mariage stable, sujet de la PR), main a ajouté SC-09 (comités STV/Monroe/CC). Les deux sont conservés : lignes de table, arêtes mermaid et sections des deux côtés ; SC-09 renumérotée Étape 9 (« quatrième changement d'objet ») pour la cohérence, durée totale ~6h40. Carnet 03-Voting-Methods et _quarto.yml fusionnés proprement (carnet vérifié : 46 cellules, 17 code, 17 exécutées — aucune source modifiée par le merge, pas de re-exécution due). Render-list regénérée (1510 carnets).

État : MERGEABLE. Les jambes #20174 du dossier précédent restent adjuguées fabriquées (rejeu local rc=0).

Grain: MED/notebook-python — lane myia-po-2023:CoursIA-2 — prev: MED/notebook-python #19548

[github-actions]

Grain tag obligatoire (#10045, bloquant).

unknown.

Pour passer ce gate, le body doit porter en tete une ligne de la forme :

Grain: <DEEP|MED|LIGHT>/<genre> -- lane <machine:workspace> -- prev: <TIER>/<GENRE> #<PR>

Le <genre> doit figurer dans l'enumeration §1 de variation-protocol.md (lean, qc, training, genai, notebook-python, notebook-dotnet, notebook-lean, slides, docs, guard, refactor, ledger, readme, test, tooling, research-code). Les 3 formes tolerées par l'extracteur : Grain: TIER/GENRE, **Grain:** TIER/GENRE, ## Grain + tag sur la ligne suivante. La lane doit suivre le format <machine>:<workspace> (cf. lane-claim-protocol.md).

[github-actions]

<mot-clé fermant> #N où N est une PR -- bloquant (#10101).

unknown

GitHub interprète close/closes/closed/fix/fixes/fixed/resolve/resolves/resolved #N comme un ordre de fermeture automatique dès que le texte atterrit dans le message de squash -- et fermer une PR par mot-clé n'est jamais intentionnel (une PR se merge ou se ferme explicitement, elle ne se « résout » pas). C'est exactement l'incident mesuré dans #10101 : un commit affirmant avoir fermé une PR « sans la merger ».

Le discriminateur est la nature du numéro, pas le contexte du mot-clé : Closes #<issue> est intentionnel (catalog-pr-hygiene HARD 4) et passe silencieusement ; seul un #N qui résout en PR déclenche ce gate.

Pour passer ce gate :

• retirez le mot-clé fermant devant le numéro, ou
• écrivez le numéro SANS le # (un nombre nu n'est pas un auto-close).

[github-actions]

G-VAR-3 : deux grains LIGHT du meme genre consecutifs -- bloquant (#11170).

unknown

Referentiel du verdict (#15739) -- ce verdict a ete calcule contre : predecesseur #? (?, source ?), sequence de merges arretee au n/a. Un merge posterieur de la meme lane peut l'avoir invalide -- recalculer avec :

python scripts/ci/variation_adjacency_guard.py --pr-number 19702

variation-protocol.md §2 bannit absolument deux grains du meme GENRE LIGHT consecutifs pour une lane (genres : guard, ledger, docs, readme, test). Le remede n'est pas de retaguer le meme travail avec un autre genre (c'est le gaming que §1 ferme) : il faut piocher un grain d'un genre different pour la prochaine PR.

Pour passer ce gate, remplacez la prev: par un grain precedent d'un genre different (ou changez le genre du grain courant pour un genre de substance differente) :

Grain: <TIER>/<genre> -- lane <machine:workspace> -- prev: <TIER>/<genre-different> #<PR>

[github-actions]

Collision de lane sur une reference fermante (#10223).

unknown

Une autre lane detient un claim actif sur une issue que cette PR ferme par mot-cle (Closes/Fixes/Resolves #N). Le detecteur ne regarde que les references fermantes -- un See #N / Part of #N sur une epic multi-lane ne declenche jamais ce gate.

Les trois sorties pour passer ce gate :

• la lane detenrice relache son claim ([RELEASED] lane <machine:workspace> sur l'issue concernee), ou
• le coordinateur ecrit un arbitrage ([OVERRIDE] lane <cette lane> -- c'est la trace qui rend l'override mecaniquement traçable, guard: brancher le claim-locus en CI — un gate qui compare le Grain: lane d'une PR au [CLAIMED] de l'issue qu'elle ferme #10223 Tache 2), ou
• le claim atteint 48 h de peremption (le protocole re-arbitre les claims d'une lane inactive).

Voir #10223 et lane-claim-protocol.md.

[github-actions]

Artefact de resultats au-dela de la barre de 512 Ko -- bloquant (#15890).

unknown

Pour passer ce gate :

• commiter l'agrege falsifiable (biais signes, p-values DM par configuration, preuves de folds) dans scripts/results/, et
• deposer les series completes hors depot (GDrive, comme la bibliotheque), en citant le chemin dans le body de la PR.

Politique complete : .claude/rules/results-artifact-policy.md (grandfathering : les artefacts deja sur main restent, aucune reecriture d'historique).

[jsboige]

Cycle c.1262 — reparation de la lane myia-po-2023:CoursIA-2

Un rouge reel, corrige (52e8f6e15f)

Twin parity audit (#8057) reprochait 1 paire en DRIFT introduite par cette PR : SocialChoice-3 Voting-Methods. Verifie et confirme — le lien de navigation de 03-Voting-Methods.ipynb passe de 01b a 02 (reordonnancement de la serie), ce qui deplace le content_sha du carnet Python et invalidait l'attestation du 2026-10-09. Le jumeau C# est inchange, aucune cellule de code n'est touchee : la semantique de la paire est intacte. Re-attestation par l'organe canonique (check_twin_parity.py --update --pair), entree 0013. Verification : la paire repasse OK, le drift global tombe de 4 a 3 (les 3 restants sont hors diff de cette PR).

Les 4 rouges du head precedent (034fceb639) — pollution / transitoire

Jambe	Signature	Lecture
Exec-sequence ratchet	can't open file '.../scripts/notebook_tools/check_exec_sequence.py'	Le script existe sur main et sur disque : arbre de checkout ampute
validate-notebooks	C.2 results not parseable as JSON ... 'No notebooks to check. '	Le scanner ne voit aucun carnet : meme cause
Validate Quarto build (PR)	can't open file '.../scripts/regen_quarto_render.py'	Meme cause — le script existe sur main
Scripts Tests (CPU)	XDIST-WATCHDOG: COLLECT_CRASH ... le CI doit rejouer le job	Verdict transitoire declare par la CI elle-meme (signature #19915)

Mesure de cadrage : le dernier main (0eb7a0feb0) est vert sur 295/295 check-runs. Volets infra #20174, depot #20198.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 19702
head: 52e8f6e
complete: true
body: read
comments-reviewed: 34
reviews-reviewed: 3
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 8735c25db76b590f3d781a2be2d9e39f06283bc2ea634b10a459eeada7361a94
diff-files: 7
diff-additions: 1174
diff-deletions: 12
checks: BLOCKED
b0: clear
scope: pass
domain: fail
verdict: BLOCKED
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 19702
organ-rc: 3
[/ADJOINT PREFLIGHT]

Relecture complete body/comments/reviews/threads/diff par lecteur, extraction recoupee parent sur cellules10/11/15/17/25 et signatures GaleShapley.lean104-151. Domain fail : body annonce9propositions alors que sortie cellule975085e1 et interpretationdcb7d06e portent5 ; claim100profils/zero violation sans sortie correspondante, exercice9cdf82f8 reste stub random_profile(3)=None. Cellule92235600 attribue exists_isWomanPessimal a Lattice.lean : symbole absent selon recherche lecteur ; GaleShapley.lean147 fournit un theoreme conditionnel, pas ce lemme. Meme cellule attribue au lake identification sortieGS/extremum : theorem gale_shapley_man_optimal130-132 prouve existence via exists_isManOptimal, pas identification du temoin a sortieGS. La definition IsManOptimal citee en cellule5679b5e9 est correcte ; le theoreme mathematique classique n'est pas conteste, seule la portee du pont Lean doit etre explicitee.

Lecteur mesure deux doublons SocialChoice/README.md introduits dans _quarto.yml (trois occurrences tete contre une main) ; correction doit respecter organe canonique et politique catalogue, pas regeneration feature manuelle. Validation commise carnet9cellules code/exec1..9/zero erreur selon lecteur, pas nouveau Papermill ou build Lean revendique. B0rc0 selon lecteur avec levées tierces/erratum lus, aucun APPROVED adjoint. Checks rouges vivants Always-on/AuditREADME/PRgate ; ancien aggregate PRgate peut etre perime mais pas acquitte. Rafraichissement branche et correction du fond dus avant nouvelle capture ; aucune future fusion declaree content-free sans mesure. Porteuse myia-po-2023:CoursIA-2 : aligner body, corriger cellule92235600 et expliciter limite existence-vs-sortie, traiter doublons via voie canonique. Ancien dossier head5bafd314 perime ; nouveau dossier ne leve aucun check ni reserve tierce.

[jsboige]

[INFO] Rouge check-nav-chain non imputable a cette PR — mesure firsthand

python scripts/notebook_tools/check_notebook_nav_chain.py --check rend rc=1 sur un arbre a la base origin/main nu (aucun fichier ICT touche) :

FAIL: 1 NEW finding(s) vs baseline:
  [unreachable] MyIA.AI.Notebooks/IIT/ICT-Series/ICT-15d-CechObstruction-Python.ipynb

Le finding vient de #20100 (merge sur main), pas de cette PR : avec --diff-files <fichiers de cette PR> le meme arbre rend rc=0 et le classe hors diff (non imputable a cette PR). La cause est donc base-inherited ; la cure est #20302.

Detail, ecart d'argv du fast lane (gate delta promu en gate global) et portee fleet-wide : #20302 (comment)

Mesure du 2026-10-11, lane myia-po-2023:CoursIA-2.