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

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

@@ -89,4 +89,89 @@ theorem reidemeister3Connected_arcPartition_witness :
                         ⟨1, 2, 10, 10⟩, ⟨3, 4, 5, 6⟩], numEdges := 10 } := by
   decide
 
+/-! ## 4. Controle negatif : le mineur designe s'effondre sur le temoin Y
+
+La section 3 etablit la **premiere** de l'argument de reindexation (la
+partition d'arcs est preservee). Le controle de **conclusion** attendu — le
+polynome signe du temoin est le meme des deux cotes — est **refute sur ce
+temoin**, et c'est une information de cadrage, pas un echec de preuve :
+
+* cote X, le mineur designe vaut `t³ - t²` (chiralite toute positive) ;
+* cote Y, le mineur designe est **identiquement nul** — et la sonde Python
+  fidele a la construction (validee sur les valeurs kernel de `trefoil` et
+  `figureEight` signe) mesure la meme nullite pour chacune des cinq colonnes
+  supprimables et chacune des 32 chiralites.
+
+La cause se lit sur les lignes de la matrice : la chirurgie reecrit
+`(9, 8, 5, 6)` en `(7, 8, 1, 6)`, dont toutes les etiquettes non singleton
+(`7`, `8`, `6`) tombent dans la grande classe du temoin — sa ligne, comme
+celle du kink `(1, 2, 10, 10)` (kink R1 exact : `e3 = e4`), ne porte plus que
+sur la colonne de l'arc singleton `{1}` et sur la colonne supprimee de la
+grande classe. Deux lignes proportionnelles : le rang tombe a 3 et tout
+mineur `4 × 4` s'annule.
+
+Le classique « tout mineur `(n-1) × (n-1)` de la matrice d'Alexander vaut
+`± t^k · Δ` » suppose la matrice de rang `n - 1` ; le kink ajoute une
+relation, et la normalisation designee (premiere ligne et derniere colonne
+supprimees, **fixes**) ne survit pas a la chirurgie. Consequence pour la
+section 1 : l'argument de reindexation du cas `i ≥ 1` devra soit s'entenir
+de diagrammes sans kink, soit rendre le couple (ligne, colonne) supprime
+adaptatif.
+-/
+
+/-- Determinant 4×4 generique, meme esprit que `det_two_aux` / `det_three_aux`
+    de `Conway.lean` : expansion de Laplace le long de la premiere colonne, les
+    mineurs 3×3 etant traites par `det_three_aux`. -/
+theorem det_four_aux (A : Matrix (Fin 4) (Fin 4) (Polynomial ℤ)) :
+    A.det = A 0 0 * (A.submatrix (Fin.succAbove 0) (Fin.succAbove 0)).det
+          - A 1 0 * (A.submatrix (Fin.succAbove 1) (Fin.succAbove 0)).det
+          + A 2 0 * (A.submatrix (Fin.succAbove 2) (Fin.succAbove 0)).det
+          - A 3 0 * (A.submatrix (Fin.succAbove 3) (Fin.succAbove 0)).det := by
+  rw [Matrix.det_succ_column_zero]
+  simp (config := { decide := true }) [Fin.sum_univ_succ]
+  simp (config := { decide := true }) [det_three_aux, Matrix.submatrix_apply,
+    Fin.succAbove]
+  ring
+
+/-- Controle de la tranche 3 : cote X, le mineur designe du polynome signe
+    (chiralite toute positive) vaut `t³ - t²` — il n'est pas degenere. C'est la
+    contrepartie positive du controle negatif suivant : c'est bien la chirurgie
+    qui effondre le mineur, pas une degenerescence anterieure. -/
+theorem reidemeister3Connected_alexanderSigned_witness_X :
+    alexanderPolynomialSigned
+        { crossings := [⟨1, 2, 7, 8⟩, ⟨3, 7, 9, 4⟩, ⟨9, 8, 5, 6⟩,
+                        ⟨1, 2, 10, 10⟩, ⟨3, 4, 5, 6⟩], numEdges := 10 }
+        [true, true, true, true, true]
+      = Polynomial.X ^ 3 - Polynomial.X ^ 2 := by
+  simp only [alexanderPolynomialSigned]
+  simp (config := { decide := true })
+  rw [det_four_aux]
+  simp only [det_three_aux]
+  simp only [Matrix.submatrix_apply, Fin.succAbove, Matrix.of_apply]
+  simp (config := { decide := true }) [alexanderEntrySigned, alexanderEntry,
+    alexanderEntryNeg]
+  ring
+
+/-- Controle negatif de la tranche 3 : cote Y, **le meme mineur designe est
+    identiquement nul** — la chirurgie R3 du temoin aligne la ligne du
+    croisement reecrit `(7, 8, 1, 6)` sur celle du kink `(1, 2, 10, 10)`
+    (toutes deux ne portent plus que sur l'arc singleton `{1}` et la grande
+    classe supprimee), le rang tombe a 3 et le determinant s'annule (sonde :
+    nullite pour les cinq colonnes supprimables et les 32 chiralites). La
+    normalisation designee ne survit pas a la chirurgie sur un temoin porteur
+    de kink — cf section 4 du module. -/
+theorem reidemeister3Connected_alexanderSigned_witness_Y_zero :
+    alexanderPolynomialSigned
+        { crossings := [⟨3, 4, 9, 7⟩, ⟨9, 2, 5, 8⟩, ⟨7, 8, 1, 6⟩,
+                        ⟨1, 2, 10, 10⟩, ⟨3, 4, 5, 6⟩], numEdges := 10 }
+        [true, true, true, true, true]
+      = 0 := by
+  simp only [alexanderPolynomialSigned]
+  simp (config := { decide := true })
+  rw [det_four_aux]
+  simp only [det_three_aux]
+  simp only [Matrix.submatrix_apply, Fin.succAbove, Matrix.of_apply]
+  simp (config := { decide := true }) [alexanderEntrySigned, alexanderEntry,
+    alexanderEntryNeg]
+
 end Knots

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

