Percolation-Lean — le noyau fini de percolation, prouvé en Lean 4

Navigation : ← Série Probas · Le lake percolation_lean · Voir #14871

Ce notebook est le compagnon exécutable du lake percolation_lean (MyIA.AI.Notebooks/Probas/Applications/Percolation/percolation_lean/). Le lake formalise la percolation par arêtes sur un graphe fini G : une configuration ω est un ensemble d’arêtes ouvertes, et le noyau démontre — sans aucun sorry — la corrélation positive des événements de connexion (Harris–Kleitman), la théorie des composantes ouvertes, et le profil isopérimétrique exact des graphes tests C₃ et C₄.

Ici, on ne retape pas les preuves : on lit le lake depuis le kernel Lean (#check, #print axioms, #eval), chaque signature étant confrontée à son sens probabiliste. Les quatre tranches de construction : #14892 (Harris–Kleitman fini), #14896 (connexité croissante), #14897 (composantes), #14907 (frontière isopérimétrique C₃/C₄).

Horizon honnête : le théorème de percolation sur la grille infinie (existence d’une probabilité critique p_c < 1) reste un horizon non prouvé dans le lake — le noyau est volontairement borné au monde fini, où tout est décidable et vérifié par le kernel.

1. Le vocabulaire : configurations, arêtes ouvertes, composantes

Sur un SimpleGraph fini G (type V à cardinal fini), le lac définit :

Edge G — le type des arêtes de G (paires non ordonnées Sym2 V dans l’edge set) ;
openAdj G ω u v — u et v sont adjacents et leur arête est ouverte dans ω ;
openEdgeClosed G ω A — l’ensemble A est ω-fermé : aucune arête ouverte ne le traverse ;
Component G ω v — la composante ouverte de v ;
boundary G ω A — la frontière finie ∂A : les arêtes ouvertes traversantes de A.

La lecture probabiliste : ω est l’état du monde aléatoire (arêtes i.i.d. Bernoulli p), et les définitions ci-dessus sont les événements/objets qu’on cherche à corréler.

-- Toutes les importations de la session viennent en tête (convention du kernel).
import Percolation
open Percolation

-- Le vocabulaire du noyau fini, chargé depuis le lake :
#check @Percolation.Edge          -- le type des arêtes d'un graphe fini
#check @openAdj                   -- adjacence OUVERTE (adjacence de G + arête dans ω)
#check @openEdgeClosed            -- ω-fermé : aucune arête ouverte ne traverse A
#check @Component                 -- composante ouverte d'un sommet
#check @boundary                  -- frontière ∂A : Finset des arêtes ouvertes traversantes

-- Toutes les importations de la session viennent en tête (convention du kernel).

import Percolation

open Percolation

-- Le vocabulaire du noyau fini, chargé depuis le lake :

#check @Percolation.Edge          -- le type des arêtes d'un graphe fini @Edge : {V : Type u_1} → SimpleGraph V → Type u_1

#check @openAdj                   -- adjacence OUVERTE (adjacence de G + arête dans ω) @openAdj : {V : Type u_1} → (G : SimpleGraph V) → Finset (Edge G) → V → V → Prop

#check @openEdgeClosed            -- ω-fermé : aucune arête ouverte ne traverse A @openEdgeClosed : {V : Type u_1} → (G : SimpleGraph V) → Finset (Edge G) → Set V → Prop

#check @Component                 -- composante ouverte d'un sommet @Component : {V : Type u_1} → (G : SimpleGraph V) → Finset (Edge G) → V → Set V

#check @boundary                  -- frontière ∂A : Finset des arêtes ouvertes traversantes @boundary : {V : Type u_1} →
  [Fintype V] →
    [DecidableEq V] →
      (G : SimpleGraph V) → [DecidableEq (Edge G)] → [DecidableRel G.Adj] → Finset (Edge G) → Finset V → Finset (Edge G)

--% env 0

Raw input

{"cmd": "-- Toutes les importations de la session viennent en t\u00eate (convention du kernel).\nimport Percolation\nopen Percolation\n\n-- Le vocabulaire du noyau fini, charg\u00e9 depuis le lake :\n#check @Percolation.Edge          -- le type des ar\u00eates d'un graphe fini\n#check @openAdj                   -- adjacence OUVERTE (adjacence de G + ar\u00eate dans \u03c9)\n#check @openEdgeClosed            -- \u03c9-ferm\u00e9 : aucune ar\u00eate ouverte ne traverse A\n#check @Component                 -- composante ouverte d'un sommet\n#check @boundary                  -- fronti\u00e8re \u2202A : Finset des ar\u00eates ouvertes traversantes"}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 6, "column": 0},
   "endPos": {"line": 6, "column": 6},
   "data": "@Edge : {V : Type u_1} → SimpleGraph V → Type u_1"},
  {"severity": "info",
   "pos": {"line": 7, "column": 0},
   "endPos": {"line": 7, "column": 6},
   "data":
   "@openAdj : {V : Type u_1} → (G : SimpleGraph V) → Finset (Edge G) → V → V → Prop"},
  {"severity": "info",
   "pos": {"line": 8, "column": 0},
   "endPos": {"line": 8, "column": 6},
   "data":
   "@openEdgeClosed : {V : Type u_1} → (G : SimpleGraph V) → Finset (Edge G) → Set V → Prop"},
  {"severity": "info",
   "pos": {"line": 9, "column": 0},
   "endPos": {"line": 9, "column": 6},
   "data":
   "@Component : {V : Type u_1} → (G : SimpleGraph V) → Finset (Edge G) → V → Set V"},
  {"severity": "info",
   "pos": {"line": 10, "column": 0},
   "endPos": {"line": 10, "column": 6},
   "data":
   "@boundary : {V : Type u_1} →\n  [Fintype V] →\n    [DecidableEq V] →\n      (G : SimpleGraph V) → [DecidableEq (Edge G)] → [DecidableRel G.Adj] → Finset (Edge G) → Finset V → Finset (Edge G)"}],
 "env": 0}

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.

