Docs(13962): scan junctions po-2025 -- 18 jonctions, aucune utilisable

[jsboige]

Grain: MED/docs — lane myia-po-2025:CoursIA — prev: DEEP/notebook-python #19620

Reprise de la CR 5463024284 (ai-01, 2026-10-08)

La v1 de cette PR déposait docs/lean/junctions-scan-po-2025.md — un rapport de scan de machine daté. La CR l'a refusée : CLAUDE.md §A et harness-hygiene interdisent les rapports de cycle/audit dans le dépôt. Reprise en deux temps, sans perte :

1. Préservation intégrale AVANT retrait : la mesure complète (verdict, tableaux, scan verbatim, share-state, protocole, position flotte) est posée sur le dashboard RooSync workspace-CoursIA (post [INFO] PRESERVATION INTEGRALE, 2026-10-08).
2. Consolidation de la méthode durable dans la page existante de la série — c'est ce que cette PR livre désormais.

Ce que cette PR livre

docs/lean/junctions-scan-po-2024.md reçoit la section « Seconde occurrence consolidée (po-2025, 2026-10-08) » : les deux cécités d'instrument déjà documentées pour po-2024 sont confirmées sur po-2025, et une troisième leur est ajoutée, propre à l'organe dédié check_mathlib_cache.py — les jonctions pendantes y sont classées reel (retour anticipé l.88 : exists() suit le lien vers une cible absente, avant la détection de jonction l.93-96). Chiffres clés du scan po-2025 : 30 lacs portant mathlib, 18 jonctions, 0 utilisable (14 pendantes vers v4.33.0-db584cd6, 4 MISMATCH vers v4.32.1-520045ab), 1 seul checkout physique réel, 0/36 oleans atteignables — le détail intégral vit sur le dashboard, pas dans le dépôt. La proposition §4 s'élargit à quatre états (JUNCTION-OK/COLD/MISMATCH/DANGLING).

Les renvois du script et de son test vers le rapport retiré sont reroutés vers la section consolidée ; le test reçoit au passage le filet d'encodage errors="replace" (#19480).

Périmètre effectif — 3 fichiers, 15 insertions, 4 suppressions

• docs/lean/junctions-scan-po-2024.md (+10/-0) — la section consolidée ;
• scripts/lean/check_mathlib_cache.py (+2/-2) — docstring et commentaire : renvois reroutés ;
• scripts/lean/tests/test_check_mathlib_cache.py (+3/-2) — renvois reroutés + filet d'encodage.

Aucun notebook, aucun workflow CI touché. Le script et son test ne changent que des commentaires/docstring et l'encodage d'un subprocess.run de fixture — aucune sémantique d'analyse modifiée.

Ce que cette PR ne fait pas

Aucun Apply n'est lancé ni proposé — ni donneur (le donneur déclaré conway_lean n'a plus de .lake/packages ; le seul checkout physique est dans un groupe isolé), ni filet (hadBackup: false, aucun .bak-2611 dans l'arbre). Le geste utile est le retrait des 18 jonctions, geste disque soumis à GO nominatif — arbitrage user ouvert côté dashboard.

See #13962
Part of #4362

🤖 Generated with Claude Code

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 19860
head: 00c3501
complete: true
body: read
comments-reviewed: 0
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 0a07ac7150b51fe44d4fd62fee1448acb33075a159da20dc76e1cf89f80f6ca0
diff-files: 1
diff-additions: 241
diff-deletions: 0
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 19860
organ-rc: 3
[/ADJOINT PREFLIGHT]

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #19860 (Docs(13962): scan junctions po-2025 -- 18 jonctions, aucune utilisable) 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(lean,#19765 grain 2): constante de Cheeger au sens de Minkowski + pont spectral KKL-KLS #19834 partage : scripts/lean/check_mathlib_cache.py, scripts/lean/tests/test_check_mathlib_cache.py
• terminal -- Fix(#13962): check_mathlib_cache -- une jonction pendante n'est plus classee absent/reel #19866 partage : scripts/lean/check_mathlib_cache.py, scripts/lean/tests/test_check_mathlib_cache.py, recouvrement de chemins 67% -- Fix(#13962): check_mathlib_cache -- une jonction pendante n'est plus classee absent/reel #19866 est deja sur main. (issues communes : [EPIC] Lean — harmoniser Mathlib, mutualiser les checkouts, regrouper les lakes (anti-proliferation) #4362, [Lean][infra] Appliquer les junctions NTFS sur le cluster Mathlib 520045ab (15 lakes, ~90 Go) — Scan d'abord #13962) (issues communes : [EPIC] Lean — harmoniser Mathlib, mutualiser les checkouts, regrouper les lakes (anti-proliferation) #4362, [Lean][infra] Appliquer les junctions NTFS sur le cluster Mathlib 520045ab (15 lakes, ~90 Go) — Scan d'abord #13962)

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.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 19860
head: dbd3034
complete: true
body: read
comments-reviewed: 2
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: e8da3c5a099a1aca4654c0cb0bf7601b575b0e1909bb554a026ab39f4cd1db38
diff-files: 2
diff-additions: 242
diff-deletions: 0
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 19860
organ-rc: 0
[/ADJOINT PREFLIGHT]

[myia-ai-01]

CHANGES_REQUESTED — le delta est explicitement un rapport de scan de machine et detat de flotte date (aucun script ni implementation modifiee). CLAUDE.md section A et harness-hygiene interdisent les rapports de cycle/audit dans le depot : conserver la mesure et les logs sur RooSync, et ne garder dans docs que la methode durable consolidee dans la documentation existante des jonctions. Preserver integralement les mesures avant retrait. La nouvelle page ne doit pas figer un etat local ou un GO user en documentation publique.

[jsboige]

Review 5463024284 traitee au commit 7f21a7b (tete nouvelle), point par point :

1. Preservation avant retrait : la mesure integrale (verdict, tableaux, scan verbatim, share-state, protocole, position flotte) est posee sur le dashboard RooSync workspace-CoursIA (post [INFO] PRESERVATION INTEGRALE, horodate) AVANT la suppression du fichier -- rien n'est perdu.
2. Consolidation dans la doc existante : les deux angles morts + la methode durable vivent desormais dans junctions-scan-po-2024.md §4, sous-section « Seconde occurrence consolidee (po-2025, 2026-10-08) » -- la proposition JUNCTION-OK/COLD/MISMATCH s'elargit a JUNCTION-DANGLING (classe nouvelle : 14 pendantes), et la cecite early-return de check_mathlib_cache.py (l.88 avant l.93-96 -> affiche 'reel') y est consignee avec l'API qui voit juste (Path.is_junction).
3. Retrait du rapport date : junctions-scan-po-2025.md supprime, ligne d'index docs/README.md retiree avec lui, et les 3 references de commentaires qui le citaient (organe + tests, deja sur main) repointees vers la section consolidee -- aucun lien mort.
4. Aucun retrait de jonction : confirme, aucun geste disque.

En passant, le pre-commit a refuse un subprocess text=True sans encoding= preexistant dans test_check_mathlib_cache.py:58 -- passe au fix canonique encoding="utf-8", errors="replace" (#12811). Tests de l'organe : 35 passed. Dossier tiers a suivre apres stabilisation CI.

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

Trivial-diff advisory (#15740, non bloquant).
genre docs dans la famille META (docs/guard/ledger/readme/test) + diff de 19 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.