@@ -92,4 +92,88 @@ theorem reidemeister3Connected_arcPartition_witness :
                         ⟨1, 2, 10, 10⟩, ⟨3, 4, 5, 6⟩], numEdges := 10 } := by
   decide
 
+/-! ## 4. Negative control: the designated minor collapses on the Y witness
+
+Section 3 establishes the **first premise** of the reindexation argument (the
+arc partition is preserved). The expected **conclusion** control — the signed
+polynomial of the witness is the same on both sides — is **refuted on this
+witness**, and that is framing information, not a proof failure:
+
+* on the X side, the designated minor is `t³ - t²` (all-positive chirality);
+* on the Y side, the designated minor is **identically zero** — and the Python
+  probe faithful to the construction (validated against the kernel values of
+  the signed `trefoil` and `figureEight`) measures the same nullity for each
+  of the five deletable columns and each of the 32 chirality assignments.
+
+The cause reads off the matrix rows: the surgery rewrites `(9, 8, 5, 6)` into
+`(7, 8, 1, 6)`, whose non-singleton labels (`7`, `8`, `6`) all fall into the
+witness's big class — its row, like the kink row `(1, 2, 10, 10)` (an exact
+R1 kink: `e3 = e4`), now only touches the singleton arc column `{1}` and the
+deleted big-class column. Two proportional rows: the rank drops to 3 and
+every `4 × 4` minor vanishes.
+
+The classical "every `(n-1) × (n-1)` minor of the Alexander matrix equals
+`± t^k · Δ`" assumes the matrix has rank `n - 1`; the kink adds a relation,
+and the designated normalization (first row and last column deleted,
+**fixed**) does not survive the surgery. Consequence for section 1: the
+reindexation argument of the `i ≥ 1` case must either restrict to kink-free
+diagrams or make the deleted (row, column) pair adaptive.
+-/
+
+/-- Generic 4×4 determinant, same spirit as `det_two_aux` / `det_three_aux`
+    from `Conway.lean`: Laplace expansion along the first column, the 3×3
+    minors being handled by `det_three_aux`. -/
+theorem det_four_aux (A : Matrix (Fin 4) (Fin 4) (Polynomial ℤ)) :
+    A.det = A 0 0 * (A.submatrix (Fin.succAbove 0) (Fin.succAbove 0)).det
+          - A 1 0 * (A.submatrix (Fin.succAbove 1) (Fin.succAbove 0)).det
+          + A 2 0 * (A.submatrix (Fin.succAbove 2) (Fin.succAbove 0)).det
+          - A 3 0 * (A.submatrix (Fin.succAbove 3) (Fin.succAbove 0)).det := by
+  rw [Matrix.det_succ_column_zero]
+  simp (config := { decide := true }) [Fin.sum_univ_succ]
+  simp (config := { decide := true }) [det_three_aux, Matrix.submatrix_apply,
+    Fin.succAbove]
+  ring
+
+/-- Tranche 3 control: on the X side, the designated minor of the signed
+    polynomial (all-positive chirality) equals `t³ - t²` — it is not
+    degenerate. This is the positive counterpart of the negative control
+    below: it is the surgery that collapses the minor, not a prior
+    degeneracy. -/
+theorem reidemeister3Connected_alexanderSigned_witness_X :
+    alexanderPolynomialSigned
+        { crossings := [⟨1, 2, 7, 8⟩, ⟨3, 7, 9, 4⟩, ⟨9, 8, 5, 6⟩,
+                        ⟨1, 2, 10, 10⟩, ⟨3, 4, 5, 6⟩], numEdges := 10 }
+        [true, true, true, true, true]
+      = Polynomial.X ^ 3 - Polynomial.X ^ 2 := by
+  simp only [alexanderPolynomialSigned]
+  simp (config := { decide := true })
+  rw [det_four_aux]
+  simp only [det_three_aux]
+  simp only [Matrix.submatrix_apply, Fin.succAbove, Matrix.of_apply]
+  simp (config := { decide := true }) [alexanderEntrySigned, alexanderEntry,
+    alexanderEntryNeg]
+  ring
+
+/-- Tranche 3 negative control: on the Y side, **the same designated minor is
+    identically zero** — the witness's R3 surgery aligns the rewritten
+    crossing's row `(7, 8, 1, 6)` with the kink row `(1, 2, 10, 10)` (both now
+    only touch the singleton arc `{1}` and the deleted big class), the rank
+    drops to 3 and the determinant vanishes (probe: null for all five
+    deletable columns and all 32 chirality assignments). The designated
+    normalization does not survive the surgery on a kink-carrying witness —
+    cf section 4 of the module. -/
+theorem reidemeister3Connected_alexanderSigned_witness_Y_zero :
+    alexanderPolynomialSigned
+        { crossings := [⟨3, 4, 9, 7⟩, ⟨9, 2, 5, 8⟩, ⟨7, 8, 1, 6⟩,
+                        ⟨1, 2, 10, 10⟩, ⟨3, 4, 5, 6⟩], numEdges := 10 }
+        [true, true, true, true, true]
+      = 0 := by
+  simp only [alexanderPolynomialSigned]
+  simp (config := { decide := true })
+  rw [det_four_aux]
+  simp only [det_three_aux]
+  simp only [Matrix.submatrix_apply, Fin.succAbove, Matrix.of_apply]
+  simp (config := { decide := true }) [alexanderEntrySigned, alexanderEntry,
+    alexanderEntryNeg]
+
 end Knots_en