[Probas/Lean] Formaliser le noyau fini de la percolation avant pont ICT

Contexte

Le concern utilisateur sur #14847 distingue explicitement deux jambes de maturation pour la distillation de Diskin–Easo–Radhakrishnan–Sudakov–Tassion, Supercritical sharpness of percolation (arXiv:2603.03257) : une simulation Python et une formalisation Lean, avant tout retour éventuel vers ICT.

La jambe Python est repositionnée vers la racine MyIA.AI.Notebooks/Probas/ dans #14847. Cette issue porte uniquement la jambe Lean.

Destination

Créer un lake frère de decision_theory_lean à la racine Probas :

MyIA.AI.Notebooks/Probas/percolation_lean/
notebook compagnon Lean à la racine Probas

Ce placement suit le précédent vérifié de decision_theory_lean : lake transversal visible des pistes de la série Probas. ICT ne possède actuellement aucun lake ; decision_theory_lean a un scope décisionnel distinct et ne doit pas absorber la percolation.

Acceptance bornée

Grounding Mathlib firsthand avant architecture : inventorier les primitives réellement disponibles dans la version pinée pour SimpleGraph, MeasureTheory/Probability, mesures produit Bernoulli et éventuelles inégalités FKG/Harris. Citer les modules et symboles exacts utilisés ; aucune supposition de disponibilité.
Créer un lake buildable et une paire FR/EN conforme i18n(lean): harmoniser les fichiers .lean en francais + traduction anglaise — inventaire, convention, PR pilote #4980, sans modifier un lake existant hors scope.
Formaliser sans sorry un noyau fini tractable, au minimum :
- configuration d'arêtes ouvertes sur un graphe fini ;
- relation de connexion / composante de sommet ;
- frontière d'un ensemble fini et un profil isopérimétrique fini ;
- au moins un lemme non trivial reliant connexion, composante et frontière, avec exemple calculable sur un petit cycle ou tore fini.
Ajouter un notebook Lean exécuté end-to-end, outputs réels committés, qui expose les définitions, vérifie l'exemple fini et relie explicitement ces briques à la simulation Python de feat(ict,#14834): percolation supercritique — companion ICT-28b (repositionnement suspendu #14873) #14847.
Traiter le théorème de l'article comme horizon de recherche, pas comme preuve livrée : distinguer exactement ce qui est prouvé dans le lake, ce qui est importé de Mathlib et ce qui reste hors portée. Ne pas introduire de sorry pour donner l'apparence d'une formalisation complète.
Vérifications obligatoires : lake build, python scripts/lean/count_code_sorry.py --json avant/après (distinct_code_sorry), proof-integrity sur les modules cibles si câblé, checker i18n siblings, exécution réelle du notebook Lean.
Ajouter la navigation Probas seulement après résolution des PRs ouvertes touchant MyIA.AI.Notebooks/Probas/README.md; ne pas provoquer de collision avec docs(probas,#12904): reconcile arc READMEs with the actuarial jambe (DecPyMC-8..12) #14825.
Aucun artefact catalogue généré modifié sur la branche feature.

Hors scope

preuve intégrale du théorème arXiv 2603.03257 ;
ajout direct sous ICT ;
ajout opportuniste dans decision_theory_lean ;
utilisation d'un sorry, native_decide ou axiome non déclaré pour franchir un mur de bibliothèque ;
réécriture de la jambe Python de feat(ict,#14834): percolation supercritique — companion ICT-28b (repositionnement suspendu #14873) #14847.

See #14834. See #14847.

Grain: DEEP/lean — lane myia-po-2027:CoursIA-2 — prev: MED/lean #14864

[CLAIMED] lane myia-po-2027:CoursIA-2 — paths: MyIA.AI.Notebooks/Probas/percolation_lean/**, MyIA.AI.Notebooks/Probas/Percolation-Lean.ipynb

Intention : construire la jambe Lean séparée de la distillation percolation, bornée au noyau fini sans sorry, après inventaire firsthand des primitives Mathlib. Le README Probas reste exclu tant que #14825 le touche ; navigation en follow-up séquencé.

Concern: Attention, les notebooks à la racine de Proba sont la première chose qu'un apprenant voit en chargeant le répertoire dans github. Or les notebooks de progression pédagogique vivent dans des sous-répertoires et ceux qui restent ici comme celui sur Pyro sont un peu ceux qui n'ont pas été rangés ailleurs. Ca porte un risque de confusion, et ça devrait sans doute être adressé dans une issue dédiée. Peut-être que nommer le répertoire "PyMC" n'était pas très judicieux à la base, ou bien il faudrait prévoir d'autres répertoires. Bref, c'est à étudier.

Au passage, je note que le readme principal de Proba a vieilli et mérite une MAJ

[ADJOINT] Le concern utilisateur est fondé : la visibilité de la racine Probas dans GitHub rend prématurée la destination annoncée pour le notebook et le lake. Le précédent decision_theory_lean prouve qu'un lake transversal existe à cet endroit ; il ne prouve pas que cette architecture est claire pour un apprenant ni qu'elle doit être étendue.

[RELEASED] lane myia-po-2027:CoursIA-2 — paths: MyIA.AI.Notebooks/Probas/percolation_lean/**, MyIA.AI.Notebooks/Probas/Percolation-Lean.ipynb

Le premier jalon technique reste utile et peut avancer sans création de fichiers : inventaire firsthand des modules/symboles Mathlib (SimpleGraph, probabilité/mesures produit Bernoulli, FKG/Harris si présents) et proposition d'un noyau fini sans sorry. En revanche, aucun lake/notebook n'est créé à la racine tant que #14873 n'a pas recommandé une taxonomie et une destination explicites.

Le vieillissement du README principal est inclus dans #14873, séquencé avec la PR #14825 pour ne pas écraser son audit actuel. Cette issue #14871 reste la source du scope mathématique ; #14873 tranche uniquement le placement et le parcours apprenant.

Jalon 1 (read-only) — inventaire Mathlib + proposition de noyau fini

Vérifié firsthand au tag v4.32.1 (pin Mathlib de decision_theory_lean, lean-toolchain = leanprover/lean4:v4.32.1). Aucun fichier/lake créé ici — destination/taxonomie suspendue à #14873.

AVAILABLE — modules (chemins exacts au tag v4.32.1)

SimpleGraph — Mathlib/Combinatorics/SimpleGraph/ :

Basic.lean — SimpleGraph (structure, Adj, neighborSet)
Finsubgraph.lean — SimpleGraph.Finsubgraph
Connectivity/Connected.lean — Reachable, Preconnected, reachable_is_equivalence, reachable_iff_reflTransGen, Reachable.refl/symm/trans
Connectivity/Subgraph.lean — SimpleGraph.Subgraph
Connectivity/Finite.lean, Connectivity/WalkCounting.lean, Connectivity/EdgeConnectivity.lean
Maps.lean, Prod.lean, Finite.lean, DeleteEdges.lean

Mesures / probabilité — Mathlib/MeasureTheory/, Mathlib/Probability/ :

MeasureTheory/Measure/MeasureSpace.lean (l'espace de mesure)
Probability/ProductMeasure.lean, Probability/ConditionalProbability.lean, Probability/Independence/, Probability/IdentDistribIndep.lean

Bernoulli / produit de Bernoulli — Mathlib/Probability/Distributions/ :

Bernoulli.lean — bernoulliMeasure (mesure de probabilité sur Bool), bernoulliMeasure_zero/one/self_eq_dirac, map_bernoulliMeasure, integral_bernoulliMeasure
Binomial.lean — comptage de tirages Bernoulli indépendants

FKG / Harris — version finie (set family) :

Combinatorics/SetFamily/HarrisKleitman.lean — IsLowerSet.le_card_inter_finset, IsUpperSet.card_inter_le_finset (inégalité de Harris–Kleitman sur familles finies de Finset)
Combinatorics/SetFamily/FourFunctions.lean — théorème des quatre fonctions (Ahlswede–Daykin, généralise FKG)
Combinatorics/SetFamily/Kleitman.lean

MISSING / à la frontière

FKG mesure-théorique (inégalité FKG sur un espace probabilisé produit, événements croissants, p-mesure) : aucun module dédié au tag v4.32.1. Code-search sur le repo: seul Combinatorics/SetFamily/FourFunctions.lean et NumberTheory/MaricaSchoenheim.lean mentionnent « FKG »; pas de FKG.lean ni Harris.lean mesure-théorique. La version finie (Harris–Kleitman, IsLowerSet/IsUpperSet sur Finset) est disponible — c'est celle applicable au noyau fini. La version produit-mesure (sharpness arXiv) reste bien un horizon non prouvé, cohérent avec l'acceptance.

Proposition de noyau fini (sans sorry)

Sur un graphe fini G = (V, E) :

Configuration d'arêtes ouvertes : ω : E → Bool (ou un SimpleGraph.Subgraph / G.Finsubgraph), chaque arête ouverte indépendamment avec probabilité p.
Connexion / composante : SimpleGraph.Reachable / Preconnected; reachable_is_equivalence fournit la partition en composantes ouvertes (la classe de v = composante contenant v dans ω).
Frontière / profil isopérimétrique fini : pour une composante C, boundary(C) = neighborSet(C) \ C (à définir au-dessus de neighborSet/Finsubgraph); isopérimétrique fini = majorant de |boundary(C)|.
Mesure produit : bernoulliMeasure p par arête, produit fini via Probability/ProductMeasure.lean; probabilité d'un événement = mesure du sous-ensemble de configurations.
≥1 lemme non trivial : monotonie en p — la probabilité que s soit relié à t (ou qu'une composante relie deux bords) est croissante en p. C'est exactement la propriété couverte par la version finie de Harris–Kleitman (événements croissants sur un poset fini, IsLowerSet/IsUpperSet sur Finset), formulable sans mesure produit.
Exemple petit : cycle C_n / tore T_{k×k} — probabilité de connexion entre deux sommets, vérification du lemme de monotonie, borne isopérimétrique simple (composante de taille ≤ r ⇒ frontière bornée).

Écriture (à faire après #14873)

Lake percolation_lean calqué sur decision_theory_lean (paire FR/EN #4980, globs #[Percolation.*, Percolation_en]), noyau fini sans sorry. La formalisation effective attend la décision de #14873 sur le placement et le parcours apprenant.

Grain: DEEP/lean — lane myia-po-2027:CoursIA-2 — prev: MED/lean #14864

[CLAIMED] lane myia-po-2027:CoursIA-2 — paths: MyIA.AI.Notebooks/Probas/Applications/Percolation/percolation_lean/**

L’arbitrage ai-01 sur #14873 a levé le gate de destination : le lake Lean peut désormais être créé immédiatement sous Applications/Percolation/percolation_lean/, sans attendre T0.

Le jalon read-only du 2026-09-06T10:24:54Z devient le grounding d’implémentation : paire FR/EN conforme #4980, noyau fini buildable sans sorry/native_decide/axiome non déclaré, exemple calculable, lake build, compte distinct_code_sorry, checker i18n et proof-integrity si la cible est câblée. Le théorème infini reste explicitement un horizon non prouvé.

Le scope est volontairement disjoint de la jambe Python de #14847 : aucun notebook Python, aucun README parent et aucun requirements.txt ne sont revendiqués ici. Aucun artefact catalogue ne doit être modifié.

fix(lean,#14871): borner Harris-Kleitman au cas uniforme p=1/2 (docst…

[Probas/Lean] Noyau fini percolation — inegalite FKG finie (Harris-Kl…

[INFO] tranche 3 livres : PR #14897 (stackee sur #14896 / feature/percolation-lean-connectivity). Module Composantes (composante connexe ouverte, openEdgeClosed, lemme connexion-composante-frontiere). Verification : lake build SUCCESS 848 jobs, distinct_code_sorry=0, axioms [propext, Classical.choice, Quot.sound] FR+EN, i18n byte-identical OK. A retargeter vers main apres merge de #14896.

feat(lean,#14871): exemple calculable sur le triangle C3 (acceptation 3)

feat(lean,#14871): exercer ReflTransGen.trans sur le carre C4 (exempl…

feat(lean,#14871): noyau percolation — évènement de connexité croissa…

Grain: DEEP/notebook-lean — lane myia-po-2027:CoursIA-2 — prev: DEEP/lean #14897

[CLAIMED] lane myia-po-2027:CoursIA-2 — paths: MyIA.AI.Notebooks/Probas/Applications/Percolation/percolation_lean/Percolation/Boundary*.lean, MyIA.AI.Notebooks/Probas/Applications/Percolation/Percolation-Lean.ipynb

[ADJOINT][DISPATCH] Deep queue séquencée, sans attente entre les deux étapes :

Frontière/profil fini — compléter l’acceptation 3 que feat(lean,#14871): composantes et frontiere du noyau percolation (tranche 3) #14897 ne clôt pas encore : définir un objet de frontière fini et un profil isopérimétrique fini dans une paire FR/EN, puis prouver au moins une borne non triviale sur C3/C4. Ne pas requalifier openEdgeClosed_iff_no_cross seul en profil isopérimétrique.
Notebook Lean exécuté — réparer d’abord le kernel, puis créer le compagnon sous le chemin revendiqué. Diagnostic canonique : python scripts/lean/setup_lean4_all.py --check-wrapper, puis python scripts/notebook_tools/notebook_tools.py execute <notebook> avec kernel Lean explicite selon le kernelspec réparé. Si lean4-wsl est utilisé, le kernelspec doit pointer vers ~/.lean4-kernel-wrapper.py v5; ne pas revenir au wrapper bash obsolète. Aucun output fabriqué, aucun contournement Python qui affiche du Lean comme texte.

Sorties exigées pour chaque tranche : lake build, distinct_code_sorry, axiomes, checker i18n; pour le notebook, exécution end-to-end, execution_count non-null, outputs réels et zéro output error. Le notebook doit distinguer prouvé/importé/hors portée et relier explicitement le noyau fini au notebook Python, sans prétendre prouver le théorème infini.

Le scope est disjoint de #14902 : ne pas toucher Percolation-Supercritique.ipynb, le README local, requirements.txt, le README ICT ni les artefacts catalogue.

feat(lean,#14871): composantes et frontiere du noyau percolation (tra…

feat(lean,#14871): exemple calculable sur le triangle C3 (acceptation 3)

feat(lean,#14871): frontiere isoperimetrique finie sur C3 et C4 (tran…

[RELEASED] lane myia-po-2027:CoursIA-2 — paths: MyIA.AI.Notebooks/Probas/Applications/Percolation/percolation_lean/Percolation/Boundary*.lean, MyIA.AI.Notebooks/Probas/Applications/Percolation/Percolation-Lean.ipynb

Grain: DEEP/notebook-lean — lane myia-po-2027:CoursIA-2 — prev: DEEP/lean #14907

[CLAIMED] lane myia-po-2027:CoursIA-2 — paths: MyIA.AI.Notebooks/Probas/Applications/Percolation/Percolation-Lean.ipynb

#14907 est fusionnée sur main au head livré a84d4c97572f : le scope Boundary*.lean est donc libéré. Le reste actif de l’acceptation 4 est désormais isolé au notebook Lean exécuté.

Procédure Stop & Repair : exécuter d’abord l’entrée canonique complète python scripts/lean/setup_lean4_all.py sans --check-wrapper, puis re-sonder le vrai lake percolation_lean. --check-wrapper seul et un résultat sain du stub_fallback ne prouvent pas le REPL du lake. Créer ensuite le notebook avec le vrai kernel Lean, l’exécuter end-to-end et committer uniquement ses outputs réels. Aucun contournement Python affichant du Lean comme texte, aucune sortie hand-éditée.

Diagnostic env (acceptance 4 — notebook-Lean) : BLOCAGE KERNEL verifie firsthand

L'execution end-to-end de Percolation-Lean.ipynb est environnement-bloquee sur cette machine au niveau du kernel Lean, independamment du lake Percolation. Diagnostic exact, controle positif, sans wrapper check seul :

Kernel lean4-wsl = REPL_STDLIB_BROKEN (signature Kernel lean4-wsl casse sur ai-01 : le binaire repl du PATH n'a plus de stdlib (#eval 2+2 -> Unknown constant OfNat) #11874). cwd kernel = ~/gtl-build (hardcode kernel.json). Sonde directe #eval 2 + 2 dans ~/gtl-build :
```
{"messages":[{"severity":"error","data":"Unknown constant `OfNat`"},
             {"severity":"error","data":"unexpected token '+'; expected command"}],"env":0}
```
Le controle positif le plus elementaire echoue => binaire repl compile pour une toolchain != toolchain resolu par cwd. Kernel inutilisable, pas seulement pour Percolation : pour tout code Lean.
import Mathlib = silencieux ({"env": 0}) dans ~/gtl-build : Mathlib n'y a que 53 oleans (pas warm) => import muet (ENV_ID_MUTE).
Aucun Mathlib Linux-ABI warm dans WSL : ~/lean-projects/ ne contient que le stub notebook_context ; find ~ -path "*mathlib/.lake/build/lib/lean/Mathlib" => 0. Toolchains elan WSL : v4.32.1 / v4.33.1 / v4.34.0-rc2.
Cote Windows natif : pas de repl (seulement lean.exe, lake.exe, ...) => lake env repl => "file not found". Le chemin natif est authentiquement indisponible pour la REPL.

Verdict SOTA : RECOVERABLE-MACHINE. Il faut une machine dont le WSL porte (a) une Mathlib Linux-ABI warm pour la toolchain resolue, et (b) un binaire repl aligne sur cette toolchain (ex. miroir lakeroot/SC/erc20_lean de discrepancy_lean sur la machine SC/po-2025, cf memo lean-wsl-miroir-sc-vs-repl). Sur une telle machine, l'execution du notebook devient possible.

Aucun notebook n'est committe : sans execution reelle, c.2/H.3 et regle 6 (secrets-hygiene / sota-not-workaround §H) interdisent de committer des sorties fabriquees ou hand-editées. Le lake source (Percolation.lean + modules) et la reparation du bord C4 (#14907) sont dans le worktree D:/dev/CoursIA-percolation-notebook ; seul l'acceptance 4 (execution notebook) reste ouvert, bloque par l'environnement ci-dessus.

Feat: notebook Percolation-Lean — compagnon exécutable du lake percol…

[Vérification candidate-delivered — lane myia-po-2027:CoursIA]

Vérification firsthand de l'acceptation sur l'artefact main courant : tranches 1-4 (#14892 / #14896 / #14897 / #14907), notebook compagnon #14927 et câblage proof-integrity #14917 tous mergés ; 0 sorry réel (count_code_sorry.py → percolation_lean : distinct_code_sorry 0), compagnon exécuté (9/9 cellules, 0 erreur, outputs réels), 6 paires FR/EN.

Seul point restant : l'acceptance 7 (navigation Probas) — condition #14825 levée depuis le 2026-09-06 mais jamais exécutée. Le résidu est livré en #15405 (2 READMEs, +18/−1, marqueur catalogue byte-identique) : au merge, l'acceptation est intégrale (la clôture est portée par cette PR).

Observation pour mémoire de famille : le placement effectif est Applications/Percolation/ (aux côtés de la jambe Python #14847), non la racine Probas du body initial — état de fait des tranches mergées, documenté tel quel par la navigation.

docs(probas,#14871): audit fichier-entier du README serie -- prose re…

docs(probas,#14871): navigation Percolation + audit fichier-entier du…

docs(probas,#14871): segmenter le paragraphe-mur de l'intro serie (33…

fix(collision,#15768): le verdict terminal enonce un fait, plus une c…

FERMEE — verification firsthand contre origin/main @ 0dcc80c1fb7b748646b500672ef4df1873ba8013.

Livree par #14892, #14896, #14897, #14907, #14927 et #15405 (toutes MERGED). Les sept acceptances sont couvertes : grounding Mathlib inventorie, percolation_lean/ buildable avec ses modules FR et EN (Basic, Boundary, Components, Connectivity, Examples), noyau fini a distinct_code_sorry=0 — le compte reel, pas un grep -c sorry — lake build SUCCESS, proof-integrity cable via #14917, notebook Lean 9/9 cellules 0 erreur, theoreme maintenu comme horizon et non comme acquis, et la navigation Probas reconciliee par #15405.

Navigation Menu

Repository navigation

[Probas/Lean] Formaliser le noyau fini de la percolation avant pont ICT #14871

Contexte

Destination

Acceptance bornée

Hors scope

Jalon 1 (read-only) — inventaire Mathlib + proposition de noyau fini

AVAILABLE — modules (chemins exacts au tag v4.32.1)

MISSING / à la frontière

Proposition de noyau fini (sans sorry)

Écriture (à faire après #14873)

5 remaining items

Diagnostic env (acceptance 4 — notebook-Lean) : BLOCAGE KERNEL verifie firsthand

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

[Probas/Lean] Formaliser le noyau fini de la percolation avant pont ICT #14871

Description

Contexte

Destination

Acceptance bornée

Hors scope

Activity

jsboigeEpita commented on Sep 6, 2026

jsboige commented on Sep 6, 2026

jsboige commented on Sep 6, 2026

jsboige commented on Sep 6, 2026

jsboige commented on Sep 6, 2026

Jalon 1 (read-only) — inventaire Mathlib + proposition de noyau fini

AVAILABLE — modules (chemins exacts au tag v4.32.1)

MISSING / à la frontière

Proposition de noyau fini (sans sorry)

Écriture (à faire après #14873)

jsboige commented on Sep 6, 2026

jsboige commented on Sep 6, 2026

jsboigeEpita commented on Sep 6, 2026

5 remaining items

jsboige commented on Sep 6, 2026

jsboige commented on Sep 6, 2026

Diagnostic env (acceptance 4 — notebook-Lean) : BLOCAGE KERNEL verifie firsthand

jsboige commented on Sep 9, 2026

myia-ai-01 commented on Sep 20, 2026

Metadata

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Issue actions