diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/KNOTS-01-Conway-Proofs-Lean-Python.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/KNOTS-01-Conway-Proofs-Lean-Python.ipynb index 067a7d0d369..be65b9e5a7b 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/KNOTS-01-Conway-Proofs-Lean-Python.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/KNOTS-01-Conway-Proofs-Lean-Python.ipynb @@ -173,11 +173,35 @@ "| Alexander polynomial | 1 | $t - 1 + t^{-1}$ | $-t + 3 - t^{-1}$ |\n", "| Jones polynomial | 1 | $-t^{-4} + t^{-3} + t^{-1}$ | $t^2 - t + 1 - t^{-1} + t^{-2}$ |\n", "| Unknotting number | 0 | 1 | 1 |\n", - "| Slice? | Oui | Non | Oui |\n", + "| Slice? | Oui | Non | Non (det 5, pas un carré) |\n", + "\n", + "Le **4₁ n'est pas slice** : un nœud slice a un déterminant qui est un\n", + "carré parfait (condition **nécessaire** de Fox–Milnor :\n", + "$|\\Delta(-1)| = 1, 4, 9, 16, \\ldots$).\n", + "Or $\\det(4_1) = |\\Delta(-1)| = 5$ — la condition de Fox–Milnor échoue\n", + "(valeur documentée par `KNOTS/knot_lean/Knots/FigureEight.lean` ligne 17 :\n", + "`det(4_1) = |Δ(-1)| = 5`).\n", + "Attention : le déterminant non-carré n'est qu'**une** obstruction parmi\n", + "d'autres, pas un critère autonome de non-sliceness. Une seconde voie, plus\n", + "élémentaire, écarte $4_1$ sans passer par Fox–Milnor : l'obstruction de\n", + "**signature** — la signature de Levine–Tristram est un invariant de\n", + "concordance, nul sur tout nœud slice, or $|\\sigma(4_1)| = 2 \\neq 0$.\n", + "C'est un fait classique, que le module Lean ne calcule pas (voir les\n", + "limitations rappelées ci-dessous). Le nœud de huit est **rationnellement slice**\n", + "\n", + "— il le devient après une somme connexe avec lui-même — mais il n'est\n", + "**pas** slice (au sens lisse) : sa sliceness lisse est une question\n", + "distincte de sa sliceness topologique, et c'est un cas d'école de la\n", + "théorie des nœuds (le « 4_1 est-il topologiquement slice ? » a été\n", + "résolu positivement, mais sa sliceness lisse n'est pas triviale et\n", + "dépend de questions de signature). Voir `Knots/FigureEight.lean` du\n", + "scaffold `knot_lean/` pour les détails et les limitations (notamment :\n", + "« Pas d'invariance de Reidemeister » dans le module, qui limite le\n", + "claim au calcul sur le diagramme désigné).\n", "\n", "La **3-colorabilité** est l'invariant le plus simple : peut-on colorer\n", "les brins du diagramme avec 3 couleurs, de sorte qu'à chaque croisement\n", - "les 3 brins soient soit tous de la même couleur, soit tous différents ?" + "les 3 brins soient soit tous de la même couleur, soit tous différents ?\n" ] }, { @@ -1254,8 +1278,8 @@ }, "outputs": [ { - "output_type": "stream", "name": "stdout", + "output_type": "stream", "text": [ "Extrait structure de knot_lean/Knots/Conway.lean\n", "\n", @@ -1463,8 +1487,8 @@ }, "outputs": [ { - "output_type": "stream", "name": "stdout", + "output_type": "stream", "text": [ "Extrait structure de knot_lean/Knots/Lidman.lean\n", "\n", @@ -2008,4 +2032,4 @@ }, "nbformat": 4, "nbformat_minor": 5 -} \ No newline at end of file +}