feat(lean,#16650): repli insensible a la permutation de paires adjacentes (brique 3 R3) by jsboige · Pull Request #17998 · jsboige/CoursIA

jsboige · 2026-09-27T00:03:03Z

Grain: DEEP/lean — lane myia-po-2024:CoursIA — prev: DEEP/lean #17646

Résumé

Troisième brique de l'invariance R3 (issue #16650, tranche 3) : le repli de arcPartition est insensible à la permutation de deux paires adjacentes. La chirurgie R3 connexe déplace les croisements réécrits dans la liste du repli — sur le témoin du lake, les paires (2,8), (7,4), (8,6) deviennent (4,7), (2,8), (8,6) : l'orientation ET la position changent. Cette brique absorbe le déplacement de position ; foldl_mergePair_swap (#17429) absorbe l'orientation ; mergePair_mergePair_comm_equiv (#17646) porte la commutation des deux fusions au niveau des classes.

Ajouts (Conway.lean + Conway_en.lean, Pattern A sibling-pair)

Lemme / théorème	Rôle
`touches_iff_sameClass`	lit `Touches` en `SameClass` — la cle qui rend la caractérisation transportable
`sameClass_mergePair_pure`	`SameClass` après une fusion, lu entièrement en `SameClass` de la partition d'origine
`foldl_mergeStep_congr`	congruence du repli : deux partitions indiscernables par `SameClass` restent indiscernables après repli d'une même liste
`foldl_mergePair_permute_adjacent`	le théorème : échanger les paires aux positions `i` et `i+1` ne change pas la relation `SameClass` du résultat du repli

Docstrings ReidemeisterInvariance FR/EN actualisées pour nommer la brique : le contrôle decide du témoin est désormais justifié par foldl_mergePair_swap (orientation) + foldl_mergePair_permute_adjacent (transposition des positions), au lieu de la mention générique « commutation ».

Preuves (critères B)

Comptage sorry (python scripts/lean/count_code_sorry.py --json, champ distinct_code_sorry) :
- avant : knot_lean code_sorry=16, distinct_code_sorry=8 ; dépôt total distinct_code_sorry=12
- après : identique (16/8, total 12) — aucun sorry introduit ni retiré
lake build SUCCESS (WSL, mathlib chaude copiée) :

$ lake build Knots.Conway
warning: Knots/Conway.lean:3639:4: declaration uses `sorry`   # dette pre-existante (4 decls, lignes 3639/3647/3671/3701)
Build completed successfully (3009 jobs).
BUILD_RC=0

$ lake build Knots.Conway_en Knots.ReidemeisterInvariance Knots.ReidemeisterInvariance_en
✔ [3015/3015] Built Knots.ReidemeisterInvariance_en (173s)
Build completed successfully (3015 jobs).
BUILD_RC=0

Tous les warnings sont pré-existants (unreachableTactic/unnecessarySeqFocus/sorry aux lignes 2936-3701, hors de la zone d'insertion ~780-900).
3. Proof integrity (B.3) : lean-knot.yml invoque lean-axiom avec target-modules: "*" (dérivation runtime de tous les modules FR du lake, #10889) — Knots.Conway et Knots.ReidemeisterInvariance sont dans le périmètre ; le job tourne sur cette PR.
4. Pas de refactor du prover Python.

Anti-régression

Additions pures : 4 nouveaux lemmes/théorèmes insérés après mergePair_mergePair_comm_equiv, aucune preuve existante modifiée ni supprimée. Sibling EN : énoncés byte-identiques, docstrings traduites (convention #4980, Pattern A).

See #16650 — tranche 3 en cours : la forme générale de la préservation (diagramme où les paires (e2,e4) diffèrent comme multi-ensemble) reste à établir.

🤖 Generated with Claude Code

…e la premiere premisse R3 Ouvre le module d'invariance de Reidemeister du socle Alexander (tranche 3 du cadrage docs/lean/alexander-strategy/c652-reidemeister-invariance.md). Contenu du module : - controle positif kernel-verifie : sur la paire temoin du move R3 connecte (celle de reidemeister3Connected_satisfiable), la chirurgie preserve arcPartition. Clos par `decide` (instance finie), sans sorry ni tactique d'evitement. - deux mises au point du cadrage, ecrites dans les docstrings puisqu'elles conditionnent la suite de la tranche : (1) R3 n'est « trivial par reindexation » que pour i >= 1. a i = 0 la ligne 0 porte un sommet du triangle et c'est precisement la ligne que le mineur de alexanderPolynomialSigned elimine : le mineur change de forme et l'invariance ne se lit qu'a une unite +-t^k pres. Les deux cas sont de nature differente et doivent etre des theoremes distincts. (2) arcPartition n'est pas gratuitement preservee : ce que l'hypothese donne est le multi-ensemble des etiquettes, pas la partition. La preservation demande que la cloture des deux relations coincide — c'est le premier verrou de la tranche. Module separe parce que le theoreme croise Knots.Reidemeister3Connected et alexanderPolynomialSigned : Knots.Conway importe Knots.Invariant qui importe Knots.Reidemeister, donc importer Knots.Conway suffit a voir les deux et l'inverse serait un cycle. Jumeau EN selon la convention #4980 (namespace Knots_en, imports suffixees), agrege aux deux racines Knots.lean / Knots_en.lean. Preuves : - `lake build Knots.ReidemeisterInvariance` SUCCESS, compile depuis la source (253 s) sous WSL Ubuntu, leanprover/lean4:v4.33.0 — 0 erreur. - Bloc du theoreme byte-identique FR/EN : 384 octets de part et d'autre, sha be5cd1779f8349d7dca5. La seule difference entre les deux fichiers est la ligne de fermeture de namespace (`end Knots` / `end Knots_en`), imposee par la convention. - `distinct_code_sorry` = 8 inchange sur le lake knot_lean (`scripts/lean/count_code_sorry.py --json`) : les deux fichiers de ce commit n'en ajoutent aucun. Portee honnete : le controle est une instance (la paire temoin du lake), pas le theoreme general. L'invariance de alexanderPolynomialSigned sous R3 n'est pas demontree ici — ni les cas i >= 1 / i = 0, ni R1, ni R2. See #16650 See #14962 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

…-- docstrings FR/EN alignees sur le cas trivial Reecriture des sections 2 et 3 (FR + EN) pour aligner le recit sur le resultat reel de \`decide\` : sur le temoin du lake (\`reidemeister3Connected_satisfiable\`), les paires \`(e2, e4)\` du triangle, prises comme multi-ensemble non ordonne, **coincident** entre X et Y -- la preservation est triviale. La preservation generale (sur diagrammes ou les paires du triangle different) reste le premier verrou de la tranche, documente comme tel. Ancienne docstring pretendait que les paires (e2,e4) different entre X et Y -- les etiquettes enumerees etaient en realite les paires **(e2, e3)**, pas (e2, e4). La colonne etait denommee incorrectement. Le \`decide\` n'en reste pas moins kernel-verifie, mais il porte sur un cas ou l'obstacle evoque n'existe pas : la PR devient un controle **trivial** et non un temoin d'obstacle. Corps du theoreme preserve byte-identique (424 octets FR/EN, sha \`be5cd1779f8349d7dca581b5\`).

…-- docstrings FR/EN alignees sur le cas trivial Reecriture des sections 2 et 3 (FR + EN) pour aligner le recit sur le resultat reel de \`decide\` : sur le temoin du lake, les paires \`(e2, e4)\` du triangle, prises comme multi-ensemble non ordonne, **coincident** entre X et Y -- la preservation est triviale. La preservation generale reste le premier verrou de la tranche, documente comme tel. Ancienne docstring pretendait que les paires (e2,e4) different entre X et Y -- les etiquettes enumerees etaient en realite les paires **(e2, e3)**, pas (e2, e4). La colonne etait denommee incorrectement. Le \`decide\` n'en reste pas moins kernel-verifie, mais il porte sur un cas ou l'obstacle evoque n'existe pas : la PR devient un controle **trivial** et non un temoin d'obstacle. Corps du theoreme preserve byte-identique (424 octets FR/EN, sha \`be5cd1779f8349d7dca581b5\`). Reponses completes aux reserves NanoClaw (VERDICT: CONCERNS) dans le body mis a jour : reserve 1 (paires (e2,e4) coincident comme multi-ensemble, donc preservation triviale -- reecriture FR/EN), reserve 2 (384 -> 424 octets, recompte first-hand), reserve 3 (les 5 differences FR/EN enumerees : import + namespace + 2 docstrings + end), reserve 4 (Lean CI en SUCCESS, sha confirme par le kernel).

… R3 n'est pas trivial Le diagnostic posé sur main (4228158) disait « paires coïncident comme multi-ensemble, préservation triviale/vide ». Calcul direct sur les littéraux du témoin : X = [(2,8),(7,4),(8,6),(2,10),(4,6)] vs Y = [(4,7),(2,8),(8,6), (2,10),(4,6)] — l'orientation de la paire centrale ET les positions de repli diffèrent. La préservation sur le témoin est portée par mergePair_symm (#17429) + la commutation (#17646), elle n'est pas vide. Le garde-fou (généralité non fondée, multi-ensemble réellement différent à exhiber) est conservé. FR + EN alignés. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

…ister-invariance # Conflicts: # MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance.lean # MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance_en.lean

Troisieme brique de l'invariance R3 : foldl_mergePair_permute_adjacent echanger les paires aux positions i, i+1 ne change pas SameClass du resultat du repli. S'appuie sur foldl_mergePair_swap (#17429, orientations) et mergePair_mergePair_comm_equiv (#17646, commutation) ; la congruence foldl_mergeStep_congr transporte l'equivalence a travers le reste du repli. Additions pures dans Conway{,_en}.lean (Pattern A, byte-identique sur les enonces) ; docstrings ReidemeisterInvariance{,_en}.lean actualisees pour nommer la brique. lake build SUCCESS (3009+3015 jobs), sorry 16/8 inchanges. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

clusterManager-Myia

[Hermes] — first review au head ec76365aa (jamais scannée).

VERDICT: LGTM (comment-with-minor) — brique 3 R3 de #16650, vérifiée indépendamment :

Claim du témoin re-dérivé par exécution Python indépendante : paires (e2,e4) des trois croisements du triangle — X : (2,8), (7,4), (8,6) ; Y : (4,7), (2,8), (8,6). Exactement les littéraux de la nouvelle prose ✓. Seule l'orientation de la paire centrale diffère (7,4)↔(4,7) et les positions changent dans la liste du repli — la prose « la preservation n'y est pas vide » est désormais exacte (l'ancienne version disait « triviale/preserve trivialement », incorrect pour ce témoin).
arcPartition re-calculé des deux côtés (fold mergeStep sur les 5 croisements) : X = Y = {1} {2,4,6,7,8,10} {3} {5} {9} — 5 classes pour 10 arêtes, identiques ✓ — le contrôle positif de la section 3 tient.
Conway.lean +93/-0 : deux lemmes nouveaux (touches_iff_sameClass, sameClass_mergePair_pure) + le théorème-cible foldl_mergePair_permute_adjacent. Architecture propre : caractérisation pure de SameClass après fusion → congruence foldl_mergeStep_congr → transport par mergePair_mergePair_comm_equiv (#17646) et foldl_mergePair_swap (#17429). Chaîne de renvois réelle (les deux briques précédentes existent et sont citées avec leur numéro d'issue).
Docstrings bilingues symétriques : Conway/Conway_en et ReidemeisterInvariance/_en diffèrent uniquement par la langue, +93/+93 et +32/+30 cohérents.
Gates au head : knot target-coverage success, Lean visibility drift success, 0 failure ; Lean CI (knot_lean) in_progress au moment de la review (commencé 00:03Z) — le decide du témoin + les nouveaux lemmes seront couverts par cette jambe ; verdict reposant sur la re-dérivation indépendante ci-dessus, pas sur la CI pendante.

Reste ouvert (assumé dans la prose) : le contre-exemple où les paires diffèrent réellement comme multi-ensemble — premier verrou de la tranche, correctement signalé comme non résolu.

[Hermes hermes-pr-review, cycle :00 27/09, host f6be46d1b7a3]

github-actions · 2026-09-27T01:51:38Z

Path-collision (organ #13359/#13615)

Cette PR #17998 (feat(lean,#16650): repli insensible a la permutation de paires adjacentes (brique 3 R3)) 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.

terminal -- feat(lean,#16650): mergePair_symm — premiere brique preservation arcPartition (stacked #17412) #17429 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/Conway.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/Conway_en.lean, recouvrement de chemins 50% -- feat(lean,#16650): mergePair_symm — premiere brique preservation arcPartition (stacked #17412) #17429 est deja sur main. (issues communes : Lean: invariance de Reidemeister de la variante signee alexanderPolynomialSigned #16650) (issues communes : Lean: invariance de Reidemeister de la variante signee alexanderPolynomialSigned #16650)
terminal -- feat(lean,#16650): theoreme de commutation SameClass — deux fusions mergePair commutent au niveau des classes #17646 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/Conway.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/Conway_en.lean, recouvrement de chemins 50% -- feat(lean,#16650): theoreme de commutation SameClass — deux fusions mergePair commutent au niveau des classes #17646 est deja sur main. (issues communes : Lean: invariance de Reidemeister de la variante signee alexanderPolynomialSigned #16650) (issues communes : Lean: invariance de Reidemeister de la variante signee alexanderPolynomialSigned #16650)

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 · 2026-09-27T06:08:58Z

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 17998
head: ec76365
complete: true
body: read
comments-reviewed: 1
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 5e9ab273bdb60003a39df1b3eb10618af0470b78cb5ef4640a71744cf729f4e1
diff-files: 4
diff-additions: 248
diff-deletions: 37
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]

Prévalidation tierce à la tête exacte : brique Lean knot_lean R3, quatre fichiers (+248/−37). Conway.lean et son sibling EN ajoutent les lemmes sur la permutation adjacente ; les deux fichiers ReidemeisterInvariance ne changent que la prose des docstrings. Aucun sorry, native_decide ni Classical.choice ajouté ; le compte réel knot_lean reste 16/8 (total distinct dépôt 12) avant et après. Le sibling i18n, Lean CI, la couverture ciblée et proof-integrity knot_lean sont verts à cette tête. Body, un commentaire advisory path-collision avec deux PRs déjà mergées, une review Hermes COMMENTED/LGTM sans réserve et zéro thread inline relus ; B.0 rend rc=0. Les 25 noms de checks sont terminés et latest-wins-green, PR gate success après rejeu à 05:36Z, mergeability MERGEABLE/CLEAN et DWELL rc=0. Le cas multi-ensemble général reste ouvert sous #16650 ; ce dossier atteste la tranche annoncée, sans prétendre fermer l'issue. Décision finale de merge réservée à ai-01.

jsboige and others added 6 commits September 22, 2026 12:55

Merge remote-tracking branch 'origin/main' into feature/16650-reideme…

ba69cb8

…ister-invariance # Conflicts: # MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance.lean # MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance_en.lean

github-actions Bot added the lean-visibility-drift La PR ajoute des declarations lake non citees par AUCUN notebook (borne large) (#11703) label Sep 27, 2026

jsboige mentioned this pull request Sep 27, 2026

feat(guard,#17679): table d'acceptation canon C# 13.0 dans le kernel drift guard #18000

Merged

clusterManager-Myia reviewed Sep 27, 2026

View reviewed changes

jsboige mentioned this pull request Sep 27, 2026

Lean: invariance de Reidemeister de la variante signee alexanderPolynomialSigned #16650

Closed

3 tasks

jsboige mentioned this pull request Sep 27, 2026

feat(lean,#16650): temoins R3 du polynome signe, le mineur designe s'effondre sur Y (brique 4) #18023

Merged

myia-ai-01 merged commit 04917f8 into main Sep 27, 2026
25 of 27 checks passed

This was referenced Sep 27, 2026

fix(ci,#18024): test_lean_exec ne depend plus de la RAM libre du runner #18026

Merged

fix(gate,#17887): un dossier BLOCKED qui ne nomme aucun champ bloquant est refuse #18030

Merged

clusterManager-Myia mentioned this pull request Sep 27, 2026

Aucun des 12 workflows Lean ne borne son job : un wedge de 3 h 17 immobilise la moitie du pool coursia-lean et son check ne conclut jamais #15698

Closed

This was referenced Sep 27, 2026

feat(lean,#16650): arcPartition_sameRel — préservation générale de la partition d'arcs sous R3 connectée (FR + EN) #18100

Merged

lean(knot,#2874): refondre Conway.lean en sous-fichiers progressifs avec commentaires de digestion #18397

Open

github-actions Bot mentioned this pull request Sep 30, 2026

feat(lean,#16650): refutation formelle de l'invariance naive R3 connectee (Alexander signe, FR+EN) #18548

Merged

Navigation Menu

Repository navigation

feat(lean,#16650): repli insensible a la permutation de paires adjacentes (brique 3 R3) - #17998

feat(lean,#16650): repli insensible a la permutation de paires adjacentes (brique 3 R3)#17998
myia-ai-01 merged 6 commits into
mainfrom
feature/16650-reidemeister-invariance

jsboige commented Sep 27, 2026

Uh oh!

clusterManager-Myia left a comment

Uh oh!

github-actions Bot commented Sep 27, 2026

Uh oh!

jsboige commented Sep 27, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

jsboige commented Sep 27, 2026

Résumé

Ajouts (Conway.lean + Conway_en.lean, Pattern A sibling-pair)

Preuves (critères B)

Anti-régression

Uh oh!

clusterManager-Myia left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions Bot commented Sep 27, 2026

Path-collision (organ #13359/#13615)

Uh oh!

jsboige commented Sep 27, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants