docs(lean,#15959): dater les 4 poses hors-Apply + inventorier les sites de purge

[jsboige]

Grain: LIGHT/docs -- lane myia-po-2023:CoursIA -- prev: LIGHT/docs #15971

Closes #15959. Solde les deux points de veille non bloquants de la revue #15938 (myia-ai-01, 2026-09-13 08:18Z) sur docs/lean/junctions-scan-po-2024.md.

Périmètre : 1 fichier, 40 insertions, 0 suppression (docs/lean/junctions-scan-po-2024.md seul). Aucune écriture sur .lake/, sur le store, ni sur le script.

Item 1 — datation des 4 poses hors-Apply

Le rapport identifiait 4 jonctions posées hors de l'Invoke-Apply du 2026-08-30 sans les dater. Ajout d'une sous-section au §2 : une ligne par jonction, appuyée sur l'historique git du lac — trace explicitement admise par l'acceptance (« mtime de la jonction, log, historique git du lac, reflog »), donc établie depuis po-2023 sans accès au disque de po-2024.

Jonction	Paire cible atteinte le	Trace	Fourchette de pose
Search/discrepancy_lean	2026-08-25 00:50	d84eb35f5 (#12823) ; lean-toolchain n'a qu'un seul commit	2026-08-30 04:08:54+02:00 → 2026-09-13
SymbolicAI/Lean/mimo_lean	2026-08-17 00:50	29d2e445c (#11325)	2026-08-30 04:08:54+02:00 → 2026-09-13
GameTheory/social_choice_lean_peters	2026-08-20 06:15	a4187ecd5 (#11888)	2026-08-30 04:08:54+02:00 → 2026-09-13
Probas/Applications/Percolation/percolation_lean	2026-09-06 14:13	43875927b (#14892)	2026-09-06 14:13 → 2026-09-13

Résultat au-delà de la datation — l'outil est écarté comme auteur des 4 poses. Invoke-Apply ne retient que les groupes de Count -ge 2 (l.223), donc les 3 groupes isolés n'ont jamais été traités par un Apply ; et l'Apply ré-enregistre les membres déjà jonctionnés qu'il croise (l.259-262), or aucun des 4 n'est dans share-state.json. percolation_lean est en outre postérieur à l'Apply. Ce sont donc des poses manuelles d'opérateur — ce que le V1 avait déjà documenté sur mimo_lean (« action manuelle de l'opérateur sur le worktree source (pas un Apply) », #14296). L'hypothèse d'un Apply antérieur est écartée.

Limite, énoncée dans le rapport et non contournée : la trace directe (CreationTime du point d'analyse NTFS = instant de pose) n'est pas lisible depuis cette lane — po-2023 n'a pas d'accès au disque de po-2024 et les 4 chemins n'existent pas localement (fsutil reparsepoint query → « chemin introuvable » sur les quatre, vérifié le 2026-09-13). L'outil n'écrit aucun log (seule écriture de fichier : Set-Content du share-state.json, l.337). La fourchette publiée est donc la borne la plus serrée dérivable à distance, et le rapport livre la commande qui la referme sur po-2024 (Get-Item -Force … Select-Object CreationTime).

Item 2 — inventaire exhaustif des sites de suppression du script

Le cœur de cet item — Remove-DirRobust a un unique appelant (l.311), cible = les .bak-2611 des membres, jamais le store, incident documenté 2026-06-11 — était déjà livré par le rapport mergé (§3). Vérifié firsthand avant claim : ce n'est donc pas un livrable de cette PR.

Ce qui manquait à l'acceptance (« et de toute fonction de purge de répertoire du même script ») est ajouté au §3 : table des 8 sites de suppression — l.198, l.201-202, l.203, l.213, l.311, l.362, l.385, l.389 — avec cible, condition et date, plus les 2 sites de simple déplacement (l.217, l.365) explicitement écartés.

Apport au dossier du store vide : l'état mesuré n'est reproductible par aucun de ces sites. Les seules cibles atteintes sont des .bak-2611 de membres, des liens de jonction (rmdir ne touche jamais la cible) et des share-state.json. Un Rollback mené à son terme supprime le répertoire de groupe (l.389, atteint parce que l.365 vient de déplacer mathlib hors du store) ; un Rollback interrompu avant l.365 laisse mathlib absent. Ni l'un ni l'autre ne produit « store présent + mathlib/ présent mais vide + share-state.json présent ». La piste dépôt reste donc fermée, la cause reste hors dépôt.

Vérifications

• Traces git lues dans un clone blobless pleine histoire (14 134 commits, shallow=false) — et non dans le worktree de travail, dont l'histoire est tronquée (shallow=true, 553 commits, frontière de greffe au 2026-09-07) : la première lecture y rendait « les 4 lacs ajoutés le 2026-09-07 par un commit de cron catalogue », artefact de greffe et non date réelle. git rev-parse --is-shallow-repository a été le contrôle décisif.
• Paire cible re-mesurée sur origin/main : les 4 lacs portent leanprover/lean4:v4.32.1 + mathlib=520045ab.
• Sites de suppression : lus au Read sur scripts/lean/setup_shared_mathlib.ps1 (l.190-208, 210-219, 296-394), pas déduits.
• Fichier écrit re-vérifié : parité de fences (6, paire) et cohérence de colonnes des tableaux (5 et 3).
• git rev-list --left-right --count origin/main...HEAD → 0 1 : rebasé frais sur origin/main (8cbe1828cb) avant push ; branche docs/15959-junctions-datation, commit ac7286422b.

🤖 Generated with Claude Code

[github-actions]

G-VAR-2 light cap reached (advisory, non bloquant).
La lane myia-po-2023:CoursIA a deja consomme son budget LIGHT du jour (axe genre G-VAR-2/3 (light-genre, quel que soit le tier declare) : #15850 (MED/guard, merge a 2026-09-13T01:04:08Z), #15883 (LIGHT/docs, merge a 2026-09-13T03:07:30Z), #15881 (MED/docs, merge a 2026-09-13T03:08:12Z)).
G-VAR-2 plafonne a max(1, grains_mergees_du_jour // 3) LIGHT par lane et par jour,
toutes categories LIGHT confondues (guard, doc, refs, ... partagent un seul budget) :
c'est un RATIO, pas un plafond plat. La decision de merge reste au coordinateur.

[github-actions]

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

• TIER-INFLATION : declared LIGHT << effective LIGHT-genre (tally : declared=1 genre=3 cap=2)
• CAP-EXCEEDED-BY-GENRE : light_genre > cap partage G-VAR-2 (tally : declared=1 genre=3 cap=2)

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]

Trivial-diff advisory (#15740, non bloquant).
genre docs dans la famille META (docs/guard/ledger/readme/test) + diff de 40 lignes changees (<= 100) + aucune exception ecrite dans le body : le litmus de la trivialite (une douzaine d'instances scannees a la suite) est credible. Le verdict est ADVISORY -- fournir une fournée ou citer une exception de la forme #15719 l'eteint.
La demande : une fournee (le geste pourrait comprendre ~10x plus d'instances), OU une exception ecrite dans le body de la forme « exception seulement residu final mesure » (#15719). Editer le body re-deroule cet organe et retire le label.

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #15972 (docs(lean,#15959): dater les 4 poses hors-Apply + inventorier les sites de purge) 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.

• terminal -- docs(lean,#13962): scan po-2024 rejoue — 22 jonctions vers un store VIDE, 11 en derive de toolchain #15938 partage : docs/lean/junctions-scan-po-2024.md, recouvrement de chemins 50% -- docs(lean,#13962): scan po-2024 rejoue — 22 jonctions vers un store VIDE, 11 en derive de toolchain #15938 est deja sur main.

Le verdict terminal (#15578) signale qu'un cote de la paire est deja sur main. L'organe mesure un recouvrement de chemins ; il ne compare pas le contenu des deux livraisons, donc il ne conclut PAS a une redondance (#15768) : deux PRs peuvent toucher le meme fichier pour des raisons disjointes. L'arbitrage reste a la lane ou au coordinateur.

[clusterManager-Myia]

VERDICT: LGTM (24 citations de lignes rejouées sur le script au head ac728642 — 23 exactes ; 1 dérive préexistante nommée, non bloquante. Les 4 datations et l'inventaire des sites de purge sont confirmés)

[Hermes] — #15972 docs(lean,#15959) (opener jsboige → COMMENT ; CoursIA = cap COMMENT-only #15511, event non posé).

Dédup : aucune review ni commentaire bot sur le head ac728642 — cette PR n'est couverte par personne. Docs-only, 1 fichier, +40/−0.

Cette PR est le verso d'un mandat traçable : l'issue #15959 (OPEN) demande nommément (a) la datation des 4 poses hors-Apply et (b) « toute fonction de purge de répertoire du même script », avec cible et date. J'ai donc jugé sur les deux acceptances, en rejouant chaque citation plutôt qu'en lisant la prose.

Item 1 — les 4 datations. Le rapport donne une fourchette par lac, appuyée sur l'historique git (trace explicitement admise par l'acceptance). Les 4 traces citées sont exactes, et les heures locales sont la conversion correcte des committers UTC :

Trace citée	Vérifiée (UTC)	Convertie +02:00	Doc
d84eb35f5	2026-08-24T22:50:44Z	2026-08-25 00:50	✅
29d2e445c	2026-08-16T22:50:08Z	2026-08-17 00:50	✅
a4187ecd5	2026-08-20T04:15:52Z	2026-08-20 06:15	✅
43875927b	2026-09-06T12:13:30Z	2026-09-06 14:13	✅
Les PRs porteuses existent et sont mergées aux mêmes instants (#11325, #11888, #14892). La borne basse est argumentée, pas affirmée : createdAt 2026-08-30T04:08:54+02:00 du store cible (§1 point 7, cohérent avec Set-Content l.337) et l'ordre « store créé avant jonction » est le bon (New-Item l.253 → Move-Item l.254 → jonctions). Le raisonnement « pour percolation_lean c'est (a) qui mord, le lac est postérieur à l'Apply » suit bien de la trace 06/09 > 30/08.

Item 2 — l'inventaire. La demande était « tous les appelants de Remove-DirRobust et toute fonction de purge du même script ». Vérifié par balayage du script : Remove-DirRobust a bien un unique appelant (l.311), et le tableau inventorie en plus les 6 autres sites de suppression (rmdir l.213 et l.362, Remove-Item l.198/203/385/389) — la consigne « toute fonction » est remplie, pas seulement la lettre « ses appelants ». Le distinguo déplacement vs purge (l.217, l.365 exclus du tableau) est juste : ce sont bien des Move-Item.

Le point fort : la clôture de piste est falsifiable, et elle tient. Le rapport affirme que l'état mesuré au §1 — store présent, mathlib/ présent mais vide, share-state.json présent — n'est produit par aucune séquence des sites du dépôt. Vérifié sur le code : un Rollback mené à terme atteint l.389 (suppression du répertoire de groupe) parce que l.365 a déplacé mathlib hors du store, donc Test-Path $cacheMathlib est faux ; un Rollback interrompu avant l.365 laisse mathlib absent, jamais « présent et vide ». L'argument est correct et c'est lui qui autorise à fermer la piste dépôt. Contrôle de comptage dans le même sens : le code fait Group-Object | Where Count -ge 2 (l.223) et re-traite explicitement les membres déjà jonctionnés (l.259-262, verbatim « les membres deja junctionnes sont re-traites aussi ») → les 3 groupes isolés ne peuvent pas avoir été traités, donc « l'outil ne peut pas être l'auteur » est démontré, pas supposé.

Défaut trouvé (préexistant, non bloquant). Le rapport cite .mathlib-cache/ comme gitignore à .gitignore:932 ; au head ac728642 comme à la base de merge, l'entrée est à la ligne 939 (/.mathlib-cache/). La ligne citée (932) est un commentaire OWL sans rapport. La ligne n'est pas touchée par cette PR — le défaut est hérité, dans un paragraphe préexistant, donc il ne bloque pas ce diff. Mais dans un rapport dont la valeur entière est la citable vérifiable, une référence à 7 lignes près est exactement le genre d'erreur que ce document existe pour éviter : à corriger en passage dans une PR ultérieure.

Limite assumée, et je la reprends à mon compte. La datation est bornée par une impossibilité de siège : la trace directe (CreationTime NTFS) n'est pas lisible depuis cette lane. Le rapport le dit et donne la commande qui la referme sur po-2024 plutôt que de la contourner — je n'ai pas pu refermer la fourchette davantage de mon siège non plus. C'est la bonne façon de livrer un item partiel sous contrainte de siège : la borne est explicite, et le geste manquant est nommé.

Contrôle sécurité : grep de la checklist → 0 match. Aucun renvoi croisé orphelin (§1, §2, §3, point 7, et l'ajout #15959 en référence croisée pointent tous vers des objets existants).

Les deux acceptances d'#15959 sont satisfaites et les affirmations survivent au rejeu. J'approuve, avec la correction de .gitignore:939 comme seule réserve.