docs(lean,#2874): knot_lean README FR+EN -- l'etat reel du code : marquee prouve #11958

[jsboige]

Grain: MED/readme — lane myia-po-2027:CoursIA — prev: DEEP/lean #16075

See #2874 — compagnon documentaire de #16075 (migration 4.33.0), sans en dépendre :
branché sur origin/main (f412b51), tout ce qui suit est mesuré sur ce SHA.

Résumé

Les deux README de knot_lean racontaient un état du code qui n'existe plus. Le
défaut central : le marquee tricolorable_invariant y est présenté OPEN (sorry) et
gated sur une re-modélisation connectée R2/R3 « en revue » — or cette re-modélisation
est livrée et mergée (Reidemeister2Connected #11469, transferts R3 connectés
#11903, induction du maître #11958), et Invariant.lean est sorry-free depuis.
L'audit §E fichier-entier a été délégué à un sous-agent read-only puis re-vérifié
firsthand claim par claim (G.1) : chaque correction ci-dessous est ancrée sur une
mesure contre origin/main.

Un seul sujet : l'honnêteté d'état de la documentation du lake — aucun .lean, aucun
méta-fichier de build n'est touché.

§E — Audit fichier-entier (preuve)

knot_lean/README.md (479 l.) + README.en.md + les claims knot_lean de
LEAN_INVENTORY.md, audités contre le disque au SHA f412b513c819. 22 claims
vérifiés, chacun avec commande + résultat ; voici les corrigés (les OK sont omis —
structure : 6 modules Knots/*.lean + siblings _en (12 au total), dépendances externes, baseline CI
"10"/real, revue humaine déclarée manquante, etc.) :

Claim auditée	Était	Devient (mesuré)
tricolorable_invariant (Verdict table, Scaffolding, Verrou, Conclusion, Prochaines étapes — FR+EN)	OPEN (sorry), gated sur remodel « en revue »	PROUVÉ (#11958), Invariant.lean L3535 ; « Le verrou — levé » ; la voie « prochaine étape 1 » est cochée faite
Colonne « sorry (prose, CI) » Invariant/Conway/total	15 / 11 / 37	5 / 12 / 28 (grep -c sorry par fichier FR, re-mesuré : 3+2+5+12+4+2 = 28 — l'ancien 37 ne se reproduisait pas sous sa propre définition)
Note post-#13312 « rend distinct_code_sorry = 11 »	11	10 (count_code_sorry.py --json sur le lake : distinct_code_sorry: 10, code_sorry: 20, naive_sorry: 55) — contredisait la table du même fichier
Réfs de ligne : tricolorable_forward « L478 », murs « L1151 »/« L1293 », unknottingNumber « ~L1006 »/« L2143 », master « L341-350 »	toutes périmées	L1734 / L1061 / L1214 / L2267 / L3535 (grep -nE sur git show origin/main:)
EN : table d'état 2026-08-17 (14 réels, Invariant 2, Conway 8, baseline « 14 »)	gelé 3 semaines en arrière	aligné sur FR : 10 / 0 / 6 / « 10 », historique étendu → 11 (2026-08-28) → 10 (#15082)
EN : scaffolding Conway « 8 sorries »	8	6
EN : « The 37 count is preserved as a raw/any-line indicator »	contradictoire avec le 28 re-mesuré	phrase retirée
Chemins « conway_cgt_lean/ », « game_theory_lean/SocialChoice/ » (FR+EN « Voir aussi »)	non résolvables depuis knot_lean/	../../../GameTheory/conway_cgt_lean/, ../../../GameTheory/SocialChoice/ (ls vérifié), ../conway_lean/
LEAN_INVENTORY.md note ² : « la majorité des 10 restants sont des définitions non définies »	faux	2/10 sont des := sorry de définitions (IsSmoothlySlice, IsTopologicallySlice) ; les 8 autres des sorries de théorèmes
LEAN_INVENTORY.md : « Notebook câblé : 4 (…2 EN-siblings comptés) » (table + §3)	faux	3 (grep -rl knot_lean --include=*.ipynb → 17a/17b/17c câblés ; Lean-24/26 ne citent qu'en prose ; aucun notebook EN-sibling n'existe)

Pourquoi le master est-il prouvé alors que le compte reste 10 ? Les 10 sorries
restants vivent dans Reidemeister.lean (2, topologie PL), Conway.lean (6) et
Lidman.lean (2) — le README le dit maintenant explicitement, table §État, Verdict,
et conclusion.

Ce que cette PR ne fait pas

• Pas de Closes : [EPIC] Knot Theory Lean — scaffolding, invariants, Conway knot & Piccirillo proof #2874 reste ouverte (Conway/Lidman/PL restent).
• README.en.md ligne 6 (toolchain) : non touchée ici — c'est le sujet de fix(lean,#15829): knot_lean migre vers Mathlib 4.33.0 -- instances Decidable a la forme du sous-but #16075
  (commit ce7e50fefbd0, EN aligné à v4.33.0 + re-mesure Mathlib). Pour la même raison,
  la ligne de table knot_lean de LEAN_INVENTORY.md (colonne notebook 4→3) et le
  bullet §3 « sorry 11 → 10 » de fix(lean,#15829): knot_lean migre vers Mathlib 4.33.0 -- instances Decidable a la forme du sous-but #16075 peuvent demander un rebase trivial d'une
  ligne entre les deux PRs — même lane, résolu par elle-même.
• Les réfs de ligne des entrées fox/col §9.1 (~L1581/~L1731, statut PROUVÉ correct)
  ne sont pas re-ancrées : elles pointent des arguments internes de preuves, non des
  déclarations — coût de re-mesure > valeur.
• La « sorry prose » reste un indicateur brut documenté comme tel (le mode CI officiel
  est real, baseline 10, inchangée).

Validation

• python scripts/lean/count_code_sorry.py --json → knot_lean distinct_code_sorry
  10 avant/après (PR docs-only : les .lean ne bougent pas, la baseline CI
  lean-knot.yml:162 reste exacte).
• Aucun workflow CI n'est déclenché par ce diff (lean-knot.yml ne filtre pas les
  .md ; pre-commit gitleaks Passed au commit ef8151538c6a).
• Liens relatifs nouveaux vérifiés par ls depuis knot_lean/ ; ancres internes
  existantes inchangées.

🤖 Generated with Claude Code

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #16079 (docs(lean,#2874): knot_lean README FR+EN -- l'etat reel du code : marquee prouve #11958) 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.

• fort -- feat(lean,#2874): Conway + KT Alexander DISCHARGED (FR+EN) — sorry 10->8 #15440 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/LEAN_INVENTORY.md, MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/README.md (issues communes : [EPIC] Knot Theory Lean — scaffolding, invariants, Conway knot & Piccirillo proof #2874)
• terminal -- docs(lean,#14821): synchro inventaire/README sur l'état mesuré de knot_lean (10 réels) #15583 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/LEAN_INVENTORY.md, MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/README.md, recouvrement de chemins 67% -- docs(lean,#14821): synchro inventaire/README sur l'état mesuré de knot_lean (10 réels) #15583 est deja sur main.
• faible -- fix(lean,#15829): knot_lean migre vers Mathlib 4.33.0 -- instances Decidable a la forme du sous-but #16075 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/LEAN_INVENTORY.md, MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/README.en.md, MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/README.md

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.