2. Harris–Kleitman fini : la corrélation positive des événements croissants

Le théorème fondamental du lake (tranche 1, #14892), dans sa forme uniforme p = 1/2 : sur l’espace des configurations Finset α (toutes équiprobables), deux événements croissants 𝒜 et ℬ (au sens de IsUpperSet : ajouter des arêtes ouvertes préserve l’appartenance) corrèlent positivement :

#𝒜 * #ℬ ≤ 2 ^ |α| * #(𝒜 ∩ ℬ)

C’est l’inégalité FKG/Harris–Kleitman duale de l’indépendance : à p = 1/2, deux événements croissants sont simultanément plus fréquents que ne le ferait croire le produit de leurs fréquences marginales. Le lake démontre aussi la forme duale « deux décroissants » (harris_kleitman_lower_lower), obtenue par passage au complémentaire.

-- La corrélation positive, forme uniforme p = 1/2 (deux croissants / deux décroissants) :
#check @harris_kleitman_upper_upper
#check @harris_kleitman_lower_lower

-- La base d'axiomes de la preuve : attendu le triplet standard de Mathlib, AUCUN sorryAx.
#print axioms harris_kleitman_upper_upper

-- La corrélation positive, forme uniforme p = 1/2 (deux croissants / deux décroissants) :

#check @harris_kleitman_upper_upper @harris_kleitman_upper_upper : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (𝒜 ℬ : Finset (Finset α)),
  IsUpperSet ↑𝒜 → IsUpperSet ↑ℬ → 𝒜.card * ℬ.card ≤ 2 ^ Fintype.card α * (𝒜 ∩ ℬ).card

#check @harris_kleitman_lower_lower @harris_kleitman_lower_lower : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (𝒜 ℬ : Finset (Finset α)),
  IsLowerSet ↑𝒜 → IsLowerSet ↑ℬ → 𝒜.card * ℬ.card ≤ 2 ^ Fintype.card α * (𝒜 ∩ ℬ).card

-- La base d'axiomes de la preuve : attendu le triplet standard de Mathlib, AUCUN sorryAx.

#print axioms harris_kleitman_upper_upper 'Percolation.harris_kleitman_upper_upper' depends on axioms: [propext, Classical.choice, Quot.sound]

--% env 1

Raw input

{"cmd": "-- La corr\u00e9lation positive, forme uniforme p = 1/2 (deux croissants / deux d\u00e9croissants) :\n#check @harris_kleitman_upper_upper\n#check @harris_kleitman_lower_lower\n\n-- La base d'axiomes de la preuve : attendu le triplet standard de Mathlib, AUCUN sorryAx.\n#print axioms harris_kleitman_upper_upper", "env": 0}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "@harris_kleitman_upper_upper : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (𝒜 ℬ : Finset (Finset α)),\n  IsUpperSet ↑𝒜 → IsUpperSet ↑ℬ → 𝒜.card * ℬ.card ≤ 2 ^ Fintype.card α * (𝒜 ∩ ℬ).card"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "@harris_kleitman_lower_lower : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (𝒜 ℬ : Finset (Finset α)),\n  IsLowerSet ↑𝒜 → IsLowerSet ↑ℬ → 𝒜.card * ℬ.card ≤ 2 ^ Fintype.card α * (𝒜 ∩ ℬ).card"},
  {"severity": "info",
   "pos": {"line": 6, "column": 0},
   "endPos": {"line": 6, "column": 6},
   "data":
   "'Percolation.harris_kleitman_upper_upper' depends on axioms: [propext, Classical.choice, Quot.sound]"}],
 "env": 1}

