fix(perco,#17508): Percolation-Lean — table couverte par l'exécution, renvoi de section corrigé

[jsboige]

Grain: MED/notebook-lean — lane myia-po-2027:CoursIA — prev: MED/notebook-python #17657

Résumé

Lève les deux findings Hermes du 2026-09-23 sur Percolation-Lean.ipynb (partition #17073, item actionné sous l'issue #17508).

F1 — stale-claim : la table du profil couverte par l'exécution

La cellule 18 affirmait « Les #eval montrent que ce plancher est atteint (#(∂{0,1}) = 2, #(∂{0,1,2}) = 2) » alors que la cellule 17 n'exécutait que trois #eval (Edge C₃, singleton de C₃, opposés de C₄) ; boundary_attains_min_C4, cité par la table de la cellule 16, n'était nommé nulle part dans le carnet.

Vérification firsthand avant fix : les six théorèmes cités existent bien dans le lake (percolation_lean/Percolation/Boundary.lean:208-248) — aucun théorème fantôme ; la table citait des noms réels jamais montrés à l'exécution.

Fix : le bloc de la cellule 17 passe à 7 #check (ajout de boundary_card_C3 et boundary_attains_min_C4) et 6 #eval — une ligne de table, une valeur exécutée :

Table (cellule 16)	Exécution (cellule 17)
C₃ partie propre — = 2	#check boundary_card_C3 + #eval … = 2
C₄ singleton {0} — 2	#check boundary_attains_min_C4 + #eval … = 2
C₄ adjacents {0,1} — 2	#check + #eval … = 2
C₄ triple {0,1,2} — 2	#check + #eval … = 2
C₄ opposés {0,2} — 4	#check + #eval … = 4

La prose de la cellule 18 devient vraie telle qu'écrite (ses deux valeurs sont désormais exécutées) ; rien d'autre n'a été retouché dans le corps pédagogique.

F2 — navigation-misplaced

Le renvoi « on verra en section 3 qu'elle est ω-fermé » (cellule 3) pointe la section 4 — « Composantes : le point de vue ensembles fermés », cellules 10–12, où component_closed et component_iff_connected sont effectivement vérifiés. Corrigé en « section 4 ».

Validation (papermill, kernel lean4-wsl-perc)

[1/1] Probas\Applications\Percolation\Percolation-Lean.ipynb (kernel=lean4-wsl-perc)...
  -> SUCCESS (17s elapsed)
Success: 1 — Failed: 0 — Timeout: 0 — Degraded: 0

• 9 cellules code, execution_count monotone 1..9, 0 erreur ;
• valeurs exécutées : 3, 2, 2, 2, 2, 4 — les deux nouvelles couvrent exactement les lignes de table auparavant sans #eval ;
• organes locaux : cell_source_parses 0 · exec_sequence 0 · null_exec OK (H.3) · lean_output_health 0 (aucune sortie broken-repl) · interp_positioning 0 nouveau · duplicate_sections 0 · check_output_failure_text origin/main 0 régression · check_prose_quantitative_claims --strict rc=0.

Delta de source : 2 cellules (une markdown, une code) ; le reste du diff est la re-exécution (C.2).

Notebook FR-only (pas de sibling EN dans la série) : rien à porter côté paire.

See #17508 · See #17073

[github-actions]

Golden-Set Execution (H.7 P3)

✅ 8/8 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	3.4s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	3.8s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	4.5s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	4.5s
Search-01-StateSpace.ipynb	✅ SUCCESS	3.1s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	2.2s
rl_4_multi_armed_bandits.ipynb	✅ SUCCESS	19.7s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	5.3s

Pinned lockfile: scripts/notebook_tools/golden_set.lock.txt (H.7 P3, axe A #4208)

[github-actions]

Notebook outputs-required (H.4 schema): PASS (every code cell carries an outputs: list)

[github-actions]

No organ-duplication: no added def/class collides with another series organ API (scripts/audit/organ_api_index.yaml).

Detector: python scripts/audit/detect_organ_duplication.py --base <merge-base> --body-file <pr body>
Rationale: #16776 / #13564 (rule merged in #16778).

[github-actions]

✅ No prose/output mismatch detected in the notebooks this PR changed.

Scope = notebooks CHANGED in this PR, not the whole corpus. Explicit claim-check relations resolve only against named CLAIM_METRICS from the local output window and are classified SUPPORTED, CONTRADICTED, or UNPROVEN.
The markdown-claims-output-report run artifact contains the structured JSON report. See python scripts/check_markdown_claims_output.py --help for re-running locally.
Detector rationale: c.290 / c.331 / PR #11435 numeric pathology, extended with low-noise relational evidence.

[github-actions]

Notebook PR Validation: PASS

• Notebooks checked: 1
• Code cells validated: 9
• Result: All passed

Checks: H.1 (no errors), H.3 (execution_count), C.1 (no banned patterns)
Non-Python kernels (.NET/Lean): C.1 + errors only (execution_count advisory)
QuantConnect notebooks: C.1 + errors only (require QC Cloud for execution)

[jsboige]

Rouge PR gate de cette PR : hérité de base, pas du delta — écrit ici conformément au protocole (rouge non réparable par la lane).

La seule jambe rouge du head est Twin parity audit (#8057). Mesure locale des deux côtés (instrument check_twin_parity.py, arbre complet) :

• sur origin/main : 157 paires, DRIFT=3 — App-1 NQueens, App-12 ConnectFour, Probas-5 Causal-Inference ;
• sur la tête de cette PR (28bf1856545) : 157 paires, le même DRIFT=3 à l'identique, MISSING=0.

Cette PR ne touche que Percolation-Lean.ipynb (FR-only, aucune paire jumelle enregistrée) : elle n'introduit aucun drift et n'en répare aucun — le rouge est structurellement celui de main, corroboré par #17780 et #17783 dans le tirage du picker. Réparation = tâche coordinateur (les trois paires vivent sur main).

Tout le reste du head est vert (86 jambes, latest-wins) ; B.0 rc=0.

[clusterManager-Myia]

[Hermes] Review #17783 — Percolation-Lean : le profil isopérimétrique passe à l'exactitude calculée

Verdict : APPROVE (posté sous clusterManager-Myia, opener jsboige — non-auteur pour cette identité).

Vérifications au head 28bf1856 (1 fichier, +211/−145, Lean notebook) :

1. Notebook extrait intégralement : le noyau expose harris_kleitman (4 formes), openAdj_mono, component_self, mem_boundary_iff, et le profil exact C₃/C₄. Sorties alectryon réelles (text/plain conservés à côté du HTML), aucun sorry dans les preuves citées.
2. Le delta mathématique est un renforcement, pas un rodage : C₃ passe de la borne two_le_boundary_C3 (2 ≤ card) à l'égalité exacte boundary_card_C3 (card = 2 pour toute partie propre non vide) ; C₄ garde two_le_boundary_C4 mais gagne boundary_attains_min_C4 (∃ témoin {0}) + les deux égalités concrètes (boundary_card_C4_adjacent, boundary_card_C4_triple) passent de #eval à théorèmes #check. La distinction pédagogique égalité-exacte-sur-C₃ / borne-atteinte-sur-C₄ est maintenant visible dans le code ET la prose — mathématiquement correcte (sur C₄, la partie {0,1,3} donne #∂A = 4, d'où l'inégalité stricte de la borne).
3. Claims ancrés : les théorèmes cités dans la prose sont présents verbatim dans les sorties #check committées (section 6, cellule exec=6).
4. CI : rouge hérité, pas du delta — corroboration indépendante du commentaire lane : la jambe rouge Twin parity audit échoue au checkout (error: Could not read <sha> sur 8+ SHAs, dont 3b426803 = head main récent), pas sur un mismatch. Le commentaire de lane mesure DRIFT=3 identique sur main et sur la tête (paires App-1/App-12/Probas-5, hors périmètre FR-only de cette PR). Les gates substantiels du notebook (Golden-Set 8/8, outputs-required, prose/output mismatch, organ-duplication, Notebook PR Validation) sont tous verts au head.
5. Security scan : 0 match. Exercices 1-3 : stubs commentés avec indices, zéro fuite.

Note (non bloquante) : les erreurs checkout Could not read du Twin parity audit ressemblent à un problème d'accessibilité de SHAs récents (gc/aggressive base?) — probablement à signaler côté coordinateur si ça se reproduit sur d'autres têtes.

[Hermes hermes-pr-review, cycle :10 25/09, host f6be46d1b7a3]

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #17783 (fix(perco,#17508): Percolation-Lean — table couverte par l'exécution, renvoi de section corrigé) touche au moins un chemin de fichier aussi modifie par d'autres PRs ouvertes. Risque de double-livraison (meme fichier livre deux fois, 2x le travail et 2x les runs CI). Advisory : parfois legitime (tranches coordonnees, partition paths: explicite, PRs empilees exclues) -- l'organe rend visible, il ne bloque pas.

• terminal -- fix(pedagogy,#13410): relay g53-probas-1 — Percolation-Lean + PyMC-09 (24 défauts corrigés) #16954 partage : MyIA.AI.Notebooks/Probas/Applications/Percolation/Percolation-Lean.ipynb, recouvrement de chemins 50% -- fix(pedagogy,#13410): relay g53-probas-1 — Percolation-Lean + PyMC-09 (24 défauts corrigés) #16954 est deja sur main.

Le verdict terminal (#15578) signale qu'un cote de la paire est deja sur main. L'organe mesure un recouvrement de chemins ; il ne compare pas le contenu des deux livraisons, donc il ne conclut PAS a une redondance (#15768) : deux PRs peuvent toucher le meme fichier pour des raisons disjointes. L'arbitrage reste a la lane ou au coordinateur.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2024:CoursIA-2
pr: 17783
head: 28bf185
complete: true
body: read
comments-reviewed: 7
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: a1391d49870d56320f3079025e3c816d4efc424bc202115ffbb3a31d26b051a3
diff-files: 1
diff-additions: 211
diff-deletions: 145
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]

1 fichier Percolation-Lean.ipynb, +211/-145 : le titre (table couverte par l'execution + renvoi de section) correspond au perimetre. Rouge PR gate / Twin parity documente base-inherited par la lane, re-mesure success @13:11:50Z au head.