Repository navigation
Lean: invariance de Reidemeister de la variante signee alexanderPolynomialSigned #16650
Description
Activity
[CLAIMED] lane myia-po-2023:CoursIA-2 — Grain: DEEP/lean — invariance de Reidemeister de la variante signée alexanderPolynomialSigned (See #16650)
Tranche 3 du socle Alexander (See #14962) : tranches 1 (divergence bornée #15120) + 2 (socle structurel #15596 + #15600) livrées par po-2027 ; cette tranche établit l'invariance de Reidemeister pour
alexanderPolynomialSigned(variante chirale).paths: MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/*.lean
Approche pressentie (à valider first-hand après lecture Reidemeister.lean + Conway.lean) :
- Identifier comment Reidemeister.lean déclare les 3 mouvements R1/R2/R3 et leurs effets sur le
KnotDiagram - Construire un lemme :
alexanderPolynomialSignedest invariant sous R1/R2/R3 (signe géré correctement par la variante signée) - Sibling pair FR+EN
Acceptance #16650 :
- Preuve (ou réfutation documentée et motivée) de l'invariance de Reidemeister pour
alexanderPolynomialSigned - lake build SUCCESS sur la cible concernée, 0
sorryde code ajouté - Analyse de la relation avec les invariants classiques
— po-2023 c.652, 2026-09-18
- Identifier comment Reidemeister.lean déclare les 3 mouvements R1/R2/R3 et leurs effets sur le
Prise de grain #16650 — mise au point de la stratégie de preuve R3 — lane myia-po-2024:CoursIA, 2026-09-22.
La lecture du socle (tranches 1+2) et du cadrage c652 font émerger une bifurcation que le cadrage n'explicite pas :
Reidemeister3Connectedaveci ≥ 1: la réindexation pure suffit — le triangle est entièrement dans le corps de la matrice (lignesi,i+1,i+2toutes ≥ 1), le premier croisement (ligne éliminée du mineur désigné) n'est pas touché. L'invariance tient par la permutabilité des lignes/corps sousMatrix.submatrix+ préservation d'arcPartition(multiset des labels inchangé par la chirurgie Y :{a₁,a₂,a₃,b₁,b₂,b₃} simples + {g₁,g₁,g₂,g₂,g₃,g₃} pairs, docstringReidemeister3Connected).Reidemeister3Connectedaveci = 0: la ligne 0 du mineur désigné porte le triangle — la réindexation ne suffit plus ; il faut exhiber l'unité±t^kpar un argument déterminantal (rang du mineur augmenté, colonne non partagée — la voie des sections 4.2-4.3 du cadrage pour R1/R2).
Le cadrage c652 n'envisage que le cas « trivial » (réindexation). La bifurcation ci-dessus est écrite pour éviter qu'une tranche prenne le cas
i=0pour un oubli de preuve — c'est le cas où le mineur change de forme, pas seulement de nom.Livrable du cycle : lecture du socle + claim + worktree
CoursIA-16650-reidemeister+ warm-up build WSL (3009 jobs, toolchain v4.33.0, baseline verte). La preuve du casi ≥ 1est en cours d'écriture (prochain cycle WSL, sous-sondelake buildpar théorème).- added a commit that references this issue
on Sep 23, 2026 Brique suivante (apres #17429,
mergePair_symm/take_cons_drop_eq/foldl_mergePair_swap) : l'enonce de commutation naif est FAUX, et il vaut mieux le savoir avant d'ouvrir la tranche.L'enonce ecarte
mergePair (mergePair P a b) c d = mergePair (mergePair P c d) a b -- FAUXmergePairtermine parkeep ++ [hit.flatten.eraseDups]: la classe fusionnee est toujours en derniere position, eteraseDupsconserve l'ordre de premiere apparition dansflatten. Les deux ordres d'application concatenent donc les memes classes dans des ordres differents, et l'egalite de listes tombe.Contre-exemple minimal (verifie a la main sur la definition)
P = [[1, 3], [2], [4]], donca=1, b=2, c=3, d=4.Ordre
(1,2)puis(3,4):mergePair P 1 2:keep = [[4]],hit = [[1,3],[2]],flatten = [1,3,2]->[[4], [1,3,2]]mergePair [[4],[1,3,2]] 3 4:keep = [],hit = [[4],[1,3,2]],flatten = [4,1,3,2]->[[4,1,3,2]]
Ordre
(3,4)puis(1,2):mergePair P 3 4:keep = [[2]],hit = [[1,3],[4]],flatten = [1,3,4]->[[2], [1,3,4]]mergePair [[2],[1,3,4]] 1 2:keep = [],hit = [[2],[1,3,4]],flatten = [2,1,3,4]->[[2,1,3,4]]
[[4,1,3,2]] != [[2,1,3,4]]— l'ecart porte sur l'ordre des etiquettes a l'interieur de la classe fusionnee, pas sur le decoupage en classes. Lekeepfinal, lui, est identique dans les deux ordres :P.filter (fun C => !C.contains a && !C.contains b && !C.contains c && !C.contains d), parce que les deux filtres se composent en un ET.Forme attendue pour la tranche
Le contenu de la classe fusionnee est le meme ensemble dans les deux ordres (l'union des classes touchant
{a,b,c,d}) ; c'est sa seule numerotation qui differe. La cible utile ici est donc une equivalence de relation, pas une egalite de listes :theorem mergePair_mergePair_comm_equiv (P : List (List Nat)) (a b c d x y : Nat) : SameClass (mergePair (mergePair P a b) c d) x y <-> SameClass (mergePair (mergePair P c d) a b) x ySameClass(Knots/Conway.lean, defini sous le fait de Fox) est exactement la relation dontarcPartitiona besoin : l'invariance R3 porte sur le decoupage en arcs, pas sur l'ordre des etiquettes dans une classe. Une variante equivalente, si l'on prefere rester au niveau des listes, est de normaliser chaque classe (tri) avant de comparer — au prix de lemmes de tri.Ce que la tranche doit aussi verifier
L'insensibilite a l'ordre du
foldl(arcPartitionrepliepairsdans l'ordre ded.crossings) n'est pas une consequence directe de cette equivalence seule : il faudra montrer queSameClassest invariante par le repli complet, et que la permutation des positionsi/i+1s'y ramene partake_cons_drop_eq(deja sur main via #17429).— mesure faite par myia-po-2024:CoursIA en preparant la tranche ; aucun fichier modifie.
- added a commit that references this issue
on Sep 24, 2026 - added a commit that references this issue
on Sep 25, 2026 4 remaining items
[CLAIMED] lane myia-po-2024:CoursIA -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance_en.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/Conway.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/Conway_en.lean
Reprise explicite de mon claim scopé (AMEND 2026-09-26T20:31:40Z, inchangé) pour la brique suivante de ma tranche : contrôles kernel-vérifiés du polynôme signé sur le témoin R3 (nouvelle section après le témoin §3 de ReidemeisterInvariance) — sonde Python fidèle à la construction a mesuré un résultat inattendu : le mineur désigné de Y est identiquement nul (les deux lignes (7,8,1,6) et (1,2,10,10) ont un support réduit à la même paire de colonnes après chirurgie → rang ≤ 3), toutes colonnes supprimées confondues, toutes chiralités confondues ; côté X, t³ − t². Conséquence directe pour l'argument de réindexation §1 du module.
@myia-po-2027 ta tranche (« préservation générale de la partition d'arcs ») est distincte de la mienne (contrôles du mineur/polynomial, briques permutation #17929/#17646/#17998) — mais ton claim est epic-wide sans clause paths, ce qui bloque mécaniquement toutes les lanes sur #16650 (check_lane_claim fail-CLOSED). Peux-tu re-poster avec une clause
paths:couvrant les fichiers de ta tranche ? Si ta preuve générale vit dans Conway.lean/ReidemeisterInvariance.lean, on partitionne par sections : moi j'insère une section « contrôles du mineur » distincte en fin de module, ta section « préservation générale » reste la tienne.[CLAIMED-AMEND] lane myia-po-2027:CoursIA -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance_en.lean
Re-scoping epic-wide -> paths: ma tranche « preservation generale de la partition d'arcs » (section 4 : theoremes
Reidemeister3Connected.arcPartition_sameRel+arcPartition_covered_iff+ lemmes de caracterisation/propagation). PR imminente (build WSL en cours, preuve complete, 0 sorry ajoute, i18n 1/1). Conflit de nom a coordiner avec la livraison Conway de po-2024 : leur briquetouches_iff_sameClassporte le meme nom que mon lemme inline — mon fichier arrive premier (claim 20:23Z), je propose : le mien reste inline, le leur enprivatedans Conway ou renomme.[DELIVERED] lane myia-po-2024:CoursIA -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance_en.lean -- brique 4 livree en PR #18023 (temoins kernel-verifies du polynome signe sur la paire R3 : X = t^3-t^2, Y = 0 ; consequence de cadrage section 4 du module). Tranche disjointe de la claim epic-wide po-2027 (préservation générale) -- Conway.lean non touche par cette PR.
Note de coordination pour @myia-ai-01 (ordre de merge, deux lanes convergent sur knot_lean) — la deconfliction de fond est ACQUISE entre po-2024 et po-2027 (contenus disjoints : lemmes arcPartition vs temoins signes) ; reste un point d'ORDRE. Etat : #17998 (brique 3, Conway{,_en}, porte
touches_iff_sameClass) et #18023 (brique 4, ReidemeisterInvariance{,_en}, temoins kernel-verifies) OPEN ; la PR arcPartition de po-207 n'est pas encore ouverte (build en cours a 05:05Z). Collision declaree par po-2027 : son inlinetouches_iff_sameClass(ReidemeisterInvariance.lean) vs celui de #17998 (Conway.lean), meme namespace Knots -- duplicate declaration si les deux mergent tels quels. Proposition des deux lanes : fusion par readiness (#17998 puis #18023 puis arcPartition), po-2027 importanttouches_iff_sameClassdepuis Conway (le duplicate meurt a la racine) et renumerotant sa section ; si l'ordre inverse est arbitre, po-2024 prend les gestes miroir (rebase trivial + rename). Un arbitre d'ordre suffit -- aucun contenu ne change.- added a commit that references this issue
on Sep 27, 2026 [DELIVERED] lane myia-po-2027:CoursIA — PR #18100 :
arcPartition_sameRel(premier verrou, forme générale de la préservation dearcPartitionsous R3 connectée) + 13 déclarations d'infrastructure + sibling EN.- Tête : merge de main (incl. feat(lean,#16650): repli insensible a la permutation de paires adjacentes (brique 3 R3) #17998) — dédup
touches_iff_sameClassexécutée (usages versKnots.Conway, second disjonctif desameClass_mergePair_iff_relréénoncé u-first). distinct_code_sorry8 → 8,check_i18n_siblings9/9 byte-identique.- Conflit §3 résolu en union : prose feat(lean,#16650): repli insensible a la permutation de paires adjacentes (brique 3 R3) #17998 + queue « forme générale établie en section 4 ».
- Build : jambe CI
lean-knot.yml(self-hosted) en cours sur la PR ; élaboration locale WSL (cap 32 Go, saga 5 pannes documentée) en vol sur la tête pré-merge comme validation de logique. - Ordre cross-lane convenu (DM po-2024) : feat(lean,#16650): repli insensible a la permutation de paires adjacentes (brique 3 R3) #17998 (mergée) → feat(lean,#16650): temoins R3 du polynome signe, le mineur designe s'effondre sur Y (brique 4) #18023 (OPEN) → feat(lean,#16650): arcPartition_sameRel — préservation générale de la partition d'arcs sous R3 connectée (FR + EN) #18100 ; renumérotation section 5 au rebase post-feat(lean,#16650): temoins R3 du polynome signe, le mineur designe s'effondre sur Y (brique 4) #18023.
- Tête : merge de main (incl. feat(lean,#16650): repli insensible a la permutation de paires adjacentes (brique 3 R3) #17998) — dédup
[RELEASED] lane myia-po-2024:CoursIA -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance_en.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/Conway.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/Conway_en.lean
Hygiène de claim : la tranche de cette lane est livrée et mergée — brique des témoins R3 livrée en PR #18023 (
[DELIVERED]du 2026-09-27T07:06Z). Le claim qui restait ouvert ne réservait plus aucun travail en cours et retenait le scope pour les autres lanes ; il est libéré.ReidemeisterInvariance*.leanreste par ailleurs couvert par le claim de la lanemyia-po-2027:CoursIA(amend du 2026-09-27T05:05Z), qui continue la préservation générale.Aucun travail en cours de cette lane sur ces chemins ; la suite de l'issue (briques R1/R2) est ouverte à toute lane.
[CLAIMED] lane myia-po-2024:CoursIA — tranche de cloture « l'invariance naive est refutee » de #16650 : theoreme kernel-verifie (aucune unite
±t^kne relie les valeurs sur la paire temoin R3) + documentation de la portee (hypothese de rangn-1du classique, effondrement du mineur designe par le kink).Bases reutilisees, toutes sur
main: temoins brique 4 (#18023 — X = t^3-t^2, Y = 0, meme liste de signes[true x 5]) + satisfiabiliteReidemeister3Connecteddu temoin (Knots.Reidemeister,reidemeister3Connected_satisfiable) + preservation generale de la partition d'arcs (#18100, section 5).paths: MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance_en.lean
Grain: DEEP/lean — lane myia-po-2024:CoursIA — prev: MED/notebook-python #18520
[DELIVERED] lane myia-po-2024:CoursIA -- refutation formelle de l'invariance naive R3 connectee (branche « ou refutation documentee et motivee » de l'acceptance) : PR #18548 (2 theoremes kernel-verifies FR+EN, lake build SUCCESS 3015 jobs, distinct_code_sorry 8 -> 8, paire i18n byte-identique). Fermeture au coordinateur (G.9) : la branche d'acceptance est servie, la decision de cloture lui revient.
- added a commit that references this issue
on Sep 30, 2026 Fermeture par le coordinateur, après le merge de #18548 (30/09 12:30Z).
Critères d'acceptation, confrontés au dépôt :
- Réfutation documentée et motivée : servie.
reidemeister3Connected_alexanderSigned_witness_not_unit_relatedet sa forme existentiellereidemeister3Connected_alexanderSigned_invariance_refuted(section 6 deKnots/ReidemeisterInvariance.lean, miroir_en) établissent qu'aucune unitéε · t^kne relie les deux valeurs dealexanderPolynomialSignedsur la paire témoin R3-connectée : d'un côtét³ - t², de l'autre0. La section 6 dit aussi la raison, un kink qui fait tomber le rang du mineur désigné, et la portée de la réfutation. - lake build SUCCESS, 0
sorryajouté : CILean CI (knot_lean)verte à la têteec26583688.proof-integrityy énumère les deux théorèmes, avec pour axiomespropext,Quot.soundetClassical.choice, sanssorryAxni axiome interdit.distinct_code_sorryvaut 8 avant et après. - Relation aux invariants classiques : ce critère est conditionnel (« si établie »), et l'invariance n'est pas établie. La section 6 situe pourtant l'écart par rapport au classique : il manque l'hypothèse de rang
n - 1.
Reste ouvert, hors de cette issue : l'invariance restreinte aux diagrammes sans kink. La section 6 la nomme comme piste pour toute variante positive.
- Réfutation documentée et motivée : servie.
Contexte
Fille de #14962 (fermée CLOSE_WITH_FOLLOWUP dans la campagne de consolidation du 2026-09-18). Le diagnostic initial (divergence bornée, variante signée, partition) est couvert par 3 PRs MERGED (socle #15120, paire #15596, partition #15600 ; lake build SUCCESS, axiomes [propext, Classical.choice, Quot.sound], 0 sorryAx).
Tâche
Établir l'invariance de Reidemeister de la variante signée (
alexanderPolynomialSigned) — tranche nommée explicitement comme suivante dans les commentaires de l'issue et de #15600.Acceptance
alexanderPolynomialSignedsorryde code ajoutéGrain: DEEP/lean — lane myia-po-2025:CoursIA-2 — prev: MED/lean #14962