Lecture. L’énoncé est fini et uniforme : il ne parle pas de mesure mais de cardinaux — #𝒜 * #ℬ ≤ 2^|α| * #(𝒜 ∩ ℬ) équivaut, en divisant par 2^(2|α|), à P(𝒜 ∩ ℬ) ≥ P(𝒜) · P(ℬ) sous la mesure uniforme. C’est exactement la positivité de la covariance. Le #print axioms rend la preuve auditée au kernel : seuls propext, Classical.choice et Quot.sound — les trois axiomes standard de Mathlib — apparaissent. Le dual lower_lower n’est pas une copie : le lake le déduit par complémentaire, et le deuxième membre (𝒜 ∩ ℬ au numérateur droit) garde la même forme.

3. Connexité croissante → la corrélation des événements de connexion

Pour brancher Harris–Kleitman sur la percolation, il faut que l’événement « u est relié à v par des arêtes ouvertes » soit croissant. Le lake démontre la chaîne complète (tranche 2, #14896) :

openAdj_mono — ouvrir des arêtes préserve l’adjacence ouverte ;
connected_mono — donc la relation de connexité ouverte (ReflTransGen de openAdj) ;
connectedEvent_isUpperSet — l’événement {ω | u ↔︎* ω v} est croissant ;
harris_kleitman_connected — et Harris–Kleitman s’applique : deux événements de connexion corrèlent positivement.

-- La monotonie, puis l'événement de connexion, puis la corrélation :
#check @openAdj_mono           -- ω₁ ⊆ ω₂ ⇒ openAdj ω₁ ≤ openAdj ω₂
#check @connected_mono         -- la connexité ouverte hérite de la monotonie
#check @connectedEvent_isUpperSet  -- {ω | u ↔* v} est un événement croissant
#check @harris_kleitman_connected  -- ⇒ #(u↔v) * #(x↔y) ≤ 2^|Edge G| * #((u↔v) ∩ (x↔y))

#print axioms harris_kleitman_connected

-- La monotonie, puis l'événement de connexion, puis la corrélation :

#check @openAdj_mono           -- ω₁ ⊆ ω₂ ⇒ openAdj ω₁ ≤ openAdj ω₂ @openAdj_mono : ∀ {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [Fintype (Edge G)]
  [DecidableEq (Edge G)] {ω₁ ω₂ : Finset (Edge G)}, ω₁ ⊆ ω₂ → openAdj G ω₁ ≤ openAdj G ω₂

#check @connected_mono         -- la connexité ouverte hérite de la monotonie @connected_mono : ∀ {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [Fintype (Edge G)]
  [DecidableEq (Edge G)] {ω₁ ω₂ : Finset (Edge G)}, ω₁ ⊆ ω₂ → ConnectedIn G ω₁ ≤ ConnectedIn G ω₂

#check @connectedEvent_isUpperSet  -- {ω | u ↔* v} est un événement croissant @connectedEvent_isUpperSet : ∀ {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [inst : Fintype (Edge G)]
  [DecidableEq (Edge G)] {u v : V}, IsUpperSet ↑(connectedEvent G u v)

#check @harris_kleitman_connected  -- ⇒ #(u↔v) * #(x↔y) ≤ 2^|Edge G| * #((u↔v) ∩ (x↔y)) @harris_kleitman_connected : ∀ {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [inst : Fintype (Edge G)]
  [inst_1 : DecidableEq (Edge G)] {u v x y : V},
  (connectedEvent G u v).card * (connectedEvent G x y).card ≤
    2 ^ Fintype.card (Edge G) * (connectedEvent G u v ∩ connectedEvent G x y).card

#print axioms harris_kleitman_connected 'Percolation.harris_kleitman_connected' depends on axioms: [propext, Classical.choice, Quot.sound]

--% env 2

Raw input

{"cmd": "-- La monotonie, puis l'\u00e9v\u00e9nement de connexion, puis la corr\u00e9lation :\n#check @openAdj_mono           -- \u03c9\u2081 \u2286 \u03c9\u2082 \u21d2 openAdj \u03c9\u2081 \u2264 openAdj \u03c9\u2082\n#check @connected_mono         -- la connexit\u00e9 ouverte h\u00e9rite de la monotonie\n#check @connectedEvent_isUpperSet  -- {\u03c9 | u \u2194* v} est un \u00e9v\u00e9nement croissant\n#check @harris_kleitman_connected  -- \u21d2 #(u\u2194v) * #(x\u2194y) \u2264 2^|Edge G| * #((u\u2194v) \u2229 (x\u2194y))\n\n#print axioms harris_kleitman_connected", "env": 1}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "@openAdj_mono : ∀ {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [Fintype (Edge G)]\n  [DecidableEq (Edge G)] {ω₁ ω₂ : Finset (Edge G)}, ω₁ ⊆ ω₂ → openAdj G ω₁ ≤ openAdj G ω₂"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "@connected_mono : ∀ {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [Fintype (Edge G)]\n  [DecidableEq (Edge G)] {ω₁ ω₂ : Finset (Edge G)}, ω₁ ⊆ ω₂ → ConnectedIn G ω₁ ≤ ConnectedIn G ω₂"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data":
   "@connectedEvent_isUpperSet : ∀ {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [inst : Fintype (Edge G)]\n  [DecidableEq (Edge G)] {u v : V}, IsUpperSet ↑(connectedEvent G u v)"},
  {"severity": "info",
   "pos": {"line": 5, "column": 0},
   "endPos": {"line": 5, "column": 6},
   "data":
   "@harris_kleitman_connected : ∀ {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [inst : Fintype (Edge G)]\n  [inst_1 : DecidableEq (Edge G)] {u v x y : V},\n  (connectedEvent G u v).card * (connectedEvent G x y).card ≤\n    2 ^ Fintype.card (Edge G) * (connectedEvent G u v ∩ connectedEvent G x y).card"},
  {"severity": "info",
   "pos": {"line": 7, "column": 0},
   "endPos": {"line": 7, "column": 6},
   "data":
   "'Percolation.harris_kleitman_connected' depends on axioms: [propext, Classical.choice, Quot.sound]"}],
 "env": 2}

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.

