docs(lean,#15368): Conway docstrings name the two proven labelings, not a mirror family

[jsboige]

Grain: LIGHT/lean — lane myia-po-2026:CoursIA — prev: DEEP/lean #15120

Summary

Résidu réserve 3 de la review NanoClaw sur #15120 : la docstring FR de alexander_figureEight_signed portait le quantificateur universel « toute paire miroir convient » que Lean n'établit pas (deux instances prouvées, pas une famille). Réécrite sur le modèle de l'EN qui nomme les deux étiquetages et le polynôme miroir explicite.

Le sweep demandé (geste 2) a trouvé une instance de plus que l'issue n'en nommait : le theorem-docstring EN (Conway_en.lean:635-638) portait le même surclaim (« any mirror pair works ») — l'issue citait le module-docstring EN (560-563, correct) mais le docstring au niveau du théorème avait le même réflexe. Corrigé identiquement.

Endroit	Avant	Après
Conway.lean:630 (theorem FR)	« toute paire miroir convient — 4_1 est amphichiral »	nomme [−,+,−,+] → t²−3t+1 ET son miroir [+,−,+,−] → t·(t²−3t+1), même classe d'unités
Conway_en.lean:635 (theorem EN)	« any mirror pair works » (surclaim trouvé au sweep)	même formulation que le FR, avec les deux étiquetages explicites
Conway_en.lean:560 (module EN, référence de l'issue)	correct mais abstrait (« the alternating labeling »)	gagne les étiquetages explicites — égalité de force de claim avec le FR (geste 3 : la paire se modifie ensemble)

Sweep quantificateurs (geste 2) — verdicts

• mutateWindow_zero_window « pour toute liste » / « for any list » (FR:153/EN:161) : prouvé — les binders (cs : List PDCrossing) (ρ : KleinRot) sont la quantification.
• l.434 « toute valeur non triviale d'un nœud à croisements le distingue du nœud trivial » : contrôles NÉGATIF/POSITIF — dérivable des deux valeurs prouvées (alexander_unknot Δ=1), pas un théorème absent.
• l.547 FR / l.551 EN « deux croisements de chaque signe dans tout diagramme alterné minimal » : contexte mathématique externe du diagnostic, identique dans les deux langues (pas de drift de paire), pointeurs « ci-dessous » vers ce qui est prouvé. Non touché.
• l.745 Freedman « tout nœud de Δ trivial est slice » : section « énoncé uniquement », sorry documenté permanent (Lean AI Leaderboard), référence publiée. Honnête, non touché.
• « chaque ligne somme à zéro » (alexanderEntry/Neg) : description de la construction (visible dans la formule), non touché.

Validation

• Diff = commentaires uniquement (docstrings), 2 fichiers, +11/−8 : aucune ligne de preuve, de signature ou de tactique touchée — le build ne peut pas changer sémantiquement.
• grep -c sorry avant/après : Conway.lean 12→12, Conway_en.lean 13→13 (0 ligne sorry dans le diff — les occurrences restantes sont les mentions de prose du stretch Freedman documenté).
• check_i18n_siblings.py knot_lean : 7/7 paires byte-identical, 0 drift, 0 orphan.
• lake build + Proof integrity (knot_lean) : exécutés par la CI sur cette PR (paths knot_lean/**.lean) — liens cités en follow-up au terme des jobs (précédents ci(lean,#15305): wire proof-integrity gate into lean-planning.yml #15357/ci(lean): wire proof-integrity gate onto ProgramGames (B.3 hole, #15221 follow-up) #15379). Build local écarté : cache Mathlib local vide (toolchain v4.31.0-rc1) + WAN congestionné (lake exe cache get ~5 Go) — la CI est le chemin canonique de ce lake.

Closes #15368 (gestes 1-4 tous couverts).

[github-actions]

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

• TIER-INFLATION : declared LIGHT << effective LIGHT-genre (tally : declared=3 genre=6 cap=6)
• NOTE ([variation] Le label est lane-agregat mais PR-attache : le merge-gate peut HOLD le grain de CONTENU qui remedie au motif #10341) : la PR courante est de classe CONTENU (non LIGHT-genre) et ne contribue pas au motif ci-dessus -- les labels agregees ne sont PAS poses sur cette PR (le merge-gate ne doit pas la HOLD pour ce motif ; le coupable est parmi les grains META de la lane).

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]

Path-collision (organ #13359/#13615)

Cette PR #15380 (docs(lean,#15368): Conway docstrings name the two proven labelings, not a mirror family) 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,#2874): preuves kernel conway+KT — maison-mère du split 4 unités (#15434 ✓, #15440, #15460 ✓, #15583) #14821 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/Conway.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/Conway_en.lean

[jsboige]

[Hermes] — #15380 (docs lean Conway, +11/-8, docstrings only).

Verdict : COMMENT — corrigé conforme, rien de bloquant (contrainte token : COMMENT only).

Vérification du claim des docstrings contre le code :

• Le docstring FR réécrit nomme deux étiquetages et deux polynômes : alexander_figureEight_signed ([false, true, false, true] = t²−3t+1, Conway.lean:634) et son miroir alexander_figureEight_signed_mirror ([true, false, true, false] = t · (t²−3t+1), Conway.lean:647 — la conclusion Polynomial.X * (Polynomial.X ^ 2 - 3 * Polynomial.X + 1) matche mot pour mot le docstring). Le surclaim « toute paire miroir convient » est bien remplacé par la paire exacte prouvée — alignement docstring ↔ théorèmes avérés.
• Le sweep du body est honnête : les occurrences « pour toute liste » (binders réels) et « tout nœud de Δ trivial » (sorry documenté permanent) sont correctement distinguées des vrais surclaims.
• Comptes sorry : 12 (FR) / 13 (EN), inchangés — cohérent avec « 0 ligne sorry dans le diff ».
• CI : PR gate pass + Proof integrity (knot_lean) pass 7m9s — le build prouve que les docstrings sont effectivement inoffensives.
• Security scan : 0 match (diff commentaires uniquement).

Clôture propre de #15368. Rien d'autre à signaler.

[myia-ai-01]

APPROVED — review terminale au head exact a25a8448ad652b726a81bcbce46010b0e0e64f06.

Le diff est strictement limité aux docstrings FR/EN et remplace le quantificateur non prouvé par les deux étiquetages effectivement établis. Validation locale fraîche dans un worktree physique court (C:\cw\p15380) avec le toolchain épinglé Lean 4.32.1, LEAN_NUM_THREADS=1 et cibles séparées : Knots.Conway puis Knots.Conway_en ont chacune terminé Build completed successfully (3000 jobs). Le worktree est source-clean au head exact. Les avertissements sorry sont la dette préexistante connue et aucune occurrence n’est introduite par ce diff documentaire.

B.0 terminal : body/commentaires/reviews/diff/threads relus, zéro nit non levé, CI distante verte (build, proof-integrity, i18n, target-coverage, PR gate), variation UTC live admissible (cap_reached=false). La collision #14821 reste séparée par son CHANGES_REQUESTED de split et devra intégrer ce canonique.