From 06bcdb8a60bda76d8b26c0e6e39cf4acffaeb7d1 Mon Sep 17 00:00:00 2001 From: jsboige Date: Tue, 22 Sep 2026 12:54:40 +0200 Subject: [PATCH 1/4] =?UTF-8?q?feat(lean,#16650):=20ReidemeisterInvariance?= =?UTF-8?q?=20=E2=80=94=20controle=20kernel-verifie=20de=20la=20premiere?= =?UTF-8?q?=20premisse=20R3?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- .../SymbolicAI/Lean/knot_lean/Knots.lean | 1 + .../Knots/ReidemeisterInvariance.lean | 92 ++++++++++++++++++ .../Knots/ReidemeisterInvariance_en.lean | 95 +++++++++++++++++++ .../SymbolicAI/Lean/knot_lean/Knots_en.lean | 1 + 4 files changed, 189 insertions(+) create mode 100644 MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance.lean create mode 100644 MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance_en.lean diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots.lean b/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots.lean index 67bd52a8bc..3733fd1cf5 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots.lean +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots.lean @@ -35,6 +35,7 @@ import Knots.Basic import Knots.Reidemeister import Knots.Invariant import Knots.Conway +import Knots.ReidemeisterInvariance import Knots.Jones import Knots.Lidman import Knots.MathlibPrerequisites diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance.lean b/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance.lean new file mode 100644 index 0000000000..03fb3ed5fc --- /dev/null +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance.lean @@ -0,0 +1,92 @@ +/- +Knots.ReidemeisterInvariance — Invariance des invariants sous Reidemeister +========================================================================= + +Domicile du theoreme d'invariance : `alexanderPolynomialSigned` est invariant +sous les trois mouvements de Reidemeister (issue #16650, tranche 3 du socle +Alexander, cadrage `docs/lean/alexander-strategy/c652-reidemeister-invariance.md`). + +Pourquoi un module separe : le theoreme croise `Reidemeister3Connected` +(`Knots.Reidemeister`) et `alexanderPolynomialSigned` (`Knots.Conway`). +`Knots.Conway` importe `Knots.Invariant`, qui importe `Knots.Reidemeister` — +importer `Knots.Conway` suffit donc a voir les deux, et l'inverse serait un +cycle. Ce module est le point ou les deux theories se rencontrent. + +Convention i18n (EPIC #4980) : ce fichier est **FR canonique**, avec son miroir +anglais dans le sibling `ReidemeisterInvariance_en.lean`. +-/ + +import Knots.Conway + +namespace Knots + +/-! ## 1. La bifurcation `i = 0` / `i ≥ 1` (mise au point du cadrage) + +Le cadrage c652 (§4.1) presente R3 comme « trivial par reindexation ». C'est +vrai **sous une condition qui n'y est pas enoncee** : que le triangle soit +entierement hors de la ligne eliminee du mineur designe. + +`alexanderPolynomialSigned` supprime la **premiere** ligne (`rest` = queue de +`crossings`) et la derniere colonne du mineur. Donc : + +* **`i ≥ 1`** — les trois lignes reecrites du triangle sont dans le corps de la + matrice ; l'invariance est un argument de reindexation : la chirurgie ne + change ni le nombre de croisements, ni le nombre d'aretes, et la partition + d'arcs est preservee (section 2 ci-dessous). Le mineur est inchange au + transport des colonnes pres. +* **`i = 0`** — la ligne 0 porte un sommet du triangle, et c'est precisement + celle que le mineur designe **elimine**. La reindexation ne suffit plus : le + mineur change de forme (des coefficients quittent les colonnes du triangle + pour d'autres), et l'invariance ne peut se lire qu'a une **unite** `±t^k` + pres — c'est l'argument determinant al des sections 4.2-4.3 du cadrage + (colonne non partagee, rang du mineur augmente). + +Les deux cas sont donc de nature differente et doivent etre des theoremes +distincts. Les confondre ferait passer `i = 0` pour un oubli de preuve alors que +c'est le cas ou le mineur designe change reellement de forme. + +## 2. L'obligation de preservation de la partition d'arcs + +L'argument de reindexation (`i ≥ 1`) repose sur une premiere que le cadrage +**suppose sans la prouver** : `arcPartition` est preservee par la chirurgie. + +L'obstacle est reel : la chirurgie R3 connectee reecrit les paires `(e2, e4)` +des trois croisements du triangle, et ces paires **different** entre X et Y — + + X : (a₁,g₁), (g₁,g₃), (g₂,b₂) Y : (b₃,g₃), (a₁,b₂), (g₂,a₂) + +— donc la relation de passage-dessus engendree change. Ce qui est preserve est +le **multi-ensemble des etiquettes** (docstring de `Reidemeister3Connected`), +d'ou `wf` ; la partition, elle, n'est preservee que si la **cloture** des deux +relations coincde, ce qui n'est pas un fait gratuit. + +Le controle de la section 3 verifie ce point sur le temoin du lake +(`reidemeister3Connected_satisfiable`) : la cloture y est identique alors que +les paires generatees diffèrent. La forme generale reste a etablir — c'est le +premier verrou de la tranche, avant tout argument de reindexation. +-/ + +/-! ## 3. Controle : la partition d'arcs du temoin R3 est preservee + +Le temoin est celui de `reidemeister3Connected_satisfiable` (litteraux repris +tels quels) : les deux diagrammes sont bien formes (`decide` sur `wf` au lake), +et leur partition d'arcs — 5 classes pour 10 aretes — est **la meme** de part et +d'autre de la chirurgie. C'est le controle positif de la section 2 : les paires +`(e2,e4)` reecrites sont differentes, leur cloture non. +-/ + +/-- Controle de la tranche 3 (etape 1) : sur la paire temoin du move R3 + connecte, la chirurgie preserve `arcPartition` — la cloture des paires de + passage-dessus est inchangee bien que les trois paires du triangle soient + reecrites. C'est la premiere que l'argument de reindexation (cas `i ≥ 1`) + suppose ; la forme generale reste a prouver. -/ +theorem reidemeister3Connected_arcPartition_witness : + arcPartition + { crossings := [⟨1, 2, 7, 8⟩, ⟨3, 7, 9, 4⟩, ⟨9, 8, 5, 6⟩, + ⟨1, 2, 10, 10⟩, ⟨3, 4, 5, 6⟩], numEdges := 10 } + = arcPartition + { crossings := [⟨3, 4, 9, 7⟩, ⟨9, 2, 5, 8⟩, ⟨7, 8, 1, 6⟩, + ⟨1, 2, 10, 10⟩, ⟨3, 4, 5, 6⟩], numEdges := 10 } := by + decide + +end Knots diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance_en.lean b/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance_en.lean new file mode 100644 index 0000000000..9a4d726411 --- /dev/null +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance_en.lean @@ -0,0 +1,95 @@ +/- +Knots.ReidemeisterInvariance — Invariance of invariants under Reidemeister moves +================================================================================ + +Home of the invariance theorem: `alexanderPolynomialSigned` is invariant under +the three Reidemeister moves (issue #16650, tranche 3 of the Alexander socle, +strategy `docs/lean/alexander-strategy/c652-reidemeister-invariance.md`). + +Why a separate module: the theorem crosses `Reidemeister3Connected` +(`Knots.Reidemeister`) and `alexanderPolynomialSigned` (`Knots.Conway`). +`Knots.Conway` imports `Knots.Invariant`, which imports `Knots.Reidemeister` — +so importing `Knots.Conway` suffices to see both, and the converse would be a +cycle. This module is where the two theories meet. + +English mirror of `ReidemeisterInvariance.lean` (FR canonical). Convention EPIC +#4980 (ratified 2026-07-04, cf `code-style.md` §Lean i18n): distinct FR + EN +sibling files — no inline bilingual block. The module docstring and the theorem +docstrings below differ from the FR version; the body signatures, proofs and +tactics remain byte-identical between the two files. +-/ + +import Knots.Conway_en + +namespace Knots_en + +/-! ## 1. The `i = 0` / `i ≥ 1` split (a point the strategy misses) + +Strategy c652 (§4.1) presents R3 as "trivial by reindexation". That holds **under +a condition it does not state**: that the triangle lies entirely outside the row +the designated minor deletes. + +`alexanderPolynomialSigned` deletes the **first** row (`rest` = tail of +`crossings`) and the last column of the minor. Hence: + +* **`i ≥ 1`** — the three rewritten rows of the triangle lie in the body of the + matrix; invariance is a reindexation argument: the surgery changes neither the + number of crossings nor the number of edges, and the arc partition is + preserved (section 2 below). The minor is unchanged up to the transport of + columns. +* **`i = 0`** — row 0 carries a vertex of the triangle, and that is precisely + the row the designated minor **deletes**. Reindexation no longer suffices: the + minor changes shape (coefficients leave the triangle's columns for others), + and invariance can only be read up to a **unit** `±t^k` — this is the + determinantal argument of sections 4.2-4.3 of the strategy (non-shared column, + rank of the augmented minor). + +The two cases are therefore of different nature and must be distinct theorems. +Conflating them would make `i = 0` look like a missing proof when it is in fact +the case where the designated minor genuinely changes shape. + +## 2. The arc-partition preservation obligation + +The reindexation argument (`i ≥ 1`) rests on a premise the strategy **assumes +without proving**: `arcPartition` is preserved by the surgery. + +The obstacle is real: the connected R3 surgery rewrites the `(e2, e4)` pairs of +the triangle's three crossings, and those pairs **differ** between X and Y — + + X : (a₁,g₁), (g₁,g₃), (g₂,b₂) Y : (b₃,g₃), (a₁,b₂), (g₂,a₂) + +— so the generated over-strand relation changes. What is preserved is the +**multiset of labels** (docstring of `Reidemeister3Connected`), whence `wf`; the +partition itself is preserved only if the **closure** of the two relations +coincides, which is not a free fact. + +The control in section 3 checks this point on the lake's witness +(`reidemeister3Connected_satisfiable`): the closure there is identical although +the generated pairs differ. The general form remains to be established — it is +the first lock of the tranche, before any reindexation argument. +-/ + +/-! ## 3. Control: the R3 witness's arc partition is preserved + +The witness is that of `reidemeister3Connected_satisfiable` (literals copied +verbatim): both diagrams are well formed (`decide` on `wf` in the lake), and +their arc partition — 5 classes for 10 edges — is **the same** on both sides of +the surgery. This is the positive control of section 2: the rewritten `(e2,e4)` +pairs differ, their closure does not. +-/ + +/-- Control of tranche 3 (step 1): on the witness pair of the connected R3 move, + the surgery preserves `arcPartition` — the closure of the over-strand pairs + is unchanged although the triangle's three pairs are rewritten. This is the + first premise the reindexation argument (case `i ≥ 1`) assumes; the general + form remains to be proved. -/ +theorem reidemeister3Connected_arcPartition_witness : + arcPartition + { crossings := [⟨1, 2, 7, 8⟩, ⟨3, 7, 9, 4⟩, ⟨9, 8, 5, 6⟩, + ⟨1, 2, 10, 10⟩, ⟨3, 4, 5, 6⟩], numEdges := 10 } + = arcPartition + { crossings := [⟨3, 4, 9, 7⟩, ⟨9, 2, 5, 8⟩, ⟨7, 8, 1, 6⟩, + ⟨1, 2, 10, 10⟩, ⟨3, 4, 5, 6⟩], numEdges := 10 } := by + decide + +end Knots_en diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots_en.lean b/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots_en.lean index 909bb9c3f9..cc8776179e 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots_en.lean +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots_en.lean @@ -35,6 +35,7 @@ import Knots.Basic_en import Knots.Reidemeister_en import Knots.Invariant_en import Knots.Conway_en +import Knots.ReidemeisterInvariance_en import Knots.Jones_en import Knots.Lidman_en import Knots.MathlibPrerequisites_en From 78e8f801d49f8ddd89651b1d1cd1ca70beb35196 Mon Sep 17 00:00:00 2001 From: jsboige Date: Tue, 22 Sep 2026 19:12:35 +0200 Subject: [PATCH 2/4] fix(lean,#16650,#17412): reidemeister3Connected_arcPartition_witness -- 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\`). --- .../Knots/ReidemeisterInvariance.lean | 40 +++++++++---------- .../Knots/ReidemeisterInvariance_en.lean | 40 +++++++++---------- 2 files changed, 40 insertions(+), 40 deletions(-) diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance.lean b/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance.lean index 03fb3ed5fc..87820ad218 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance.lean +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance.lean @@ -50,20 +50,18 @@ c'est le cas ou le mineur designe change reellement de forme. L'argument de reindexation (`i ≥ 1`) repose sur une premiere que le cadrage **suppose sans la prouver** : `arcPartition` est preservee par la chirurgie. -L'obstacle est reel : la chirurgie R3 connectee reecrit les paires `(e2, e4)` -des trois croisements du triangle, et ces paires **different** entre X et Y — - - X : (a₁,g₁), (g₁,g₃), (g₂,b₂) Y : (b₃,g₃), (a₁,b₂), (g₂,a₂) - -— donc la relation de passage-dessus engendree change. Ce qui est preserve est -le **multi-ensemble des etiquettes** (docstring de `Reidemeister3Connected`), -d'ou `wf` ; la partition, elle, n'est preservee que si la **cloture** des deux -relations coincde, ce qui n'est pas un fait gratuit. - -Le controle de la section 3 verifie ce point sur le temoin du lake -(`reidemeister3Connected_satisfiable`) : la cloture y est identique alors que -les paires generatees diffèrent. La forme generale reste a etablir — c'est le -premier verrou de la tranche, avant tout argument de reindexation. +L'enonce general demande : la chirurgie R3 connectee reecrit les paires +`(e2, e4)` des trois croisements du triangle (cf `Conway.lean:350-354`, +`pairs := d.crossings.map (fun c => (c.e2, c.e4))`). Sur le temoin du lake +(`reidemeister3Connected_satisfiable`), ces paires, prises comme multi-ensemble +non ordonne (`mergePair` est symetrique en ses deux arguments), **coincident** +entre X et Y — la partition est donc preservee trivialement, et `decide` au +kernel suffit a etablir le theoreme. + +Ce temoin ne suffit donc pas, a lui seul, a fonder la preservation generale : +un contre-exemple minimal ou les paires `(e2, e4)` du triangle different entre +X et Y reste a exhiber. C'est le premier verrou de la tranche, avant tout +argument de reindexation. -/ /-! ## 3. Controle : la partition d'arcs du temoin R3 est preservee @@ -71,15 +69,17 @@ premier verrou de la tranche, avant tout argument de reindexation. Le temoin est celui de `reidemeister3Connected_satisfiable` (litteraux repris tels quels) : les deux diagrammes sont bien formes (`decide` sur `wf` au lake), et leur partition d'arcs — 5 classes pour 10 aretes — est **la meme** de part et -d'autre de la chirurgie. C'est le controle positif de la section 2 : les paires -`(e2,e4)` reecrites sont differentes, leur cloture non. +d'autre de la chirurgie. C'est le **controle trivial** de la section 2 : sur ce +temoin, les paires `(e2, e4)` du triangle, prises comme multi-ensemble, sont les +memes des deux cotes — la preservation est vide. Un contre-exemple ou elles +different reste a exhiber pour etablir la preservation generale. -/ /-- Controle de la tranche 3 (etape 1) : sur la paire temoin du move R3 - connecte, la chirurgie preserve `arcPartition` — la cloture des paires de - passage-dessus est inchangee bien que les trois paires du triangle soient - reecrites. C'est la premiere que l'argument de reindexation (cas `i ≥ 1`) - suppose ; la forme generale reste a prouver. -/ + connecte, la chirurgie preserve `arcPartition`. Sur ce temoin, les paires + `(e2, e4)` du triangle coincident comme multi-ensemble entre X et Y, donc la + preservation est triviale ; la forme generale (sur des diagrammes ou les + paires du triangle different) reste a prouver. -/ theorem reidemeister3Connected_arcPartition_witness : arcPartition { crossings := [⟨1, 2, 7, 8⟩, ⟨3, 7, 9, 4⟩, ⟨9, 8, 5, 6⟩, diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance_en.lean b/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance_en.lean index 9a4d726411..1f3d28d933 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance_en.lean +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance_en.lean @@ -53,20 +53,18 @@ the case where the designated minor genuinely changes shape. The reindexation argument (`i ≥ 1`) rests on a premise the strategy **assumes without proving**: `arcPartition` is preserved by the surgery. -The obstacle is real: the connected R3 surgery rewrites the `(e2, e4)` pairs of -the triangle's three crossings, and those pairs **differ** between X and Y — - - X : (a₁,g₁), (g₁,g₃), (g₂,b₂) Y : (b₃,g₃), (a₁,b₂), (g₂,a₂) - -— so the generated over-strand relation changes. What is preserved is the -**multiset of labels** (docstring of `Reidemeister3Connected`), whence `wf`; the -partition itself is preserved only if the **closure** of the two relations -coincides, which is not a free fact. - -The control in section 3 checks this point on the lake's witness -(`reidemeister3Connected_satisfiable`): the closure there is identical although -the generated pairs differ. The general form remains to be established — it is -the first lock of the tranche, before any reindexation argument. +The general statement requires: the connected R3 surgery rewrites the +`(e2, e4)` pairs of the triangle's three crossings (cf `Conway_en.lean:350-354`, +`pairs := d.crossings.map (fun c => (c.e2, c.e4))`). On the lake's witness +(`reidemeister3Connected_satisfiable`), those pairs, taken as an unordered +multiset (`mergePair` is symmetric in its two arguments), **coincide** between +X and Y — the partition is therefore preserved trivially, and `decide` at the +kernel suffices to discharge the theorem. + +This witness alone does not, however, ground the general preservation: a +minimal counterexample where the triangle's `(e2, e4)` pairs genuinely differ +between X and Y remains to be exhibited. This is the first lock of the +tranche, before any reindexation argument. -/ /-! ## 3. Control: the R3 witness's arc partition is preserved @@ -74,15 +72,17 @@ the first lock of the tranche, before any reindexation argument. The witness is that of `reidemeister3Connected_satisfiable` (literals copied verbatim): both diagrams are well formed (`decide` on `wf` in the lake), and their arc partition — 5 classes for 10 edges — is **the same** on both sides of -the surgery. This is the positive control of section 2: the rewritten `(e2,e4)` -pairs differ, their closure does not. +the surgery. This is the **trivial control** of section 2: on this witness, +the triangle's `(e2, e4)` pairs coincide as a multiset between X and Y — the +preservation is vacuous. A counterexample where they differ remains to be +exhibited to ground the general preservation. -/ /-- Control of tranche 3 (step 1): on the witness pair of the connected R3 move, - the surgery preserves `arcPartition` — the closure of the over-strand pairs - is unchanged although the triangle's three pairs are rewritten. This is the - first premise the reindexation argument (case `i ≥ 1`) assumes; the general - form remains to be proved. -/ + the surgery preserves `arcPartition`. On this witness, the triangle's + `(e2, e4)` pairs coincide as a multiset between X and Y, so the preservation + is trivial; the general form (on diagrams where the triangle's pairs differ) + remains to be proved. -/ theorem reidemeister3Connected_arcPartition_witness : arcPartition { crossings := [⟨1, 2, 7, 8⟩, ⟨3, 7, 9, 4⟩, ⟨9, 8, 5, 6⟩, From 6d0760e014ebf4abcbffff8699db26fc71659ef7 Mon Sep 17 00:00:00 2001 From: jsboige Date: Sat, 26 Sep 2026 22:16:50 +0200 Subject: [PATCH 3/4] fix(lean,#16650): docstrings FR/EN ReidemeisterInvariance - le temoin R3 n'est pas trivial MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Le diagnostic posé sur main (42281584939) 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 --- .../Knots/ReidemeisterInvariance.lean | 51 ++++++++++++------- .../Knots/ReidemeisterInvariance_en.lean | 47 ++++++++++------- 2 files changed, 61 insertions(+), 37 deletions(-) diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance.lean b/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance.lean index 87820ad218..74a8ca57ab 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance.lean +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance.lean @@ -50,18 +50,28 @@ c'est le cas ou le mineur designe change reellement de forme. L'argument de reindexation (`i ≥ 1`) repose sur une premiere que le cadrage **suppose sans la prouver** : `arcPartition` est preservee par la chirurgie. -L'enonce general demande : la chirurgie R3 connectee reecrit les paires -`(e2, e4)` des trois croisements du triangle (cf `Conway.lean:350-354`, +Precisons l'obstacle sur le temoin : la chirurgie R3 connectee reecrit les +paires `(e2, e4)` des trois croisements du triangle (cf `Conway.lean`, `pairs := d.crossings.map (fun c => (c.e2, c.e4))`). Sur le temoin du lake -(`reidemeister3Connected_satisfiable`), ces paires, prises comme multi-ensemble -non ordonne (`mergePair` est symetrique en ses deux arguments), **coincident** -entre X et Y — la partition est donc preservee trivialement, et `decide` au -kernel suffit a etablir le theoreme. - -Ce temoin ne suffit donc pas, a lui seul, a fonder la preservation generale : -un contre-exemple minimal ou les paires `(e2, e4)` du triangle different entre -X et Y reste a exhiber. C'est le premier verrou de la tranche, avant tout -argument de reindexation. +(`reidemeister3Connected_satisfiable`), ces paires coincident comme paires +**non orientees** — + + X : (2,8), (7,4), (8,6) Y : (4,7), (2,8), (8,6) + +— mais seule l'**orientation** de la paire centrale differe ((7,4) contre +(4,7)), et les croisements reecrits changent de **position** dans la liste du +repli. Le repli voit des paires orientees prises dans l'ordre de la liste : +la preservation n'y est donc **pas vide** — elle exige d'absorber l'une et +l'autre difference, par l'insensibilite a l'orientation d'une paire +(`mergePair_symm`, #17429) puis par la commutation des fusions au niveau des +classes (`mergePair_mergePair_comm_equiv`, #17646). Ce qui est preserve par +ailleurs est le **multi-ensemble des etiquettes** (docstring de +`Reidemeister3Connected`), d'ou `wf`. + +Ce temoin ne suffit pas, a lui seul, a fonder la preservation generale : un +diagramme ou les paires `(e2, e4)` du triangle different reellement comme +multi-ensemble reste a exhiber. C'est le premier verrou de la tranche, avant +tout argument de reindexation. -/ /-! ## 3. Controle : la partition d'arcs du temoin R3 est preservee @@ -69,17 +79,20 @@ argument de reindexation. Le temoin est celui de `reidemeister3Connected_satisfiable` (litteraux repris tels quels) : les deux diagrammes sont bien formes (`decide` sur `wf` au lake), et leur partition d'arcs — 5 classes pour 10 aretes — est **la meme** de part et -d'autre de la chirurgie. C'est le **controle trivial** de la section 2 : sur ce -temoin, les paires `(e2, e4)` du triangle, prises comme multi-ensemble, sont les -memes des deux cotes — la preservation est vide. Un contre-exemple ou elles -different reste a exhiber pour etablir la preservation generale. +d'autre de la chirurgie. C'est le controle positif de la section 2 : les paires +`(e2,e4)` du triangle y coincident non orientees, avec une orientation et une +position de repli differentes — le repli produit la meme partition, et c'est +`mergePair_symm` + la commutation des fusions qui le justifient. Un temoin ou +les paires different comme multi-ensemble reste a exhiber pour la preservation +generale. -/ /-- Controle de la tranche 3 (etape 1) : sur la paire temoin du move R3 - connecte, la chirurgie preserve `arcPartition`. Sur ce temoin, les paires - `(e2, e4)` du triangle coincident comme multi-ensemble entre X et Y, donc la - preservation est triviale ; la forme generale (sur des diagrammes ou les - paires du triangle different) reste a prouver. -/ + connecte, la chirurgie preserve `arcPartition` — les paires `(e2,e4)` du + triangle coincident non orientees, et le repli absorbe leurs differences + d'orientation et de position (`mergePair_symm`, commutation). C'est la + premiere que l'argument de reindexation (cas `i ≥ 1`) suppose ; la forme + generale reste a prouver. -/ theorem reidemeister3Connected_arcPartition_witness : arcPartition { crossings := [⟨1, 2, 7, 8⟩, ⟨3, 7, 9, 4⟩, ⟨9, 8, 5, 6⟩, diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance_en.lean b/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance_en.lean index 1f3d28d933..bf62637c6e 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance_en.lean +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance_en.lean @@ -53,18 +53,27 @@ the case where the designated minor genuinely changes shape. The reindexation argument (`i ≥ 1`) rests on a premise the strategy **assumes without proving**: `arcPartition` is preserved by the surgery. -The general statement requires: the connected R3 surgery rewrites the -`(e2, e4)` pairs of the triangle's three crossings (cf `Conway_en.lean:350-354`, -`pairs := d.crossings.map (fun c => (c.e2, c.e4))`). On the lake's witness -(`reidemeister3Connected_satisfiable`), those pairs, taken as an unordered -multiset (`mergePair` is symmetric in its two arguments), **coincide** between -X and Y — the partition is therefore preserved trivially, and `decide` at the -kernel suffices to discharge the theorem. +Let us make the obstacle precise on the witness: the connected R3 surgery +rewrites the `(e2, e4)` pairs of the triangle's three crossings (cf +`Conway_en.lean`, `pairs := d.crossings.map (fun c => (c.e2, c.e4))`). On the +lake's witness (`reidemeister3Connected_satisfiable`), those pairs coincide as +**unordered** pairs — + + X : (2,8), (7,4), (8,6) Y : (4,7), (2,8), (8,6) + +— but only the **orientation** of the middle pair differs ((7,4) versus (4,7)), +and the rewritten crossings change **position** in the fold's list. The fold +sees oriented pairs taken in list order: the preservation is therefore **not +vacuous** — it requires absorbing both differences, through insensitivity to a +pair's orientation (`mergePair_symm`, #17429) and through commutation of the +fusions at the class level (`mergePair_mergePair_comm_equiv`, #17646). What is +preserved besides is the **multiset of labels** (docstring of +`Reidemeister3Connected`), whence `wf`. This witness alone does not, however, ground the general preservation: a -minimal counterexample where the triangle's `(e2, e4)` pairs genuinely differ -between X and Y remains to be exhibited. This is the first lock of the -tranche, before any reindexation argument. +diagram where the triangle's `(e2, e4)` pairs genuinely differ as a multiset +remains to be exhibited. This is the first lock of the tranche, before any +reindexation argument. -/ /-! ## 3. Control: the R3 witness's arc partition is preserved @@ -72,17 +81,19 @@ tranche, before any reindexation argument. The witness is that of `reidemeister3Connected_satisfiable` (literals copied verbatim): both diagrams are well formed (`decide` on `wf` in the lake), and their arc partition — 5 classes for 10 edges — is **the same** on both sides of -the surgery. This is the **trivial control** of section 2: on this witness, -the triangle's `(e2, e4)` pairs coincide as a multiset between X and Y — the -preservation is vacuous. A counterexample where they differ remains to be -exhibited to ground the general preservation. +the surgery. This is the positive control of section 2: the triangle's `(e2,e4)` +pairs there coincide unordered, with differing orientation and fold position — +the fold still yields the same partition, and it is `mergePair_symm` plus the +commutation of the fusions that justify it. A witness where the pairs differ as +a multiset remains to be exhibited for the general preservation. -/ /-- Control of tranche 3 (step 1): on the witness pair of the connected R3 move, - the surgery preserves `arcPartition`. On this witness, the triangle's - `(e2, e4)` pairs coincide as a multiset between X and Y, so the preservation - is trivial; the general form (on diagrams where the triangle's pairs differ) - remains to be proved. -/ + the surgery preserves `arcPartition` — the triangle's `(e2,e4)` pairs + coincide unordered, and the fold absorbs their orientation and position + differences (`mergePair_symm`, commutation). This is the first premise the + reindexation argument (case `i ≥ 1`) assumes; the general form remains to be + proved. -/ theorem reidemeister3Connected_arcPartition_witness : arcPartition { crossings := [⟨1, 2, 7, 8⟩, ⟨3, 7, 9, 4⟩, ⟨9, 8, 5, 6⟩, From ec76365aaf5bc1cd3845c84ec10a075f5f81c958 Mon Sep 17 00:00:00 2001 From: jsboige Date: Sun, 27 Sep 2026 02:02:35 +0200 Subject: [PATCH 4/4] feat(lean,#16650): fold insensible a la permutation de paires adjacentes 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 --- .../Lean/knot_lean/Knots/Conway.lean | 93 +++++++++++++++++++ .../Lean/knot_lean/Knots/Conway_en.lean | 93 +++++++++++++++++++ .../Knots/ReidemeisterInvariance.lean | 12 +-- .../Knots/ReidemeisterInvariance_en.lean | 13 +-- 4 files changed, 199 insertions(+), 12 deletions(-) diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/Conway.lean b/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/Conway.lean index 80c85d44a2..f5744e19b6 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/Conway.lean +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/Conway.lean @@ -777,6 +777,99 @@ theorem mergePair_mergePair_comm_equiv (P : List (List Nat)) (a b c d x y : Nat) rw [sameClass_two_merges_iff, sameClass_two_merges_comm_form, ← sameClass_two_merges_iff (a := c) (b := d) (c := a) (d := b)] +/-- `Touches` lu en `SameClass` : une étiquette est happée par la fusion + `{x, y}` exactement quand elle partage une classe avec `x` ou avec `y`. + C'est la cle qui rend la caractérisation de `SameClass` après fusion + transportable d'une partition à une autre. -/ +lemma touches_iff_sameClass {P : List (List Nat)} {x y z : Nat} : + Touches P x y z ↔ (SameClass P x z ∨ SameClass P y z) := by + constructor + · rintro ⟨C, hC, hz, hcond⟩ + rw [hit_iff_mem] at hcond + rcases hcond with hx | hy + · exact Or.inl ⟨C, hC, hx, hz⟩ + · exact Or.inr ⟨C, hC, hy, hz⟩ + · rintro (⟨C, hC, hx, hz⟩ | ⟨C, hC, hy, hz⟩) + · exact ⟨C, hC, hz, by rw [hit_iff_mem]; exact Or.inl hx⟩ + · exact ⟨C, hC, hz, by rw [hit_iff_mem]; exact Or.inr hy⟩ + +/-- Caractérisation pure de `SameClass` après une fusion : une classe + commune conservée, ou deux étiquettes toutes deux happées — lu + entièrement en `SameClass` de la partition d'origine. C'est cette forme + qui fait du repli une congruence pour `SameClass`. -/ +lemma sameClass_mergePair_pure {P : List (List Nat)} {x y u v : Nat} : + SameClass (mergePair P x y) u v ↔ + SameClass P u v ∨ + ((SameClass P x u ∨ SameClass P y u) ∧ + (SameClass P x v ∨ SameClass P y v)) := by + rw [sameClass_mergePair_iff, touches_iff_sameClass, touches_iff_sameClass] + constructor + · rintro (⟨C, hC, hu, hv, _⟩ | h) + · exact Or.inl ⟨C, hC, hu, hv⟩ + · exact Or.inr h + · rintro (⟨C, hC, hu, hv⟩ | h) + · by_cases hcond : ((C.contains x || C.contains y) = true) + · rw [hit_iff_mem] at hcond + rcases hcond with hx | hy + · exact Or.inr ⟨Or.inl ⟨C, hC, hx, hu⟩, Or.inl ⟨C, hC, hx, hv⟩⟩ + · exact Or.inr ⟨Or.inr ⟨C, hC, hy, hu⟩, Or.inr ⟨C, hC, hy, hv⟩⟩ + · exact Or.inl ⟨C, hC, hu, hv, hcond⟩ + · exact Or.inr h + +/-- **Congruence du repli** : si deux partitions sont indiscernables par + `SameClass`, le repli d'une même liste de paires les laisse + indiscernables. Le repli ne voit jamais la forme des listes de classes, + seulement qui partage une classe. -/ +lemma foldl_mergeStep_congr {Q₁ Q₂ : List (List Nat)} + (h : ∀ w z, SameClass Q₁ w z ↔ SameClass Q₂ w z) + (pairs : List (Nat × Nat)) : + ∀ w z, SameClass (pairs.foldl mergeStep Q₁) w z ↔ + SameClass (pairs.foldl mergeStep Q₂) w z := by + induction pairs generalizing Q₁ Q₂ with + | nil => exact h + | cons p rest ih => + refine ih ?_ + intro w z + show SameClass (mergePair Q₁ p.1 p.2) w z ↔ SameClass (mergePair Q₂ p.1 p.2) w z + rw [sameClass_mergePair_pure, sameClass_mergePair_pure, + h w z, h p.1 w, h p.2 w, h p.1 z, h p.2 z] + +/-- **Le repli est insensible à la permutation de deux paires adjacentes** : + échanger les positions `i` et `i + 1` de la liste de paires ne change + pas la relation `SameClass` du résultat du repli. Troisième brique de + l'invariance R3 (issue #16650) : la chirurgie R3 connexe déplace les + croisements réécrits dans la liste du repli, `foldl_mergePair_swap` + absorbe l'orientation, `mergePair_mergePair_comm_equiv` la commutation + des deux fusions, et la congruence `foldl_mergeStep_congr` transporte + l'équivalence à travers le reste du repli. Ensemble, elles fondent la + préservation de la partition d'arcs sur le témoin du lake. -/ +theorem foldl_mergePair_permute_adjacent (pairs : List (Nat × Nat)) (i : Nat) + (hi : i + 1 < pairs.length) (P₀ : List (List Nat)) (w z : Nat) : + SameClass + ((pairs.take i ++ [pairs.get ⟨i, Nat.lt_of_succ_lt hi⟩, + pairs.get ⟨i + 1, hi⟩] ++ pairs.drop (i + 2)).foldl + mergeStep P₀) w z ↔ + SameClass + ((pairs.take i ++ [pairs.get ⟨i + 1, hi⟩, + pairs.get ⟨i, Nat.lt_of_succ_lt hi⟩] ++ pairs.drop + (i + 2)).foldl mergeStep P₀) w z := by + have hfold : ∀ (r s : Nat × Nat), + ((pairs.take i ++ [r, s] ++ pairs.drop (i + 2)).foldl mergeStep P₀) + = (pairs.drop (i + 2)).foldl mergeStep + (mergeStep (mergeStep ((pairs.take i).foldl mergeStep P₀) r) s) := by + intro r s + rw [List.foldl_append, List.foldl_append, List.foldl_cons, List.foldl_cons, + List.foldl_nil] + rw [hfold (pairs.get ⟨i, Nat.lt_of_succ_lt hi⟩) (pairs.get ⟨i + 1, hi⟩), + hfold (pairs.get ⟨i + 1, hi⟩) (pairs.get ⟨i, Nat.lt_of_succ_lt hi⟩)] + exact foldl_mergeStep_congr + (mergePair_mergePair_comm_equiv ((pairs.take i).foldl mergeStep P₀) + (pairs.get ⟨i, Nat.lt_of_succ_lt hi⟩).1 + (pairs.get ⟨i, Nat.lt_of_succ_lt hi⟩).2 + (pairs.get ⟨i + 1, hi⟩).1 + (pairs.get ⟨i + 1, hi⟩).2) + (pairs.drop (i + 2)) w z + /-- Toute étiquette de la plage `1..n` est couverte par les singletons initiaux. -/ lemma covered_singles {n z : Nat} (h1 : 1 ≤ z) (h2 : z ≤ n) : Covered ((List.range n).map (fun i => [i + 1])) z := by diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/Conway_en.lean b/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/Conway_en.lean index 71ef72e1e4..679491ad0d 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/Conway_en.lean +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/Conway_en.lean @@ -781,6 +781,99 @@ theorem mergePair_mergePair_comm_equiv (P : List (List Nat)) (a b c d x y : Nat) rw [sameClass_two_merges_iff, sameClass_two_merges_comm_form, ← sameClass_two_merges_iff (a := c) (b := d) (c := a) (d := b)] +/-- `Touches` read as `SameClass`: a label is caught by the merge `{x, y}` + exactly when it shares a class with `x` or with `y`. This is the key + that makes the characterization of `SameClass` after a merge + transportable from one partition to another. -/ +lemma touches_iff_sameClass {P : List (List Nat)} {x y z : Nat} : + Touches P x y z ↔ (SameClass P x z ∨ SameClass P y z) := by + constructor + · rintro ⟨C, hC, hz, hcond⟩ + rw [hit_iff_mem] at hcond + rcases hcond with hx | hy + · exact Or.inl ⟨C, hC, hx, hz⟩ + · exact Or.inr ⟨C, hC, hy, hz⟩ + · rintro (⟨C, hC, hx, hz⟩ | ⟨C, hC, hy, hz⟩) + · exact ⟨C, hC, hz, by rw [hit_iff_mem]; exact Or.inl hx⟩ + · exact ⟨C, hC, hz, by rw [hit_iff_mem]; exact Or.inr hy⟩ + +/-- Pure characterization of `SameClass` after one merge: a common class + kept intact, or two labels both caught — read entirely in `SameClass` + of the source partition. This shape is what turns the fold into a + congruence for `SameClass`. -/ +lemma sameClass_mergePair_pure {P : List (List Nat)} {x y u v : Nat} : + SameClass (mergePair P x y) u v ↔ + SameClass P u v ∨ + ((SameClass P x u ∨ SameClass P y u) ∧ + (SameClass P x v ∨ SameClass P y v)) := by + rw [sameClass_mergePair_iff, touches_iff_sameClass, touches_iff_sameClass] + constructor + · rintro (⟨C, hC, hu, hv, _⟩ | h) + · exact Or.inl ⟨C, hC, hu, hv⟩ + · exact Or.inr h + · rintro (⟨C, hC, hu, hv⟩ | h) + · by_cases hcond : ((C.contains x || C.contains y) = true) + · rw [hit_iff_mem] at hcond + rcases hcond with hx | hy + · exact Or.inr ⟨Or.inl ⟨C, hC, hx, hu⟩, Or.inl ⟨C, hC, hx, hv⟩⟩ + · exact Or.inr ⟨Or.inr ⟨C, hC, hy, hu⟩, Or.inr ⟨C, hC, hy, hv⟩⟩ + · exact Or.inl ⟨C, hC, hu, hv, hcond⟩ + · exact Or.inr h + +/-- **Congruence of the fold**: if two partitions are indistinguishable + through `SameClass`, folding the same list of pairs leaves them + indistinguishable. The fold never sees the shape of the class lists, + only who shares a class. -/ +lemma foldl_mergeStep_congr {Q₁ Q₂ : List (List Nat)} + (h : ∀ w z, SameClass Q₁ w z ↔ SameClass Q₂ w z) + (pairs : List (Nat × Nat)) : + ∀ w z, SameClass (pairs.foldl mergeStep Q₁) w z ↔ + SameClass (pairs.foldl mergeStep Q₂) w z := by + induction pairs generalizing Q₁ Q₂ with + | nil => exact h + | cons p rest ih => + refine ih ?_ + intro w z + show SameClass (mergePair Q₁ p.1 p.2) w z ↔ SameClass (mergePair Q₂ p.1 p.2) w z + rw [sameClass_mergePair_pure, sameClass_mergePair_pure, + h w z, h p.1 w, h p.2 w, h p.1 z, h p.2 z] + +/-- **The fold is insensitive to permuting two adjacent pairs**: swapping + positions `i` and `i + 1` of the pair list does not change the + `SameClass` relation of the fold's result. Third brick of R3 invariance + (issue #16650): the connected R3 surgery moves the rewritten crossings + inside the fold's list, `foldl_mergePair_swap` absorbs the orientation, + `mergePair_mergePair_comm_equiv` the commutation of the two merges, and + the congruence `foldl_mergeStep_congr` carries the equivalence through + the rest of the fold. Together they ground the preservation of the arc + partition on the lake's witness. -/ +theorem foldl_mergePair_permute_adjacent (pairs : List (Nat × Nat)) (i : Nat) + (hi : i + 1 < pairs.length) (P₀ : List (List Nat)) (w z : Nat) : + SameClass + ((pairs.take i ++ [pairs.get ⟨i, Nat.lt_of_succ_lt hi⟩, + pairs.get ⟨i + 1, hi⟩] ++ pairs.drop (i + 2)).foldl + mergeStep P₀) w z ↔ + SameClass + ((pairs.take i ++ [pairs.get ⟨i + 1, hi⟩, + pairs.get ⟨i, Nat.lt_of_succ_lt hi⟩] ++ pairs.drop + (i + 2)).foldl mergeStep P₀) w z := by + have hfold : ∀ (r s : Nat × Nat), + ((pairs.take i ++ [r, s] ++ pairs.drop (i + 2)).foldl mergeStep P₀) + = (pairs.drop (i + 2)).foldl mergeStep + (mergeStep (mergeStep ((pairs.take i).foldl mergeStep P₀) r) s) := by + intro r s + rw [List.foldl_append, List.foldl_append, List.foldl_cons, List.foldl_cons, + List.foldl_nil] + rw [hfold (pairs.get ⟨i, Nat.lt_of_succ_lt hi⟩) (pairs.get ⟨i + 1, hi⟩), + hfold (pairs.get ⟨i + 1, hi⟩) (pairs.get ⟨i, Nat.lt_of_succ_lt hi⟩)] + exact foldl_mergeStep_congr + (mergePair_mergePair_comm_equiv ((pairs.take i).foldl mergeStep P₀) + (pairs.get ⟨i, Nat.lt_of_succ_lt hi⟩).1 + (pairs.get ⟨i, Nat.lt_of_succ_lt hi⟩).2 + (pairs.get ⟨i + 1, hi⟩).1 + (pairs.get ⟨i + 1, hi⟩).2) + (pairs.drop (i + 2)) w z + /-- Every label of the range `1..n` is covered by the initial singletons. -/ lemma covered_singles {n z : Nat} (h1 : 1 ≤ z) (h2 : z ≤ n) : Covered ((List.range n).map (fun i => [i + 1])) z := by diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance.lean b/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance.lean index 74a8ca57ab..6bcdbc6c3e 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance.lean +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance.lean @@ -82,17 +82,17 @@ et leur partition d'arcs — 5 classes pour 10 aretes — est **la meme** de par d'autre de la chirurgie. C'est le controle positif de la section 2 : les paires `(e2,e4)` du triangle y coincident non orientees, avec une orientation et une position de repli differentes — le repli produit la meme partition, et c'est -`mergePair_symm` + la commutation des fusions qui le justifient. Un temoin ou -les paires different comme multi-ensemble reste a exhiber pour la preservation -generale. +`foldl_mergePair_swap` (orientation) puis `foldl_mergePair_permute_adjacent` +(transposition des positions) qui le justifient. Un temoin ou les paires +different comme multi-ensemble reste a exhiber pour la preservation generale. -/ /-- Controle de la tranche 3 (etape 1) : sur la paire temoin du move R3 connecte, la chirurgie preserve `arcPartition` — les paires `(e2,e4)` du triangle coincident non orientees, et le repli absorbe leurs differences - d'orientation et de position (`mergePair_symm`, commutation). C'est la - premiere que l'argument de reindexation (cas `i ≥ 1`) suppose ; la forme - generale reste a prouver. -/ + d'orientation et de position (`foldl_mergePair_swap`, + `foldl_mergePair_permute_adjacent`). C'est la premiere que l'argument de + reindexation (cas `i ≥ 1`) suppose ; la forme generale reste a prouver. -/ theorem reidemeister3Connected_arcPartition_witness : arcPartition { crossings := [⟨1, 2, 7, 8⟩, ⟨3, 7, 9, 4⟩, ⟨9, 8, 5, 6⟩, diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance_en.lean b/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance_en.lean index bf62637c6e..402f681355 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance_en.lean +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance_en.lean @@ -83,17 +83,18 @@ verbatim): both diagrams are well formed (`decide` on `wf` in the lake), and their arc partition — 5 classes for 10 edges — is **the same** on both sides of the surgery. This is the positive control of section 2: the triangle's `(e2,e4)` pairs there coincide unordered, with differing orientation and fold position — -the fold still yields the same partition, and it is `mergePair_symm` plus the -commutation of the fusions that justify it. A witness where the pairs differ as -a multiset remains to be exhibited for the general preservation. +the fold still yields the same partition, and it is `foldl_mergePair_swap` +(orientation) then `foldl_mergePair_permute_adjacent` (transposition of +positions) that justify it. A witness where the pairs differ as a multiset +remains to be exhibited for the general preservation. -/ /-- Control of tranche 3 (step 1): on the witness pair of the connected R3 move, the surgery preserves `arcPartition` — the triangle's `(e2,e4)` pairs coincide unordered, and the fold absorbs their orientation and position - differences (`mergePair_symm`, commutation). This is the first premise the - reindexation argument (case `i ≥ 1`) assumes; the general form remains to be - proved. -/ + differences (`foldl_mergePair_swap`, `foldl_mergePair_permute_adjacent`). + This is the first premise the reindexation argument (case `i ≥ 1`) assumes; + the general form remains to be proved. -/ theorem reidemeister3Connected_arcPartition_witness : arcPartition { crossings := [⟨1, 2, 7, 8⟩, ⟨3, 7, 9, 4⟩, ⟨9, 8, 5, 6⟩,