diff --git a/MyIA.AI.Notebooks/Probas/Applications/Percolation/Percolation-Lean.ipynb b/MyIA.AI.Notebooks/Probas/Applications/Percolation/Percolation-Lean.ipynb index 5259fcf610..68fcbdbde1 100644 --- a/MyIA.AI.Notebooks/Probas/Applications/Percolation/Percolation-Lean.ipynb +++ b/MyIA.AI.Notebooks/Probas/Applications/Percolation/Percolation-Lean.ipynb @@ -5,10 +5,10 @@ "id": "5f6b425b", "metadata": { "papermill": { - "duration": 0.003124, - "end_time": "2026-09-06T18:08:49.496273+00:00", + "duration": 0.006283, + "end_time": "2026-09-25T08:57:31.479272+00:00", "exception": false, - "start_time": "2026-09-06T18:08:49.493149+00:00", + "start_time": "2026-09-25T08:57:31.472989+00:00", "status": "completed" }, "tags": [] @@ -40,10 +40,10 @@ "id": "b31fddc6", "metadata": { "papermill": { - "duration": 0.002276, - "end_time": "2026-09-06T18:08:49.501530+00:00", + "duration": 0.004369, + "end_time": "2026-09-25T08:57:31.489007+00:00", "exception": false, - "start_time": "2026-09-06T18:08:49.499254+00:00", + "start_time": "2026-09-25T08:57:31.484638+00:00", "status": "completed" }, "tags": [] @@ -71,16 +71,16 @@ "id": "8c4d7384", "metadata": { "execution": { - "iopub.execute_input": "2026-09-06T18:08:49.510084Z", - "iopub.status.busy": "2026-09-06T18:08:49.509689Z", - "iopub.status.idle": "2026-09-06T18:08:50.532529Z", - "shell.execute_reply": "2026-09-06T18:08:50.531174Z" + "iopub.execute_input": "2026-09-25T08:57:31.500921Z", + "iopub.status.busy": "2026-09-25T08:57:31.500678Z", + "iopub.status.idle": "2026-09-25T08:57:35.293681Z", + "shell.execute_reply": "2026-09-25T08:57:35.292686Z" }, "papermill": { - "duration": 1.028582, - "end_time": "2026-09-06T18:08:50.532546+00:00", + "duration": 3.801081, + "end_time": "2026-09-25T08:57:35.295795+00:00", "exception": false, - "start_time": "2026-09-06T18:08:49.503964+00:00", + "start_time": "2026-09-25T08:57:31.494714+00:00", "status": "completed" }, "tags": [] @@ -222,16 +222,16 @@ "id": "64b453c5", "metadata": { "papermill": { - "duration": 0.004464, - "end_time": "2026-09-06T18:08:50.542775+00:00", + "duration": 0.004988, + "end_time": "2026-09-25T08:57:35.308712+00:00", "exception": false, - "start_time": "2026-09-06T18:08:50.538311+00:00", + "start_time": "2026-09-25T08:57:35.303724+00:00", "status": "completed" }, "tags": [] }, "source": [ - "**Lecture.** Le `#check` confirme que le lake expose les cinq briques du modèle — `Edge` (les arêtes d'un graphe fini), `openAdj` (adjacence ouverte = adjacence de `G` **plus** appartenance à `ω`), `openEdgeClosed` (ω-fermé), `Component` (composante ouverte d'un sommet), `boundary` (frontière ∂A). Chaque signature porte la structure du modèle : `openAdj` prend la configuration `ω` en argument — l'adjacence dépend de l'état du monde ; `boundary` retourne un `Finset (Edge G)` (pas une `Set`), ce qui rend la frontière **cardinalisable** et calculable — c'est elle qui portera le profil isopérimétrique de la section 5. Notez que `Component` est une `Set V` définie par connexité ouverte ; on verra en section 3 qu'elle est ω-fermé, et même le **plus grand** ω-fermé contenant son sommet." + "**Lecture.** Le `#check` confirme que le lake expose les cinq briques du modèle — `Edge` (les arêtes d'un graphe fini), `openAdj` (adjacence ouverte = adjacence de `G` **plus** appartenance à `ω`), `openEdgeClosed` (ω-fermé), `Component` (composante ouverte d'un sommet), `boundary` (frontière ∂A). Chaque signature porte la structure du modèle : `openAdj` prend la configuration `ω` en argument — l'adjacence dépend de l'état du monde ; `boundary` retourne un `Finset (Edge G)` (pas une `Set`), ce qui rend la frontière **cardinalisable** et calculable — c'est elle qui portera le profil isopérimétrique de la section 5. Notez que `Component` est une `Set V` définie par connexité ouverte ; on verra en section 4 qu'elle est ω-fermé, et même le **plus grand** ω-fermé contenant son sommet." ] }, { @@ -239,10 +239,10 @@ "id": "c81bf454", "metadata": { "papermill": { - "duration": 0.003088, - "end_time": "2026-09-06T18:08:50.549808+00:00", + "duration": 0.006554, + "end_time": "2026-09-25T08:57:35.321919+00:00", "exception": false, - "start_time": "2026-09-06T18:08:50.546720+00:00", + "start_time": "2026-09-25T08:57:35.315365+00:00", "status": "completed" }, "tags": [] @@ -271,16 +271,16 @@ "id": "475d4f67", "metadata": { "execution": { - "iopub.execute_input": "2026-09-06T18:08:50.559105Z", - "iopub.status.busy": "2026-09-06T18:08:50.558921Z", - "iopub.status.idle": "2026-09-06T18:08:50.729361Z", - "shell.execute_reply": "2026-09-06T18:08:50.728705Z" + "iopub.execute_input": "2026-09-25T08:57:35.335687Z", + "iopub.status.busy": "2026-09-25T08:57:35.335446Z", + "iopub.status.idle": "2026-09-25T08:57:35.493096Z", + "shell.execute_reply": "2026-09-25T08:57:35.492316Z" }, "papermill": { - "duration": 0.176499, - "end_time": "2026-09-06T18:08:50.729343+00:00", + "duration": 0.165379, + "end_time": "2026-09-25T08:57:35.494174+00:00", "exception": false, - "start_time": "2026-09-06T18:08:50.552844+00:00", + "start_time": "2026-09-25T08:57:35.328795+00:00", "status": "completed" }, "tags": [] @@ -388,10 +388,10 @@ "id": "b77344ae", "metadata": { "papermill": { - "duration": 0.004254, - "end_time": "2026-09-06T18:08:50.737770+00:00", + "duration": 0.002638, + "end_time": "2026-09-25T08:57:35.499924+00:00", "exception": false, - "start_time": "2026-09-06T18:08:50.733516+00:00", + "start_time": "2026-09-25T08:57:35.497286+00:00", "status": "completed" }, "tags": [] @@ -411,10 +411,10 @@ "id": "0fdcb427", "metadata": { "papermill": { - "duration": 0.00275, - "end_time": "2026-09-06T18:08:50.743499+00:00", + "duration": 0.003603, + "end_time": "2026-09-25T08:57:35.507154+00:00", "exception": false, - "start_time": "2026-09-06T18:08:50.740749+00:00", + "start_time": "2026-09-25T08:57:35.503551+00:00", "status": "completed" }, "tags": [] @@ -441,16 +441,16 @@ "id": "efc83852", "metadata": { "execution": { - "iopub.execute_input": "2026-09-06T18:08:50.753907Z", - "iopub.status.busy": "2026-09-06T18:08:50.753749Z", - "iopub.status.idle": "2026-09-06T18:08:50.932929Z", - "shell.execute_reply": "2026-09-06T18:08:50.932128Z" + "iopub.execute_input": "2026-09-25T08:57:35.515567Z", + "iopub.status.busy": "2026-09-25T08:57:35.515417Z", + "iopub.status.idle": "2026-09-25T08:57:35.695655Z", + "shell.execute_reply": "2026-09-25T08:57:35.694916Z" }, "papermill": { - "duration": 0.185453, - "end_time": "2026-09-06T18:08:50.932720+00:00", + "duration": 0.186498, + "end_time": "2026-09-25T08:57:35.697187+00:00", "exception": false, - "start_time": "2026-09-06T18:08:50.747267+00:00", + "start_time": "2026-09-25T08:57:35.510689+00:00", "status": "completed" }, "tags": [] @@ -591,10 +591,10 @@ "id": "e6360062", "metadata": { "papermill": { - "duration": 0.003216, - "end_time": "2026-09-06T18:08:50.940210+00:00", + "duration": 0.005986, + "end_time": "2026-09-25T08:57:35.709592+00:00", "exception": false, - "start_time": "2026-09-06T18:08:50.936994+00:00", + "start_time": "2026-09-25T08:57:35.703606+00:00", "status": "completed" }, "tags": [] @@ -608,10 +608,10 @@ "id": "6cf2b94a", "metadata": { "papermill": { - "duration": 0.003001, - "end_time": "2026-09-06T18:08:50.946422+00:00", + "duration": 0.006387, + "end_time": "2026-09-25T08:57:35.721917+00:00", "exception": false, - "start_time": "2026-09-06T18:08:50.943421+00:00", + "start_time": "2026-09-25T08:57:35.715530+00:00", "status": "completed" }, "tags": [] @@ -636,16 +636,16 @@ "id": "a28f3fce", "metadata": { "execution": { - "iopub.execute_input": "2026-09-06T18:08:50.956527Z", - "iopub.status.busy": "2026-09-06T18:08:50.956230Z", - "iopub.status.idle": "2026-09-06T18:08:51.131489Z", - "shell.execute_reply": "2026-09-06T18:08:51.130732Z" + "iopub.execute_input": "2026-09-25T08:57:35.739100Z", + "iopub.status.busy": "2026-09-25T08:57:35.738758Z", + "iopub.status.idle": "2026-09-25T08:57:35.911761Z", + "shell.execute_reply": "2026-09-25T08:57:35.910903Z" }, "papermill": { - "duration": 0.18103, - "end_time": "2026-09-06T18:08:51.130994+00:00", + "duration": 0.185077, + "end_time": "2026-09-25T08:57:35.914147+00:00", "exception": false, - "start_time": "2026-09-06T18:08:50.949964+00:00", + "start_time": "2026-09-25T08:57:35.729070+00:00", "status": "completed" }, "tags": [] @@ -807,10 +807,10 @@ "id": "ee797190", "metadata": { "papermill": { - "duration": 0.003477, - "end_time": "2026-09-06T18:08:51.138705+00:00", + "duration": 0.007628, + "end_time": "2026-09-25T08:57:35.930571+00:00", "exception": false, - "start_time": "2026-09-06T18:08:51.135228+00:00", + "start_time": "2026-09-25T08:57:35.922943+00:00", "status": "completed" }, "tags": [] @@ -824,10 +824,10 @@ "id": "001333ec", "metadata": { "papermill": { - "duration": 0.003977, - "end_time": "2026-09-06T18:08:51.146672+00:00", + "duration": 0.005737, + "end_time": "2026-09-25T08:57:35.943314+00:00", "exception": false, - "start_time": "2026-09-06T18:08:51.142695+00:00", + "start_time": "2026-09-25T08:57:35.937577+00:00", "status": "completed" }, "tags": [] @@ -853,16 +853,16 @@ "id": "50d6bc5d", "metadata": { "execution": { - "iopub.execute_input": "2026-09-06T18:08:51.156905Z", - "iopub.status.busy": "2026-09-06T18:08:51.156735Z", - "iopub.status.idle": "2026-09-06T18:08:51.320159Z", - "shell.execute_reply": "2026-09-06T18:08:51.319337Z" + "iopub.execute_input": "2026-09-25T08:57:35.958890Z", + "iopub.status.busy": "2026-09-25T08:57:35.958647Z", + "iopub.status.idle": "2026-09-25T08:57:36.139939Z", + "shell.execute_reply": "2026-09-25T08:57:36.139142Z" }, "papermill": { - "duration": 0.1695, - "end_time": "2026-09-06T18:08:51.319602+00:00", + "duration": 0.191338, + "end_time": "2026-09-25T08:57:36.141056+00:00", "exception": false, - "start_time": "2026-09-06T18:08:51.150102+00:00", + "start_time": "2026-09-25T08:57:35.949718+00:00", "status": "completed" }, "tags": [] @@ -1006,10 +1006,10 @@ "id": "4ef7396d", "metadata": { "papermill": { - "duration": 0.00409, - "end_time": "2026-09-06T18:08:51.328809+00:00", + "duration": 0.003351, + "end_time": "2026-09-25T08:57:36.148349+00:00", "exception": false, - "start_time": "2026-09-06T18:08:51.324719+00:00", + "start_time": "2026-09-25T08:57:36.144998+00:00", "status": "completed" }, "tags": [] @@ -1023,10 +1023,10 @@ "id": "9b6b2a62", "metadata": { "papermill": { - "duration": 0.00403, - "end_time": "2026-09-06T18:08:51.337579+00:00", + "duration": 0.003374, + "end_time": "2026-09-25T08:57:36.155187+00:00", "exception": false, - "start_time": "2026-09-06T18:08:51.333549+00:00", + "start_time": "2026-09-25T08:57:36.151813+00:00", "status": "completed" }, "tags": [] @@ -1054,16 +1054,16 @@ "id": "c4545c71", "metadata": { "execution": { - "iopub.execute_input": "2026-09-06T18:08:51.353697Z", - "iopub.status.busy": "2026-09-06T18:08:51.353405Z", - "iopub.status.idle": "2026-09-06T18:08:51.562824Z", - "shell.execute_reply": "2026-09-06T18:08:51.561868Z" + "iopub.execute_input": "2026-09-25T08:57:36.163825Z", + "iopub.status.busy": "2026-09-25T08:57:36.163566Z", + "iopub.status.idle": "2026-09-25T08:57:36.415689Z", + "shell.execute_reply": "2026-09-25T08:57:36.414906Z" }, "papermill": { - "duration": 0.218663, - "end_time": "2026-09-06T18:08:51.562331+00:00", + "duration": 0.259392, + "end_time": "2026-09-25T08:57:36.417866+00:00", "exception": false, - "start_time": "2026-09-06T18:08:51.343668+00:00", + "start_time": "2026-09-25T08:57:36.158474+00:00", "status": "completed" }, "tags": [] @@ -1082,21 +1082,27 @@ " \n", "
\n", " 
-- Le profil isopérimétrique exact, en théorèmes puis en valeurs calculées :
\n", - "
 two_le_boundary_C3 : ∀ (A : Finset (Fin 3)), A.Nonempty → A ≠ Finset.univ → 2 ≤ (boundary C3 full3 A).card
\n", - "
 two_le_boundary_C4 : ∀ (A : Finset (Fin 4)), A.Nonempty → A ≠ Finset.univ → 2 ≤ (boundary C4 full4 A).card
\n", - "
 boundary_card_C4_adjacent : (boundary C4 full4 {0, 1}).card = 2
\n", - "
 boundary_card_C4_triple : (boundary C4 full4 {0, 1, 2}).card = 2
\n", - "
 boundary_card_C4_opposite : (boundary C4 full4 {0, 2}).card = 4
\n", + "
 boundary_card_C3 : ∀ (A : Finset (Fin 3)), A.Nonempty → A ≠ Finset.univ → (boundary C3 full3 A).card = 2
\n", + "
 two_le_boundary_C3 : ∀ (A : Finset (Fin 3)), A.Nonempty → A ≠ Finset.univ → 2 ≤ (boundary C3 full3 A).card
\n", + "
 two_le_boundary_C4 : ∀ (A : Finset (Fin 4)), A.Nonempty → A ≠ Finset.univ → 2 ≤ (boundary C4 full4 A).card
\n", + "
 boundary_attains_min_C4 : ∃ A, A.Nonempty ∧ A ≠ Finset.univ ∧ (boundary C4 full4 A).card = 2
\n", + "
 boundary_card_C4_adjacent : (boundary C4 full4 {0, 1}).card = 2
\n", + "
 boundary_card_C4_triple : (boundary C4 full4 {0, 1, 2}).card = 2
\n", + "
 boundary_card_C4_opposite : (boundary C4 full4 {0, 2}).card = 4
\n", "
\n", "
-- Les mêmes valeurs, calculées par évaluation native du kernel :
\n", - "
 3
\n", - "
 2
\n", - "
 4
\n", + "
 3
\n", + "
 2
\n", + "
 2
\n", + "
 2
\n", + "
 2
\n", + "
 4
\n", + "
\n", "
--% env 5
\n", "
\n", "
\n", " Raw input\n", - " {\"cmd\": \"-- Le profil isop\\u00e9rim\\u00e9trique exact, en th\\u00e9or\\u00e8mes puis en valeurs calcul\\u00e9es :\\n#check @two_le_boundary_C3 -- borne universelle sur C\\u2083\\n#check @two_le_boundary_C4 -- borne universelle sur C\\u2084\\n#check @boundary_card_C4_adjacent -- #(\\u2202{0,1}) = 2\\n#check @boundary_card_C4_triple -- #(\\u2202{0,1,2}) = 2\\n#check @boundary_card_C4_opposite -- #(\\u2202{0,2}) = 4 (les deux faces du carr\\u00e9)\\n\\n-- Les m\\u00eames valeurs, calcul\\u00e9es par \\u00e9valuation native du kernel :\\n#eval Fintype.card (Edge C3) -- 3 ar\\u00eates au triangle\\n#eval (boundary C3 full3 ({0} : Finset (Fin 3))).card -- fronti\\u00e8re du singleton\\n#eval (boundary C4 full4 ({0, 2} : Finset (Fin 4))).card -- fronti\\u00e8re des oppos\\u00e9s\", \"env\": 4}\n", + " {\"cmd\": \"-- Le profil isop\\u00e9rim\\u00e9trique exact, en th\\u00e9or\\u00e8mes puis en valeurs calcul\\u00e9es :\\n#check @boundary_card_C3 -- #(\\u2202A) = 2 exactement sur C\\u2083 (parties propres non vides)\\n#check @two_le_boundary_C3 -- borne universelle sur C\\u2083\\n#check @two_le_boundary_C4 -- borne universelle sur C\\u2084\\n#check @boundary_attains_min_C4 -- le minimum est atteint sur C\\u2084 (t\\u00e9moin {0})\\n#check @boundary_card_C4_adjacent -- #(\\u2202{0,1}) = 2\\n#check @boundary_card_C4_triple -- #(\\u2202{0,1,2}) = 2\\n#check @boundary_card_C4_opposite -- #(\\u2202{0,2}) = 4 (les deux faces du carr\\u00e9)\\n\\n-- Les m\\u00eames valeurs, calcul\\u00e9es par \\u00e9valuation native du kernel :\\n#eval Fintype.card (Edge C3) -- 3 ar\\u00eates au triangle\\n#eval (boundary C3 full3 ({0} : Finset (Fin 3))).card -- fronti\\u00e8re du singleton de C\\u2083\\n#eval (boundary C4 full4 ({0} : Finset (Fin 4))).card -- singleton du carr\\u00e9\\n#eval (boundary C4 full4 ({0, 1} : Finset (Fin 4))).card -- adjacents du carr\\u00e9\\n#eval (boundary C4 full4 ({0, 1, 2} : Finset (Fin 4))).card -- triple du carr\\u00e9\\n#eval (boundary C4 full4 ({0, 2} : Finset (Fin 4))).card -- fronti\\u00e8re des oppos\\u00e9s\\n\", \"env\": 4}\n", "
\n", "
\n", " Raw output\n", @@ -1105,35 +1111,57 @@ " \"pos\": {\"line\": 2, \"column\": 0},\r\n", " \"endPos\": {\"line\": 2, \"column\": 6},\r\n", " \"data\":\r\n", - " \"two_le_boundary_C3 : ∀ (A : Finset (Fin 3)), A.Nonempty → A ≠ Finset.univ → 2 ≤ (boundary C3 full3 A).card\"},\r\n", + " \"boundary_card_C3 : ∀ (A : Finset (Fin 3)), A.Nonempty → A ≠ Finset.univ → (boundary C3 full3 A).card = 2\"},\r\n", " {\"severity\": \"info\",\r\n", " \"pos\": {\"line\": 3, \"column\": 0},\r\n", " \"endPos\": {\"line\": 3, \"column\": 6},\r\n", " \"data\":\r\n", - " \"two_le_boundary_C4 : ∀ (A : Finset (Fin 4)), A.Nonempty → A ≠ Finset.univ → 2 ≤ (boundary C4 full4 A).card\"},\r\n", + " \"two_le_boundary_C3 : ∀ (A : Finset (Fin 3)), A.Nonempty → A ≠ Finset.univ → 2 ≤ (boundary C3 full3 A).card\"},\r\n", " {\"severity\": \"info\",\r\n", " \"pos\": {\"line\": 4, \"column\": 0},\r\n", " \"endPos\": {\"line\": 4, \"column\": 6},\r\n", - " \"data\": \"boundary_card_C4_adjacent : (boundary C4 full4 {0, 1}).card = 2\"},\r\n", + " \"data\":\r\n", + " \"two_le_boundary_C4 : ∀ (A : Finset (Fin 4)), A.Nonempty → A ≠ Finset.univ → 2 ≤ (boundary C4 full4 A).card\"},\r\n", " {\"severity\": \"info\",\r\n", " \"pos\": {\"line\": 5, \"column\": 0},\r\n", " \"endPos\": {\"line\": 5, \"column\": 6},\r\n", - " \"data\": \"boundary_card_C4_triple : (boundary C4 full4 {0, 1, 2}).card = 2\"},\r\n", + " \"data\":\r\n", + " \"boundary_attains_min_C4 : ∃ A, A.Nonempty ∧ A ≠ Finset.univ ∧ (boundary C4 full4 A).card = 2\"},\r\n", " {\"severity\": \"info\",\r\n", " \"pos\": {\"line\": 6, \"column\": 0},\r\n", " \"endPos\": {\"line\": 6, \"column\": 6},\r\n", + " \"data\": \"boundary_card_C4_adjacent : (boundary C4 full4 {0, 1}).card = 2\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 7, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 7, \"column\": 6},\r\n", + " \"data\": \"boundary_card_C4_triple : (boundary C4 full4 {0, 1, 2}).card = 2\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 8, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 8, \"column\": 6},\r\n", " \"data\": \"boundary_card_C4_opposite : (boundary C4 full4 {0, 2}).card = 4\"},\r\n", " {\"severity\": \"info\",\r\n", - " \"pos\": {\"line\": 9, \"column\": 0},\r\n", - " \"endPos\": {\"line\": 9, \"column\": 5},\r\n", + " \"pos\": {\"line\": 11, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 11, \"column\": 5},\r\n", " \"data\": \"3\"},\r\n", " {\"severity\": \"info\",\r\n", - " \"pos\": {\"line\": 10, \"column\": 0},\r\n", - " \"endPos\": {\"line\": 10, \"column\": 5},\r\n", + " \"pos\": {\"line\": 12, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 12, \"column\": 5},\r\n", " \"data\": \"2\"},\r\n", " {\"severity\": \"info\",\r\n", - " \"pos\": {\"line\": 11, \"column\": 0},\r\n", - " \"endPos\": {\"line\": 11, \"column\": 5},\r\n", + " \"pos\": {\"line\": 13, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 13, \"column\": 5},\r\n", + " \"data\": \"2\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 14, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 14, \"column\": 5},\r\n", + " \"data\": \"2\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 15, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 15, \"column\": 5},\r\n", + " \"data\": \"2\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 16, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 16, \"column\": 5},\r\n", " \"data\": \"4\"}],\r\n", " \"env\": 5}\n", "
\n", @@ -1141,10 +1169,14 @@ ], "text/plain": [ "-- Le profil isopérimétrique exact, en théorèmes puis en valeurs calculées :\n", + "#check @boundary_card_C3 -- #(∂A) = 2 exactement sur C₃ (parties propres non vides)\n", + "──────▶ boundary_card_C3 : ∀ (A : Finset (Fin 3)), A.Nonempty → A ≠ Finset.univ → (boundary C3 full3 A).card = 2\n", "#check @two_le_boundary_C3 -- borne universelle sur C₃\n", "──────▶ two_le_boundary_C3 : ∀ (A : Finset (Fin 3)), A.Nonempty → A ≠ Finset.univ → 2 ≤ (boundary C3 full3 A).card\n", "#check @two_le_boundary_C4 -- borne universelle sur C₄\n", "──────▶ two_le_boundary_C4 : ∀ (A : Finset (Fin 4)), A.Nonempty → A ≠ Finset.univ → 2 ≤ (boundary C4 full4 A).card\n", + "#check @boundary_attains_min_C4 -- le minimum est atteint sur C₄ (témoin {0})\n", + "──────▶ boundary_attains_min_C4 : ∃ A, A.Nonempty ∧ A ≠ Finset.univ ∧ (boundary C4 full4 A).card = 2\n", "#check @boundary_card_C4_adjacent -- #(∂{0,1}) = 2\n", "──────▶ boundary_card_C4_adjacent : (boundary C4 full4 {0, 1}).card = 2\n", "#check @boundary_card_C4_triple -- #(∂{0,1,2}) = 2\n", @@ -1155,49 +1187,78 @@ "-- Les mêmes valeurs, calculées par évaluation native du kernel :\n", "#eval Fintype.card (Edge C3) -- 3 arêtes au triangle\n", "─────▶ 3\n", - "#eval (boundary C3 full3 ({0} : Finset (Fin 3))).card -- frontière du singleton\n", + "#eval (boundary C3 full3 ({0} : Finset (Fin 3))).card -- frontière du singleton de C₃\n", + "─────▶ 2\n", + "#eval (boundary C4 full4 ({0} : Finset (Fin 4))).card -- singleton du carré\n", + "─────▶ 2\n", + "#eval (boundary C4 full4 ({0, 1} : Finset (Fin 4))).card -- adjacents du carré\n", + "─────▶ 2\n", + "#eval (boundary C4 full4 ({0, 1, 2} : Finset (Fin 4))).card -- triple du carré\n", "─────▶ 2\n", "#eval (boundary C4 full4 ({0, 2} : Finset (Fin 4))).card -- frontière des opposés\n", "─────▶ 4\n", + "\n", "--% env 5\n", "\n", "Raw input:\n", - "{\"cmd\": \"-- Le profil isop\\u00e9rim\\u00e9trique exact, en th\\u00e9or\\u00e8mes puis en valeurs calcul\\u00e9es :\\n#check @two_le_boundary_C3 -- borne universelle sur C\\u2083\\n#check @two_le_boundary_C4 -- borne universelle sur C\\u2084\\n#check @boundary_card_C4_adjacent -- #(\\u2202{0,1}) = 2\\n#check @boundary_card_C4_triple -- #(\\u2202{0,1,2}) = 2\\n#check @boundary_card_C4_opposite -- #(\\u2202{0,2}) = 4 (les deux faces du carr\\u00e9)\\n\\n-- Les m\\u00eames valeurs, calcul\\u00e9es par \\u00e9valuation native du kernel :\\n#eval Fintype.card (Edge C3) -- 3 ar\\u00eates au triangle\\n#eval (boundary C3 full3 ({0} : Finset (Fin 3))).card -- fronti\\u00e8re du singleton\\n#eval (boundary C4 full4 ({0, 2} : Finset (Fin 4))).card -- fronti\\u00e8re des oppos\\u00e9s\", \"env\": 4}\n", + "{\"cmd\": \"-- Le profil isop\\u00e9rim\\u00e9trique exact, en th\\u00e9or\\u00e8mes puis en valeurs calcul\\u00e9es :\\n#check @boundary_card_C3 -- #(\\u2202A) = 2 exactement sur C\\u2083 (parties propres non vides)\\n#check @two_le_boundary_C3 -- borne universelle sur C\\u2083\\n#check @two_le_boundary_C4 -- borne universelle sur C\\u2084\\n#check @boundary_attains_min_C4 -- le minimum est atteint sur C\\u2084 (t\\u00e9moin {0})\\n#check @boundary_card_C4_adjacent -- #(\\u2202{0,1}) = 2\\n#check @boundary_card_C4_triple -- #(\\u2202{0,1,2}) = 2\\n#check @boundary_card_C4_opposite -- #(\\u2202{0,2}) = 4 (les deux faces du carr\\u00e9)\\n\\n-- Les m\\u00eames valeurs, calcul\\u00e9es par \\u00e9valuation native du kernel :\\n#eval Fintype.card (Edge C3) -- 3 ar\\u00eates au triangle\\n#eval (boundary C3 full3 ({0} : Finset (Fin 3))).card -- fronti\\u00e8re du singleton de C\\u2083\\n#eval (boundary C4 full4 ({0} : Finset (Fin 4))).card -- singleton du carr\\u00e9\\n#eval (boundary C4 full4 ({0, 1} : Finset (Fin 4))).card -- adjacents du carr\\u00e9\\n#eval (boundary C4 full4 ({0, 1, 2} : Finset (Fin 4))).card -- triple du carr\\u00e9\\n#eval (boundary C4 full4 ({0, 2} : Finset (Fin 4))).card -- fronti\\u00e8re des oppos\\u00e9s\\n\", \"env\": 4}\n", "Raw output:\n", "{\"messages\":\r\n", " [{\"severity\": \"info\",\r\n", " \"pos\": {\"line\": 2, \"column\": 0},\r\n", " \"endPos\": {\"line\": 2, \"column\": 6},\r\n", " \"data\":\r\n", - " \"two_le_boundary_C3 : ∀ (A : Finset (Fin 3)), A.Nonempty → A ≠ Finset.univ → 2 ≤ (boundary C3 full3 A).card\"},\r\n", + " \"boundary_card_C3 : ∀ (A : Finset (Fin 3)), A.Nonempty → A ≠ Finset.univ → (boundary C3 full3 A).card = 2\"},\r\n", " {\"severity\": \"info\",\r\n", " \"pos\": {\"line\": 3, \"column\": 0},\r\n", " \"endPos\": {\"line\": 3, \"column\": 6},\r\n", " \"data\":\r\n", - " \"two_le_boundary_C4 : ∀ (A : Finset (Fin 4)), A.Nonempty → A ≠ Finset.univ → 2 ≤ (boundary C4 full4 A).card\"},\r\n", + " \"two_le_boundary_C3 : ∀ (A : Finset (Fin 3)), A.Nonempty → A ≠ Finset.univ → 2 ≤ (boundary C3 full3 A).card\"},\r\n", " {\"severity\": \"info\",\r\n", " \"pos\": {\"line\": 4, \"column\": 0},\r\n", " \"endPos\": {\"line\": 4, \"column\": 6},\r\n", - " \"data\": \"boundary_card_C4_adjacent : (boundary C4 full4 {0, 1}).card = 2\"},\r\n", + " \"data\":\r\n", + " \"two_le_boundary_C4 : ∀ (A : Finset (Fin 4)), A.Nonempty → A ≠ Finset.univ → 2 ≤ (boundary C4 full4 A).card\"},\r\n", " {\"severity\": \"info\",\r\n", " \"pos\": {\"line\": 5, \"column\": 0},\r\n", " \"endPos\": {\"line\": 5, \"column\": 6},\r\n", - " \"data\": \"boundary_card_C4_triple : (boundary C4 full4 {0, 1, 2}).card = 2\"},\r\n", + " \"data\":\r\n", + " \"boundary_attains_min_C4 : ∃ A, A.Nonempty ∧ A ≠ Finset.univ ∧ (boundary C4 full4 A).card = 2\"},\r\n", " {\"severity\": \"info\",\r\n", " \"pos\": {\"line\": 6, \"column\": 0},\r\n", " \"endPos\": {\"line\": 6, \"column\": 6},\r\n", + " \"data\": \"boundary_card_C4_adjacent : (boundary C4 full4 {0, 1}).card = 2\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 7, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 7, \"column\": 6},\r\n", + " \"data\": \"boundary_card_C4_triple : (boundary C4 full4 {0, 1, 2}).card = 2\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 8, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 8, \"column\": 6},\r\n", " \"data\": \"boundary_card_C4_opposite : (boundary C4 full4 {0, 2}).card = 4\"},\r\n", " {\"severity\": \"info\",\r\n", - " \"pos\": {\"line\": 9, \"column\": 0},\r\n", - " \"endPos\": {\"line\": 9, \"column\": 5},\r\n", + " \"pos\": {\"line\": 11, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 11, \"column\": 5},\r\n", " \"data\": \"3\"},\r\n", " {\"severity\": \"info\",\r\n", - " \"pos\": {\"line\": 10, \"column\": 0},\r\n", - " \"endPos\": {\"line\": 10, \"column\": 5},\r\n", + " \"pos\": {\"line\": 12, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 12, \"column\": 5},\r\n", " \"data\": \"2\"},\r\n", " {\"severity\": \"info\",\r\n", - " \"pos\": {\"line\": 11, \"column\": 0},\r\n", - " \"endPos\": {\"line\": 11, \"column\": 5},\r\n", + " \"pos\": {\"line\": 13, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 13, \"column\": 5},\r\n", + " \"data\": \"2\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 14, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 14, \"column\": 5},\r\n", + " \"data\": \"2\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 15, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 15, \"column\": 5},\r\n", + " \"data\": \"2\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 16, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 16, \"column\": 5},\r\n", " \"data\": \"4\"}],\r\n", " \"env\": 5}" ] @@ -1208,16 +1269,21 @@ ], "source": [ "-- Le profil isopérimétrique exact, en théorèmes puis en valeurs calculées :\n", + "#check @boundary_card_C3 -- #(∂A) = 2 exactement sur C₃ (parties propres non vides)\n", "#check @two_le_boundary_C3 -- borne universelle sur C₃\n", "#check @two_le_boundary_C4 -- borne universelle sur C₄\n", + "#check @boundary_attains_min_C4 -- le minimum est atteint sur C₄ (témoin {0})\n", "#check @boundary_card_C4_adjacent -- #(∂{0,1}) = 2\n", "#check @boundary_card_C4_triple -- #(∂{0,1,2}) = 2\n", "#check @boundary_card_C4_opposite -- #(∂{0,2}) = 4 (les deux faces du carré)\n", "\n", "-- Les mêmes valeurs, calculées par évaluation native du kernel :\n", "#eval Fintype.card (Edge C3) -- 3 arêtes au triangle\n", - "#eval (boundary C3 full3 ({0} : Finset (Fin 3))).card -- frontière du singleton\n", - "#eval (boundary C4 full4 ({0, 2} : Finset (Fin 4))).card -- frontière des opposés" + "#eval (boundary C3 full3 ({0} : Finset (Fin 3))).card -- frontière du singleton de C₃\n", + "#eval (boundary C4 full4 ({0} : Finset (Fin 4))).card -- singleton du carré\n", + "#eval (boundary C4 full4 ({0, 1} : Finset (Fin 4))).card -- adjacents du carré\n", + "#eval (boundary C4 full4 ({0, 1, 2} : Finset (Fin 4))).card -- triple du carré\n", + "#eval (boundary C4 full4 ({0, 2} : Finset (Fin 4))).card -- frontière des opposés\n" ] }, { @@ -1225,10 +1291,10 @@ "id": "071493f5", "metadata": { "papermill": { - "duration": 0.004305, - "end_time": "2026-09-06T18:08:51.571407+00:00", + "duration": 0.00807, + "end_time": "2026-09-25T08:57:36.434972+00:00", "exception": false, - "start_time": "2026-09-06T18:08:51.567102+00:00", + "start_time": "2026-09-25T08:57:36.426902+00:00", "status": "completed" }, "tags": [] @@ -1242,10 +1308,10 @@ "id": "966a8691", "metadata": { "papermill": { - "duration": 0.004629, - "end_time": "2026-09-06T18:08:51.580511+00:00", + "duration": 0.004571, + "end_time": "2026-09-25T08:57:36.443481+00:00", "exception": false, - "start_time": "2026-09-06T18:08:51.575882+00:00", + "start_time": "2026-09-25T08:57:36.438910+00:00", "status": "completed" }, "tags": [] @@ -1266,16 +1332,16 @@ "id": "3901d0d0", "metadata": { "execution": { - "iopub.execute_input": "2026-09-06T18:08:51.592711Z", - "iopub.status.busy": "2026-09-06T18:08:51.592551Z", - "iopub.status.idle": "2026-09-06T18:08:51.786650Z", - "shell.execute_reply": "2026-09-06T18:08:51.784798Z" + "iopub.execute_input": "2026-09-25T08:57:36.461883Z", + "iopub.status.busy": "2026-09-25T08:57:36.461638Z", + "iopub.status.idle": "2026-09-25T08:57:36.615659Z", + "shell.execute_reply": "2026-09-25T08:57:36.614648Z" }, "papermill": { - "duration": 0.201778, - "end_time": "2026-09-06T18:08:51.786970+00:00", + "duration": 0.16468, + "end_time": "2026-09-25T08:57:36.616787+00:00", "exception": false, - "start_time": "2026-09-06T18:08:51.585192+00:00", + "start_time": "2026-09-25T08:57:36.452107+00:00", "status": "completed" }, "tags": [] @@ -1351,16 +1417,16 @@ "id": "255520c8", "metadata": { "execution": { - "iopub.execute_input": "2026-09-06T18:08:51.817324Z", - "iopub.status.busy": "2026-09-06T18:08:51.816770Z", - "iopub.status.idle": "2026-09-06T18:08:51.970343Z", - "shell.execute_reply": "2026-09-06T18:08:51.969486Z" + "iopub.execute_input": "2026-09-25T08:57:36.629407Z", + "iopub.status.busy": "2026-09-25T08:57:36.629235Z", + "iopub.status.idle": "2026-09-25T08:57:36.776511Z", + "shell.execute_reply": "2026-09-25T08:57:36.775767Z" }, "papermill": { - "duration": 0.169911, - "end_time": "2026-09-06T18:08:51.969551+00:00", + "duration": 0.156207, + "end_time": "2026-09-25T08:57:36.778473+00:00", "exception": false, - "start_time": "2026-09-06T18:08:51.799640+00:00", + "start_time": "2026-09-25T08:57:36.622266+00:00", "status": "completed" }, "tags": [] @@ -1442,16 +1508,16 @@ "id": "3d9807f6", "metadata": { "execution": { - "iopub.execute_input": "2026-09-06T18:08:51.984925Z", - "iopub.status.busy": "2026-09-06T18:08:51.984758Z", - "iopub.status.idle": "2026-09-06T18:08:52.135153Z", - "shell.execute_reply": "2026-09-06T18:08:52.134368Z" + "iopub.execute_input": "2026-09-25T08:57:36.796412Z", + "iopub.status.busy": "2026-09-25T08:57:36.796240Z", + "iopub.status.idle": "2026-09-25T08:57:36.949757Z", + "shell.execute_reply": "2026-09-25T08:57:36.949084Z" }, "papermill": { - "duration": 0.160596, - "end_time": "2026-09-06T18:08:52.135691+00:00", + "duration": 0.165129, + "end_time": "2026-09-25T08:57:36.951068+00:00", "exception": false, - "start_time": "2026-09-06T18:08:51.975095+00:00", + "start_time": "2026-09-25T08:57:36.785939+00:00", "status": "completed" }, "tags": [] @@ -1538,10 +1604,10 @@ "id": "f7eb46df", "metadata": { "papermill": { - "duration": 0.015836, - "end_time": "2026-09-06T18:08:52.165847+00:00", + "duration": 0.005988, + "end_time": "2026-09-25T08:57:36.964648+00:00", "exception": false, - "start_time": "2026-09-06T18:08:52.150011+00:00", + "start_time": "2026-09-25T08:57:36.958660+00:00", "status": "completed" }, "tags": [] @@ -1578,14 +1644,14 @@ }, "papermill": { "default_parameters": {}, - "duration": 4.287036, - "end_time": "2026-09-06T18:08:52.408354+00:00", + "duration": 14.708284, + "end_time": "2026-09-25T08:57:37.196720+00:00", "environment_variables": {}, "exception": null, "input_path": "Percolation-Lean.ipynb", "output_path": "Percolation-Lean.ipynb", "parameters": {}, - "start_time": "2026-09-06T18:08:48.121318+00:00", + "start_time": "2026-09-25T08:57:22.488436+00:00", "version": "2.7.0" } },