4. Composantes : le point de vue « ensembles fermés »

La tranche 3 (#14897) réorganise le paysage : plutôt que les paires de sommets, les ensembles de sommets. Trois caractérisations équivalentes d’un ω-fermé :

openEdgeClosed_iff_no_cross — fermé ⟺ aucune arête ouverte ne sort de A ;
openEdgeClosed_iff_contains_components — fermé ⟺ union de composantes ouvertes ;
et la composante Component G ω v est ω-fermé (component_closed), maximale pour cette propriété parmi les ensembles contenant v (component_iff_connected).

-- La composante comme plus grand ω-fermé contenant son sommet :
#check @component_self                        -- v ∈ Component ω v
#check @component_closed                      -- Component ω v est ω-fermé
#check @component_iff_connected               -- w ∈ Component ω v ⟺ v ↔* w
#check @mem_component_of_adj                  -- l'adjacence ouverte propage l'appartenance

-- Les deux caractérisations équivalentes du ω-fermé :
#check @openEdgeClosed_iff_no_cross
#check @openEdgeClosed_iff_contains_components

-- La composante comme plus grand ω-fermé contenant son sommet :

#check @component_self                        -- v ∈ Component ω v @component_self : ∀ {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [Fintype (Edge G)]
  [DecidableEq (Edge G)] {ω : Finset (Edge G)} (v : V), v ∈ Component G ω v

#check @component_closed                      -- Component ω v est ω-fermé @component_closed : ∀ {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [Fintype (Edge G)]
  [DecidableEq (Edge G)] {ω : Finset (Edge G)} (v : V), openEdgeClosed G ω (Component G ω v)

#check @component_iff_connected               -- w ∈ Component ω v ⟺ v ↔* w @component_iff_connected : ∀ {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [Fintype (Edge G)]
  [DecidableEq (Edge G)] {ω : Finset (Edge G)} (v w : V), w ∈ Component G ω v ↔ ConnectedIn G ω v w

#check @mem_component_of_adj                  -- l'adjacence ouverte propage l'appartenance @mem_component_of_adj : ∀ {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [Fintype (Edge G)]
  [DecidableEq (Edge G)] {ω : Finset (Edge G)} {u v : V}, openAdj G ω u v → v ∈ Component G ω u

-- Les deux caractérisations équivalentes du ω-fermé :

#check @openEdgeClosed_iff_no_cross @openEdgeClosed_iff_no_cross : ∀ {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [Fintype (Edge G)]
  [DecidableEq (Edge G)] {ω : Finset (Edge G)} (A : Set V),
  openEdgeClosed G ω A ↔ ∀ ⦃u v : V⦄, u ∈ A → v ∉ A → ¬openAdj G ω u v

#check @openEdgeClosed_iff_contains_components @openEdgeClosed_iff_contains_components : ∀ {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V)
  [Fintype (Edge G)] [DecidableEq (Edge G)] {ω : Finset (Edge G)} (A : Set V),
  openEdgeClosed G ω A ↔ ∀ ⦃u : V⦄, u ∈ A → Component G ω u ⊆ A

--% env 3

Raw input

{"cmd": "-- La composante comme plus grand \u03c9-ferm\u00e9 contenant son sommet :\n#check @component_self                        -- v \u2208 Component \u03c9 v\n#check @component_closed                      -- Component \u03c9 v est \u03c9-ferm\u00e9\n#check @component_iff_connected               -- w \u2208 Component \u03c9 v \u27fa v \u2194* w\n#check @mem_component_of_adj                  -- l'adjacence ouverte propage l'appartenance\n\n-- Les deux caract\u00e9risations \u00e9quivalentes du \u03c9-ferm\u00e9 :\n#check @openEdgeClosed_iff_no_cross\n#check @openEdgeClosed_iff_contains_components", "env": 2}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "@component_self : ∀ {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [Fintype (Edge G)]\n  [DecidableEq (Edge G)] {ω : Finset (Edge G)} (v : V), v ∈ Component G ω v"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "@component_closed : ∀ {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [Fintype (Edge G)]\n  [DecidableEq (Edge G)] {ω : Finset (Edge G)} (v : V), openEdgeClosed G ω (Component G ω v)"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data":
   "@component_iff_connected : ∀ {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [Fintype (Edge G)]\n  [DecidableEq (Edge G)] {ω : Finset (Edge G)} (v w : V), w ∈ Component G ω v ↔ ConnectedIn G ω v w"},
  {"severity": "info",
   "pos": {"line": 5, "column": 0},
   "endPos": {"line": 5, "column": 6},
   "data":
   "@mem_component_of_adj : ∀ {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [Fintype (Edge G)]\n  [DecidableEq (Edge G)] {ω : Finset (Edge G)} {u v : V}, openAdj G ω u v → v ∈ Component G ω u"},
  {"severity": "info",
   "pos": {"line": 8, "column": 0},
   "endPos": {"line": 8, "column": 6},
   "data":
   "@openEdgeClosed_iff_no_cross : ∀ {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [Fintype (Edge G)]\n  [DecidableEq (Edge G)] {ω : Finset (Edge G)} (A : Set V),\n  openEdgeClosed G ω A ↔ ∀ ⦃u v : V⦄, u ∈ A → v ∉ A → ¬openAdj G ω u v"},
  {"severity": "info",
   "pos": {"line": 9, "column": 0},
   "endPos": {"line": 9, "column": 6},
   "data":
   "@openEdgeClosed_iff_contains_components : ∀ {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V)\n  [Fintype (Edge G)] [DecidableEq (Edge G)] {ω : Finset (Edge G)} (A : Set V),\n  openEdgeClosed G ω A ↔ ∀ ⦃u : V⦄, u ∈ A → Component G ω u ⊆ A"}],
 "env": 3}

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).

