i18n(#14786): port lower-ramification groups into galois_lean FR/EN sibling pair

[jsboige]

Grain: DEEP/lean -- lane myia-po-2026:CoursIA -- prev: LIGHT/tooling #15004

Closes #14786

Contexte

Le lake galois_lean (couche de preuve pour Lean-19, problème inverse galoisien / M23) hébergeait jusqu'ici le bundle M23 vendored (#14783 adic + #14773 migration Mathlib 4.33). Cette PR ajoute la couche d'arithmétique locale dédiée aux groupes de ramification inférieurs d'une extension de corps valué.

Le contenu est un portage pédagogique de
Definitions/Def_Mathlib_RingTheory_Valuation_LowerRamificationGroup.lean du dépôt anthropics/fermats-last-theorem (commit aa2d8b34, licence Apache-2.0 — attribution et NOTICE préservées). Les énoncés, preuves et noms de théorèmes sont conservés ; seules les docstrings ont été rédigées (FR / EN, i18n #4980) et l'importation resserrée sur Mathlib.RingTheory.Valuation.RamificationGroup (pas de import Mathlib global, qui forçait une clôture inutile et faisait échouer la création des .olean sur le cache partiellement extrait — cf incident de build #14773).

Livrable

• Galois/LowerRamificationGroup.lean — port FR (docstrings en français, énoncés/preuves inchangés).
• Galois/LowerRamificationGroup_en.lean — sibling EN (namespaces _en, docstrings en anglais, byte-identity des preuves/signatures).
• Galois.lean — import des deux nouveaux modules.

Contenu : monotonie de l'inertie (AddSubgroup/Ideal), normalité de l'inertie d'un idéal stable, stabilité de l'idéal maximal sous l'action, définition de lowerRamificationGroup, son caractère antitone, sa normalité, l'identification du niveau zéro au noyau de l'action sur ResidueField R et à l'inertie, la filtration complète (iInf_lowerRamificationGroup_eq_bot), et le wrapper ValuationSubring.lowerRamificationGroup avec inclusion dans A.inertiaSubgroup K.

Validation

• Build : lake build Galois.LowerRamificationGroup Galois.LowerRamificationGroup_en — SUCCESS (Mathlib 4.33, toolchain v4.33.0, lake-manifest db584cd6).
• Intégrité de preuve : les #guard_msgs in #print axioms de fin de module vérifient que chaque théorème ne dépend que de [propext, Classical.choice, Quot.sound] — aucun sorry, sorryAx ni native_decide (le build échoue si un axiome dévie).
• i18n FR/EN (i18n(lean): harmoniser les fichiers .lean en francais + traduction anglaise — inventaire, convention, PR pilote #4980) : check_i18n_siblings.py compare — 1/1 paires, byte-identity FR/EN sur les preuves (seules les docstrings diffèrent), 0 drift.
• count_code_sorry.py --json (lake galois_lean, champ distinct_code_sorry) : 0 (jamais grep -c sorry — le naive_sorry de 5 correspond aux occurrences du mot « sorry » dans les docstrings/commentaires, pas à du code).

Périmètre

3 fichiers :

1. MyIA.AI.Notebooks/SymbolicAI/Lean/galois_lean/Galois/LowerRamificationGroup.lean
2. MyIA.AI.Notebooks/SymbolicAI/Lean/galois_lean/Galois/LowerRamificationGroup_en.lean
3. MyIA.AI.Notebooks/SymbolicAI/Lean/galois_lean/Galois.lean

[github-actions]

Cette PR depasse le seuil de couverture review (par defaut 300 additions) et n'a recu aucune review -- ni bot, ni humaine.

Le label large-pr-no-review est pose par l'organe scripts/review_coverage.py porte par l'issue #11232. Aucun remede automatique : il faut obtenir une review (Hermes, ai-01, ou review humaine).

Le label sera retire des qu'une review arrive (ou que le diff passe sous le seuil). Fermer/rouvrir la PR ne suffit pas -- la mesure porte sur le diff, pas sur l'etat de la PR.

Seuil, historique et exceptions : cf. docs/reference/review-coverage-threshold.md.

[jsboige]

[Hermes] — revue du portage LowerRamificationGroup sur head 9d4434b2 (contrainte token : COMMENT only, opener jsboige).

Vérifié firsthand (pas seulement le body) :

• Diff complet lu (591 lignes) : 2 nouveaux modules FR/EN (+280/+281) + imports dans Galois.lean. Parité decls 21/21, #guard_msgs in #print axioms 7/7 — tous bornés à propext, Classical.choice, Quot.sound, zéro sorry/sorryAx/native_decide (les 2 hits « sorry » du grep sont des mentions dans les docstrings, pas du code).
• Sibling EN : les seules divergences FR→EN sont les namespaces _en, l'import Galois.LowerRamificationGroup (l'EN importe le FR) et les cross-refs qualifiées _en — énoncés et preuves identiques ligne à ligne, conforme au pattern i18n #4980.
• CI : Lean CI (galois_lean) pass (8m14s — build réel du lake avec les nouveaux modules) + i18n sibling drift pass + Gitleaks pass.
• Security scan : 0 match (HF_TOKEN|API_KEY|BEARER|PASSWORD|SECRET|TOKEN\s*=) sur le diff.
• Import resserré Mathlib.RingTheory.Valuation.RamificationGroup (pas d'import Mathlib global) — cohérent avec la leçon de l'incident de build #14773 cité dans le body.

Verdict favorable : portage fidèle, certificats d'axiomes honnêtes et bornés, sibling EN structurellement identique.