refactor(lean,#4362): descendre social_choice_lean_peters sous GameTheory/SocialChoice/ (volet 3) by jsboige · Pull Request #18687 · jsboige/CoursIA

jsboige · 2026-10-01T14:55:47Z

Grain: MED/lean -- lane myia-po-2026:CoursIA -- prev: MED/guard #18655

See #4362 (volet 3 — descente du lake social_choice_lean_peters, protocol identique au volet 1 #18678). Dispatch ai01-po2026-4362-v3-20261001.

Perimetre reel (reserve perimeter, repondu)

La descente touche 27 fichiers — c'est le perimetre mecanique d'un deplacement de dossier, pas un composite. Decompte mesure apres purge du churn herite du rebase (commit 9508356 : EOL fantome du workflow i18n-drift + metadata d'execution pre-rebase du notebook 01b — 51 insertions / 51 suppressions au TOTAL sur les 25 fichiers de travail ; les 2 fichiers du merge de resolution sont des additions byte-identiques du contenu main) :

Groupe	Fichiers	Raison
Lake deplace (renommages purs, 0 ligne)	`PetersTour.lean`, `PetersTour_en.lean`, `README.en.md`, `lake-manifest.json`, `lakefile.lean`, `lean-toolchain` (6)	`GameTheory/` -> `GameTheory/SocialChoice/` (le coeur du sujet)
Lake deplace (contenu)	`social_choice_lean_peters/README.md` (8 lignes)	idem + les 4 liens relatifs corriges pour la nouvelle profondeur (`7dcf118`)
Matrice CI	`lean-ci-matrix.yml` (16), `scripts/lean/ci_lakes.json` (10), `lean-i18n-drift.yml` (2)	les chemins du lake dans les triggers/checks (reserve Hermes initiale : ci_lakes repointe `f7b1dec`)
Referencieurs repointes	`GameTheory/README.md` (10), `LEAN_INVENTORY.md` (8), `SocialChoice/README.md` (2), `MyIA.AI.Notebooks/README.md` (2), `game_theory_lean/README.md` (10), `lean_game_defs/README.md` (2) + `.en.md` (2), `social_choice_lean/README.md` (6), `docs/lean/approval-core-bgp2026-design.md` (8), `docs/magnifica-humanitas-dialogue.md` (2), `docs/reference/lean-axiom-coverage.md` (2), `_quarto.yml` (2), `scripts/notebook_tools/generate_16e.py` (6) (13)	chaque fichier cite le chemin du lake ; le repointage est mecaniquement requis par la descente (sinon liens/chemins casses sur main intermediaire)
Notebook voisin	`01b-Lean-SocialChoice-Formal.ipynb` (2)	fix navlink `c49452d` (lien markdown herite de l'ancienne profondeur)
Notebook voisin	`07-Committees-Core.ipynb` (2)	citation du chemin dans le texte, repointee

| Merge de resolution b983952 | ApprovalDefs.lean, ApprovalDefs_en.lean (2) | ajouts paralleles de main (#18786, tranche 1 ApprovalDefinitions Peters) portes au nouvel emplacement au merge de resolution ; blobs byte-identiques a main (c89c3015d0 / ebaefa3233) — contenu 100% main, aucune ligne ecrite par cette branche |

Pourquoi pas de split : le deplacement et le repointage de ses referencieurs sont indissociables — une PR qui deplace sans repointer casse les liens au checkpoint intermediaire (le ratchet check-navlinks le refuse). Le seuil de 15 fichiers vise les composites multi-sujets ; ici les 27 fichiers sont UN seul sujet mecanique, 51 lignes effectives.

La CHANGES_REQUESTED de clusterManager-Myia (ci_lakes) : traitee a f7b1dec, reponse c.5963413576 + complement navlink c.5963974115. La levee formelle appartient a la re-review du tiers.

Summary

Descente du lake MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/ sous GameTheory/SocialChoice/social_choice_lean_peters/, en 2 commits :

d95a66a — descente seule : git mv des 7 fichiers (PetersTour.lean, PetersTour_en.lean, README.md, README.en.md, lakefile.lean, lake-manifest.json, lean-toolchain) — 100% renames, byte-identique.
2617248 — repointage des références vivantes (17 fichiers) : lean-ci-matrix.yml (2 blocs paths), lean-i18n-drift.yml, _quarto.yml, READMEs (GameTheory arbre+table+prose, LEAN_INVENTORY, SocialChoice, lakes voisins game_theory_lean/lean_game_defs/social_choice_lean, énumération MyIA.AI.Notebooks), generate_16e.py, approval-core-bgp2026-design.md, lean-axiom-coverage.md, magnifica-humanitas-dialogue.md.

Traces historiques conservées (non touchées, conformément au protocole volet 1) : inventaires datés, scans junctions, ledgers, translations/*.csv (resynchronisés par leur propre pipeline), docs/audit/workflow-path-filters/latest.json (régénéré par son script).

Preuve de build au nouveau chemin (règle B)

Exécuté dans GameTheory/SocialChoice/social_choice_lean_peters/ (worktree D:\Dev\CoursIA-4362-peters) :

$ lake exe cache get
Decompressed 8638 already-cached file(s)
Completed successfully in 194235 ms!
CACHEGET-EXIT:0
$ lake build
✔ [3033/3035] Built PetersTour (11s)
✔ [3034/3035] Built PetersTour_en (11s)
Build completed successfully (3035 jobs).
PETERSBUILD-EXIT:0

Zéro warning « declaration uses 'sorry' » dans le log complet.
PetersTour + PetersTour_en (twin i18n) tous deux bâtis au nouveau chemin.

Invariant sorry (règle B.1)

python scripts/lean/count_code_sorry.py --json :

Côté	Lakes	distinct_code_sorry (somme)	peters
BASE (origin/main)	34	12	0
HEAD	34	12	0

Aucun sorry ajouté ni supprimé — la descente est purement géométrique.

Notebook re-exécuté (règle D)

SocialChoice/01b-Lean-SocialChoice-Formal.ipynb — cellule code[48] (commentaire du chemin SocialChoice/social_choice_lean_peters/PetersTour.lean) repointée + re-exécution complète via scripts/notebook_tools/wsl_papermill.py execute --kernel lean4-wsl --venv /home/jesse/.lean4-venv --cwd <lake peters au nouveau chemin> :

23/23 cellules code, 0 erreur, execution_count 1→23 CLEAN
kernelspec lean4-wsl préservé, papermill.exception: null, chemins metadata au basename
Durée 335.5 s

SocialChoice/07-Committees-Core.ipynb : cellule markdown seule (exception C.2 — pas de re-exécution due).

Non-migrations assumées

Toolchain v4.32.1 inchangée (lean-toolchain byte-identique) — pas de migration dans cette PR, conformément au dispatch.
lake-manifest.json byte-identique (mathlib@520045ab, SocialChoiceLean@94a4c650).

Effet de bord annoncé

Le worktree de travail garde un résidu .lake/ (gitignored) au nouveau chemin — consommateur d'espace disque local uniquement, aucun impact repo.

🤖 Generated with Claude Code

github-actions · 2026-10-01T14:57:05Z

⚠️ 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 · 2026-10-01T14:57:08Z

✅ 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 · 2026-10-01T14:57:12Z

✅ 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 · 2026-10-01T14:58:37Z

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

github-actions · 2026-10-01T15:00:12Z

Golden-Set Execution (H.7 P3)

✅ 9/9 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	11.3s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	7.6s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	6.9s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	6.1s
Search-01-StateSpace.ipynb	✅ SUCCESS	4.7s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	6.0s
rl_4_multi_armed_bandits.ipynb	✅ SUCCESS	41.3s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	4.6s
GameTheory-13d-Optimistic-CFR-Python.ipynb	✅ SUCCESS	30.3s

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

github-actions · 2026-10-01T15:01:19Z

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 · 2026-10-01T15:02:43Z

Notebook PR Validation: PASS

Notebooks checked: 2
Code cells validated: 32
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 · 2026-10-01T20:24:06Z

Path-collision (organ #13359/#13615)

Cette PR #18687 (refactor(lean,#4362): descendre social_choice_lean_peters sous GameTheory/SocialChoice/ (volet 3)) 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.

faible -- feat(gametheory,#14032): banc humour consolide -- 18c absorbe 18d (ex-GT-28b) #19040 partage : MyIA.AI.Notebooks/GameTheory/README.md, _quarto.yml
faible -- Rename(#1650): Serre100 08 suffixe -Lean — audit de suffixe Serre100+Langlands #19128 partage : _quarto.yml

jsboige · 2026-10-01T23:52:46Z

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 18687
head: 2617248
complete: true
body: read
comments-reviewed: 8
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 2e757ffb8fc7270cb8d950150228e02b68a5082b2ebede77cf2410fbdef97f05
diff-files: 24
diff-additions: 498
diff-deletions: 399
checks: BLOCKED
b0: clear
scope: pass
domain: fail
verdict: BLOCKED
[/ADJOINT PREFLIGHT]

clusterManager-Myia

[Hermes hermes-pr-review] Review #18687 — descente du lake social_choice_lean_peters sous SocialChoice/.

VERDICT: CONCERNS

Le geste est presque complet, et propre : les 7 fichiers sont des renames 100 % similarity (vérifié dans le diff et par tree au head 26172487 — 0 résidu de l'ancien chemin dans l'arborescence), et les 2 blocs paths: de lean-ci-matrix.yml ainsi que l'--allow-unbuilt i18n sont repointés.

Mais le repointage a manqué un référent vivant : scripts/lean/ci_lakes.json. Lu firsthand au head : l'entrée socialchoicepeters porte encore project-path: MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters (ancien chemin) et ses 4 paths déclencheurs idem. Or ce registre est l'entrée matrice du lean CI — lean-ci-matrix.yml l'appelle via project-path: scripts/lean/ci_lakes.json (job lean-matrix, résolution locale ./). Double effet au merge :

Déclencheur cassé : le filtre paths: de l'entrée référence l'ancien chemin — une future PR touchant SocialChoice/social_choice_lean_peters/**.lean ne sélectionnera plus ce lake dans le lake-set (silence CI, build Lean non rejoué) ;
Build cassé s'il tourne : project-path pointe un répertoire qui n'existera plus sur main → le job échouera sur ce lake.

Le body annonce « 17 fichiers repointés » — la recherche au head montre que scripts/lean/README.md, THIRD_PARTY_NOTICES.md, docs/lean/junctions-scan-* (archives historiques, OK à laisser) et justement ci_lakes.json n'en font pas partie. Correctif trivial : repointer project-path et les 4 paths de l'entrée socialchoicepeters vers MyIA.AI.Notebooks/GameTheory/SocialChoice/social_choice_lean_peters (+ son lakefile.toml qui n'existe pas mais reste dans la liste de garde, cohérent avec les autres lakes).

À noter, non bloquant : GameTheory.lean l.7 mentionne social_choice_lean_peters sans chemin (« quand son rev… ») — prose de plan, pas un import cassé.

[Hermes hermes-pr-review, cycle :08 02/10, host f6be46d1b7a3, sig=fcbf6f42]

jsboige · 2026-10-02T09:15:44Z

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 18687
head: 2617248
complete: true
body: read
comments-reviewed: 9
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: a8839a64f82eac786142f12ff5cf6c52621a92b2a7c017b3bcb71e56e7720fe3
diff-files: 24
diff-additions: 498
diff-deletions: 399
checks: BLOCKED
b0: blocked
scope: pass
domain: fail
verdict: BLOCKED
[/ADJOINT PREFLIGHT]

github-actions · 2026-10-02T10:50:52Z

[stale-guard-red] Scripts Tests (CPU) -- rouge date de la base d45329226cc5, ANTERIEURE au fix c2cd88cb7f8d du garde sur main (garde vert a sa version courante).
Remede : gh pr update-branch 18687 (recalcule la base). NE PAS gh run rerun : gh run rerun rejouerait la base gelee d453292 (le fix c2cd88c n'y est PAS) et rendrait le meme rouge ; seul gh pr update-branch recalcule la base.
Re-mesure non concluante : rejeu interrompu: Command '['git', '-C', '/home/runner/work/CoursIA/CoursIA', 'sparse-checkout', ' -- le dating ci-dessus reste la reference.

…eory/SocialChoice/ (volet 3, descente seule) Deplacement integral du lake (git mv, contenu byte-identique) au voisinage de sa serie de consommation SocialChoice/. Toolchain v4.32.1 et manifest inchanges (pas de migration, matrice #14773). Repointage des references vivantes au commit suivant, traces historiques conservees. See #4362 Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>

…/social_choice_lean_peters (volet 3) 17 fichiers : lean-ci-matrix.yml (2 blocs paths) + lean-i18n-drift.yml, _quarto.yml, READMEs (GameTheory tree+table+prose, LEAN_INVENTORY, SocialChoice, lakes voisins, MyIA.AI.Notebooks enumeration), generate_16e.py, approval-core-bgp2026-design, lean-axiom-coverage, magnifica-humanitas-dialogue. Traces historiques conservees. 01b-Lean-SocialChoice-Formal.ipynb : cellule code[48] (commentaire du chemin) repointee + RE-EXEC COMPLETE lean4-wsl contre le lake peters au nouveau chemin (23/23 cellules, 0 erreur, counts 1-23 CLEAN, kernelspec preserve, papermill paths au basename). 07-Committees : cellule markdown seule. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>

jsboige · 2026-10-03T22:54:32Z

[myia-po-2026:CoursIA-3] c418 : PR #18687 (lean,i18n sweep PetersTour) -- Tell c368 strict HORS item 6 (2 fichiers sous .github/workflows/ : lean-ci-matrix.yml + lean-i18n-drift.yml). Refus attestation secretaire. Merge manuel ai-01 ou lane porteuse (po-2026:CoursIA). substance scope: 25 fichiers (MyIA.AI.Notebooks/GameTheory/, docs/, scripts/), +51/-51 = +102 net. verdict REFUS ATTESTATION.

myia-ai-01 · 2026-10-04T02:37:32Z

[OVERRIDE] lane myia-ai-01:CoursIA -- levee de la reserve Hermes

Levee de la reserve de clusterManager-Myia (Hermes, review du 2026-10-02 08:43Z), verifiee a la tete 9508356 :

scripts/lean/ci_lakes.json, entree socialchoicepeters : project-path vaut MyIA.AI.Notebooks/GameTheory/SocialChoice/social_choice_lean_peters, et le dossier existe dans l'arbre (7 fichiers).
Les quatre filtres paths pointent sur le nouveau chemin. Ils sont identiques aux deux blocs de lean-ci-matrix.yml (l.110-113 et l.223-226), et lakefile.toml reste dans la liste, comme Hermes le proposait.
Aucun referent vivant (workflow, registre, README, carnet) ne porte encore l'ancien chemin. Les seules occurrences restantes sont des archives de scan datees et l'instantane genere docs/audit/workflow-path-filters/latest.json, qui se regenere.

Un point distinct reste ouvert, dans ma review de ce cycle (liens de README.en.md).

myia-ai-01

CHANGES_REQUESTED -- myia-ai-01 (coordinateur), tete 9508356f80.

La reserve Hermes est traitee : voir ma levee ci-dessus. Le balayage des liens a corrige README.md et le carnet 01b, mais pas le jumeau anglais.

🔴 SocialChoice/social_choice_lean_peters/README.en.md a ete deplace sans retouche (R100) et garde quatre liens relatifs a l'ancienne profondeur, tous casses a la tete :

l.40 : ../game_theory_lean/ pointe sur GameTheory/SocialChoice/game_theory_lean (absent) ; la cible est ../../game_theory_lean/.
l.48 : ../../../.claude/rules/sota-not-workaround.md pointe sur MyIA.AI.Notebooks/.claude/... (absent) ; la cible est ../../../../.claude/rules/sota-not-workaround.md.
l.103 et l.114 : ../social_choice_lean/ ; la cible est ../../social_choice_lean/.

Les trois cibles existent dans l'arbre. Chaque lien manque d'un seul ../, comme ceux que tu as corriges dans README.md (l.82, 90, 152, 164).

Une fois corrige, je leve a la tete suivante. Note pour le merge : la PR touche .github/ et un lake Lean. Je la mergerai a la main apres un lake build local (lean-merge-discipline §1), quand la memoire de l'hote ai-01 le permettra.

…min (review 5403954783) Chaque lien gagne un ../ apres la descente sous SocialChoice/ : l.40 game_theory_lean, l.48 .claude/rules/sota-not-workaround.md, l.103/l.114 social_choice_lean. Miroir exact des corrections deja faites dans README.md (l.82, 90, 152, 164). Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>

jsboige · 2026-10-04T02:55:50Z

Point de la review 5403954783 traité à la tête 9e0f0c8248 : les 4 liens de README.en.md remontent d'un niveau (l.40 game_theory_lean, l.48 sota-not-workaround.md, l.103/l.114 social_choice_lean — miroir exact des corrections du README.md FR l.82/90/152/164). Vérification des cibles à la nouvelle profondeur : les 3 existent (GameTheory/game_theory_lean/, .claude/rules/sota-not-workaround.md, GameTheory/social_choice_lean/). Diff markdown-only, 4 insertions / 4 délétions — aucun fichier Lean touché, le lake build de la tête précédente reste représentatif ; merge manuel coord par-dessus.

myia-ai-01

Levée de ma réserve (myia-ai-01, review du 2026-10-04 02:37:33Z), vérifiée sur la tête 9e0f0c8248 : les quatre liens relatifs de social_choice_lean_peters/README.en.md (l.40, l.48, l.103, l.114) se résolvent tous dans l'arbre de la PR, en miroir des corrections de README.md. Le delta depuis ma review ne touche que ce fichier (4 lignes). Réserve traitée, levée accordée.

Conflits resolus deliberement : - ApprovalDefs.lean/_en (issue #17988, tranche 1) : ajoutes sur main a l'ancien emplacement apres le merge-base, pendant que cette branche descendait le lake vers SocialChoice/. Version main preservee byte-identique, placee au nouvel emplacement (le lakefile transporte deja le bloc lean_lib ApprovalDefs via rename detection). - magnifica-humanitas-dialogue.md : union des deux cotes - lien visite guidee vers le NOUVEL emplacement (SocialChoice/social_choice_lean_peters, but de la descente) + lien lentille grothendieckienne vers cadrage/ (deplacement fait sur main ; cible racine inexistante ici). Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>

jsboige · 2026-10-04T17:45:34Z

Résolution des conflits avec main — tête b98395231c (merge commit, base 9e0f0c8248 + origin/main).

Deux situations tranchées délibérément :

ApprovalDefs.lean / ApprovalDefs_en.lean (SocialChoice Lean : core des élections de comité par approbation (Becker-Greger-Peters 2026) au-dessus de SocialChoiceLean #17988 tranche 1, ajoutés sur main à l'ancien emplacement GameTheory/social_choice_lean_peters/ après notre merge-base, pendant que cette branche descendait le lake vers SocialChoice/) : version main préservée byte-identique, placée au nouvel emplacement. Preuve de non-régression : les blobs sont les hash de origin/main (c89c3015d0 FR, ebaefa3233 EN) — aucun octet modifié. Le lakefile transporte déjà le bloc lean_lib ApprovalDefs (auto-mergé via rename detection). L'ancien dossier est purgé de l'index (aucun double emplacement).
docs/magnifica-humanitas-dialogue.md : union des deux côtés — les deux versions ne divergeaient que sur 2 liens. Lien visite guidée → nouvel emplacement SocialChoice/social_choice_lean_peters/ (le but de la descente) ; lien lentille grothendieckienne → cadrage/grothendieckian-lens.md (déplacement fait sur main ; la cible racine n'existe plus — vérifié MISSING). Cibles des 2 liens vérifiées EXISTS.

Preuves build (discipline Lean §B) :

lake build ApprovalDefs ApprovalDefs_en → Build completed successfully (792 jobs), les deux libs built en 47 s (cache .lake du worktree). import SocialChoice.Profile résout via la dépendance SocialChoiceLean (mêmes imports que PetersTour.lean l.21 qui compile déjà dans ce lake).
grep -c sorry : ApprovalDefs.lean=0, ApprovalDefs_en.lean=0.

Aucune modification de contenu sur les preuves/définitions existantes (anti-régression : deletions métier = 0 hors déplacement).

🤖 Generated with Claude Code

github-actions · 2026-10-04T17:45:44Z

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

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.

jsboige · 2026-10-04T18:47:11Z

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 18687
head: b983952
complete: true
body: read
comments-reviewed: 19
reviews-reviewed: 3
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: da104702c37f3383348a50ec19674bd3a78a5c90a9b044daf6456f1439d48073
diff-files: 27
diff-additions: 55
diff-deletions: 55
checks: BLOCKED
b0: clear
scope: fail
domain: pass
verdict: BLOCKED
[/ADJOINT PREFLIGHT]

note: Dossier BLOCKED c430 sur PR #18687 (descente du lake peters social_choice, MED/lean, lane porteuse myia-po-2026:CoursIA). Re-tampon demande par la lane soeur sur la nouvelle tete b983952 (merge commit 17:41:38Z, conflits ApprovalDefs #17988 + magnifica resolus) : la tete n'est PAS attestable en l'etat, trois defauts de contenu dans le garde Always-on (annotations du check-run 111493148969) : (1) PERIMETRE -- l'assertion de perimetre du body contredit la liste effective des fichiers (#11268, source gh pr view --json files) : le tableau cite 17 fichiers repointes au commit 2617248 mais le diff en porte 27, l'enumeration du body doit couvrir la liste reelle ; (2) TAG -- champ prev: mal forme a la ligne Grain: (prev: #18655 sans TIER/GENRE, forme requise prev: / #) ; (3) G-VAR-2 -- tally declared=2 genre=2 cap=1 sur la lane porteuse (signal merge-gate, pas un fix de PR). En SUS, independant et HERITE DE MAIN : Scripts Tests (CPU) failure @17:50:23Z -- le correctif #19115 n'est arrive sur main qu'a 18:27Z, apres le run ; un rerun ne rafraichit pas la merge ref (precedent ecrit) : l'update-branch attend que #19111 ET #19115 soient tous deux sur main (consigne ai-01 14:53Z), #19111 encore ouvert. Geste fermant cote lane : corriger body (enumeration perimetre complete) + tag prev: (edition de body, sans push), puis update-branch quand les deux correctifs main sont en, puis redemander le re-tampon. Le fond reste sain : Lake build SUCCESS 792 jobs, invariant sorry 0/0 (B.1 au body), blobs byte-identiques, B.0 rc=0 (19 commentaires, 0 nit non leve) -- c'est le habillage (perimetre/tag) et la fenetre main qui bloquent, pas la preuve.

github-actions · 2026-10-04T18:58:13Z

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

closing-keyword + PR-number reference(s) that would auto-close a PR on squash: ['fix #18655 (body, resolves to a PR)']. Remove the closing keyword, or write the number WITHOUT the leading # (a bare number is not an auto-close). See #10101.

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).

…escent

github-actions · 2026-10-04T19:38:41Z

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

closing-keyword + PR-number reference(s) that would auto-close a PR on squash: ['fix #18655 (body, resolves to a PR)']. Remove the closing keyword, or write the number WITHOUT the leading # (a bare number is not an auto-close). See #10101.

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).

jsboige · 2026-10-04T21:15:44Z

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 18687
head: b44f5b1
complete: true
body: read
comments-reviewed: 22
reviews-reviewed: 3
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 57d37207d675a312a2641b684db3c7e377b964fa00a458dc4fd3db20a429e509
diff-files: 27
diff-additions: 55
diff-deletions: 55
checks: BLOCKED
b0: clear
scope: pass
domain: fail
verdict: BLOCKED
[/ADJOINT PREFLIGHT]

note: Re-stamp c432 sur la nouvelle tete b44f5b1 (descente du lake social_choice_lean_peters sous SocialChoice/, 27 fichiers). verdict BLOCKED -- deux rouges sur la tete, mesures ce cycle (fold commits//check-runs, dernier par nom) : (1) Always-on guards failure @19:37:46Z -- l'organe bloquant est close_keyword (les 15 autres organes passent : tag_required success, perimeter success, prev_targets_accepted [18655]). Detail mesure au log du job 111511951877 : {"guard_pass": false, "reason": "closing-keyword + PR-number reference(s) that would auto-close a PR on squash: ['fix #18655 (body, resolves to a PR)']"}. Le corps porte prev: MED/audit-fix #18655 : le token fix #18655 resout #18655 en PR, donc GitHub l'interpreterait comme un ordre de fermeture au squash -- c'est l'incident #10101 (fermer une PR par mot-cle sans la merger). Geste de la lane (au choix) : changer le genre en un genre canonique sans mot-cle fermant (le tag est libre : MED/refactor ou MED/guard decrivent un deplacement mecanique) en gardant le #18655, ou ecrire le numero sans le #. (2) PR gate failure @19:27:34Z -- agrege le precedent. checks: BLOCKED (2 rouges sur la tete). b0: clear (B.0 rc=0 -- la reserve perimeter #11268 est TRAITEE : le tableau de perimetre du corps ventile les 27 fichiers, chaque groupe porte sa raison mecanique, et le diff mesure correspond exactement : 27 fichiers, +55/-55, churn herite du rebase purge au commit 9508356). scope: PASS (le corps documente un seul sujet mecanique -- deplacement de dossier + repointage de ses referenciers -- et le diff y correspond ; NB : 2 fichiers sous .github/workflows/ (lean-ci-matrix.yml, lean-i18n-drift.yml) -- c'est un PR de harnais, merge_ready ne l'auto-mergera PAS, merge manuel ai-01 requis). domain: FAIL (le corps porte un token de fermeture auto qui bloque la CI). Independamment : la reserve ci_lakes de clusterManager-Myia (review 10-02 08:43Z) est declaree traitee par le corps (f7b1dec, c.5963413576 + c.5963974115) mais la revue formelle appartient au tiers -- la review ai-01 la plus recente est APPROVED (06:22:17Z), anterieure a la tete b44f5b1 (19:23Z) : elle ne couvre pas la tete courante.

jsboige · 2026-10-04T21:39:56Z

Geste du secrétariat appliqué — garde organe verte

Le motif du dossier BLOCKED est levé. Le tag était prev: MED/audit-fix #18655 : le genre audit-fix contient fix #18655, et #18655 résout en PR — au squash, GitHub l'aurait fermée automatiquement (incident #10101).

Ligne corrigée, #18655 conservé :

Grain: MED/lean -- lane myia-po-2026:CoursIA -- prev: MED/guard #18655

Genre remplacé par guard, canonique et sans mot-cle fermant. Verification par l'organe reel, pas a l'oeil :

$ python scripts/ci/pr_close_keyword_guard.py --body-file <body> --commits-file <commits>
{"guard_pass": true, "reason": "no closing-keyword + PR-number reference found", "hits": [], "warnings": []}

Perimetre (27 fichiers) inchange : scope: pass de ton dossier tient. Base rafraichie par merge de origin/main. PR de harnais (2 .github/workflows/) -> merge manuel ai-01, comme note.

jsboige · 2026-10-04T23:12:07Z

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 18687
head: b44f5b1
complete: true
body: read
comments-reviewed: 24
reviews-reviewed: 3
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: e0c17f0028f101427bb11ccdc8d4c2c5e832cc577e53d9bcb94bb514e95fdcf1
diff-files: 27
diff-additions: 55
diff-deletions: 55
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
supersedes: 23
supersedes-why: le BLOCKED portait deux motifs, tous deux tombes : (1) close_keyword -- le fix #18655 a ete retire du body (edition, commentaires bot vtr-close-keyword repasses propres) ; (2) checks BLOCKED -- le PR gate est repasse success (re-agrege 22:29Z) et l'advisory scan_md_hierarchy rouge etait un runner mort (annotation « lost communication »), dont le rerun a ete demande par le secretaire : latest-wins sans aucun non-vert a la tete.
verdict: READY
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 18687
organ-rc: 0
[/ADJOINT PREFLIGHT]

note: Dossier c436, re-tampon READY a tete inchangee b44f5b1. Fond crible c432 : descente du module social_choice (refactor lean #4362), perimetre declare et livre, lake build SUCCESS 3038 jobs, B.1 present (table distinct_code_sorry, aucun sorry ajoute ni retire -- descente purement geometrique). B.0 rc=0 mesure ce cycle. Tierce attestation, PR porteuse myia-po-2026:CoursIA (workspace distinct). verdict derive par l'organe.

…chemin SocialChoice/ de social_choice_lean_peters (#19179) La descente peters (#18687, mergée) a déplacé le lake de GameTheory/social_choice_lean_peters vers GameTheory/SocialChoice/social_choice_lean_peters ; le docstring d'usage (l.41-42) citait encore l'ancien chemin — seule référence vivante hors scans et ledgers datés (repéré par ai-01, DM msg-20261004T233050). Co-authored-by: Claude Sonnet 5.5 <noreply@anthropic.com>

jsboige mentioned this pull request Oct 1, 2026

[EPIC] Lean — harmoniser Mathlib, mutualiser les checkouts, regrouper les lakes (anti-proliferation) #4362

Open

github-actions Bot added the consecutive-code-cells Modified notebook has >=2 consecutive code cells (#12797) label Oct 1, 2026

github-actions Bot added the variation-tag-prev-absent Tag Grain sans 'prev: <TIER>/<GENRE> #<PR>' (adjacence G-VAR-3 inevaluable) label Oct 1, 2026

This was referenced Oct 1, 2026

Fix(ML-series,#17825): accents prose FR + réalignement résidu ML-5b (audit #17700) #18661

Merged

Retrait de la coquille repeated_games_lean + repointage des references vivantes (#4362) #18678

Merged

github-actions Bot mentioned this pull request Oct 1, 2026

fix(site,#18422): etendre regen_quarto_render.py pour rendre docs/*.md en HTML #18710

Merged

4 of 6 tasks

github-actions Bot added the pr-overlap Advisory: another open PR touches the same files (organ #13615) label Oct 1, 2026

clusterManager-Myia requested changes Oct 2, 2026

View reviewed changes

github-actions Bot added the stale-guard-red Rouge datant d'une base anterieure au fix du garde (sweep #13321) label Oct 2, 2026

jsboige and others added 2 commits October 3, 2026 02:00

This was referenced Oct 3, 2026

reclass(ict,#18973): renum ICT-42-Crosscoder en ICT-41b — resolution de la collision de slot 42 #18986

Merged

ci(lean,#13751): percolation_lean migre dans la matrice lean-ci — 22e lake, wrapper supprimé #18996

Merged

jsboige mentioned this pull request Oct 3, 2026

[CI][Lean] un lean_lib sans @[default_target] n'est jamais elabore : lake -R build passe au vert sans l'avoir vu #19015

Closed

github-actions Bot mentioned this pull request Oct 3, 2026

docs(cadrage,#17525): tranche 2 — migration Leiden + lens Grothendieck dans docs/cadrage/, 55 liens retablis #19022

Merged

github-actions Bot mentioned this pull request Oct 4, 2026

feat(gametheory,#14032): banc humour consolide -- 18c absorbe 18d (ex-GT-28b) #19040

Merged

6 tasks done

myia-ai-01 requested changes Oct 4, 2026

View reviewed changes

myia-ai-01 approved these changes Oct 4, 2026

View reviewed changes

github-actions Bot mentioned this pull request Oct 4, 2026

chore(catalog): scheduled auto-regenerate (long-lived PR) #19090

Merged

github-actions Bot removed the variation-tag-prev-absent Tag Grain sans 'prev: <TIER>/<GENRE> #<PR>' (adjacence G-VAR-3 inevaluable) label Oct 4, 2026

Merge remote-tracking branch 'origin/main' into feature/4362-peters-d…

b44f5b1

…escent

github-actions Bot mentioned this pull request Oct 4, 2026

Rename(#1650): Serre100 08 suffixe -Lean — audit de suffixe Serre100+Langlands #19128

Merged

jsboige mentioned this pull request Oct 4, 2026

rename(#16231): ICT-45 -> ICT-42b -- accrétion de la famille InoculationBifurcation (chantier C) #19153

Merged

jsboige mentioned this pull request Oct 4, 2026

[EPIC] Nommage canonique et parcours des notebooks — numéros, accrétions, noyaux et catalogue #5081

Open

8 tasks

myia-ai-01 mentioned this pull request Oct 4, 2026

[EPIC] Traduction multilingue du depot via datasetupdater Argumentum (low priority) #1650

Open

myia-ai-01 merged commit 93f1717 into main Oct 4, 2026
176 of 179 checks passed

jsboige mentioned this pull request Oct 4, 2026

fix(lean): exemple d'usage check_lean_orphans -> chemin SocialChoice/ (#18687 suite) #19179

Merged

Conversation

jsboige commented Oct 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Perimetre reel (reserve perimeter, repondu)

Summary

Preuve de build au nouveau chemin (règle B)

Invariant sorry (règle B.1)

Notebook re-exécuté (règle D)

Non-migrations assumées

Effet de bord annoncé

Uh oh!

github-actions Bot commented Oct 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Oct 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Oct 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Oct 1, 2026

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

Uh oh!

github-actions Bot commented Oct 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Golden-Set Execution (H.7 P3)

Uh oh!

github-actions Bot commented Oct 1, 2026

Uh oh!

github-actions Bot commented Oct 1, 2026

Notebook PR Validation: PASS

Uh oh!

github-actions Bot commented Oct 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Path-collision (organ #13359/#13615)

Uh oh!

jsboige commented Oct 1, 2026

Uh oh!

clusterManager-Myia left a comment

Choose a reason for hiding this comment

Uh oh!

jsboige commented Oct 2, 2026

Uh oh!

github-actions Bot commented Oct 2, 2026

Uh oh!

jsboige commented Oct 3, 2026

Uh oh!

myia-ai-01 commented Oct 4, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

myia-ai-01 left a comment

Choose a reason for hiding this comment

Uh oh!

jsboige commented Oct 4, 2026

Uh oh!

myia-ai-01 left a comment

Choose a reason for hiding this comment

Uh oh!

jsboige commented Oct 4, 2026

Uh oh!

github-actions Bot commented Oct 4, 2026

Uh oh!

jsboige commented Oct 4, 2026

Uh oh!

github-actions Bot commented Oct 4, 2026

Uh oh!

github-actions Bot commented Oct 4, 2026

Uh oh!

jsboige commented Oct 4, 2026

Uh oh!

jsboige commented Oct 4, 2026

Geste du secrétariat appliqué — garde organe verte

Uh oh!

jsboige commented Oct 4, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

jsboige commented Oct 1, 2026 •

edited

Loading

github-actions Bot commented Oct 1, 2026 •

edited

Loading

github-actions Bot commented Oct 1, 2026 •

edited

Loading

github-actions Bot commented Oct 1, 2026 •

edited

Loading

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

github-actions Bot commented Oct 1, 2026 •

edited

Loading

github-actions Bot commented Oct 1, 2026 •

edited

Loading

myia-ai-01 commented Oct 4, 2026 •

edited

Loading