5. Frontière isopérimétrique : le lemme frontière et les bornes C₃/C₄

La tranche 4 (#14907) définit la frontière finie boundary G ω A : Finset (Edge G) (les arêtes ouvertes traversantes de A) et démontre :

boundary_empty_iff_closed — ∂A = ∅ ⟺ A ω-fermé (le pont arêtes/sommets) ;
closed_eq_empty_or_univ_of_connected — le lemme isopérimétrique qualitatif : dans une configuration ω-connexe, les seuls ensembles ω-fermés sont ∅ et l’univers ;
les bornes exactes sur les graphes tests : C3_closed_iff / C4_closed_iff, puis le profil cardinal boundary_card_C3, two_le_boundary_C4, et les témoins C₄.

-- Le pont frontière ↔ fermé, et le lemme isopérimétrique qualitatif :
#check @mem_boundary_iff               -- e ∈ ∂A ⟺ arête ouverte traversante
#check @boundary_empty_iff_closed      -- ∂A = ∅ ⟺ A ω-fermé
#check @closed_eq_empty_or_univ_of_connected

-- Les caractérisations fermé/non-fermé sur les graphes tests :
#check @C3_closed_iff                  -- sur C₃ complet : fermé ⟺ A = ∅ ∨ A = univ
#check @C4_closed_iff

-- Le pont frontière ↔ fermé, et le lemme isopérimétrique qualitatif :

#check @mem_boundary_iff               -- e ∈ ∂A ⟺ arête ouverte traversante @mem_boundary_iff : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [Fintype (Edge G)]
  [inst_3 : DecidableEq (Edge G)] [inst_4 : DecidableRel G.Adj] (ω : Finset (Edge G)) (A : Finset V) (e : Edge G),
  e ∈ boundary G ω A ↔ e ∈ ω ∧ ∃ u v, ∃ (huv : G.Adj u v), u ∈ A ∧ v ∉ A ∧ e = ⟨s(u, v), ⋯⟩

#check @boundary_empty_iff_closed      -- ∂A = ∅ ⟺ A ω-fermé @boundary_empty_iff_closed : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V)
  [Fintype (Edge G)] [inst_3 : DecidableEq (Edge G)] [inst_4 : DecidableRel G.Adj] (ω : Finset (Edge G)) (A : Finset V),
  boundary G ω A = ∅ ↔ openEdgeClosed G ω ↑A

#check @closed_eq_empty_or_univ_of_connected @closed_eq_empty_or_univ_of_connected : ∀ {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V)
  [Fintype (Edge G)] [DecidableEq (Edge G)] {ω : Finset (Edge G)} (A : Set V),
  (∀ (u v : V), ConnectedIn G ω u v) → (openEdgeClosed G ω A ↔ A = Set.univ ∨ A = ∅)

-- Les caractérisations fermé/non-fermé sur les graphes tests :

#check @C3_closed_iff                  -- sur C₃ complet : fermé ⟺ A = ∅ ∨ A = univ C3_closed_iff : ∀ (A : Set (Fin 3)), openEdgeClosed C3 full3 A ↔ A = Set.univ ∨ A = ∅

#check @C4_closed_iff C4_closed_iff : ∀ (A : Set (Fin 4)), openEdgeClosed C4 full4 A ↔ A = Set.univ ∨ A = ∅

--% env 4

Raw input

{"cmd": "-- Le pont fronti\u00e8re \u2194 ferm\u00e9, et le lemme isop\u00e9rim\u00e9trique qualitatif :\n#check @mem_boundary_iff               -- e \u2208 \u2202A \u27fa ar\u00eate ouverte traversante\n#check @boundary_empty_iff_closed      -- \u2202A = \u2205 \u27fa A \u03c9-ferm\u00e9\n#check @closed_eq_empty_or_univ_of_connected\n\n-- Les caract\u00e9risations ferm\u00e9/non-ferm\u00e9 sur les graphes tests :\n#check @C3_closed_iff                  -- sur C\u2083 complet : ferm\u00e9 \u27fa A = \u2205 \u2228 A = univ\n#check @C4_closed_iff", "env": 3}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "@mem_boundary_iff : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [Fintype (Edge G)]\n  [inst_3 : DecidableEq (Edge G)] [inst_4 : DecidableRel G.Adj] (ω : Finset (Edge G)) (A : Finset V) (e : Edge G),\n  e ∈ boundary G ω A ↔ e ∈ ω ∧ ∃ u v, ∃ (huv : G.Adj u v), u ∈ A ∧ v ∉ A ∧ e = ⟨s(u, v), ⋯⟩"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "@boundary_empty_iff_closed : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V)\n  [Fintype (Edge G)] [inst_3 : DecidableEq (Edge G)] [inst_4 : DecidableRel G.Adj] (ω : Finset (Edge G)) (A : Finset V),\n  boundary G ω A = ∅ ↔ openEdgeClosed G ω ↑A"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data":
   "@closed_eq_empty_or_univ_of_connected : ∀ {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V)\n  [Fintype (Edge G)] [DecidableEq (Edge G)] {ω : Finset (Edge G)} (A : Set V),\n  (∀ (u v : V), ConnectedIn G ω u v) → (openEdgeClosed G ω A ↔ A = Set.univ ∨ A = ∅)"},
  {"severity": "info",
   "pos": {"line": 7, "column": 0},
   "endPos": {"line": 7, "column": 6},
   "data":
   "C3_closed_iff : ∀ (A : Set (Fin 3)), openEdgeClosed C3 full3 A ↔ A = Set.univ ∨ A = ∅"},
  {"severity": "info",
   "pos": {"line": 8, "column": 0},
   "endPos": {"line": 8, "column": 6},
   "data":
   "C4_closed_iff : ∀ (A : Set (Fin 4)), openEdgeClosed C4 full4 A ↔ A = Set.univ ∨ A = ∅"}],
 "env": 4}

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.

