fix(pedagogy,#13410): relay g53-probas-1 — Percolation-Lean + PyMC-09 (24 défauts corrigés)

MyIA.AI.Notebooks/Probas/Applications/Percolation/Percolation-Lean.ipynb

@@ -231,12 +231,7 @@
     "tags": []
    },
    "source": [
-    "**Lecture.** Chaque signature porte la structure du modèle : `openAdj` prend la\n",
-    "configuration `ω` en argument — l'adjacence dépend de l'état du monde ; `boundary`\n",
-    "retourne un `Finset (Edge G)` (pas une `Set`), ce qui rend la frontière **cardinalisable**\n",
-    "et calculable — c'est elle qui portera le profil isopérimétrique de la section 5. Notez\n",
-    "que `Component` est une `Set V` définie par connexité ouverte ; on verra en section 3\n",
-    "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 3 qu'elle est ω-fermé, et même le **plus grand** ω-fermé contenant son sommet."
    ]
   },
   {
@@ -605,12 +600,7 @@
     "tags": []
    },
    "source": [
-    "**Lecture.** `harris_kleitman_connected` est le théorème « physique » du lake : sous\n",
-    "arêtes i.i.d. `p = 1/2`, savoir que `x` est relié à `y` **augmente** la probabilité que\n",
-    "`u` soit relié à `v` — les connexions s'entraînent au lieu de s'ignorer. La preuve est la\n",
-    "composition des trois lemmes de monotonie (chacun trivial en apparence, mais l'échelon\n",
-    "`ReflTransGen.mono` doit être franchi explicitement) avec la forme uniforme de la section 2.\n",
-    "Le `#print axioms` confirme une preuve kernel pure : aucun `sorry`, aucun `native_decide`."
+    "**Lecture.** La monotonie `openAdj_mono` et `connected_mono` établit que l'ajout d'arêtes ouvertes ne peut que renforcer la connexité : l'adjacence ouverte croît avec `ω`, et la connexité suit. C'est la propriété clé que `harris_kleitman_connected` consomme — sous arêtes i.i.d. `p = 1/2`, savoir que `x` est relié à `y` **augmente** la probabilité que `u` soit relié à `v` : les connexions s'entraînent au lieu de s'ignorer. La preuve est la composition des trois lemmes de monotonie (chacun trivial en apparence, mais l'échelon `ReflTransGen.mono` doit être franchi explicitement) avec la forme uniforme de la section 2. Le `#print axioms` confirme une preuve kernel pure : aucun `sorry`, aucun `native_decide`."
    ]
   },
   {
@@ -826,12 +816,7 @@
     "tags": []
    },
    "source": [
-    "**Lecture.** `component_iff_connected` donne la lecture probabiliste : la composante est\n",
-    "exactement la classe de connexité ouverte. `openEdgeClosed_iff_contains_components` dit\n",
-    "que « fermé » = « saturé pour la relation ↔* » : un ω-fermé ne peut pas contenir un\n",
-    "sommet sans contenir toute sa composante. Ces équivalences sont l'outillage qui rend le\n",
-    "théorème isopérimétrique de la section 5 démontrable : raisonner sur `∂A` (des arêtes)\n",
-    "revient à raisonner sur l'interaction entre `A` et les composantes (des sommets)."
+    "**Lecture.** Les quatre `#check` de cette cellule établissent la composante comme plus grand ω-fermé contenant son sommet : `component_self` (`v ∈ Component G ω v`), `component_closed` (la composante est ω-fermé), `component_iff_connected` (`w ∈ Component G ω v ⟺ v ↔* w`) et `mem_component_of_adj` (l'adjacence ouverte propage l'appartenance) ; suivent les deux caractérisations équivalentes du ω-fermé, `openEdgeClosed_iff_no_cross` et `openEdgeClosed_iff_contains_components`. C'est `component_iff_connected` qui donne la lecture probabiliste : la composante est exactement la classe de connexité ouverte. Et `openEdgeClosed_iff_contains_components` dit que « fermé » = « saturé pour la relation ↔* » : un ω-fermé ne peut pas contenir un sommet sans contenir toute sa composante. Ces équivalences sont l'outillage qui rend le théorème isopérimétrique de la section 5 démontrable : raisonner sur `∂A` (des arêtes) revient à raisonner sur l'interaction entre `A` et les composantes (des sommets)."
    ]
   },
   {
@@ -1030,12 +1015,7 @@
     "tags": []
    },
    "source": [
-    "**Lecture.** `closed_eq_empty_or_univ_of_connected` est la version qualitative du\n",
-    "principe isopérimétrique : un ensemble ω-connexe ne peut pas être « à moitié isolé » —\n",
-    "soit rien n'en sort (il est tout), soit une arête ouverte en sort (frontière non vide).\n",
-    "Les `*_closed_iff` en sont l'instanciation calculée : sur le triangle et le carré en\n",
-    "configuration **complète** (`full3`/`full4` : toutes arêtes ouvertes), la disjonction est\n",
-    "décidable arête par arête."
+    "**Lecture.** Les deux premiers `#check` posent le pont frontière ↔ fermé : `mem_boundary_iff` caractérise `e ∈ ∂A` comme « `e` ouverte et traversante », et `boundary_empty_iff_closed` donne `∂A = ∅ ⟺ A` ω-fermé — c'est ce qui relie la topologie des composantes ouvertes à la théorie isopérimétrique des sections suivantes. `closed_eq_empty_or_univ_of_connected` en est la version qualitative : un ensemble ω-connexe ne peut pas être « à moitié isolé » — soit rien n'en sort (il est tout), soit une arête ouverte en sort (frontière non vide). Les `*_closed_iff` en sont l'instanciation calculée : sur le triangle et le carré en configuration **complète** (`full3`/`full4` : toutes arêtes ouvertes), la disjonction est décidable arête par arête."
    ]
   },
   {
@@ -1254,13 +1234,7 @@
     "tags": []
    },
    "source": [
-    "**Lecture.** Le profil de `C₄` raconte la géométrie du carré : pour `k = 1, 2, 3`,\n",
-    "n'importe quelle partie propre non vide « compacte » garde exactement `2` arêtes de\n",
-    "sortie — mais la paire d'**opposés** `{0,2}` coupe le carré en deux faces et double la\n",
-    "frontière à `4`. La taille ne décide pas : la **forme** du bord décide. C'est la\n",
-    "signature isopérimétrique que, sur la grille infinie, le principe du même nom rend\n",
-    "exponentiellement coûteuse (`|∂A| ≥ c·√|A|`) — l'ingrédient clé des bornes de percolation\n",
-    "sous-critique, ici visible à l'état fini."
+    "**Lecture.** `two_le_boundary_C3` et `two_le_boundary_C4` posent la borne universelle **inférieure** : sur C₃ comme sur C₄, tout sous-ensemble non vide et différent de `univ` a une frontière d'**au moins 2** arêtes ouvertes (`2 ≤ (boundary ...).card`), quel que soit l'état du monde ω. Les `#eval` montrent que ce plancher est atteint (`#(∂{0,1}) = 2`, `#(∂{0,1,2}) = 2`) et que les opposés font mieux (`#(∂{0,2}) = 4`). Le profil de `C₄` raconte alors la géométrie du carré : pour `k = 1, 2, 3`, n'importe quelle partie propre non vide « compacte » garde exactement `2` arêtes de sortie — mais la paire d'**opposés** `{0,2}` coupe le carré en deux faces et double la frontière à `4`. La taille ne décide pas : la **forme** du bord décide. C'est la signature isopérimétrique que, sur la grille infinie, le principe du même nom rend exponentiellement coûteuse (`|∂A| ≥ c·√|A|`) — l'ingrédient clé des bornes de percolation sous-critique, ici visible à l'état fini."
    ]
   },
   {
@@ -1617,4 +1591,4 @@
  },
  "nbformat": 4,
  "nbformat_minor": 5
-}
+}