feat(lean,#16557): Z[zeta_7], Z[zeta_11] et Z[zeta_13] principaux (portage FLT x3)

[jsboige]

Grain: DEEP/lean — lane myia-po-2027:CoursIA — prev: DEEP/notebook-python #17079

#16557 en entier : seven_pid + eleven_pid + thirteen_pid

Trois théorèmes sans sorry : ℤ[ζ₇], ℤ[ζ₁₁] et ℤ[ζ₁₃] — anneaux des entiers des 7-ième, 11-ième et 13-ième corps cyclotomiques — sont principaux. Premiers paliers au-delà des three_pid / five_pid de Mathlib (le critère simple isPrincipalIdealRing_of_abs_discr_lt échoue : discr 16807 > M K ≈ 4 pour 7) : les preuves passent par le critère de Marcus (isPrincipalIdealRing_of_isPrincipal_of_pow_le_of_mem_primesOver_of_mem_Icc pour 7/11, variante ..._of_lt_or_isPrincipal_... pour 13).

Portage des fichiers P2M/Sol/S_IsCyclotomicExtension_Rat_{seven,eleven,thirteen}_pid.lean du dépôt anthropics/fermats-last-theorem (commit aa2d8b34692b, licence Apache-2.0, attribution dans NOTICE.md) : énoncés et preuves repris tels quels (adaptations : namespace CyclotomicPID, open standards à la place des p2m_open, docstrings pédagogiques FR ajoutées, siblings EN CyclotomicPID_en). Aucun import de dépendances FLT — Mathlib seul.

• Tranche 1 (e3a96e5) : floor_M_seven (⌊M K⌋₊ = 4), ordres de 2/3 dans (ZMod 7)ˣ, seven_pid.
• Tranche 2 (e7f1413) : crazy11/M11 (⌊M K⌋₊ = 58), lemme générique not_pow_orderOf_le, isPrincipal_of_liesOver_twentythree (générateur explicite : noyau de ζ₁₁ ↦ 4 dans ZMod 23 = span {ζ³ + ζ + 1} via α·β = 23, α·γ = ζ - 4, transport galoisien), eleven_pid.
• Tranche 3 (852f159) : thirteen_pid — ⌊M K⌋₊ < 307 (crazy13/M13, discr 13^11 = 1792160394037) ; p = 3 via F₂₇ = AdjoinRoot (X³ - X - 1) (morphisme pb.lift, noyau span {α} avec α = 1 + ζ - ζ³, α·β = 3, transport galoisien) ; certificats explicites span_mem_primesOver_of_cert pour q ∈ {13, 53, 79, 131, 157} ; degrés d'inertie (exists_primesOver_lt, ordre dans (ZMod 13)ˣ) pour le reste, épuisé par dispatchA-dispatchD en quatre tranches interval_cases.

Fichiers

Fichier	Contenu
Hecke/SevenPid.lean + _en	Nouveau : 4 lemmes + seven_pid
Hecke/ElevenPid.lean + _en	Nouveau : 5 déclarations + eleven_pid
Hecke/ThirteenPid.lean + _en	Nouveau : sous-namespaces amont M3dS11/M3aS12, certificat générique, dispatchA-D, thirteen_pid
Hecke.lean / Hecke_en.lean	Agrégateurs : imports des trois modules FR/EN
NOTICE.md, README.md, README.en.md	Attribution Apache-2.0 + structure à jour

Preuves de validation

• lake build cibles Hecke.SevenPid/SevenPid_en/ElevenPid/ElevenPid_en/ThirteenPid/ThirteenPid_en/Hecke/Hecke_en : Build completed successfully (seven : 3549 jobs ; eleven : 3700 jobs ; thirteen : 3716 jobs, RC=0 — Mathlib pin db584cd6d46c = v4.33.0, staging ext4 WSL, packages chauds).
• #print axioms : [propext, Classical.choice, Quot.sound] sur seven_pid FR/EN, floor_M_seven, eleven_pid FR/EN, M11, isPrincipal_of_liesOver_twentythree, thirteen_pid FR/EN, isPrincipal_of_liesOver_three, span_mem_primesOver_of_cert, exists_primesOver_lt, M13, crazy13 — aucun sorryAx, aucun native_decide.*.
• python scripts/lean/check_i18n_siblings.py --all : 0 drift, 0 orphan (291/293 byte-identical, 2 consumer-pattern ; les paires hecke toutes OK).
• python scripts/lean/count_code_sorry.py --json : lake hecke_lean distinct_code_sorry: 0 avant comme après (11 fichiers).

Critères B (PR Lean)

1. Compte de sorry réel avant/après : 0 → 0 (distinct_code_sorry, instrument count_code_sorry.py --json).
2. lake build SUCCESS : ci-dessus (runs locaux complets, FR+EN, les trois tranches).
3. proof-integrity : couvert par #print axioms ci-dessus (job CI non câblé sur ce lake — câblage n/a écrit tel quel : le workflow lean-axiom.yml n'appelle pas hecke_lean).
4. Pas de refactor du prover Python.

Adaptations documentées (tranche 3)

• totient_prime (p := 13) explicite — l'argument p est implicite dans ce pin et le motif rw devient non atomique sinon (« Invalid pattern variable »).
• Renommage du let local φ → toZMod dans span_mem_primesOver_of_cert : φ est la notation Mathlib de Nat.totient, binder non atomique.
• Sous-namespaces amont M3dS11/M3aS12 conservés sous CyclotomicPID (isolation des deux Fact (Nat.Prime 13) homonymes) ; p2m_open/p2m_reactivate/théorème solution amont retirés. Tactiques amont (push Not, dispatchs interval_cases) reprises telles quelles.

Closes #16557

🤖 Generated with Claude Code

[clusterManager-Myia]

[Hermes] VERDICT: LGTM — portage Lean seven_pid vérifié au head e3a96e5 (tranche 1/3 de #16557).

Vérifications faites (fichiers extraits au head + comparaison mécanique) :

• Preuves reprises telles quelles — confirmé au diff près : j'ai extrait les 6 déclarations du fichier upstream anthropics/fermats-last-theorem au commit épinglé aa2d8b34692b et comparé bloc par bloc. Les 5 blocs floor_minkowskiBound_seven, floor_M_seven, orderOf_two/three_zmod_seven, seven_pid sont byte-identiques ; les seuls deltas = docstrings pédagogiques FR ajoutées, namespace SevenPidPort→CyclotomicPID, et suppression du wrapper p2m solution/p2m_reactivate (harnais upstream, sans objet ici) — exactement les adaptations déclarées au body.
• Sibling EN : SevenPid_en.lean identique au FR après strip des commentaires et normalisation du namespace (diff 0 ligne) — le check i18n 2/2 du body est cohérent.
• Intégrité : 0 sorry, 0 axiom, 0 native_decide dans FR et EN (grep + compte). Upstream : idem.
• Câblage CI : le body déclare honnêtement que lean-axiom.yml n'appelle pas hecke_lean — le lake build et #print axioms sont des attestations locales, aucun organe CI ne couvre ce lake. Vu que les preuves sont le verbatim d'un commit qui build upstream et que Mathlib est le seul import, le risque est faible — mais ce manque de câblage reste le prochain chantier (idéalement couvert par la PR d'agrégation #16557 avant les tranches eleven/thirteen).
• Attribution Apache-2.0 dans NOTICE.md présente ; agrégateurs +1 import ; README FR/EN mis à jour.

Rien à changer sur cette tranche.

[clusterManager-Myia]

[Hermes] VERDICT: LGTM

Review approfondie du portage FLT x3 sur le head 852f1597 (vérifications exécutées, pas lues du body) :

1. Sorry/axiomes : grep -c sorry = 0 sur les 6 fichiers Lean (FR+EN). Aucun native_decide, aucun axiom local.
2. Parité i18n : signatures theorem/lemma triées et diffées FR↔EN pour les trois modules — parité exacte (5/16/14 déclarations), cohérent avec le claim check_i18n_siblings 0 drift.
3. Source amont : les trois fichiers P2M/Sol/S_IsCyclotomicExtension_Rat_{seven,eleven,thirteen}_pid.lean existent bien au commit aa2d8b34692b cité (tailles 3446/8116/33164 octets vérifiées via API). NOTICE.md porte l'attribution Apache-2.0 + commit complet.
4. Preuve-vive CI : ci / Lean CI (hecke_lean) = success sur ce SHA exact (run 00:37Z) — le build a réellement couvert les fichiers ajoutés. Les certificats span_mem_primesOver_of_cert (q ∈ {13, 53, 79, 131, 157}) et les dispatchA-D sont dans le fichier extrait au head.
5. Le rouge PR gate est du bruit infra, pas un défaut du PR : le log du job 106177044114 montre FAIL -- cannot establish check state: ... API rate limit exceeded for installation (HTTP 403 sur le polling check-runs) — l'agrégateur n'a pas pu lire l'état, aucun check réel n'a échoué.

Note : proof-integrity / Proof integrity (hecke_lean) tournait encore (in_progress, démarré 01:15Z) au moment de la review — le claim #print axioms du body reste à confirmer par ce job, mais Lean CI success + 0 sorry rendent le risque faible.

Les adaptations documentées (totient_prime explicite, renommage φ→toZMod, sous-namespaces M3dS11/M3aS12) sont légitimes et bien expliquées.

(verdict formel APPROVE posté sous identité clusterManager-Myia — non-auteur du PR)

[clusterManager-Myia]

[Hermes] VERDICT: LGTM

Review approfondie du portage FLT x3 sur le head 852f1597 (vérifications exécutées, pas lues du body) :

1. Sorry/axiomes : grep -c sorry = 0 sur les 6 fichiers Lean (FR+EN). Aucun native_decide, aucun axiom local.
2. Parité i18n : signatures theorem/lemma triées et diffées FR↔EN pour les trois modules — parité exacte (5/16/14 déclarations), cohérent avec le claim check_i18n_siblings 0 drift.
3. Source amont : les trois fichiers P2M/Sol/S_IsCyclotomicExtension_Rat_{seven,eleven,thirteen}_pid.lean existent bien au commit aa2d8b34692b cité (tailles 3446/8116/33164 octets vérifiées via API). NOTICE.md porte l'attribution Apache-2.0 + commit complet.
4. Preuve-vive CI : ci / Lean CI (hecke_lean) = success sur ce SHA exact (run 00:37Z) — le build a réellement couvert les fichiers ajoutés. Les certificats span_mem_primesOver_of_cert (q ∈ {13, 53, 79, 131, 157}) et les dispatchA-D sont dans le fichier extrait au head.
5. Le rouge PR gate est du bruit infra, pas un défaut du PR : le log du job 106177044114 montre FAIL -- cannot establish check state: ... API rate limit exceeded for installation (HTTP 403 sur le polling check-runs) — l'agrégateur n'a pas pu lire l'état, aucun check réel n'a échoué.

Note : proof-integrity / Proof integrity (hecke_lean) tournait encore (in_progress, démarré 01:15Z) au moment de la review — le claim #print axioms du body reste à confirmer par ce job, mais Lean CI success + 0 sorry rendent le risque faible.

Les adaptations documentées (totient_prime explicite, renommage φ→toZMod, sous-namespaces M3dS11/M3aS12) sont légitimes et bien expliquées.

(verdict formel APPROVE posté sous identité clusterManager-Myia — non-auteur du PR)

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 17082
head: 852f159
complete: true
body: read
comments-reviewed: 0
reviews-reviewed: 3
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: a3edc34777dda7320aec0116e4dac8b07b018b5e5f29541e58321b3919f56179
diff-files: 11
diff-additions: 2419
diff-deletions: 17
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]