docs(lean,#15568): borner la portee du scan junctions au worktree + table 5 machines

docs/lean/junctions-scan-po-2027.md

@@ -27,7 +27,9 @@ Voir aussi :
 | Empreinte totale Mathlib | **0 Go** |
 | Économie jonction-cluster potentielle | **0 GB** |
 
-**Verdict** : **machine po-2027 = réservoir identifié, pas amorcé**. Aucun checkout Mathlib réel n'existe sur cette machine ; les `.lake/packages/` sont soit absents, soit restreints à `config/` (lake jamais exécuté localement). C'est le cas prédit par l'acceptance de #13962 : « Une lane qui trouve 0 checkout réel n'a rien à faire et le dit ».
+**Verdict** : **worktree scanné de po-2027 = réservoir identifié, pas amorcé**. Dans le seul worktree couvert par ce Scan, aucun checkout Mathlib réel n'existe ; les `.lake/packages/` y sont soit absents, soit restreints à `config/` (lake jamais exécuté localement). C'est le cas prédit par l'acceptance de #13962 : « Une lane qui trouve 0 checkout réel n'a rien à faire et le dit ».
+
+> **Portée (#15568)** — le Scan opère depuis le repo-root courant et ne voit donc que **ce worktree-là**. Un checkout Mathlib logé dans un autre worktree de po-2027 échappe à la mesure : c'est le faux négatif déjà observé au c.857 (#14296, un checkout dans un autre worktree que le scanné). Ce rapport ne consigne pas le `git worktree list` de po-2027, donc rien ici ne soutient une formulation au niveau **machine**. Les énoncés de portée machine de ce document ont été bornés au worktree scanné ; pour une mesure réellement machine-wide, il faudrait rejouer le Scan dans chaque worktree listé et publier le total.
 
 ## Sortie verbatim du Scan
 
@@ -81,23 +83,27 @@ Note : l'alignement des manifests (#2611 etape 2) peut elargir les groupes.
 
 ## Comparaison multi-machine
 
-| Mesure | ai-01 (#13962) | po-2026 (#14038) | po-2027 (c.1059) |
-|---|---:|---:|---:|
-| Checkouts Mathlib réels | **17** | 0 | **0** |
-| Jonctions actives | 0 | 0 | **0** |
-| Empreinte totale | ~110 Go | 0 Go | **0 Go** |
-| Groupes mutualisables | 1 (15 lacs) | 1 (19 lacs) | **2 (13 + 9 lacs)** |
-| Économie jonction-cluster | ~90 Go | 0 Go | **0 GB** |
+| Mesure | ai-01 (#13962) | po-2023 (#15070) | po-2024 (#14296) | po-2026 (#14038) | po-2027 (c.1059) |
+|---|---:|---:|---:|---:|---:|
+| Checkouts Mathlib réels | **17** | **3** | 0 | 0 | **0** |
+| Jonctions actives | 0 | 0 | 0 | 0 | **0** |
+| Empreinte totale | ~110 Go | **1,28 Go** | 0 Go | 0 Go | **0 Go** |
+| Groupes mutualisables | 1 (15 lacs) | **2 (13 + 9 lacs)** | 1 (19 lacs) | 1 (19 lacs) | **2 (13 + 9 lacs)** |
+| Économie jonction-cluster | ~90 Go | **0,64 Go** | 0 Go | 0 Go | **0 GB** |
+
+> **Provenance des colonnes (#15568)** — po-2023 vient de #15070 (Scan du 2026-09-07, PR fermée) et po-2024 de `docs/lean/cluster-junctions-c857.md` (#14296, c.857, Scan du 2026-09-02). Ces deux mesures ont été produites par leurs lanes avec le même instrument ; leurs chiffres sont repris **tels quels**, sans re-mesure (acceptance 3 de #15568). Elles partagent la borne de portée décrite plus haut : chacune est une mesure **de worktree**, pas de machine.
 
-Le réservoir identifié sur po-2027 (22 lacs mutualisables) **excède en nombre** celui de po-2026 (19), mais reste à **0 Go** faute de checkout donneur. La conclusion est homogène sur les 3 machines scannées : le réservoir est large, l'amorçage est nul.
+Le réservoir identifié sur po-2027 (22 lacs mutualisables) **excède en nombre** celui de po-2026 (19), mais reste à **0 Go** faute de checkout donneur. Les **cinq** machines mesurées à ce jour — ai-01, po-2023, po-2024, po-2026, po-2027 — partagent le même profil : **le réservoir est large, l'amorçage est quasi nul**. La seule valeur non nulle du plateau est po-2023, dont les 3 checkouts physiques (1,28 Go cumulés) rendent **0,64 Go** récupérables ; sa lane a conclu que cette économie marginale ne justifiait pas un Apply.
 
 ## Cause
 
-**Aucun des 27 lacs n'a exécuté `lake update` localement sur po-2027** : les `.lake/packages/mathlib` n'existent pas ou se limitent à `config/`. La machine porte les **manifests** (qui définissent la dépendance transitive) mais pas les **build artifacts**. C'est cohérent avec le profil po-2027 = worker CPU non Lean dédié (kernel `lean4-wsl` invoqué pour les preuves Lean mais sans cache Mathlib local — exécution sur runners `coursia-lean` self-hosted).
+**Aucun des 27 lacs n'a exécuté `lake update` localement dans le worktree scanné de po-2027** : les `.lake/packages/mathlib` n'y existent pas ou se limitent à `config/`. Ce worktree porte les **manifests** (qui définissent la dépendance transitive) mais pas les **build artifacts**. C'est cohérent avec le profil po-2027 = worker CPU non Lean dédié (kernel `lean4-wsl` invoqué pour les preuves Lean mais sans cache Mathlib local — exécution sur runners `coursia-lean` self-hosted).
 
 ## Conclusion opérationnelle
 
-Le périmètre po-2027 du grain #13962 est **vide**. C'est exactement le cas que l'acceptance prédit : « Une lane qui trouve 0 checkout réel n'a rien à faire et le dit ».
+Le périmètre de po-2027 **dans le worktree scanné** est **vide**. C'est exactement le cas que l'acceptance prédit : « Une lane qui trouve 0 checkout réel n'a rien à faire et le dit ».
+
+Nuance de portée (#15568) : « vide » qualifie le worktree mesuré, pas la machine. Un checkout présent dans un autre worktree de po-2027 resterait invisible ici, et un Apply y aurait alors une cible. La recommandation ci-dessous (« aucune action sur po-2027 ») porte donc sur ce seul worktree.
 
 **Recommandation pour coordinateur** :