6. Le profil isopérimétrique calculé : `C₃` et `C₄` en configuration complète

Les valeurs exactes, démontrées et calculables par le kernel (décidabilité des Finset finis) :

Graphe	Partie `A`	`#∂A`
`C₃`	toute partie propre non vide	`= 2` exactement (`boundary_card_C3`)
`C₄`	singleton `{0}`	`2` (`boundary_attains_min_C4`)
`C₄`	adjacents `{0,1}`	`2` (`boundary_card_C4_adjacent`)
`C₄`	triple `{0,1,2}`	`2` (`boundary_card_C4_triple`)
`C₄`	opposés `{0,2}`	`4` (`boundary_card_C4_opposite`)

-- Le profil isopérimétrique exact, en théorèmes puis en valeurs calculées :
#check @boundary_card_C3               -- #(∂A) = 2 exactement sur C₃ (parties propres non vides)
#check @two_le_boundary_C3             -- borne universelle sur C₃
#check @two_le_boundary_C4             -- borne universelle sur C₄
#check @boundary_attains_min_C4        -- le minimum est atteint sur C₄ (témoin {0})
#check @boundary_card_C4_adjacent      -- #(∂{0,1}) = 2
#check @boundary_card_C4_triple        -- #(∂{0,1,2}) = 2
#check @boundary_card_C4_opposite      -- #(∂{0,2}) = 4  (les deux faces du carré)

