[myia-ai-01]

Grain: MED/harness — lane myia-ai-01:CoursIA — prev: Concern user #24179 / #24183

Ce que fait cette PR

Elle écrit le texte de référence de la doctrine des lakes Lean, que le user a validée le 2026-11-02 en réponse à ma question de gouvernance (registre, Q160) :

« a) Je valide b) OK poure redescendre c) On le garde avec la notice qui doit exister, et on documente la comparaison des preuves comme tu as proposé »

• docs/reference/lean-lakes-doctrine.md (nouveau) :
  • pourquoi une doctrine : deux mouvements contradictoires, et les deux raisons de la mutualisation tombées ;
  • les quatre règles R1-R4 ;
  • la précondition Mathlib et les exceptions nommées ;
  • un tableau « appliquer la doctrine », geste par geste ;
  • les organes ;
  • l'historique.
• docs/lean/README.md : une ligne d'index (section « Organisation des lakes »). CLAUDE.md pointe déjà docs/lean/.

Ce qui n'est pas dans cette PR. Le pointeur d'une ligne dans CLAUDE.md attend #23813 (lane myia-po-2024:CoursIA), qui touche aussi ce fichier ; il fera l'objet d'une PR séparée après son merge.

Gouvernance (CLAUDE.md §A)

Ce changement est normatif : il retire un motif de fusion, pose R1-R4 et renverse #4365 pour game_theory_lean. Le sign-off user est la réponse citée ci-dessus. Le même accord a déjà été reporté dans l'en-tête de #4362 (titre et body réécrits) et dans #24183.

Vérifications

Contrôle	Résultat
Matrice CI	scripts/lean/ci_lakes.json : 33 entrées (mesuré à la base)
Organes cités	lean_material_map.py, setup_shared_mathlib.ps1, count_code_sorry.py et lean-ci-matrix.yml existent à la base
check_prose_quantitative_claims.py --diff origin/main...HEAD	[OK] aucun compteur quantitatif en prose
Claim	[CLAIMED-AMEND] sur #4362, scope = les deux fichiers ; check_lane_claim.py rc=0

See #4362
See #24183

🤖 Generated with Claude Code

[github-actions]

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

• GENRE-MISMATCH : declared genre != genre infere depuis les chemins du diff
• GENRE-UNKNOWN : le genre canonise `harness` est hors enumeration close -- trou d'adjacence G-VAR-3, requalifier le genre dans le body (Un genre hors énumération passe silencieusement : canonicalize_genre le rend tel quel, aucun signal, adjacence G-VAR-3 inatteignable #12158)

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.