[CI/Lean] Cabler lean-axiom.yml sur percolation_lean — B.3 non applicable par absence de workflow #14904

Contexte — d'ou vient cette issue

Reserve posee par NanoClaw en review de #14896 ([Probas/Lean] Noyau percolation — evenement de connexite croissant (tranche 2)), verbatim :

proof-integrity n'est pas cable sur ce lake — la seule preuve de compilation est lane-locale (lake build 846 jobs + #print axioms revendiques dans le body, non rejouables depuis mon conteneur node-only).

Le reviewer a explicitement defere la decision de merge au coordinateur. Cette issue est ouverte avant ce merge, pour que la reserve soit levee par un suivi nomme et non par l'ecoulement du temps (CLAUDE.md B.0 : une issue de suivi ne leve une remarque que si elle est ouverte et nommee AVANT le merge).

Mesure firsthand

$ grep -ln "lean-axiom" .github/workflows/*.yml | grep -v "lean-axiom.yml"
lean-asymmetric-information.yml
lean-conway.yml
lean-galois.yml
lean-grothendieck.yml
lean-hecke.yml
lean-knot.yml
lean-mimo.yml
lean-sensitivity.yml
lean-social-choice.yml

-> 9 workflows appellent lean-axiom.yml

$ ls .github/workflows/ | grep -i perco
(aucune sortie — AUCUN workflow percolation)

Le lake percolation_lean n'a aucun workflow, ni lean-*.yml dedie ni entree dans un workflow existant. Le critere B.3 de pr-review-discipline s'y lit donc « non applicable » — cas (a) de la regle : le job n'est pas cable sur le lake de la PR.

Pourquoi ce n'est pas cosmetique

B.3 « n/a » n'est pas un vert : c'est l'absence de mesure. Concretement, sur percolation_lean aujourd'hui :

• aucune verification que les preuves ne reposent pas sur sorryAx (le sorry transitif, qu'aucun grep -c sorry ne voit) ;
• aucune verification anti-native_decide (reduction par le noyau natif sans preuve — vide le theoreme de son contenu) ;
• aucun cliquet sur l'apparition d'un axiome nouveau ;
• la seule preuve de compilation est celle que l'auteur revendique dans le corps de sa PR, non rejouable par un reviewer.

C'est exactement la classe de defaut que le gate de niveau 3 existe pour attraper, et le lake y est actuellement aveugle.

Ce qui a laisse le trou — et pourquoi c'etait legitime

L'acceptance §6 de #14871 (issue mere du lake) dit :

lake build, python scripts/lean/count_code_sorry.py --json avant/apres (distinct_code_sorry), proof-integrity sur les modules cibles si cable, checker i18n siblings, execution reelle du notebook Lean.

La clause « si cable » etait correcte a la redaction : on ne demande pas a la tranche qui cree un lake de cabler aussi sa CI. Elle a fait son travail — et elle laisse precisement ce reste. C'est ce reste que cette issue porte.

Acceptance

1. Creer .github/workflows/lean-percolation.yml sur le gabarit de lean-sensitivity.yml (le plus proche : petit lake, sorry-filter-mode: real), avec les deux jobs :
   • ci: -> lean-build.yml (sorry-baseline mesure, sorry-filter-mode: real) ;
   • proof-integrity: -> lean-axiom.yml.
2. Parametres mesures (a re-mesurer au moment de l'implementation, ne pas recopier) :
   • project-path: MyIA.AI.Notebooks/Probas/Applications/Percolation/percolation_lean
   • display-name: percolation_lean
   • sorry-baseline: "0" — mesure du jour : count_code_sorry.py --json rend distinct_code_sorry: 0 sur 5 fichiers
   • fail-on-sorry: true — le lake est integralement prouve, le cliquet doit mordre des le premier sorry
   • target-modules: "*" — liste derivee du parcours du lake a l'execution, donc insensible a la derive (lean: target-modules tenu a la main -> proof-integrity vert hors-cible (26 modules hors vue sur 4 lakes) #10889) ; c'est ce qui evite le defaut (b) de B.3 (un vert hors-cible indiscernable d'un vert sur cible)
   • allow-axioms: "" — les defauts du workflow reutilisable suffisent ; tout axiome nouveau doit rougir, c'est toute la valeur du gate
3. Declencheurs paths: incluant, outre les **.lean / lakefile.lean / lean-toolchain du lake : le workflow lui-meme, lean-axiom.yml, et les deux entrees Python du gate (agent_tests/lean_server.py, agent_tests/prover/lean_utils.py) — cf fix(knot,#8604): remove misleading hwell placeholder field, wf extrinsic sole notion #8712 / proof-integrity: l'enumerateur de declarations fabrique des constantes inconnues (namespaces + prose de docstring) #8722 / ci(secu,#8949): harden GITHUB_TOKEN scope on Lean CI workflows — contents:read on 22 callers + drop dead pull-requests:write #8951, dont lean-sensitivity.yml porte deja la justification en commentaire.
4. Controle positif obligatoire avant de declarer le cablage acquis : ne pas se contenter d'un vert. Introduire temporairement un sorry (ou un native_decide) dans un module du lake, verifier que le job rougit, puis retirer. Un gate qui n'a jamais ete vu rougir n'est pas un gate mesure — cf verify-before-claiming et la lecon « un motif de detection se valide par ses faux negatifs ».
5. Mettre a jour docs/reference/lean-axiom-coverage.md : le triage y liste 7 lakes et ignore percolation.

Hors scope

• Toute modification des preuves du lake — cette issue ne touche que la CI.
• Le placement du lake : [Probas/Lean] Formaliser le noyau fini de la percolation avant pont ICT #14871 prescrivait MyIA.AI.Notebooks/Probas/percolation_lean/, la tranche 1 a livre sous MyIA.AI.Notebooks/Probas/Applications/Percolation/percolation_lean/. La divergence est anterieure a [Probas/Lean] Noyau percolation — évènement de connexité croissant (tranche 2) #14896 et se tranche separement — la nommer ici pour qu'elle ne se perde pas, pas pour la traiter.
• Le cablage des autres lakes non couverts : cette issue porte percolation seul.

See #14871. See #14896. See #14847.