-- Les mêmes valeurs, calculées par évaluation native du kernel :
#eval Fintype.card (Edge C3)                                   -- 3 arêtes au triangle
#eval (boundary C3 full3 ({0} : Finset (Fin 3))).card          -- frontière du singleton de C₃
#eval (boundary C4 full4 ({0} : Finset (Fin 4))).card          -- singleton du carré
#eval (boundary C4 full4 ({0, 1} : Finset (Fin 4))).card       -- adjacents du carré
#eval (boundary C4 full4 ({0, 1, 2} : Finset (Fin 4))).card    -- triple du carré
#eval (boundary C4 full4 ({0, 2} : Finset (Fin 4))).card       -- frontière des opposés

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.

7. Exercices

Les trois exercices suivent la convention du dépôt : l’énoncé en commentaire, la solution à décommenter puis exécuter. Tant que la solution est commentée, la cellule reste neutre (example : True := trivial) et le notebook s’exécute de bout en bout.

-- Exercice 1 : la base d'axiomes de la corrélation des connexions.
-- Décommentez et exécutez :
-- #print axioms harris_kleitman_connected

-- Indice : attendez-vous au triplet standard (propext, Classical.choice, Quot.sound)
-- et à AUCUN sorryAx — la corrélation est une preuve kernel, pas un constat numérique.

example : True := trivial    -- cellule neutre tant que la solution est commentée

-- Exercice 1 : la base d'axiomes de la corrélation des connexions.

-- Décommentez et exécutez :

-- #print axioms harris_kleitman_connected

-- Indice : attendez-vous au triplet standard (propext, Classical.choice, Quot.sound)

-- et à AUCUN sorryAx — la corrélation est une preuve kernel, pas un constat numérique.

example : True := trivial    -- cellule neutre tant que la solution est commentée

--% env 6

Raw input

{"cmd": "-- Exercice 1 : la base d'axiomes de la corr\u00e9lation des connexions.\n-- D\u00e9commentez et ex\u00e9cutez :\n-- #print axioms harris_kleitman_connected\n\n-- Indice : attendez-vous au triplet standard (propext, Classical.choice, Quot.sound)\n-- et \u00e0 AUCUN sorryAx \u2014 la corr\u00e9lation est une preuve kernel, pas un constat num\u00e9rique.\n\nexample : True := trivial    -- cellule neutre tant que la solution est comment\u00e9e", "env": 5}

Raw output

{"env": 6}

-- Exercice 2 : le profil du triangle, à la main.
-- La paire adjacente {0,1} du triangle C₃ : quelle frontière attendez-vous ?
-- Décommentez et exécutez, puis confrontez au théorème two_le_boundary_C3 :
-- #eval (boundary C3 full3 ({0, 1} : Finset (Fin 3))).card
-- #check @boundary_card_C3

