ci(lean,#13751): geometry_lean migre dans la matrice lean-ci -- 23e lake, wrapper supprime

[jsboige]

Grain: LIGHT/tooling — lane myia-po-2026:CoursIA — prev: MED/tooling #19311

See #13751 (tranche workflows — 2e lake apres le pilote percolation #18996 ; residuel : 11 per-lake reels)

ci(lean,#13751): geometry_lean migre dans la matrice lean-ci -- 23e lake, wrapper supprime

Summary

Tranche workflows de #13751 (axe « 12 per-lake restants ») : le dispatcher dedie lean-geometry.yml (69 lignes) migre dans lean-ci-matrix.yml. Lake suivant de la consolidation (22 lakes au manifeste avant celle-ci : sudoku, kelly, ... serre100, percolation) -- meme recette mecanique que le pilote, lake par lake.

Diff (4 fichiers, +25/-74)

• scripts/lean/ci_lakes.json (+13) : entree geometry -- sorry-baseline: "0", sorry-filter-mode: real, axiom-target-modules: "*" (parametres reportes a l'identique du wrapper ; le manifeste est la source unique de verite du dispatcher). allow-axioms vide + fail-on-sorry: true du wrapper = valeurs par defaut de la matrice, aucun champ requis.
• .github/workflows/lean-ci-matrix.yml (+12) : bloc paths geometry_lean ajoute aux DEUX unions (push + pull_request), avec commentaire d'heritage.
• .github/workflows/lean-geometry.yml (-74) : wrapper supprime -- la regle du manifeste interdit les deux declencheurs a la fois (double build).
• MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/README.md : lien CI recalle de lean-geometry.yml vers la matrice + entree du manifeste (grep post-suppression : 0 reference residuelle au wrapper hors commentaires d'heritage).

Couverture preservee (rien perdu)

Ce que le wrapper faisait	Couvert par
ci via lean-build.yml (build + sorry ratchet real, baseline 0)	job lean-matrix -> lean-build.yml@./ mode matrice
proof-integrity via lean-axiom.yml (target-modules "*", allow-axioms vide, fail-on-sorry true)	lean-build.yml l.369-377 : if: matrix.axiom-target-modules != '' -> action lean-axiom (le manifeste porte "*")
self-cover (lean_server.py, lean_utils.py, lean-axiom.yml)	deja presents au on.paths du dispatcher (self-cover B.3 herite des wrappers supprimes)
workflow_dispatch manuel	workflow_dispatch du dispatcher = tous les lakes du manifeste (self-cover)

Preuves

• Garde anti-drift locale : python scripts/ci/check_lake_matrix_paths.py -> lake-matrix OK : 23 lake(s) couvert(s), union push/pr coherente avec le manifeste, aucun double declencheur.
• Manifeste : splice textuel, JSON re-valide (23 lakes), LF byte-identique sur les lignes inchangees (+13 exactement, comme le pilote).
• Pre-commit passe sur les 4 fichiers.

Perimetre: .github/workflows/lean-ci-matrix.yml, .github/workflows/lean-geometry.yml, scripts/lean/ci_lakes.json, MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/README.md.

🤖 Generated with Claude Code

[github-actions]

G-VAR-2/3 GENRE signals (advisory, non bloquant, #10020).
La lane `myia-po-2026:CoursIA` voit ces signaux actifs sur les mergees du jour (UTC 2026-10-05) :

• TIER-INFLATION : declared LIGHT << effective LIGHT-genre (tally : declared=3 genre=12 cap=6)
• CAP-EXCEEDED-BY-GENRE : light_genre > cap partage G-VAR-2 (tally : declared=3 genre=12 cap=6)
• NOTE ([variation] Le label est lane-agregat mais PR-attache : le merge-gate peut HOLD le grain de CONTENU qui remedie au motif #10341) : la PR courante est de classe CONTENU (non LIGHT-genre) et ne contribue pas au motif ci-dessus -- les labels agregees ne sont PAS poses sur cette PR (le merge-gate ne doit pas la HOLD pour ce motif ; le coupable est parmi les grains META de la lane).

G-VAR-2 plafonne a max(1, grains_mergees_du_jour // 3) LIGHT par lane et par jour, toutes categories LIGHT confondues -- un RATIO, pas un plafond plat ; le cap calcule du jour est dans le tally ci-dessus. G-VAR-3 interdit deux genres LIGHT consecutifs. Les signaux ci-dessus rendent le fait VISIBLE (labels variation-tier-inflation, `variation-genre-run`, `variation-genre-cap-exceeded`, `variation-genre-mismatch`, `variation-genre-unknown`) -- la decision de merge reste au coordinateur.

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #19313 (ci(lean,#13751): geometry_lean migre dans la matrice lean-ci -- 23e lake, wrapper supprime) 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 -- ci(lean,#13751): percolation_lean migre dans la matrice lean-ci — 22e lake, wrapper supprimé #18996 partage : .github/workflows/lean-ci-matrix.yml, scripts/lean/ci_lakes.json, recouvrement de chemins 50% -- ci(lean,#13751): percolation_lean migre dans la matrice lean-ci — 22e lake, wrapper supprimé #18996 est deja sur main. (issues communes : [consolidation] Navigation transversale : racine <=12 entrees, 23 workflows lean -> matrice, hubs (V3) #13751) (issues communes : [consolidation] Navigation transversale : racine <=12 entrees, 23 workflows lean -> matrice, hubs (V3) #13751)

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-2026:CoursIA-3
pr: 19313
head: bd12fa9
complete: true
body: read
comments-reviewed: 2
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: b8410118048e0210d11bd3a47ee76a771795c18c771c0591ebb868832f429326
diff-files: 4
diff-additions: 29
diff-deletions: 72
checks: latest-wins-green
b0: clear
scope: pass
domain: not-applicable
verdict: READY
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 19313
organ-rc: 0
[/ADJOINT PREFLIGHT]