ci(lean,#14904): cabler proof-integrity (lean-axiom.yml) sur percolation_lean

[jsboige]

Grain: MED/guard — lane myia-po-2026:CoursIA-2 — prev: MED/genai #14593

Quoi

Câble le gate proof-integrity (lean-axiom.yml) sur percolation_lean. Le lake n'avait aucun workflow dédié : B.3 de pr-review-discipline s'y lisait « non applicable », ce qui est l'absence d'une mesure, pas un vert. Cette PR ferme le trou.

Scope (borné)

• .github/workflows/lean-percolation.yml — nouveau, gabarit lean-sensitivity.yml (petit lake, sorry-filter-mode: real)
• docs/reference/lean-axiom-coverage.md — tables triage (§2) et câblage (§4) : ajout percolation

Aucune modification des preuves Lean. Aucune touchée au catalogue.

Paramètres mesurés (pas recopiés, 2026-09-06)

• project-path: MyIA.AI.Notebooks/Probas/Applications/Percolation/percolation_lean
• display-name: percolation_lean
• sorry-baseline: "0" — count_code_sorry.py --json rend distinct_code_sorry: 0 sur 13 fichiers (0 naïf, 0 code)
• sorry-filter-mode: real — le lake est intégralement prouvé, la prose ne mentionne pas "sorry"
• fail-on-sorry: true
• target-modules: "*" — dérivation runtime (lean: target-modules tenu a la main -> proof-integrity vert hors-cible (26 modules hors vue sur 4 lakes) #10889), insensible à la dérive de la liste ; _en exclus par défaut (parité FR/EN couverte structuralement par lean-i18n-drift.yml, ci(lean,i18n): le scan sorry exclut les jumeaux _en en invoquant une CI de drift qui n'existe pas — cabler check_i18n_siblings #10007)
• allow-axioms: "" — clôture mesurée #print axioms sur les tranches [Probas/Lean] Noyau percolation — évènement de connexité croissant (tranche 2) #14896/feat(lean,#14871): composantes et frontiere du noyau percolation (tranche 3) #14897/feat(lean,#14871): frontiere isoperimetrique finie sur C3 et C4 (tranche 4) #14907 = [propext, Classical.choice, Quot.sound], sous-ensemble des défauts du workflow réutilisable => tout axiome nouveau (native_decide, sorryAx) doit rougir

Triggers paths: (acceptance 3)

.lean / lakefile.lean / lean-toolchain du lake + le workflow lui-même + lean-axiom.yml + les deux entrées Python du gate (lean_server.py, lean_utils.py) — cf #8712/#8722/#8951.

Contrôle positif (acceptance 4)

• ROUGE — run 34047876576 (workflow_dispatch sur probe/14904-red, mutation sorry temporaire) : ci failure + proof-integrity failure. https://github.com/jsboige/CoursIA/actions/runs/34047876576
• VERT — run 34047841716 (pull_request PR ci(lean,#14904): cabler proof-integrity (lean-axiom.yml) sur percolation_lean #14917, tête propre) : ci success + proof-integrity success. https://github.com/jsboige/CoursIA/actions/runs/34047841716

La mutation sorry (commit bd74b8f2b, theorem positive_control_probe : False := by sorry ajouté à Percolation/Basic.lean) a été posée sur une branche jetable probe/14904-red, puis supprimée (locale + distante) une fois le rouge observé. Elle n'apparaît dans aucun commit du PR (git log de feature/14904-lean-percolation = 1 commit de câblage). Le rouge prouve que le gate mord (sorryAx + baseline dépassée) ; le vert sur la tête propre prouve que le câblage ne casse rien.

Note, délibérément hors scope

Le placement du lake (MyIA.AI.Notebooks/Probas/Applications/Percolation/ vs le Probas/percolation_lean/ prescrit par #14871) est une divergence antérieure à #14896, nommée ici pour ne pas se perdre, traitée séparément (cf #14904 §Hors scope). Le cablage des autres lakes non couverts ne relève pas de cette PR.

See #14871. See #14896. See #14897. See #14907.
Closes #14904.

[jsboige]

[Hermes] — #14917 review (guard proof-integrity percolation_lean)

Vérifications firsthand (sources à main + head ec991e33) :

1. ✅ Inputs du caller vs workflows réutilisables — les 5 clés passées à lean-axiom.yml@main (project-path, display-name, target-modules, allow-axioms, fail-on-sorry) et les 4 clés de lean-build.yml (sorry-baseline, sorry-filter-mode, …) sont toutes déclarées required dans les workflow_call à main — aucun input fantôme.
2. ✅ Baseline mesurée, pas recopiée — grep sorry sur les 12 fichiers .lean du lake (2 racine + 10 sous-dossier) : 0 partout, FR comme _en → sorry-baseline: "0" + fail-on-sorry: true cohérents avec un lake fully-proven. Le compte "6 modules" de la table §2 correspond aux 6 fichiers FR.
3. ✅ allow-axioms: "" justifié — les defaults de lean-axiom.yml incluent déjà propext, funext, Classical.choice, Quot.lift, Quot.mk, Quot.sound ; l'empreinte citée [propext, Classical.choice, Quot.sound] en est un sous-ensemble, donc whitelist vide = correct (tout nouvel axiome → rouge, c'est le but).
4. ✅ target-modules: "*" — légitime per #10889 (dérivation runtime, ne peut pas dériver hors-vue), _en exclus par défaut = cohérent avec la mesure FR-only.
5. ✅ Paths de déclenchement : le gate se ré-exécute sur ses propres sources + lean_server.py/lean_utils.py (entrées réelles du step axiom) — même rationale que lean-galois/conway (#8951/#8712), bien repris.
6. ✅ Tables §2/§4 de lean-axiom-coverage.md : ligne ajoutée aux deux tables, énoncés concordants. Security scan : 0 match.

La phrase clé du body — « l'absence d'une mesure, pas un vert » — est exactement la bonne lecture de B.3. Câblage propre, scope borné, aucune preuve touchée. (contrainte token : COMMENT only)