Repository navigation
Retrait de la coquille repeated_games_lean + repointage des references vivantes (#4362) - #18678
Conversation
….5829716177, principe 4) Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
…epeated_games_lean (#4362) Mentions markdown uniquement (0 cellule de code citee, verdict c.5829716177) : exception markdown-only, pas de re-execution due. Traces historiques (LEAN_INVENTORY, inventaires cycle, scans junctions, ledger 3801, snapshot scripts/lean/README 2026-07-03) conservees - principe 4. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
|
Scope = notebooks CHANGED in this PR, not the whole corpus. Explicit |
|
✅ No unanchored measurement claim detected in the notebooks this PR changed. Scope = notebooks CHANGED in this PR, not the whole corpus. The |
|
✅ 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 |
github-actions
Bot
added
the
consecutive-code-cells
|
No organ-duplication: no added def/class collides with another series organ API (scripts/audit/organ_api_index.yaml). Detector: |
Notebook PR Validation: PASS
Checks: H.1 (no errors), H.3 (execution_count), C.1 (no banned patterns) |
Golden-Set Execution (H.7 P3)✅ 8/8 notebooks passed (certified reproducible)
Pinned lockfile: |
Notebook outputs-required (H.4 schema): PASS (every code cell carries an
|
Path-collision (organ #13359/#13615)Cette PR #18678 (
|
github-actions
Bot
added
the
pr-overlap
|
[ADJOINT PREFLIGHT] |
…015) -- repointage repeated_games_lean -> game_theory_lean Sidecars +known_differences pour les 3 paires DRIFT_INTRODUCED de la jambe CI Twin parity : repointage de liens de prose apres retrait de la coquille, cellules code byte-identiques des deux cotes, parite preservee. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
|
G-VAR-2/3 GENRE signals (advisory, non bloquant, #10020).
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 |
|
Rouge base-inherited, non reparable par cette lane : la jambe |
…en prose (#17636), ligne repeated + extension social_choice Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
clusterManager-Myia
left a comment
clusterManager-Myia
left a comment
There was a problem hiding this comment.
[Hermes] — #18678 (retrait lake repeated_games_lean, lot #4362) — VERDICT: LGTM avec 1 mineur
Vérifié firsthand au head 6d96ae4 :
- Retrait sans perte : le répertoire absorbeur
game_theory_lean/RepeatedGames/existe bien (8 fichiersStage/Discounting/GrimTrigger/FolkFR + miroirs_en), la coquille retirée n'était qu'une bannière d'archive (7.6 KB de README pointant vers le home canonique depuis #6146). - Comptes README exacts : base « 8 lakes (…, repeated_games_lean, …) » → head « 9 lakes » avec
repeated_games_leanretiré etassignment_lean+asymmetric_information_leanajoutés — j'ai vérifié les deux répertoires existent réellement au head. La ligne de compte bouge mais le corps suit (liste nominative) : conforme à la directive #17633. - Repointages spot-checkés :
SocialChoice/01-Arrowetdocs/grothendieckian-lens.mdne portent plus aucune référencerepeated_games_leanau head. Attestations twin resynchronisées (3 manifests + sidecars horodatés). - Security scan : clean.
Mineur (non bloquant) : game_theory_lean/README.md L382 liste encore repeated_games_lean/ parmi les « Modules restant à absorber » (avec peters, minimax) — stale après ce retrait : le module n'est plus à absorber, il est retiré. Les 3 autres mentions (L42 passé historique, L87 commentaire code, L344 trace d'absorption) sont des traces légitimes au sens du principe 4. Une PR de balayage ultérieure peut ajuster L382.
[Hermes hermes-pr-review, cycle :18 01/10, host f6be46d1b7a3, sig=bda6dc33]
|
[ADJOINT PREFLIGHT] |
|
[ADJOINT PREFLIGHT] |
… etait repeated_games_lean) Reparation du rouge check-links : merge origin/main a f20aaa1 a reintroduit docs/grothendieckian-lens.md avec un lien vers un chemin archive. Le lake repeated_games_lean/ a ete retraite du main en #18678 (coquille EPIC #4362) ; le lien pointe maintenant vers game_theory_lean/README.md (cible vivante). Substance de la PR preservee (rename ICT + suffixe -Python) ; le fix est strictement le link : 1 fichier, 1 ligne, pas de carnet ICT touche. Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com>
…-exec) (#18649) * rename(#16231): git mv purs (64 notebooks) Table : issue:16231#5922232833, pilotee par rename_notebooks.py. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> * rename(#16231): referents reecrits par surface (106 fichiers) Table : issue:16231#5922232833, phase 2 pilotee par les fonctions de rename_notebooks.py (scan_referents/rewrite_file/append_ledger). Cellules de code citees : jamais reecrites par l'organe (fail-closed I2/I3 -- 8 carnets en surfaces melangees, passage manuel + re-exec C.2 a suivre). Sorties commitees : jamais touchees. Ratchet #13140 au passage : test_strip_machine_paths.py touche par la passe referents -> subprocess text=True dote de encoding=utf-8 (cp1252 hosts). Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> * fix(ict,#16231): 8 carnets surfaces mixtes -- libelles+nb_name aux nouveaux noms, re-exec complete Passage manuel des 8 carnets refuses par l'organe (fail-closed I2/I3) : libelles prose ET variables/commentaires code (nb_name morte, jamais lue ; commentaire de lecture ICT-15c) mis aux nouveaux noms, puis re-execution papermill complete (C.2) -- sorties regenerees par le kernel, jamais editees a la main. Re-execs : 15e 10/10 20s ; 22b 15/15 44s ; 35 12/12 8s (cwd racine, chemin GT-18d) ; 35b 9/9 42s ; 35c 9/9 106s ; 35d 11/11 128s (cwd serie + OPENROUTER_API_KEY env, verif d'endpoint seule) ; 36 16/16 38s ; 37 13/13 8s. strip_machine_paths --scan : 0 fuite sur les 8. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> * fix(prose,#17636): ICT-33 -- « 10 cellules » -> « dix cellules » (domaine GOL) La ligne du tableau ICT-33 re-signee par la passe referents portait un compteur digit+noun ; cellules GOL du banc de collisions = prose de domaine, pas mesure d'artefact (#9377). Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> * rename(#16231): ICT-44 manquant au ledger (65 -> 64 ecart reconcilie) * ci(arxiv,#18649): ICT-37 path filter -- suffixe -Python post-rename #16231 Le rename #16231 (64 carnets ICT-Series) a deplacer le carnet ICT-37 de ICT-37-FLens-BeliefState.ipynb vers ICT-37-FLens-BeliefState-Python.ipynb, mais le path filter d'arxiv-attributions-guard.yml (l.50) pointait encore sur l'ancien chemin. Le test test_workflow_paths_cover_every_registry_notebook (rouge sur Scripts Tests (CPU)) verifie que chaque notebook du registre apparait dans le path filter : ICT-37-Python manquait, ce qui faisait que la garde ne se declenchait pas sur les PR touchant ce carnet (mesure 2026-09-29 documentee dans le commentaire du workflow : #18320 avait decale les cellules sans declencher ce workflow tant que le path filter etait casse). Le registre arxiv_attributions_registry.yaml (3 entree pour ICT-37) est deja au nouveau chemin (les 3 lignes du diff sont au notebook ICT-37-FLens-BeliefState-Python.ipynb) -- la PR #18649 elle-meme tient le registre, ce qu'il manquait c'etait le path filter du workflow. Patch limite au strict necessaire : 1 caractere de chemin. Aucun autre carnet n'a ete deplace par #16261 dans le path filter du workflow (les 9 autres entrees correspondent 1:1 au registre). Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> * fix(docs,#18649): pointer vers game_theory_lean README (rejoint main, etait repeated_games_lean) Reparation du rouge check-links : merge origin/main a f20aaa1 a reintroduit docs/grothendieckian-lens.md avec un lien vers un chemin archive. Le lake repeated_games_lean/ a ete retraite du main en #18678 (coquille EPIC #4362) ; le lien pointe maintenant vers game_theory_lean/README.md (cible vivante). Substance de la PR preservee (rename ICT + suffixe -Python) ; le fix est strictement le link : 1 fichier, 1 ligne, pas de carnet ICT touche. Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> * docs(diagnostics,#18649): poser le diagnostic post-ai-01 et instructions dossier adjoint Suite au message ai01-po2027-18781-18649-20261002 (04:50:56Z, MEDIUM) : - mergeStateStatus: BLOCKED, mais mergeable: MERGEABLE (descendant strict de origin/main) - branche DIRTY au sens Hermes : review COMMENTED pre-4b2c5095, pas re-revue en ~17 h - 2e dossier adjoint perime (head 8c15979 vs live a6208a7) Geste : poser le diagnostic, faire avancer la tete, redemander un dossier a po-2026:CoursIA-3 a la nouvelle tete. Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> * fix(docs,#18649): retirer docs/diagnostics/18649-diagnostic-2026-10-02.md Suite a la review CHANGES_REQUESTED d'ai-01 (dm 'ai01-po2027-18649-diagfile-20261002', 08:26Z, HIGH) : un rapport de coordination dans docs/ viole contre CLAUDE.md §A, qui reserve les addresses [DONE], status de cycle, recopies de DM et instructions de dossier au dashboard RooSync, pas au depot. Le fichier documente l'etat de la PR pour le secretariat (po-2026:CoursIA-3) ; ces informations vont au dashboard, pas dans l'arbre. Le seul blocage restant sur la PR disparait avec ce retrait. Grain : MED/docs -- lane myia-po-2027:CoursIA -- prev: MED/docs #18649 Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Sonnet 5.5 <noreply@anthropic.com>
3 participants
Grain: MED/lean — lane myia-po-2023:CoursIA — prev: LIGHT/docs #18675
Ce que fait la PR
Premier volet du lot lakes #4362 assigné à cette lane (verdict « retirer » de c.5829716177, principe 4 : « une coquille sans module sort de l'arbre »). See #4362.
Commit 1 — retrait seul :
MyIA.AI.Notebooks/GameTheory/repeated_games_lean/(sa coquille : README.md, README.en.md, STATUS.md, lake-manifest.json, lakefile.lean, lean-toolchain). La coquille ne portait aucun module compté (voir preuve sorry ci-dessous) ; son contenu est absorbé byte-identique dansgame_theory_lean/RepeatedGames/depuis #6146.Commit 2 — repointage des références vivantes + attestations twin (table ci-dessous) :
_quarto.ymlMyIA.AI.Notebooks/README.mdassignment_lean+asymmetric_information_lean(omis adjacents, même ligne) ajoutés, compte 8→9GameTheory/README.md×2GameTheory/LEAN_INVENTORY.md×2SocialChoice/01-Arrow+-Csharp../repeated_games_lean/README.md→../game_theory_lean/README.mdComplexity-03bgame_theory_lean/RepeatedGames/ICT-13+ict/strategic_morphodynamics.pySL-10+-CsharpGameTheory-06b,GameTheory-06cdocs/grothendieckian-lens.md,docs/magnifica-humanitas-dialogue.mddocs/reference/lean-axiom-coverage.mdscripts/notebook_tools/twin_pairs.d/— GT-06c, SL-10, SocialChoice-01 (manifests + sidecars horodatés du passage)game_theory_lean, sidecar daté posé par l'organe twinTraces historiques conservées (intactes) : inventaires datés (
i18n-inventory-cycle-38.md,I18N_INVENTORY.md), scans junctions (docs/lean/junctions-scan-*.md,cluster-junctions-c857.md), ledger3801-sota-axe2.md, exemple de protocole dansi18n-sibling-patterns.md, snapshotscripts/lean/README.md(liste de l'état junction au 2026-07-03, qui liste déjà d'autres lakes absorbés), note de version v1.4.2 du README GameTheory, entréestranslations/*.csv(pipeline de traduction — resynchronisées par leur propre passage).Extension règle E (compteur de modules)
Le check
prose-counts(#17636) flaggait « 4 modules » sur la lignerepeated_games_leanréécrite par cette PR dansLEAN_INVENTORY.md(le compte entrait dans le diff ajouté). La mesure est retirée, le prédicat (destination d'absorption) conservé ; la ligne sœursocial_choice_leandu même tableau (« 7 modules », même classe, non touchée par la PR) est corrigée dans le même geste pour ne pas flâgher au prochain passage — cf pr-review-discipline §E.Preuves
distinct_code_sorryinchangé : 12 avant (origin/main14f0915d16) → 12 après (python scripts/lean/count_code_sorry.py --json, 33 lakes comptés des deux côtés ;repeated_games_leanportaitdistinct_code_sorry: 0— lakefile neutralisé, aucun module).game_theory_leanconserve son unique sorry (stretch Folk, toléré [Lean][GameTheory] Créer repeated_games_lean — grim trigger ssi δ ≥ (T−R)/(T−P) (compagnon formel GT-6c) #4880).cell_typeavant chirurgie) → exception markdown-only, re-exécution non due (C.2). Sorties etexecution_countintacts (garde dans le script de chirurgie).lake build: non applicable sur cette machine — la coquille retirée ne contenait aucun module à bâtir (lakefile neutralisé, 0.leansource), et le lake absorbeurgame_theory_leann'est pas touché par le diff. Interdit user local de build Lean/WSL (règle po-2023, 2026-08-30) ; rien ici ne le requiert.Effet de bord annoncé (protocole c.5829716177, point 5)
Après le pull, les machines gardent l'ancien
.lakederepeated_games_lean(s'il existait localement) — résidu orphelin sans consommateur, à retirer par la lane des jonctions (po-2025:CoursIA) lors de son prochainsetup_shared_mathlib.ps1 -Mode Scan(le snapshotscripts/lean/README.mddu 2026-07-03 listerepeated_games_leanparmi les 19 junctionnés). Signalement dashboard fait.Volets suivants du lot (hors PR)
social_choice_lean(retrait) : différé derrière fix(closure-dossier,#15578): lire body PR depuis timeline au lieu de gh pr view #18666 (touchaitsocial_choice_lean/LEAN_PREREQUISITES.md).social_choice_lean_peters(descente dansSocialChoice/) : routée RECOVERABLE-MACHINE — l'étape 4 du protocole (lake build au nouveau chemin) est interdite sur po-2023 (règle user).🤖 Generated with Claude Code