From 06704b023653297d02fa3fbeee71093cd5be6532 Mon Sep 17 00:00:00 2001 From: jsboige Date: Sat, 10 Oct 2026 16:34:04 +0200 Subject: [PATCH] fix(lean,#9768): KNOTS-03 -- prose exercice 2 realignee sur la baseline CI reelle (9 -> 8, post-#19107) Finding n.1 de la tranche d'audit Phase 0 famille SymbolicAI/Lean : la prose de l'exercice 2 et sa constante BASELINE portaient encore 9 alors que sorry-baseline vaut 8 depuis #19107 et que les outputs re-executees par #19872 mesurent 8. Cellules 37/38 uniquement ; re-execution complete 14/14 cellules, 0 echec (C.2). See #9768. Co-Authored-By: Claude Sonnet 5.5 --- ...NOTS-03-Companion-Formel-Lean-Python.ipynb | 635 ++++++++++-------- 1 file changed, 348 insertions(+), 287 deletions(-) diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/KNOTS-03-Companion-Formel-Lean-Python.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/KNOTS-03-Companion-Formel-Lean-Python.ipynb index b8fbb55126..a0c1cf3293 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/KNOTS-03-Companion-Formel-Lean-Python.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/KNOTS-03-Companion-Formel-Lean-Python.ipynb @@ -5,10 +5,10 @@ "id": "34287b8c", "metadata": { "papermill": { - "duration": 0.00374, - "end_time": "2026-10-08T08:38:03.306473+00:00", + "duration": 0.004543, + "end_time": "2026-10-10T14:29:52.427011+00:00", "exception": false, - "start_time": "2026-10-08T08:38:03.302733+00:00", + "start_time": "2026-10-10T14:29:52.422468+00:00", "status": "completed" }, "tags": [] @@ -28,10 +28,10 @@ "id": "8ac57465", "metadata": { "papermill": { - "duration": 0.003579, - "end_time": "2026-10-08T08:38:03.314014+00:00", + "duration": 0.003021, + "end_time": "2026-10-10T14:29:52.433451+00:00", "exception": false, - "start_time": "2026-10-08T08:38:03.310435+00:00", + "start_time": "2026-10-10T14:29:52.430430+00:00", "status": "completed" }, "tags": [] @@ -48,16 +48,16 @@ "id": "048a3415", "metadata": { "execution": { - "iopub.execute_input": "2026-10-08T08:38:03.323734Z", - "iopub.status.busy": "2026-10-08T08:38:03.323530Z", - "iopub.status.idle": "2026-10-08T08:38:03.459415Z", - "shell.execute_reply": "2026-10-08T08:38:03.458242Z" + "iopub.execute_input": "2026-10-10T14:29:52.443823Z", + "iopub.status.busy": "2026-10-10T14:29:52.443560Z", + "iopub.status.idle": "2026-10-10T14:29:52.729920Z", + "shell.execute_reply": "2026-10-10T14:29:52.729100Z" }, "papermill": { - "duration": 0.142031, - "end_time": "2026-10-08T08:38:03.460175+00:00", + "duration": 0.292816, + "end_time": "2026-10-10T14:29:52.730952+00:00", "exception": false, - "start_time": "2026-10-08T08:38:03.318144+00:00", + "start_time": "2026-10-10T14:29:52.438136+00:00", "status": "completed" }, "tags": [] @@ -67,20 +67,27 @@ "name": "stdout", "output_type": "stream", "text": [ - "Modules FR du lake : 14\n", + "Modules FR du lake : 15\n", + " ArcPartition.lean 942 lignes sibling _en : oui\n", " Basic.lean 664 lignes sibling _en : oui\n", - " Conway.lean 3366 lignes sibling _en : oui\n", + " Conway.lean 2459 lignes sibling _en : oui\n", " ConwayPD.lean 110 lignes sibling _en : oui\n", " FigureEight.lean 224 lignes sibling _en : oui\n", " Invariant.lean 3708 lignes sibling _en : oui\n", " Jones.lean 651 lignes sibling _en : oui\n", - " Lidman.lean 1080 lignes sibling _en : oui\n", - " MathlibPrerequisites.lean 138 lignes sibling _en : oui\n", + " Lidman.lean 1196 lignes sibling _en : oui\n", + " MathlibPrerequisites.lean 138 lignes sibling _en : oui\n" + ] + }, + { + "name": "stdout", + "output_type": "stream", + "text": [ " Mutation.lean 211 lignes sibling _en : oui\n", " Reidemeister.lean 1069 lignes sibling _en : oui\n", - " ReidemeisterCombinatorial.lean 298 lignes sibling _en : oui\n", + " ReidemeisterCombinatorial.lean 715 lignes sibling _en : oui\n", " ReidemeisterInvariance.lean 672 lignes sibling _en : oui\n", - " ReidemeisterMoves.lean 649 lignes sibling _en : oui\n", + " ReidemeisterMoves.lean 910 lignes sibling _en : oui\n", " Slice.lean 153 lignes sibling _en : oui\n" ] } @@ -103,10 +110,10 @@ "id": "3e52bfd7", "metadata": { "papermill": { - "duration": 0.004615, - "end_time": "2026-10-08T08:38:03.468371+00:00", + "duration": 0.004351, + "end_time": "2026-10-10T14:29:52.741186+00:00", "exception": false, - "start_time": "2026-10-08T08:38:03.463756+00:00", + "start_time": "2026-10-10T14:29:52.736835+00:00", "status": "completed" }, "tags": [] @@ -121,10 +128,10 @@ "id": "ba0a717b", "metadata": { "papermill": { - "duration": 0.00322, - "end_time": "2026-10-08T08:38:03.475090+00:00", + "duration": 0.004349, + "end_time": "2026-10-10T14:29:52.750567+00:00", "exception": false, - "start_time": "2026-10-08T08:38:03.471870+00:00", + "start_time": "2026-10-10T14:29:52.746218+00:00", "status": "completed" }, "tags": [] @@ -141,16 +148,16 @@ "id": "6df80a7f", "metadata": { "execution": { - "iopub.execute_input": "2026-10-08T08:38:03.483483Z", - "iopub.status.busy": "2026-10-08T08:38:03.483301Z", - "iopub.status.idle": "2026-10-08T08:38:03.489791Z", - "shell.execute_reply": "2026-10-08T08:38:03.488838Z" + "iopub.execute_input": "2026-10-10T14:29:52.763725Z", + "iopub.status.busy": "2026-10-10T14:29:52.763378Z", + "iopub.status.idle": "2026-10-10T14:29:52.771914Z", + "shell.execute_reply": "2026-10-10T14:29:52.771132Z" }, "papermill": { - "duration": 0.011868, - "end_time": "2026-10-08T08:38:03.490590+00:00", + "duration": 0.016316, + "end_time": "2026-10-10T14:29:52.772500+00:00", "exception": false, - "start_time": "2026-10-08T08:38:03.478722+00:00", + "start_time": "2026-10-10T14:29:52.756184+00:00", "status": "completed" }, "tags": [] @@ -221,10 +228,10 @@ "id": "95c9a4f6", "metadata": { "papermill": { - "duration": 0.003263, - "end_time": "2026-10-08T08:38:03.497162+00:00", + "duration": 0.005261, + "end_time": "2026-10-10T14:29:52.782768+00:00", "exception": false, - "start_time": "2026-10-08T08:38:03.493899+00:00", + "start_time": "2026-10-10T14:29:52.777507+00:00", "status": "completed" }, "tags": [] @@ -239,10 +246,10 @@ "id": "923dfd00", "metadata": { "papermill": { - "duration": 0.003451, - "end_time": "2026-10-08T08:38:03.503789+00:00", + "duration": 0.00471, + "end_time": "2026-10-10T14:29:52.792899+00:00", "exception": false, - "start_time": "2026-10-08T08:38:03.500338+00:00", + "start_time": "2026-10-10T14:29:52.788189+00:00", "status": "completed" }, "tags": [] @@ -259,16 +266,16 @@ "id": "f8e81189", "metadata": { "execution": { - "iopub.execute_input": "2026-10-08T08:38:03.514550Z", - "iopub.status.busy": "2026-10-08T08:38:03.514286Z", - "iopub.status.idle": "2026-10-08T08:38:03.523423Z", - "shell.execute_reply": "2026-10-08T08:38:03.520567Z" + "iopub.execute_input": "2026-10-10T14:29:52.804250Z", + "iopub.status.busy": "2026-10-10T14:29:52.803977Z", + "iopub.status.idle": "2026-10-10T14:29:52.810825Z", + "shell.execute_reply": "2026-10-10T14:29:52.810092Z" }, "papermill": { - "duration": 0.01594, - "end_time": "2026-10-08T08:38:03.524416+00:00", + "duration": 0.013975, + "end_time": "2026-10-10T14:29:52.812037+00:00", "exception": false, - "start_time": "2026-10-08T08:38:03.508476+00:00", + "start_time": "2026-10-10T14:29:52.798062+00:00", "status": "completed" }, "tags": [] @@ -311,10 +318,10 @@ "id": "054abd8b", "metadata": { "papermill": { - "duration": 0.003172, - "end_time": "2026-10-08T08:38:03.530755+00:00", + "duration": 0.005338, + "end_time": "2026-10-10T14:29:52.823274+00:00", "exception": false, - "start_time": "2026-10-08T08:38:03.527583+00:00", + "start_time": "2026-10-10T14:29:52.817936+00:00", "status": "completed" }, "tags": [] @@ -329,10 +336,10 @@ "id": "9e5c54dc", "metadata": { "papermill": { - "duration": 0.003619, - "end_time": "2026-10-08T08:38:03.537603+00:00", + "duration": 0.005133, + "end_time": "2026-10-10T14:29:52.833749+00:00", "exception": false, - "start_time": "2026-10-08T08:38:03.533984+00:00", + "start_time": "2026-10-10T14:29:52.828616+00:00", "status": "completed" }, "tags": [] @@ -349,16 +356,16 @@ "id": "f41d2568", "metadata": { "execution": { - "iopub.execute_input": "2026-10-08T08:38:03.545816Z", - "iopub.status.busy": "2026-10-08T08:38:03.545623Z", - "iopub.status.idle": "2026-10-08T08:38:07.702834Z", - "shell.execute_reply": "2026-10-08T08:38:07.701590Z" + "iopub.execute_input": "2026-10-10T14:29:52.843975Z", + "iopub.status.busy": "2026-10-10T14:29:52.843775Z", + "iopub.status.idle": "2026-10-10T14:29:53.307274Z", + "shell.execute_reply": "2026-10-10T14:29:53.306656Z" }, "papermill": { - "duration": 4.162687, - "end_time": "2026-10-08T08:38:07.704135+00:00", + "duration": 0.471568, + "end_time": "2026-10-10T14:29:53.310260+00:00", "exception": false, - "start_time": "2026-10-08T08:38:03.541448+00:00", + "start_time": "2026-10-10T14:29:52.838692+00:00", "status": "completed" }, "tags": [] @@ -393,92 +400,98 @@ " \n", " \n", " 0\n", + " ArcPartition\n", + " 0\n", + " 0\n", + " \n", + " \n", + " 1\n", " Basic\n", " 3\n", " 0\n", " \n", " \n", - " 1\n", + " 2\n", " Conway\n", - " 2\n", + " 3\n", " 0\n", " \n", " \n", - " 2\n", + " 3\n", " ConwayPD\n", " 0\n", " 0\n", " \n", " \n", - " 3\n", + " 4\n", " FigureEight\n", " 0\n", " 0\n", " \n", " \n", - " 4\n", + " 5\n", " Invariant\n", " 6\n", " 0\n", " \n", " \n", - " 5\n", + " 6\n", " Jones\n", " 1\n", " 0\n", " \n", " \n", - " 6\n", + " 7\n", " Lidman\n", - " 8\n", + " 10\n", " 2\n", " \n", " \n", - " 7\n", + " 8\n", " MathlibPrerequisites\n", " 2\n", " 0\n", " \n", " \n", - " 8\n", + " 9\n", " Mutation\n", " 1\n", " 0\n", " \n", " \n", - " 9\n", + " 10\n", " Reidemeister\n", " 2\n", " 2\n", " \n", " \n", - " 10\n", + " 11\n", " ReidemeisterCombinatorial\n", - " 3\n", + " 2\n", " 0\n", " \n", " \n", - " 11\n", + " 12\n", " ReidemeisterInvariance\n", " 0\n", " 0\n", " \n", " \n", - " 12\n", + " 13\n", " ReidemeisterMoves\n", " 1\n", " 0\n", " \n", " \n", - " 13\n", + " 14\n", " Slice\n", " 8\n", " 4\n", " \n", " \n", - " 14\n", + " 15\n", " TOTAL\n", - " 37\n", + " 39\n", " 8\n", " \n", " \n", @@ -487,21 +500,22 @@ ], "text/plain": [ " module grep naif sorry reels\n", - "0 Basic 3 0\n", - "1 Conway 2 0\n", - "2 ConwayPD 0 0\n", - "3 FigureEight 0 0\n", - "4 Invariant 6 0\n", - "5 Jones 1 0\n", - "6 Lidman 8 2\n", - "7 MathlibPrerequisites 2 0\n", - "8 Mutation 1 0\n", - "9 Reidemeister 2 2\n", - "10 ReidemeisterCombinatorial 3 0\n", - "11 ReidemeisterInvariance 0 0\n", - "12 ReidemeisterMoves 1 0\n", - "13 Slice 8 4\n", - "14 TOTAL 37 8" + "0 ArcPartition 0 0\n", + "1 Basic 3 0\n", + "2 Conway 3 0\n", + "3 ConwayPD 0 0\n", + "4 FigureEight 0 0\n", + "5 Invariant 6 0\n", + "6 Jones 1 0\n", + "7 Lidman 10 2\n", + "8 MathlibPrerequisites 2 0\n", + "9 Mutation 1 0\n", + "10 Reidemeister 2 2\n", + "11 ReidemeisterCombinatorial 2 0\n", + "12 ReidemeisterInvariance 0 0\n", + "13 ReidemeisterMoves 1 0\n", + "14 Slice 8 4\n", + "15 TOTAL 39 8" ] }, "execution_count": 4, @@ -534,10 +548,10 @@ "id": "99245d15", "metadata": { "papermill": { - "duration": 0.004127, - "end_time": "2026-10-08T08:38:07.712612+00:00", + "duration": 0.005452, + "end_time": "2026-10-10T14:29:53.323842+00:00", "exception": false, - "start_time": "2026-10-08T08:38:07.708485+00:00", + "start_time": "2026-10-10T14:29:53.318390+00:00", "status": "completed" }, "tags": [] @@ -552,10 +566,10 @@ "id": "67dc2946", "metadata": { "papermill": { - "duration": 0.003679, - "end_time": "2026-10-08T08:38:07.720674+00:00", + "duration": 0.004382, + "end_time": "2026-10-10T14:29:53.331637+00:00", "exception": false, - "start_time": "2026-10-08T08:38:07.716995+00:00", + "start_time": "2026-10-10T14:29:53.327255+00:00", "status": "completed" }, "tags": [] @@ -572,16 +586,16 @@ "id": "d284ef54", "metadata": { "execution": { - "iopub.execute_input": "2026-10-08T08:38:07.732194Z", - "iopub.status.busy": "2026-10-08T08:38:07.731853Z", - "iopub.status.idle": "2026-10-08T08:38:07.740388Z", - "shell.execute_reply": "2026-10-08T08:38:07.738873Z" + "iopub.execute_input": "2026-10-10T14:29:53.340840Z", + "iopub.status.busy": "2026-10-10T14:29:53.340599Z", + "iopub.status.idle": "2026-10-10T14:29:53.345577Z", + "shell.execute_reply": "2026-10-10T14:29:53.344982Z" }, "papermill": { - "duration": 0.015154, - "end_time": "2026-10-08T08:38:07.741365+00:00", + "duration": 0.01086, + "end_time": "2026-10-10T14:29:53.347014+00:00", "exception": false, - "start_time": "2026-10-08T08:38:07.726211+00:00", + "start_time": "2026-10-10T14:29:53.336154+00:00", "status": "completed" }, "tags": [] @@ -648,10 +662,10 @@ "id": "018a9781", "metadata": { "papermill": { - "duration": 0.003956, - "end_time": "2026-10-08T08:38:07.748901+00:00", + "duration": 0.006566, + "end_time": "2026-10-10T14:29:53.360252+00:00", "exception": false, - "start_time": "2026-10-08T08:38:07.744945+00:00", + "start_time": "2026-10-10T14:29:53.353686+00:00", "status": "completed" }, "tags": [] @@ -666,10 +680,10 @@ "id": "e3eec5ed", "metadata": { "papermill": { - "duration": 0.004636, - "end_time": "2026-10-08T08:38:07.758889+00:00", + "duration": 0.003926, + "end_time": "2026-10-10T14:29:53.370908+00:00", "exception": false, - "start_time": "2026-10-08T08:38:07.754253+00:00", + "start_time": "2026-10-10T14:29:53.366982+00:00", "status": "completed" }, "tags": [] @@ -687,10 +701,10 @@ "id": "60172fe0", "metadata": { "papermill": { - "duration": 0.004092, - "end_time": "2026-10-08T08:38:07.766957+00:00", + "duration": 0.005427, + "end_time": "2026-10-10T14:29:53.380726+00:00", "exception": false, - "start_time": "2026-10-08T08:38:07.762865+00:00", + "start_time": "2026-10-10T14:29:53.375299+00:00", "status": "completed" }, "tags": [] @@ -707,16 +721,16 @@ "id": "f3493015", "metadata": { "execution": { - "iopub.execute_input": "2026-10-08T08:38:07.775851Z", - "iopub.status.busy": "2026-10-08T08:38:07.775640Z", - "iopub.status.idle": "2026-10-08T08:38:07.787282Z", - "shell.execute_reply": "2026-10-08T08:38:07.786093Z" + "iopub.execute_input": "2026-10-10T14:29:53.389229Z", + "iopub.status.busy": "2026-10-10T14:29:53.388971Z", + "iopub.status.idle": "2026-10-10T14:29:53.396565Z", + "shell.execute_reply": "2026-10-10T14:29:53.395936Z" }, "papermill": { - "duration": 0.017408, - "end_time": "2026-10-08T08:38:07.788393+00:00", + "duration": 0.013328, + "end_time": "2026-10-10T14:29:53.397657+00:00", "exception": false, - "start_time": "2026-10-08T08:38:07.770985+00:00", + "start_time": "2026-10-10T14:29:53.384329+00:00", "status": "completed" }, "tags": [] @@ -726,7 +740,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "ReidemeisterMoves.lean : 31 declarations\n", + "ReidemeisterMoves.lean : 44 declarations\n", " L 74 def SameRelOn\n", " L 82 def RefinesOn\n", " L 88 lemma SameRel.sameRelOn\n", @@ -758,6 +772,19 @@ " L 562 theorem reidemeister2Connected_arcPartition_refinesOn_witness\n", " L 584 theorem reidemeister3Connected_arcPartition_sameRelOn_witness\n", " L 596 theorem reidemeister3Connected_witness_movesConnects\n", + " L 687 def PDCrossing.fourDistinct\n", + " L 693 def allFourDistinct\n", + " L 705 theorem not_fourDistinct_kink\n", + " L 713 theorem not_fourDistinct_bigon\n", + " L 722 theorem changeCrossing_fourDistinct\n", + " L 755 theorem changeCrossingAt_allFourDistinct\n", + " L 766 theorem foldl_changeCrossingAt_allFourDistinct\n", + " L 784 theorem reidemeisterStep_length_le_of_allFourDistinct\n", + " L 827 theorem movesConnects_length_le_of_allFourDistinct\n", + " L 856 theorem movesConnects_not_unknot_of_allFourDistinct\n", + " L 880 theorem reidemeister1Connected_descent_is_certified\n", + " L 893 theorem not_allFourDistinct_reidemeister1Connected_witness\n", + " L 903 theorem allFourDistinct_reidemeister1Connected_witness_small\n", "\n", "def SameRelOn (n : Nat) (P Q : List (List Nat)) : Prop :=\n", " ∀ ⦃x y : Nat⦄, x ≤ n → y ≤ n → (SameClass P x y ↔ SameClass Q x y)\n", @@ -825,10 +852,10 @@ "id": "00d202cb", "metadata": { "papermill": { - "duration": 0.00577, - "end_time": "2026-10-08T08:38:07.799323+00:00", + "duration": 0.004944, + "end_time": "2026-10-10T14:29:53.406596+00:00", "exception": false, - "start_time": "2026-10-08T08:38:07.793553+00:00", + "start_time": "2026-10-10T14:29:53.401652+00:00", "status": "completed" }, "tags": [] @@ -843,10 +870,10 @@ "id": "9997cd78", "metadata": { "papermill": { - "duration": 0.004595, - "end_time": "2026-10-08T08:38:07.809463+00:00", + "duration": 0.003354, + "end_time": "2026-10-10T14:29:53.414905+00:00", "exception": false, - "start_time": "2026-10-08T08:38:07.804868+00:00", + "start_time": "2026-10-10T14:29:53.411551+00:00", "status": "completed" }, "tags": [] @@ -863,16 +890,16 @@ "id": "82a3ce81", "metadata": { "execution": { - "iopub.execute_input": "2026-10-08T08:38:07.821461Z", - "iopub.status.busy": "2026-10-08T08:38:07.821033Z", - "iopub.status.idle": "2026-10-08T08:38:07.827782Z", - "shell.execute_reply": "2026-10-08T08:38:07.826692Z" + "iopub.execute_input": "2026-10-10T14:29:53.424454Z", + "iopub.status.busy": "2026-10-10T14:29:53.424263Z", + "iopub.status.idle": "2026-10-10T14:29:53.431108Z", + "shell.execute_reply": "2026-10-10T14:29:53.430534Z" }, "papermill": { - "duration": 0.014414, - "end_time": "2026-10-08T08:38:07.828846+00:00", + "duration": 0.012307, + "end_time": "2026-10-10T14:29:53.431967+00:00", "exception": false, - "start_time": "2026-10-08T08:38:07.814432+00:00", + "start_time": "2026-10-10T14:29:53.419660+00:00", "status": "completed" }, "tags": [] @@ -882,18 +909,42 @@ "name": "stdout", "output_type": "stream", "text": [ - "ReidemeisterCombinatorial.lean : 11 declarations\n", - " L 79 inductive MoveSequence\n", - " L 107 def movesConnects\n", - " L 122 theorem movesConnects_sound\n", - " L 143 def ReidemeisterStep.toWitness\n", - " L 166 def oneStepWitnesses\n", - " L 188 def verifyMovesAux\n", - " L 200 def verifyMoves\n", - " L 231 theorem oneStepWitnesses_sound\n", - " L 235 theorem verifyMoves_sound\n", - " L 272 def foldChangeCrossingsAt\n", - " L 277 structure UnknottingWitness\n", + "ReidemeisterCombinatorial.lean : 35 declarations\n", + " L 91 inductive MoveSequence\n", + " L 119 def movesConnects\n", + " L 134 theorem movesConnects_sound\n", + " L 155 def ReidemeisterStep.toWitness\n", + " L 204 structure StepWitness\n", + " L 213 def finEmbed\n", + " L 218 theorem list_set_current\n", + " L 230 theorem list_set_eq\n", + " L 235 theorem list_get_set_self\n", + " L 242 def renameOptsWith\n", + " L 250 def rename2OptsWith\n", + " L 259 def unRenameOptsWith\n", + " L 266 def unRename2Opts\n", + " L 276 def PDCrossing.allRenamesWith\n", + " L 285 def PDCrossing.allDoubleRenamesWith\n", + " L 295 def PDCrossing.allUnRenamesWith\n", + " L 304 def PDCrossing.allUnDoubleRenamesWith\n", + " L 313 def arcCandidatesWith\n", + " L 320 def properArcWitnesses\n", + " L 330 def r1ForwardWitnesses\n", + " L 350 def r1BackwardWitnesses\n", + " L 410 def r2ForwardWitnesses\n", + " L 428 def r2BackwardWitnesses\n", + " L 513 def r3ForwardWitnesses\n", + " L 548 def oneStepWitnessesWithProof\n", + " L 556 def oneStepWitnesses\n", + " L 574 def verifyMovesAux\n", + " L 586 def verifyMoves\n", + " L 619 theorem oneStepWitnesses_sound\n", + " L 628 theorem verifyMoves_one_r1_witness\n", + " L 637 theorem verifyMoves_one_r3_witness\n", + " L 645 theorem verifyMoves_sound\n", + " L 678 structure existe\n", + " L 685 def foldChangeCrossingsAt\n", + " L 690 structure UnknottingWitness\n", "\n", "inductive MoveSequence : KnotDiagram → KnotDiagram → Type where\n", " /-- Suite vide : un diagramme se relie trivialement à lui-même. -/\n", @@ -931,10 +982,10 @@ "id": "1f23958e", "metadata": { "papermill": { - "duration": 0.005549, - "end_time": "2026-10-08T08:38:07.838911+00:00", + "duration": 0.004528, + "end_time": "2026-10-10T14:29:53.443093+00:00", "exception": false, - "start_time": "2026-10-08T08:38:07.833362+00:00", + "start_time": "2026-10-10T14:29:53.438565+00:00", "status": "completed" }, "tags": [] @@ -949,10 +1000,10 @@ "id": "6ae862ca", "metadata": { "papermill": { - "duration": 0.005864, - "end_time": "2026-10-08T08:38:07.850770+00:00", + "duration": 0.004964, + "end_time": "2026-10-10T14:29:53.454662+00:00", "exception": false, - "start_time": "2026-10-08T08:38:07.844906+00:00", + "start_time": "2026-10-10T14:29:53.449698+00:00", "status": "completed" }, "tags": [] @@ -969,16 +1020,16 @@ "id": "d9cf4d27", "metadata": { "execution": { - "iopub.execute_input": "2026-10-08T08:38:07.865424Z", - "iopub.status.busy": "2026-10-08T08:38:07.864957Z", - "iopub.status.idle": "2026-10-08T08:38:07.873721Z", - "shell.execute_reply": "2026-10-08T08:38:07.872258Z" + "iopub.execute_input": "2026-10-10T14:29:53.465956Z", + "iopub.status.busy": "2026-10-10T14:29:53.465678Z", + "iopub.status.idle": "2026-10-10T14:29:53.471292Z", + "shell.execute_reply": "2026-10-10T14:29:53.470369Z" }, "papermill": { - "duration": 0.017267, - "end_time": "2026-10-08T08:38:07.874946+00:00", + "duration": 0.012781, + "end_time": "2026-10-10T14:29:53.471951+00:00", "exception": false, - "start_time": "2026-10-08T08:38:07.857679+00:00", + "start_time": "2026-10-10T14:29:53.459170+00:00", "status": "completed" }, "tags": [] @@ -1037,10 +1088,10 @@ "id": "fc84ae81", "metadata": { "papermill": { - "duration": 0.006412, - "end_time": "2026-10-08T08:38:07.887458+00:00", + "duration": 0.003858, + "end_time": "2026-10-10T14:29:53.480392+00:00", "exception": false, - "start_time": "2026-10-08T08:38:07.881046+00:00", + "start_time": "2026-10-10T14:29:53.476534+00:00", "status": "completed" }, "tags": [] @@ -1055,10 +1106,10 @@ "id": "25cbfad6", "metadata": { "papermill": { - "duration": 0.005195, - "end_time": "2026-10-08T08:38:07.898850+00:00", + "duration": 0.004037, + "end_time": "2026-10-10T14:29:53.488904+00:00", "exception": false, - "start_time": "2026-10-08T08:38:07.893655+00:00", + "start_time": "2026-10-10T14:29:53.484867+00:00", "status": "completed" }, "tags": [] @@ -1075,16 +1126,16 @@ "id": "46acbd06", "metadata": { "execution": { - "iopub.execute_input": "2026-10-08T08:38:07.908996Z", - "iopub.status.busy": "2026-10-08T08:38:07.908509Z", - "iopub.status.idle": "2026-10-08T08:38:07.925631Z", - "shell.execute_reply": "2026-10-08T08:38:07.924351Z" + "iopub.execute_input": "2026-10-10T14:29:53.502920Z", + "iopub.status.busy": "2026-10-10T14:29:53.502734Z", + "iopub.status.idle": "2026-10-10T14:29:53.516190Z", + "shell.execute_reply": "2026-10-10T14:29:53.515378Z" }, "papermill": { - "duration": 0.02312, - "end_time": "2026-10-08T08:38:07.926593+00:00", + "duration": 0.022171, + "end_time": "2026-10-10T14:29:53.517130+00:00", "exception": false, - "start_time": "2026-10-08T08:38:07.903473+00:00", + "start_time": "2026-10-10T14:29:53.494959+00:00", "status": "completed" }, "tags": [] @@ -1216,10 +1267,10 @@ "id": "4cc1f357", "metadata": { "papermill": { - "duration": 0.004266, - "end_time": "2026-10-08T08:38:07.934932+00:00", + "duration": 0.007115, + "end_time": "2026-10-10T14:29:53.528106+00:00", "exception": false, - "start_time": "2026-10-08T08:38:07.930666+00:00", + "start_time": "2026-10-10T14:29:53.520991+00:00", "status": "completed" }, "tags": [] @@ -1241,10 +1292,10 @@ "id": "a29df633", "metadata": { "papermill": { - "duration": 0.00517, - "end_time": "2026-10-08T08:38:07.945731+00:00", + "duration": 0.006717, + "end_time": "2026-10-10T14:29:53.543217+00:00", "exception": false, - "start_time": "2026-10-08T08:38:07.940561+00:00", + "start_time": "2026-10-10T14:29:53.536500+00:00", "status": "completed" }, "tags": [] @@ -1261,16 +1312,16 @@ "id": "0e5f7024", "metadata": { "execution": { - "iopub.execute_input": "2026-10-08T08:38:07.956077Z", - "iopub.status.busy": "2026-10-08T08:38:07.955684Z", - "iopub.status.idle": "2026-10-08T08:38:08.015404Z", - "shell.execute_reply": "2026-10-08T08:38:08.014317Z" + "iopub.execute_input": "2026-10-10T14:29:53.558922Z", + "iopub.status.busy": "2026-10-10T14:29:53.558596Z", + "iopub.status.idle": "2026-10-10T14:29:53.600555Z", + "shell.execute_reply": "2026-10-10T14:29:53.599994Z" }, "papermill": { - "duration": 0.065785, - "end_time": "2026-10-08T08:38:08.016308+00:00", + "duration": 0.051825, + "end_time": "2026-10-10T14:29:53.601908+00:00", "exception": false, - "start_time": "2026-10-08T08:38:07.950523+00:00", + "start_time": "2026-10-10T14:29:53.550083+00:00", "status": "completed" }, "tags": [] @@ -1307,6 +1358,14 @@ " \n", " \n", " 0\n", + " ArcPartition\n", + " 60\n", + " 51\n", + " 0\n", + " 0.00\n", + " \n", + " \n", + " 1\n", " Basic\n", " 34\n", " 14\n", @@ -1314,15 +1373,15 @@ " 0.00\n", " \n", " \n", - " 1\n", + " 2\n", " Conway\n", - " 74\n", - " 64\n", + " 14\n", + " 13\n", " 0\n", " 0.00\n", " \n", " \n", - " 2\n", + " 3\n", " ConwayPD\n", " 6\n", " 2\n", @@ -1330,7 +1389,7 @@ " 0.00\n", " \n", " \n", - " 3\n", + " 4\n", " FigureEight\n", " 12\n", " 11\n", @@ -1338,7 +1397,7 @@ " 0.00\n", " \n", " \n", - " 4\n", + " 5\n", " Invariant\n", " 86\n", " 59\n", @@ -1346,7 +1405,7 @@ " 0.00\n", " \n", " \n", - " 5\n", + " 6\n", " Jones\n", " 72\n", " 35\n", @@ -1354,15 +1413,15 @@ " 0.00\n", " \n", " \n", - " 6\n", + " 7\n", " Lidman\n", - " 7\n", - " 5\n", + " 12\n", + " 10\n", " 2\n", - " 0.29\n", + " 0.17\n", " \n", " \n", - " 7\n", + " 8\n", " MathlibPrerequisites\n", " 11\n", " 11\n", @@ -1370,7 +1429,7 @@ " 0.00\n", " \n", " \n", - " 8\n", + " 9\n", " Mutation\n", " 18\n", " 11\n", @@ -1378,7 +1437,7 @@ " 0.00\n", " \n", " \n", - " 9\n", + " 10\n", " Reidemeister\n", " 36\n", " 22\n", @@ -1386,15 +1445,15 @@ " 0.06\n", " \n", " \n", - " 10\n", + " 11\n", " ReidemeisterCombinatorial\n", - " 10\n", - " 3\n", + " 34\n", + " 8\n", " 0\n", " 0.00\n", " \n", " \n", - " 11\n", + " 12\n", " ReidemeisterInvariance\n", " 19\n", " 18\n", @@ -1402,15 +1461,15 @@ " 0.00\n", " \n", " \n", - " 12\n", + " 13\n", " ReidemeisterMoves\n", - " 30\n", - " 12\n", + " 43\n", + " 23\n", " 0\n", " 0.00\n", " \n", " \n", - " 13\n", + " 14\n", " Slice\n", " 5\n", " 3\n", @@ -1423,20 +1482,21 @@ ], "text/plain": [ " module declarations theoremes sorries reels \\\n", - "0 Basic 34 14 0 \n", - "1 Conway 74 64 0 \n", - "2 ConwayPD 6 2 0 \n", - "3 FigureEight 12 11 0 \n", - "4 Invariant 86 59 0 \n", - "5 Jones 72 35 0 \n", - "6 Lidman 7 5 2 \n", - "7 MathlibPrerequisites 11 11 0 \n", - "8 Mutation 18 11 0 \n", - "9 Reidemeister 36 22 2 \n", - "10 ReidemeisterCombinatorial 10 3 0 \n", - "11 ReidemeisterInvariance 19 18 0 \n", - "12 ReidemeisterMoves 30 12 0 \n", - "13 Slice 5 3 4 \n", + "0 ArcPartition 60 51 0 \n", + "1 Basic 34 14 0 \n", + "2 Conway 14 13 0 \n", + "3 ConwayPD 6 2 0 \n", + "4 FigureEight 12 11 0 \n", + "5 Invariant 86 59 0 \n", + "6 Jones 72 35 0 \n", + "7 Lidman 12 10 2 \n", + "8 MathlibPrerequisites 11 11 0 \n", + "9 Mutation 18 11 0 \n", + "10 Reidemeister 36 22 2 \n", + "11 ReidemeisterCombinatorial 34 8 0 \n", + "12 ReidemeisterInvariance 19 18 0 \n", + "13 ReidemeisterMoves 43 23 0 \n", + "14 Slice 5 3 4 \n", "\n", " sorries/decl \n", "0 0.00 \n", @@ -1445,14 +1505,15 @@ "3 0.00 \n", "4 0.00 \n", "5 0.00 \n", - "6 0.29 \n", - "7 0.00 \n", + "6 0.00 \n", + "7 0.17 \n", "8 0.00 \n", - "9 0.06 \n", - "10 0.00 \n", + "9 0.00 \n", + "10 0.06 \n", "11 0.00 \n", "12 0.00 \n", - "13 0.80 " + "13 0.00 \n", + "14 0.80 " ] }, "execution_count": 10, @@ -1477,10 +1538,10 @@ "id": "1b665535", "metadata": { "papermill": { - "duration": 0.004522, - "end_time": "2026-10-08T08:38:08.025051+00:00", + "duration": 0.005446, + "end_time": "2026-10-10T14:29:53.613875+00:00", "exception": false, - "start_time": "2026-10-08T08:38:08.020529+00:00", + "start_time": "2026-10-10T14:29:53.608429+00:00", "status": "completed" }, "tags": [] @@ -1495,10 +1556,10 @@ "id": "45c0d3ad", "metadata": { "papermill": { - "duration": 0.004816, - "end_time": "2026-10-08T08:38:08.036061+00:00", + "duration": 0.004266, + "end_time": "2026-10-10T14:29:53.624475+00:00", "exception": false, - "start_time": "2026-10-08T08:38:08.031245+00:00", + "start_time": "2026-10-10T14:29:53.620209+00:00", "status": "completed" }, "tags": [] @@ -1515,16 +1576,16 @@ "id": "3a6d4311", "metadata": { "execution": { - "iopub.execute_input": "2026-10-08T08:38:08.049127Z", - "iopub.status.busy": "2026-10-08T08:38:08.048833Z", - "iopub.status.idle": "2026-10-08T08:38:09.447454Z", - "shell.execute_reply": "2026-10-08T08:38:09.446537Z" + "iopub.execute_input": "2026-10-10T14:29:53.636514Z", + "iopub.status.busy": "2026-10-10T14:29:53.636227Z", + "iopub.status.idle": "2026-10-10T14:29:54.683992Z", + "shell.execute_reply": "2026-10-10T14:29:54.682801Z" }, "papermill": { - "duration": 1.405635, - "end_time": "2026-10-08T08:38:09.448124+00:00", + "duration": 1.055345, + "end_time": "2026-10-10T14:29:54.685192+00:00", "exception": false, - "start_time": "2026-10-08T08:38:08.042489+00:00", + "start_time": "2026-10-10T14:29:53.629847+00:00", "status": "completed" }, "tags": [] @@ -1534,7 +1595,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "15/15 pairs byte-identical | 0 consumer-pattern | 0 drift | 0 orphan | 0 unbuilt (0 whitelisted) | 0 half-done (advisory)\n" + "16/16 pairs byte-identical | 0 consumer-pattern | 0 drift | 0 orphan | 0 unbuilt (0 whitelisted) | 1 half-done (advisory)\n" ] } ], @@ -1563,10 +1624,10 @@ "id": "c64c9030", "metadata": { "papermill": { - "duration": 0.004387, - "end_time": "2026-10-08T08:38:09.456530+00:00", + "duration": 0.004101, + "end_time": "2026-10-10T14:29:54.694396+00:00", "exception": false, - "start_time": "2026-10-08T08:38:09.452143+00:00", + "start_time": "2026-10-10T14:29:54.690295+00:00", "status": "completed" }, "tags": [] @@ -1581,10 +1642,10 @@ "id": "2382dfb5", "metadata": { "papermill": { - "duration": 0.004341, - "end_time": "2026-10-08T08:38:09.467128+00:00", + "duration": 0.00562, + "end_time": "2026-10-10T14:29:54.704522+00:00", "exception": false, - "start_time": "2026-10-08T08:38:09.462787+00:00", + "start_time": "2026-10-10T14:29:54.698902+00:00", "status": "completed" }, "tags": [] @@ -1606,16 +1667,16 @@ "id": "8f805f22", "metadata": { "execution": { - "iopub.execute_input": "2026-10-08T08:38:09.476268Z", - "iopub.status.busy": "2026-10-08T08:38:09.476055Z", - "iopub.status.idle": "2026-10-08T08:38:09.480455Z", - "shell.execute_reply": "2026-10-08T08:38:09.479462Z" + "iopub.execute_input": "2026-10-10T14:29:54.718804Z", + "iopub.status.busy": "2026-10-10T14:29:54.718487Z", + "iopub.status.idle": "2026-10-10T14:29:54.723627Z", + "shell.execute_reply": "2026-10-10T14:29:54.722574Z" }, "papermill": { - "duration": 0.010097, - "end_time": "2026-10-08T08:38:09.481172+00:00", + "duration": 0.012825, + "end_time": "2026-10-10T14:29:54.724422+00:00", "exception": false, - "start_time": "2026-10-08T08:38:09.471075+00:00", + "start_time": "2026-10-10T14:29:54.711597+00:00", "status": "completed" }, "tags": [] @@ -1633,10 +1694,10 @@ "id": "c52ef1db", "metadata": { "papermill": { - "duration": 0.004482, - "end_time": "2026-10-08T08:38:09.489533+00:00", + "duration": 0.004221, + "end_time": "2026-10-10T14:29:54.734724+00:00", "exception": false, - "start_time": "2026-10-08T08:38:09.485051+00:00", + "start_time": "2026-10-10T14:29:54.730503+00:00", "status": "completed" }, "tags": [] @@ -1644,9 +1705,9 @@ "source": [ "## Exercice 2 — Le compte qui fonde la baseline CI\n", "\n", - "Le CI gate sur **9 sorries réels** (lean-knot.yml `sorry-baseline: \"9\"`, post-#18615). Recomptez avec l'instrument `real` ci-dessus et confrontez à la baseline.\n", + "Le CI gate sur **8 sorries réels** (lean-knot.yml `sorry-baseline: \"8\"`, post-#19107). Recomptez avec l'instrument `real` ci-dessus et confrontez à la baseline.\n", "\n", - "**Indice :** la fonction `count_sorry(path, 'real')` est déjà écrite. Le résultat doit être comparé à la constante 9 — un écart dans un sens ou l'autre est un signal (régression ou baseline périmée).\n", + "**Indice :** la fonction `count_sorry(path, 'real')` est déjà écrite. Le résultat doit être comparé à la constante 8 — un écart dans un sens ou l'autre est un signal (régression ou baseline périmée).\n", "\n", "**Étape 1 :** total real sur les modules. \n", "**Étape 2 :** afficher la comparaison au format `total vs baseline : OK/ECART`." @@ -1658,24 +1719,24 @@ "id": "7e7f464b", "metadata": { "execution": { - "iopub.execute_input": "2026-10-08T08:38:09.498922Z", - "iopub.status.busy": "2026-10-08T08:38:09.498608Z", - "iopub.status.idle": "2026-10-08T08:38:09.502255Z", - "shell.execute_reply": "2026-10-08T08:38:09.501260Z" + "iopub.execute_input": "2026-10-10T14:29:54.745571Z", + "iopub.status.busy": "2026-10-10T14:29:54.745083Z", + "iopub.status.idle": "2026-10-10T14:29:54.750224Z", + "shell.execute_reply": "2026-10-10T14:29:54.749244Z" }, "papermill": { - "duration": 0.009266, - "end_time": "2026-10-08T08:38:09.503005+00:00", + "duration": 0.011397, + "end_time": "2026-10-10T14:29:54.751024+00:00", "exception": false, - "start_time": "2026-10-08T08:38:09.493739+00:00", + "start_time": "2026-10-10T14:29:54.739627+00:00", "status": "completed" }, "tags": [] }, "outputs": [], "source": [ - "# Exercice a completer : confrontez le compte real a la baseline CI (9)\n", - "BASELINE = 9\n", + "# Exercice a completer : confrontez le compte real a la baseline CI (8)\n", + "BASELINE = 8\n", "pass" ] }, @@ -1684,10 +1745,10 @@ "id": "3cb867c6", "metadata": { "papermill": { - "duration": 0.003981, - "end_time": "2026-10-08T08:38:09.511144+00:00", + "duration": 0.003924, + "end_time": "2026-10-10T14:29:54.760263+00:00", "exception": false, - "start_time": "2026-10-08T08:38:09.507163+00:00", + "start_time": "2026-10-10T14:29:54.756339+00:00", "status": "completed" }, "tags": [] @@ -1709,16 +1770,16 @@ "id": "7af659c5", "metadata": { "execution": { - "iopub.execute_input": "2026-10-08T08:38:09.519868Z", - "iopub.status.busy": "2026-10-08T08:38:09.519670Z", - "iopub.status.idle": "2026-10-08T08:38:09.523791Z", - "shell.execute_reply": "2026-10-08T08:38:09.522766Z" + "iopub.execute_input": "2026-10-10T14:29:54.773023Z", + "iopub.status.busy": "2026-10-10T14:29:54.772809Z", + "iopub.status.idle": "2026-10-10T14:29:54.777282Z", + "shell.execute_reply": "2026-10-10T14:29:54.776122Z" }, "papermill": { - "duration": 0.009689, - "end_time": "2026-10-08T08:38:09.524613+00:00", + "duration": 0.013262, + "end_time": "2026-10-10T14:29:54.778431+00:00", "exception": false, - "start_time": "2026-10-08T08:38:09.514924+00:00", + "start_time": "2026-10-10T14:29:54.765169+00:00", "status": "completed" }, "tags": [] @@ -1739,10 +1800,10 @@ "id": "9454d97a", "metadata": { "papermill": { - "duration": 0.004174, - "end_time": "2026-10-08T08:38:09.534073+00:00", + "duration": 0.004384, + "end_time": "2026-10-10T14:29:54.787237+00:00", "exception": false, - "start_time": "2026-10-08T08:38:09.529899+00:00", + "start_time": "2026-10-10T14:29:54.782853+00:00", "status": "completed" }, "tags": [] @@ -1764,10 +1825,10 @@ "id": "d34e7144", "metadata": { "papermill": { - "duration": 0.003951, - "end_time": "2026-10-08T08:38:09.541886+00:00", + "duration": 0.003791, + "end_time": "2026-10-10T14:29:54.795420+00:00", "exception": false, - "start_time": "2026-10-08T08:38:09.537935+00:00", + "start_time": "2026-10-10T14:29:54.791629+00:00", "status": "completed" }, "tags": [] @@ -1799,14 +1860,14 @@ }, "papermill": { "default_parameters": {}, - "duration": 13.490191, - "end_time": "2026-10-08T08:38:09.881616+00:00", + "duration": 4.242185, + "end_time": "2026-10-10T14:29:55.134967+00:00", "environment_variables": {}, "exception": null, "input_path": "KNOTS-03-Companion-Formel-Lean-Python.ipynb", - "output_path": "KNOTS-03-Companion-Formel-Lean-Python_output.ipynb", + "output_path": "KNOTS-03-Companion-Formel-Lean-Python.ipynb", "parameters": {}, - "start_time": "2026-10-08T08:37:56.391425+00:00", + "start_time": "2026-10-10T14:29:50.892782+00:00", "version": "2.7.0" } },