Skip to content
Original file line number Diff line number Diff line change
Expand Up @@ -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"
]
},
{
Expand Down Expand Up @@ -1254,8 +1278,8 @@
},
"outputs": [
{
"output_type": "stream",
"name": "stdout",
"output_type": "stream",
"text": [
"Extrait structure de knot_lean/Knots/Conway.lean\n",
"\n",
Expand Down Expand Up @@ -1463,8 +1487,8 @@
},
"outputs": [
{
"output_type": "stream",
"name": "stdout",
"output_type": "stream",
"text": [
"Extrait structure de knot_lean/Knots/Lidman.lean\n",
"\n",
Expand Down Expand Up @@ -2008,4 +2032,4 @@
},
"nbformat": 4,
"nbformat_minor": 5
}
}
Loading