-- Indice : sur le triangle complet, toute partie propre non vide a exactement 2 arêtes
-- de sortie — la borne universelle est atteinte partout (pas de paire d'opposés sur C₃).

example : True := trivial    -- cellule neutre tant que la solution est commentée

-- Exercice 2 : le profil du triangle, à la main.

-- La paire adjacente {0,1} du triangle C₃ : quelle frontière attendez-vous ?

-- Décommentez et exécutez, puis confrontez au théorème two_le_boundary_C3 :

-- #eval (boundary C3 full3 ({0, 1} : Finset (Fin 3))).card

-- #check @boundary_card_C3

-- Indice : sur le triangle complet, toute partie propre non vide a exactement 2 arêtes

-- de sortie — la borne universelle est atteinte partout (pas de paire d'opposés sur C₃).

example : True := trivial    -- cellule neutre tant que la solution est commentée

--% env 7

Raw input

{"cmd": "-- Exercice 2 : le profil du triangle, \u00e0 la main.\n-- La paire adjacente {0,1} du triangle C\u2083 : quelle fronti\u00e8re attendez-vous ?\n-- D\u00e9commentez et ex\u00e9cutez, puis confrontez au th\u00e9or\u00e8me two_le_boundary_C3 :\n-- #eval (boundary C3 full3 ({0, 1} : Finset (Fin 3))).card\n-- #check @boundary_card_C3\n\n-- Indice : sur le triangle complet, toute partie propre non vide a exactement 2 ar\u00eates\n-- de sortie \u2014 la borne universelle est atteinte partout (pas de paire d'oppos\u00e9s sur C\u2083).\n\nexample : True := trivial    -- cellule neutre tant que la solution est comment\u00e9e", "env": 6}

Raw output

{"env": 7}

-- Exercice 3 : que devient le lemme isopérimétrique en configuration complète ?
-- closed_eq_empty_or_univ_of_connected exige ω connexe ; le lake démontre que full3
-- et full4 le sont. Décommentez et exécutez :
-- #check @C3_full_connected
-- #check @C4_full_connected

-- Indice : composez mentalement les deux — sur C₄ complet, la disjonction fermé = ∅/univ
-- est bien vraie (C4_closed_iff la déduit du lemme isopérimétrique). La paire d'opposés
-- {0,2} n'est donc PAS fermée (frontière 4 ≠ 0) : c'est sur la frontière, pas sur la
-- fermeture, que la géométrie du carré s'exprime.

example : True := trivial    -- cellule neutre tant que la solution est commentée

-- Exercice 3 : que devient le lemme isopérimétrique en configuration complète ?

-- closed_eq_empty_or_univ_of_connected exige ω connexe ; le lake démontre que full3

-- et full4 le sont. Décommentez et exécutez :

-- #check @C3_full_connected

-- #check @C4_full_connected

-- Indice : composez mentalement les deux — sur C₄ complet, la disjonction fermé = ∅/univ

-- est bien vraie (C4_closed_iff la déduit du lemme isopérimétrique). La paire d'opposés

-- {0,2} n'est donc PAS fermée (frontière 4 ≠ 0) : c'est sur la frontière, pas sur la

-- fermeture, que la géométrie du carré s'exprime.

example : True := trivial    -- cellule neutre tant que la solution est commentée

--% env 8

Raw input

{"cmd": "-- Exercice 3 : que devient le lemme isop\u00e9rim\u00e9trique en configuration compl\u00e8te ?\n-- closed_eq_empty_or_univ_of_connected exige \u03c9 connexe ; le lake d\u00e9montre que full3\n-- et full4 le sont. D\u00e9commentez et ex\u00e9cutez :\n-- #check @C3_full_connected\n-- #check @C4_full_connected\n\n-- Indice : composez mentalement les deux \u2014 sur C\u2084 complet, la disjonction ferm\u00e9 = \u2205/univ\n-- est bien vraie (C4_closed_iff la d\u00e9duit du lemme isop\u00e9rim\u00e9trique). La paire d'oppos\u00e9s\n-- {0,2} n'est donc PAS ferm\u00e9e (fronti\u00e8re 4 \u2260 0) : c'est sur la fronti\u00e8re, pas sur la\n-- fermeture, que la g\u00e9om\u00e9trie du carr\u00e9 s'exprime.\n\nexample : True := trivial    -- cellule neutre tant que la solution est comment\u00e9e", "env": 7}

Raw output

{"env": 8}

Conclusion

Le lake percolation_lean livre un noyau de percolation fini et entièrement vérifié : corrélation positive des événements de connexion (Harris–Kleitman), théorie des composantes fermées, et profil isopérimétrique exact sur les graphes tests — zéro sorry, chaque preuve auditée par #print axioms (triplet standard de Mathlib seul).

Ce que le noyau ne prouve pas (encore) : le passage à la grille infinie — existence de p_c, bornes sous-critiques, unicité de la composante infinie. Chacun de ces résultats exige des outils d’analyse (couplages, injections multi-échelles) hors de portée d’un noyau fini décidable ; le tracking vit dans #14871.

Pour les preuves elles-mêmes : percolation_lean/Percolation/ — cinq modules FR et leurs miroirs EN (convention i18n #4980), build lake build 1024 jobs.

Retour au sommet

1. Le vocabulaire : configurations, arêtes ouvertes, composantes

2. Harris–Kleitman fini : la corrélation positive des événements croissants

3. Connexité croissante → la corrélation des événements de connexion

4. Composantes : le point de vue « ensembles fermés »

5. Frontière isopérimétrique : le lemme frontière et les bornes C₃/C₄

6. Le profil isopérimétrique calculé : C₃ et C₄ en configuration complète

7. Exercices

Conclusion

6. Le profil isopérimétrique calculé : `C₃` et `C₄` en configuration complète