Fix(lean,#19506): Angel bibliographie alignee sur le gisement (Gacs, Bibliographie IA)

[jsboige]

Grain: LIGHT/lean -- lane myia-ai-01:CoursIA-2 -- prev: DEEP/tooling #19926

Cible

Fix #19506 : Conway/Angel.lean (FR) et Conway/Angel_en.lean (EN) citent la bibliographie sous des formes qui ne correspondent pas au gisement reel. Le reste de la review NanoClaw de #18004 (2026-09-27), reporte sur #17666 qui se ferme aujourd'hui sur son perimetre principal.

Cas mesure

Verifie sur main le 2026-10-06 :

• Angel.lean ligne 16 : cite 2007 - Gács - The Angel Wins.pdf (avec accent). Fichier reel = 2007 - Gacs - The Angel Wins.pdf (sans accent).
• Angel.lean ligne 20 : meme correction (chemin de l'archive).
• Angel_en.lean ligne 18 : cite Bibliography IA\GameTheory\ (EN). Dossier reel = Bibliographie IA\GameTheory\ (le nom du dossier est en francais dans le gisement, ce n'est pas une prose a traduire).
• Angel_en.lean ligne 117 : meme correction (deuxieme chemin de l'archive).

La ligne 136 d'Angel.lean utilisait deja la bonne forme (corrigee lors d'un passage anterieur) ; les lignes 12, 19, 120, 135, 137, et les lignes 11, 132, 133, 134 d'Angel_en.lean mentionnent Gács dans la prose (nom de l'auteur, accent legitime) ou utilisent deja Gacs/Bibliographie IA.

Fix

Quatre substitutions s/ sur deux fichiers, portees par la convention i18n sibling pair (#4980) : les enonces de theoremes, les tactiques Lean, les noms de lemmes, les references Mathlib restent en anglais dans les deux fichiers ; seules les docstrings et les commentaires -- different. Mes modifs sont toutes dans des commentaires (les chemins d'archive), pas dans le code.

Compte de sorry

Distinct code sorry = 0 dans conway_lean (les mentions dans la doc ne sont pas des sorry reels). Le fix ne touche aucun token de code : le compte reste a 0.

Verification

• python scripts/lean/count_code_sorry.py --lake conway_lean : TOTAL 0 (avant = 0, apres = 0).
• git diff --stat : 2 fichiers, +4/-4 lignes, scope minimal.
• Convention i18n : les modifications sont dans des commentaires uniquement (FR/EN) -- le coeur du lake (theoremes, tactiques, namespace) reste byte-identique entre Angel.lean et Angel_en.lean.

Fichiers

• MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Angel.lean : 2 substitutions dans des commentaires.
• MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Angel_en.lean : 2 substitutions dans des commentaires.

Refs

• fix(lean,#17666): Angel -- aligner les noms de la bibliographie sur le gisement (Gacs, Bibliographie IA) #19506 (issue, fix bibliographie Angel)
• feat(lean,#1453): archiver biblio Angel + sorry assumé INTRINSIC k≥2 dans Angel.lean #17666 (EPIC parente, ferme aujourd'hui sur son perimetre principal)
• fix(lean,#17949,#17666,#1453): Angel.lean/en siblings -- 5 chemins canoniques GDrive au bloc LITTERATURE #18004 (review NanoClaw fondatrice du constat)
• i18n(lean): harmoniser les fichiers .lean en francais + traduction anglaise — inventaire, convention, PR pilote #4980 (convention i18n sibling pair)
• c.298 (PR fix(merge_ready,#19002): PR empilee via convention body sur base=main #19921 fix fix(gate): le dossier READY et merge_ready ignorent la branche de base -- une PR empilee peut etre mergee dans une branche morte #19002), c.300 (PR Fix(check_adjoint,#19869): --emit pre-remplit supersedes/supersedes-why sur READY-sur-BLOCKED meme tete #19926 fix fix(coordination): --emit ne produit pas supersedes/supersedes-why -- un READY sur un BLOCKED de la meme lane part puis est refuse #19869)

Co-Authored-By: Claude Haiku 4.5 (1M context) noreply@anthropic.com

[github-actions]

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

• TIER-INFLATION : declared LIGHT << effective LIGHT-genre (tally : declared=1 genre=10 cap=6)
• GENRE-RUN : run consecutif d'un genre LIGHT (voir signals.runs dans le log du job)
• CAP-EXCEEDED-BY-GENRE : light_genre > cap partage G-VAR-2 (tally : declared=1 genre=10 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.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 19927
head: 916e532
complete: true
body: read
comments-reviewed: 1
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: a80efee5a55fc766f4967f1b95ac78a539146a27a0cb85bd41ee0a691c887085
diff-files: 2
diff-additions: 4
diff-deletions: 4
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 19927
organ-rc: 0
[/ADJOINT PREFLIGHT]