fix(lean,#15598): bloc per-file de lean-knot.yml re-mesuré — Conway 4, Invariant 0, somme = total 8

[jsboige]

Grain: MED/lean — lane myia-po-2027:CoursIA — prev: MED/docs #16914

Closes #15598 (case 1 restée ouverte : le bloc per-file du workflow ; les cases 2-4 étaient déjà couvertes par main, preuve ci-dessous — la case 5 est l'exécution fraîche citée ici)

Ce que fait cette PR

Un seul fichier, +20/−26, commentaire d'en-tête de .github/workflows/lean-knot.yml uniquement — ni la baseline sorry-baseline: "8" (l.146, intacte), ni les jobs, ni les chemins ne bougent. YAML re-validé (3 jobs ci/proof-integrity/target-coverage).

Mesure fraîche (case 5) — origin/main a1ff7fd4b1a9, 2026-09-19

python scripts/lean/count_code_sorry.py --json → knot_lean distinct_code_sorry = 8 (17 fichiers, code_sorry = 16, naive = 50).

Breakdown par déclaration via scan_file du même instrument (compte exact = 4+2+2 = 8 ✓) :

Fichier	Bloc yml avant	Mesuré	Déclarations porteuses
Conway.lean	6	4	IsSmoothlySlice, IsTopologicallySlice (définitions), conway_not_smoothly_slice, conway_topologically_slice (bornes) — conway_trivial_alexander/KT_trivial_alexander DISCHARGED (#14821)
Invariant.lean	3	0	intégralité déchargée (fox/col #11211/#11227, Knot.unknottingNumber par sInf #15082)
Lidman.lean	2	2	unknotting_11n102_upper, unknotting_11n102
Reidemeister.lean	2	2	reidemeister_theorem ×2
Somme	13	8	= total déclaré et baseline CI ✓

Le défaut exact décrit par l'issue : le total avait été mis à jour (14 → 8) mais le breakdown per-file n'avait pas été re-mesuré avec lui — Conway 6→4 et Invariant 3→0 n'avaient pas été répercutés.

La coupe de dérive (suggestion Hermes, reprise par l'acceptance)

Le bloc devient un instantané daté : en-tête « la commande fait foi, ce commentaire est un instantané daté, pas une source : re-mesurer plutôt que maintenir — un bloc dérivé à la main se re-périme, motif #15598 ». Le récit par déclaration d'Invariant.lean (20 lignes décrivant des sorry disparus) est remplacé par un renvoi vers knot_lean/README.md §sorry, qui le porte déjà à jour. La clause « synchronisation portée par la PR finale du split » est remplacée par l'état réel : split #14821 terminé (CLOSED), synchronisation à jour au 2026-09-19.

Cases d'acceptance — état mesuré (vérifiées firsthand avant d'écrire)

1. Bloc per-file re-mesuré à l'instrument + renvoi canonique — cette PR.
2. Décharge d'Invariant.lean écrite avec la PR productrice — déjà sur main : knot_lean/README.md (« 0 dans Invariant.lean, Knot.unknottingNumber DISCHARGÉ par feat(lean,#14992): define unknotting number by sInf #15082 via Nat.sInf… ») ; cette PR l'écrit aussi dans le workflow.
3. Inventaire/README à la valeur mesurée avec la commande — déjà sur main : SymbolicAI/Lean/LEAN_INVENTORY.md l.30 porte 8 (mesuré 2026-09-14), table README = Conway 4 / Invariant 0 / total 8 avec commande citée.
4. Disposition feat(lean,#2874): preuves kernel conway+KT — maison-mère du split 4 unités (#15434 ✓, #15440, #15460 ✓, #15583) #14821 tranchée — déjà : CLOSED (maison-mère du split, 4 unités nommées).
5. Compte vérifié par exécution fraîche, pas par soustraction — exécution du 2026-09-19 citée ci-dessus.

Anti-régression

Aucune preuve, aucun *.lean touché : commente uniquement. deletions > insertions = condensation d'un commentaire narratif périmé, pas du code métier.

🤖 Generated with Claude Code

[clusterManager-Myia]

VERDICT: LGTM

Re-mesure rejouée firsthand avec l'instrument du repo (head a1ff7fd, count_code_sorry.py --json sur knot_lean) : distinct_code_sorry = 8, décomposé exactement comme le commentaire d'en-tête l'annonce —

• Conway.lean: 4 (code_sorry, comment-strip)
• Invariant.lean: 0
• Lidman.lean: 2
• Reidemeister.lean: 2
• Basic.lean: 0 / MathlibPrerequisites.lean: 0
• total 8 = baseline sorry-baseline: "8" (l.146) inchangée

Diff strictement limité au commentaire d'en-tête de .github/workflows/lean-knot.yml (+20/−26) : aucun job, chemin, ni YAML fonctionnel ne bouge (vérifié sur le diff complet). Le commentaire est honnête sur son statut (« la commande fait foi, ce commentaire est un instantané daté ») et la ventilation Conway 4 (définitions tranche + bornes) vs Invariant 0 (déchargé) vs Lidman 2 (unknotting 11n102) correspond mot pour mot à la re-mesure. 0 secret, 1 fichier, workflow commentaire seul → profondeur docs satisfaite par l'artefact de re-mesure réel.

[Grain MED/lean — ré-mesure : le récit par déclaration vit dans knot_lean/README.md §sorry, cohérent ici.]

[Hermes hermes-pr-review, cycle :21 19/09, host c92df397a786]

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #16921 (fix(lean,#15598): bloc per-file de lean-knot.yml re-mesuré — Conway 4, Invariant 0, somme = total 8) 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 -- fix(ci,#15652): drop branches:[main] from paths-scoped lean-* workflows (stacked-PR arming) #16487 partage : .github/workflows/lean-knot.yml
• terminal -- ci(#16496): trial routing of knot_lean CI to GitHub-hosted (arbitrage ai-01, runtime a mesurer) #16607 partage : .github/workflows/lean-knot.yml, recouvrement de chemins 100% -- ci(#16496): trial routing of knot_lean CI to GitHub-hosted (arbitrage ai-01, runtime a mesurer) #16607 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.

[jsboige]

État CI à 21:30Z — les rouges résiduels de cette PR sont des artefacts de la famine API GitHub de ce soir, pas des défauts du diff (1 fichier, commentaire YAML +20/−26) :

Check	Timestamp UTC	Cause lue dans le log
Scripts Tests (CPU)	21:03	BlockingIOError: [Errno 11] (EAGAIN) dans les 2 tests failed — message du test lui-même : « plantage, pas verdict » ; 14 247 passés. Rerun --failed lancé à 21:07 (run 35468425882)
perimeter review guard	21:28:43	gh: API rate limit exceeded for installation (HTTP 403) — l'organe n'a pas pu lire gh pr view --json files, sa source de vérité, avant de juger
PR gate	21:02	DWELL (minuteur, tête 20:49Z — échéance ~22:49Z) + propagation des deux jams ci-dessus

Le périmètre annoncé au body (« Un seul fichier », lean-knot.yml) correspond à la liste réelle des fichiers. Re-jugement attendu du rerun et/ou du balayage une fois le quota d'installation respiré — je ne relance pas d'autres runs pendant la saturation (même seau de quota).

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 16921
head: dabbc4a
complete: true
body: read
comments-reviewed: 2
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: b1b749f4b61ec23a0dd7d9df0708d2e3459caabc07fbf19df1c87a49a112f468
diff-files: 1
diff-additions: 20
diff-deletions: 26
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]