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

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

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

MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance.lean

@@ -50,36 +50,49 @@ 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
 
 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
+`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`. 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 (`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⟩,

MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance_en.lean

@@ -53,36 +53,48 @@ 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
 
 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 `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`. 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 (`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⟩,