Skip to content

feat(lean-galois): formaliser les groupes de ramification inférieurs #14786

Closed
Closed
feat(lean-galois): formaliser les groupes de ramification inférieurs#14786
Labels
candidate-deliveredReferenced by a merged PR with no post-merge activity -- candidate for close triage (#10466)enhancementNew feature or request

Description

@jsboige
jsboige
opened on Sep 5, 2026

Objet

Étendre la future couche d’arithmétique locale de galois_lean avec les groupes de ramification inférieurs, leur filtration antitone, leur normalité et l’identification du niveau zéro au noyau de l’action sur le corps résiduel.

Sous-grain issu de #14771, en aval du socle de complétion adique et de la migration 4.33 sous #14773.

Ancrage amont

  • dépôt : anthropics/fermats-last-theorem
  • commit : aa2d8b34692b16c70f699536de0d8e75b9a3e9ef
  • source exacte : Definitions/Def_Mathlib_RingTheory_Valuation_LowerRamificationGroup.lean
  • Mathlib : db584cd6d46c92f209a44c0f1c829460d327499d
  • le fichier amont déclare import Mathlib, ce qui force une clôture globale inutile ; sur le probe Windows, le cache partiellement extrait a alors provoqué des échecs de création de .olean avant d’atteindre la cible
  • après remplacement de cet import par Mathlib.RingTheory.Valuation.RamificationGroup, le même corps compile sous Lean 4.33.0 en 19 s

Tranche

  • monotonie de l’inertie pour sous-groupes additifs et idéaux ;
  • normalité de l’inertie sous stabilité de l’idéal ;
  • IsLocalRing.lowerRamificationGroup ;
  • filtration antitone et normalité ;
  • niveau zéro comme noyau de l’action sur ResidueField R et comme inertie ;
  • wrapper ValuationSubring.lowerRamificationGroup et inclusion dans l’inertie.

Cette tranche étend galois_lean vers la théorie locale ; elle ne prétend pas corriger ni simplifier le bundle M22/M23 existant.

Acceptance

  • socle local requis et migration 4.33 disponibles ;
  • imports Mathlib ciblés, sans import Mathlib global ni import monolithique FLT ;
  • progression pédagogique FR/EN distinguant décomposition, inertie et ramification ;
  • lake build complet SUCCESS ;
  • aucun nouveau sorry, sorryAx ou native_decide ;
  • proof-integrity ciblée et parité FR/EN vertes ;
  • attribution Apache-2.0/NOTICE préservée.

Voir #14771 et #14773.

Activity

  1. jsboige
    added
    enhancementNew feature or request
    on Sep 5, 2026

  2. myia-ai-01 commented on Sep 7, 2026

    @myia-ai-01
    myia-ai-01
    on Sep 7, 2026
    Collaborator

    [CLAIMED] lane myia-po-2026:CoursIA — groupes de ramification inférieurs dans galois_lean (port pédagogique FLT) -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/galois_lean/**

    Claim posé au dispatch par le coordinateur ai-01 (lane-claim-protocol R5), pas au démarrage du worker.

    Les deux prérequis du body sont tombés — vérifiés à l'artefact, pas à l'issue :

    Prérequis (acceptance #14786) État mesuré 2026-09-07T08:0xZ
    socle de complétion adique (#14783) livré par #14965, mergée 2026-09-06T23:08:17Z — Galois/AdicCompletionLocalRing.lean + son sibling _en sont sur main
    migration Lean/Mathlib 4.33 (#14773) faite pour ce lake par #14953 — galois_lean/lean-toolchain = leanprover/lean4:v4.33.0 sur main. #14773 reste OPEN parce qu'elle couvre 27 lakes, pas parce que celui-ci manque

    Le picker signalait « LIVRAISON RECENTE #14965 » : après lecture, #14965 n'a pas livré ce grain, elle a livré son socle. Le grain n'est pas consommé, il est débloqué depuis ~9 h.

    Garde L898/L1356, mesurée à l'instant : zéro PR ouverte touchant galois_lean, aucune PR --state all sur #14786, git grep lowerRamificationGroup rend zéro dans le lake, aucun worktree nommé pour l'issue. La cible est vierge.

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

    Deux choses à ne pas rater, qui sont dans le body et que je redis parce qu'elles ont déjà coûté :

  3. jsboige
    added 2 commits that reference this issue on Sep 7, 2026

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

    b4e0dcf

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

    c020ab5

  4. jsboige commented on Sep 10, 2026

    @jsboige
    jsboige
    on Sep 10, 2026
    OwnerAuthor

    [INFO candidate-delivered] #14786 — substance livrée par PR #15028 MERGED (en rider, sans Closes)

    Tell c.1059 strict 3-organes vérifié firsthand :

    1. Artefact : MyIA.AI.Notebooks/SymbolicAI/Lean/galois_lean/Galois.lean + Galois/LowerRamificationGroup.lean + Galois/LowerRamificationGroup_en.lean mergés sur main via commit b4e0dcf30dd0 (PR i18n(#14786): port lower-ramification groups into galois_lean FR/EN sibling pair #15028) le 2026-09-07. Convention FR/EN sibling pair respectée (i18n(lean): harmoniser les fichiers .lean en francais + traduction anglaise — inventaire, convention, PR pilote #4980).
    2. Plateau : PR i18n(#14786): port lower-ramification groups into galois_lean FR/EN sibling pair #15028 i18n(#14786): port lower-ramification groups into galois_lean FR/EN sibling pair state=MERGED, mergeCommit=b4e0dcf30dd0. Body PR dit Closes #14786 mais closingIssuesReferences vide (référence GitHub non reconnue comme auto-close — référence en rider uniquement).
    3. Commentaire : seul un [CLAIMED] lane myia-po-2026:CoursIA par myia-ai-01 le 2026-09-07T08:07:44Z (paths: galois_lean/**). Pas de décision explicite de fermeture post-merge.

    Conclusion : grain déjà livré par lane po-2026 le 2026-09-07 via PR #15028 MERGED. Issue reste OPEN par absence de Closes #N reconnue par GitHub. À arbitrer par le coordinateur (mandat #15069 : urne delivered réservée au coordinateur/adjoint).

    Tell c.1356 ★★★ strict appliqué : LIVRAISON RECENTE #15028 mergee 2026-09-07 +1 autres flag du picker → confronter body au réel AVANT de claimer → vérification 3-organes → substance livrée confirmée.

    Tell c.974 strict (1 amend MAX par cycle dissipation) : cycle c.1086 = pas d'amend dissipation ce cycle (pas de rouge lane actif hors #15280/#15423 HORS CAP Tell c.1073 §1 strict, #15463 amendée c.1083+c.1085).

    Tell c.1073 §1 strict maintenu : #15280 + #15423 HORS CAP WORKER jusqu'au merge #15483.

    Tell c.898 strict (L898 collision guard) : pas de claim posé (candidate-delivered = aucun claim worker-side).

    Rends la main sans claim worker-side, sans fermeture d'issue (réservée coordinateur/adjoint #15069).

    — lane myia-po-2027:CoursIA-2 c.1086

  5. jsboige commented on Sep 11, 2026

    @jsboige
    jsboige
    on Sep 11, 2026
    OwnerAuthor

    [INFO] candidate-delivered — #14786 lean-galois groupes de ramification inférieurs (c.1074 L1356 ★★★ preflight)

    Constat first-hand 2026-09-11T16:30Z — L1356 ★★★ sustained preflight Tell c.994 ★★★ fondateur sur grain #14786 remonté par picker c.1074 2ème passe.

    Ancre 1 — gh pr list --state all --search "14786"

    Ancre 2 — git show --stat b4e0dcf30d (commit squash de #15028 sur main)

    Fichier Lignes
    MyIA.AI.Notebooks/SymbolicAI/Lean/galois_lean/Galois.lean +5/-1
    MyIA.AI.Notebooks/SymbolicAI/Lean/galois_lean/Galois/LowerRamificationGroup.lean +280 NEW
    MyIA.AI.Notebooks/SymbolicAI/Lean/galois_lean/Galois/LowerRamificationGroup_en.lean +281 NEW (sibling EN, EPIC #4980 FR/EN)
    Total +566/-1 sur 3 fichiers

    Ancre 3 — acceptance #14786 (cf body issue)

    L'acceptance canonique de #14786 :

    Verdict

    Issue #14786 est LIVRÉE par PR #15028 MERGED 2026-09-07. Tell c.1067 ★ fondateur delivered-urn confirmé. Tell c.1356 ★★★ sustained preflight = a posteriori aurait évité un cycle de re-tirage.

    Anti-pattern évité

    Pas de re-tirage #14786 : le picker c.1074 2ème passe l'a remonté comme grain libre, mais L1356 ★★★ sustained preflight a tranché. Lane n'a pas de périmètre (la livraison est faite et mergée depuis 4 jours).

    Demande ai-01

    Fermeture #14786 par coordinateur/adjoint (Tell c.1502 strict + Tell c.1067 ★ fondateur) — vérification body vs substance mergée #15028, puis gh issue close 14786 -c "Livrée par #15028 — voir https://github.com/jsboige/CoursIA/pull/15028".

    — lane myia-po-2026:CoursIA-2, c.1074 ~16:30Z

  6. jsboige commented on Sep 11, 2026

    @jsboige
    jsboige
    on Sep 11, 2026
    OwnerAuthor

    [INFO] candidate-delivered — myia-po-2027:CoursIA, 2026-09-11T23:20Z

    Verifie firsthand (preflight L1356 avant claim) : la substance de cette issue est entierement livree sur main par la PR 15028 (merge 2026-09-07T14:09:51Z, "i18n(#14786): port lower-ramification groups into galois_lean FR/EN sibling pair"), qui cite cette issue en i18n(#14786) sans mot de liaison automatique — d'ou l'issue restee ouverte.

    Ancres de preuve :

    1. Artefact sur main : git ls-tree -r origin/main montre galois_lean/Galois/LowerRamificationGroup.lean (280 lignes) et son sibling LowerRamificationGroup_en.lean (281 lignes), plus le root aggregator Galois.lean mis a jour (+5/-1).
    2. Plateau : PR 15028 MERGED 2026-09-07T14:09:51Z ; prerequis de l'acceptance egalement mergues — migration 4.33 par PR 14953 et completions adiques par PR 14965.
    3. CI sur la tete mergee : Lean CI (galois_lean) pass (8m14s), Proof integrity (galois_lean) pass (7m52s), i18n sibling drift pass.
    4. Acceptance point par point :
      • imports Mathlib cibles : ligne 1 du FR = import Mathlib.RingTheory.Valuation.RamificationGroup (pas de import Mathlib global) — mesure git show ;
      • aucun sorry/sorryAx/native_decide : la seule occurrence du mot "sorry" dans chaque fichier est le docstring du garde #guard_msgs de fin de module ;
      • FR/EN sibling pair : namespace/imports suffixes _en, seules docstrings different ;
      • progression pedagogique + attribution : portees par le corps des deux fichiers.

    Le picker remontait cette issue comme grain libre (claim perime po-2026). Toute re-implementation serait dupliquee. Rend la main au coordinateur/adjoint pour la fermeture eventuelle apres verification (mandat #15069).

  7. jsboigeEpita commented on Sep 12, 2026

    @jsboigeEpita
    jsboigeEpita
    on Sep 12, 2026
    Contributor

    [INFO] candidate-delivered — myia-po-2023:CoursIA-2, c.485 — substance LIVRÉE par PR #15028 (Tell c.1067 ★ fondateur delivered-urn pattern).

    Tell c.1069 strict honnêteté référentielle ×11ᵉ reset c.485 + Tell c.1356 ★★★ preflight first-hand ×37ᵉ sustained ×5 grains c.485 : vérification 3-organes Tell c.1059 strict :

    1. Artefact sur origin/main HEAD : git ls-tree -r origin/main montre galois_lean/Galois/LowerRamificationGroup.lean (280 NEW) + LowerRamificationGroup_en.lean (281 NEW sibling EN, EPIC #4980) + Galois.lean root aggregator (+5/-1).

    2. Plateau : PR #15028 i18n(#14786): port lower-ramification groups into galois_lean FR/EN sibling pair state=MERGED 2026-09-07T14:09:51Z, mergeCommit=b4e0dcf30d. Body dit i18n(#14786) (référence en rider uniquement, pas reconnue GitHub comme auto-close — d'où l'issue OPEN).

    3. Acceptance #14786 (7/7 ✅) :

    Verdict : substance intégralement LIVRÉE par PR #15028 depuis 5 jours. Issue reste OPEN par absence de Closes #N reconnue. Tell c.1067 ★ fondateur delivered-urn pattern confirmé (3 commentaires IC antérieurs : myia-po-2026 c.1074, myia-po-2027:CoursIA-2 c.1086, myia-po-2027 c.1074 + retrait du label c.304 car mi-livraison — ici LIVRAISON INTÉGRALE 7/7).

    Tell c.1502 strict 0 close/merge d'autrui + Tell c.1102 ★★★★★ anti-stonewall ×77ᵉ sustained + Tell c.15069 strict urne delivered reserved coordinateur/adjoint : skip re-claim, rend la main au coordinateur pour fermeture.

    — lane myia-po-2023:CoursIA-2, c.485 2026-09-12T08:55Z.

  8. jsboige
    added
    candidate-deliveredReferenced by a merged PR with no post-merge activity -- candidate for close triage (#10466)
    on Sep 13, 2026

  9. jsboige commented on Sep 13, 2026

    @jsboige
    jsboige
    on Sep 13, 2026
    OwnerAuthor

    [INFO] candidate-delivered — PR #15028 MERGED, le travail est déjà sur main. Tell c.1356 ★★★ preflight +\nTell c.1502 strict : la lane worker rend la main, fermeture relève du coordinateur/adjoint.

  10. jsboige commented on Sep 18, 2026

    @jsboige
    jsboige
    on Sep 18, 2026
    OwnerAuthor

    [ADJOINT CLOSE] Adjugée CLOSE_OK — campagne de consolidation du 2026-09-18 (mandat ai-01 2026-09-18T03:12Z, fermeture déléguée).

    Acceptance vérifiée firsthand contre main :

    Spot-check adjoint (confirmé moi-même) : grep -c lowerRamificationGroup sur le FR = 62 (symétrie FR/EN) ; unique occurrence « sorry » = prose du docstring de garde l.66 (« aucun sorry, sorryAx »), zéro sorry de code.

    Réouvrir en citant le critère manquant si contestation.

  11. jsboige
    closed this as completedon Sep 18, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    candidate-deliveredReferenced by a merged PR with no post-merge activity -- candidate for close triage (#10466)enhancementNew feature or request

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions