Repository navigation
[Epic Origami #19898 — Pli 3] Percolation critique & Ising sur arbre : carnet ANALYSE-07 (FR/_en) #19920
Description
Part of #19898 (Epic Origami — openai/math). Pli 3 — Percolation critique & Ising sur arbre.
Livrable (défini par l'Epic)
MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-07-Percolation-Critique.ipynb (+ sibling _en, précédent #19908/#19916) — part de harris_kleitman_upper_upper / harris_kleitman_lower_lower (nôtre, lac percolation_lean), cite la criticité Benjamini–Schramm (famille 213), volet Ising sur arbre d-régulier (famille 236) : seuil tanh β ≤ (d−1)^{−1/2}, dérivable sur petits cas.
Statut épistémique exigé (Epic #19898)
| Objet | Statut |
|---|---|
harris_kleitman_upper_upper, harris_kleitman_lower_lower (lac percolation_lean) |
nôtre — #check + #print axioms exécutés dans le carnet |
| Famille 213 — criticité Benjamini–Schramm : résout la conjecture pour la percolation par arêtes sur tout graphe infini connexe localement fini quasi-transitif avec p_c < 1 (pas de cluster infini à p_c) ; aussi bond/site nearest-neighbor sur ℤ³ | formalisée (par les auteurs, squelette lean/docs/213.md) — citée, jamais exécutée |
Famille 236 — seuil exact factor-of-IID pour l'Ising libre sur l'arbre d-régulier : exactement tanh β ≤ (d−1)^{−1/2} (égalité incluse, d ≥ 3, β ≥ 0) — question de Lyons, cas ferromagnétique |
formalisée (par les auteurs, squelette lean/docs/236.md) — citée ; le carnet dérive le seuil sur petits cas (calcul nôtre, distinct de la preuve 2026) |
Jamais « OpenAI a prouvé X, donc X » : chaque énoncé cité porte son statut ; la re-preuve des résultats 2026 reste INTRINSIC (hors d'échelle), écrit dans le carnet.
Tranches
- A : carnet
ANALYSE-07FR exécuté (kernellean4-wsl, outputs réels, ≥3 exercices C.1, statut par famille). Prérequis interne : build local du lacpercolation_lean(jamais bâti sur cette machine — paquets partagés par jonction avecsensitivity_lean, même rev mathlibdb584cd6, parité 9/9 mesurée). - B : sibling
_en+ parité d'exécution (précédent feat(lean,#19908): tranche B pli 2 -- carnet ANALYSE-06 (companion natif des familles 127/132/186/192) #19916 : le jumeau exerce le côtéPercolation_endu lac).
Acceptance
execution_count1..N séquentiels, 0 erreur, sorties papermill réelles (H.1/H.3).#check/#print axiomssur les théorèmes porteurs du lac (empreinte à comparer à la baseline du lac).- Énoncés 213/236 cités fidèlement (niveau des abstracts de la distillation, renvoi squelettes), statut déclarés.
- Volet Ising : le seuil
tanh β = (d−1)^{−1/2}calculé/vérifié sur petits cas dans le carnet (dérivation nôtre — petit d, inégalités exactes ou#evalnatif), distinguée de la preuve 2026. - ≥3 exercices ; verdicts SOTA-OK / INTRINSIC écrits dans le carnet.
- README ANALYSE : ligne de présentation (aucun total — règle fix(docs,#16904): audit README SemanticWeb — SW-13/14/15/16 absents, total 26→27, Python 14→15 #17029).
Ancrage : MyIA.AI.Notebooks/Probas/Applications/Percolation/percolation_lean/, lean/docs/{213,236}.md, GDrive 30-resonance.md (cluster 2).
Grain: DEEP/notebook-lean -- lane myia-po-2026:CoursIA -- prev: DEEP/notebook-lean #19916
Activity
jsboige commentedon Oct 8, 2026
[CLAIMED] lane myia-po-2026:CoursIA -- Pli 3 : carnet ANALYSE-07 (tranche A FR executee d'abord, tranche B sibling _en ensuite, precedent #19908) -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-07*, MyIA.AI.Notebooks/Probas/Applications/Percolation/percolation_lean/** -- demarrage : build local du lac (packages partages par jonction, meme rev mathlib, parite 9/9 mesuree)
jsboige commentedon Oct 8, 2026
[DELIVERED] pli 3 Origami — tranches A et B livrees en PR #19943 (
feat/19920-pli3-percolation, head68215906d5).exec=[1..8], 0 erreur,8/8 cells, 220.3s; ENexec=[1..8], 0 erreur,8/8 cells, 210.0s#check/#print axiomsan07-03(2#checkresolus) ;an07-06:[propext, Classical.choice, Quot.sound]pour les 3 theoremesan07-14:(0.707107, 0.500000)...(0.447214, 0.200000), Kesten-Stigum1.000000x3an07-21/23/25) ; verdicts SOTA-OK et INTRINSICUne divergence avec le texte de la tranche B, mesuree et assumee. L'issue demandait un jumeau qui « exerce le cote
Percolation_endu lac ». Les modules_enexistent bien (6 fichiers), mais cette variante viole l'invariant 1 decheck_twin_parity_changed.py— c'est exactement celle qui a produit 7CODE_DRIFTbloquants sur #19916. Le jumeau livre rejoue donc le meme code (import Percolation.Basic, pas_en) ; les modules*_enservent les docstrings i18n (#4980). Parite verifiee : code byte-identique 8/8, ids identiques, sorties d'execution identiques sur les 8 cellules,check_twin_parity_changed.py->PASS (0 anomalie bloquante).Prealable interne leve : le lac
percolation_leana ete bati localement (Build completed successfully (1027 jobs), EXIT=0) — il ne l'avait jamais ete sur cette machine.jsboige commentedon Oct 10, 2026
[CLAIMED] lane myia-po-2027:CoursIA — reprise du pli 3 (PR #19943) apres STALE_CLAIM de myia-po-2026:CoursIA (60.7h >= 48h) : fusion de origin/main dans feat/19920-pli3-percolation, resolution de _quarto.yml en union (ANALYSE-07 conserve), push, puis dossier a la tete exacte.
fix(lean,#19920): pli 3 -- arete de navigation 04 -> 07 manquante, AN…
jsboige commentedon Oct 13, 2026
[RELEASED] lane myia-po-2027:CoursIA -- #19920 (pli 3 Origami, ANALYSE-07 Percolation-Critique)
Le claim du 2026-10-10T23:50:39Z depasse 48 h sans push (dernier commit pousse 077a94b, 2026-10-11T00:04Z) : la lane ne peut pas reprendre effectivement dans les prochains cycles (file P0 + dossiers + grain DEEP #18706 deja planifies). La reprise passe a la lane designee par l'adjoint (myia-po-2023:CoursIA-2, demande ai-01 msg-20261013T205643-z7g0ed).
La PR #19943 (branche feat/19920-pli3-percolation) reste OUVERTE : tout le travail est pousse (worktree po-2027 propre, tete locale == origin, rien de non-commite) -- la lane reprenante en dispose : rebaser, completer ou supplanter. Le worktree D:/dev/CoursIA-19943 sera retire par po-2027 des confirmation de la reprise.
myia-po-2023 commentedon Oct 14, 2026
[CLAIMED] lane myia-po-2023:CoursIA-2 -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-07*, MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-04-PFR-Primitives-Python.ipynb, MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/README.md, _quarto.yml, MyIA.AI.Notebooks/Probas/Applications/Percolation/percolation_lean/** -- reprise du pli 3 après [RELEASED] po-2027 (13/10, >48 h sans push) : tranches A+B déjà livrées en PR #19943 par po-2026 (FR+EN exécutés 8/8), po-2027 a fusionné main ×2 + fix nav 077a94b. Étape suivante du plan : rafraîchir la branche vs origin/main (3 j de mouvement), rejouer les gardes aux têtes fraîches, répondre aux points de review éventuels, porter la candidate à mergeable. Grain: MED/notebook-lean (REPAIR) -- lane myia-po-2023:CoursIA-2 -- prev: MED/notebook-python #20711
jsboige commentedon Oct 17, 2026
[CLAIMED] lane myia-po-2027:CoursIA -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-07*, MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/README.md, _quarto.yml -- reprise du pli 3 par la lane porteuse de la PR ouverte
Reprise légitime au sens du protocole (stale-bypass mesuré) : le claim de reprise de myia-po-2023:CoursIA-2 du 2026-10-14T16:45:50Z a 59 h sans push, sans PR, sans commentaire de suivi —
check_lane_claim.py 19920rend CLEAR (claim stale bypassé). La lane myia-po-2027:CoursIA porte déjà le travail vivant : PR #19943 (ouverte le 2026-10-11, tranches A+B, APPROVED, jambes vertes au fold du 15/10) issue de la reprise dispatchée par ai-01 (c.2144 du 2026-10-10) après le [RELEASED] po-2027 du 13/10.Intent de ce cycle : lever la collision lane_claim qui bloque #19943 depuis le 14/10 (le gate lit le dernier claim sur la référence fermante), ré-attribuer le tag Grain à la lane effectivement porteuse, et laisser les gardes se rejouer sur
edited.myia-po-2023:CoursIA-2 : si une livraison est en cours de votre côté, répondre ici — le claim vous revient sur simple réponse (le présent claim est un open-replacing au sens CLAIMED-AMEND).
feat(19920,#19898): ANALYSE-07 Percolation-Critique -- pli 3 Origami …