[jsboige]

Grain: MED/docs — lane myia-po-2027:CoursIA — prev: MED/docs #24642

Contexte

Trois modules Lean documentaient une absence de Mathlib que leur propre pin contredit. Le fait est mesuré dans l'arbre du pin, pas rapporté : chaque ligne citée ci-dessous a été lue à sa source.

Ces trois groundings avaient été relevés le 2026-10-07 puis consignés au registre de la lane (« à corriger par PR après merge #24477 »). C'est cette PR.

Mesures (à chaque lac, sur son propre pin)

Module	Ce que la doc affirmait	Mesure au pin
Riemann200/Memoire1859.lean L19-20	« Mathlib ne porte pas la fonction ζ … aucun RiemannZeta dans l'arbre »	FAUX au pin db584cd6d4 : def riemannZeta := hurwitzZetaEven 0 (NumberTheory/LSeries/RiemannZeta.lean:121)
idem L24-26	« Le prolongement, l'équation fonctionnelle et les zéros restent hors Mathlib »	FAUX : differentiableAt_riemannZeta (l.139), riemannZeta_one_sub (l.178), riemannZeta_neg_two_mul_nat_add_one (l.173), def RiemannHypothesis (l.185), et NumberTheory/LSeries/ZetaZeros.lean (riemannZetaZeros l.35, fermé l.59, discret l.62, intersection finie avec tout compact l.66)
Riemann200/LiminfForme.lean L21-23	« Mathlib ne porte pas la fonction ζ ni ses zéros »	FAUX au même pin ; la partie vraie de la phrase est conservée : le théorème A d'Alpöge–Furman n'est pas dans Mathlib, qui n'énonce la RH que comme Prop
ANALYSE/kls_lean/KLS/Defs.lean L72-73	« Aucun lemme de convexité du carré n'existe au pin (audit du 2026-10-07) »	FAUX au pin 520045ab14 : Even.convexOn_pow (Mathlib.Analysis.Convex.Mul:161) et convexOn_univ_norm (Mathlib.Analysis.Normed.Module.Convex:53)

Le pin 520045ab14 a été identifié par son message de commit (chore: bump toolchain to v4.32.1) — la prose ne certifie donc pas un tag, seulement le SHA que le lake-manifest.json du lake déclare.

Méthode : grep -n dans .lake/packages/mathlib pour riemann200_lean (mathlib vendorié au pin du lac) ; lecture du fichier au SHA exact via raw GitHub pour kls_lean, dont le .lake/packages/ est vide sur cette machine.

Diff commentaire-seul — prouvé mécaniquement

Le diff ne touche aucune ligne de code, de type ou de preuve. Preuve : comparaison, fichier par fichier, du code privé de ses commentaires (/- … -/ et --) entre HEAD et l'arbre de travail.

IDENTIQUE Memoire1859.lean | len code 703
IDENTIQUE LiminfForme.lean | len code 1478
IDENTIQUE Defs.lean        | len code 3252

Compte sorry réel — inchangé

python scripts/lean/count_code_sorry.py --json (champ distinct_code_sorry), avant → après, par lac :

Lac	code_sorry	distinct_code_sorry
Lean/Riemann200/riemann200_lean	0 → 0	0 → 0
Lean/ANALYSE/kls_lean	0 → 0	0 → 0

(naive_sorry kls = 3, prose seulement, inchangé — c'est le sur-comptage que l'instrument canonique écarte.)

Build — ce qui est prouvé, et ce qui ne l'est pas

• riemann200_lean est dans la matrice CI (.github/workflows/lean-ci-matrix.yml, chemins L175-178 et L395-398) : ce diff déclenche la jambe du lac, et le Lake build de cette jambe est la preuve.
• kls_lean n'est pas couvert par la matrice Lean (aucune entrée kls_lean dans .github/workflows/). Je ne prétends pas un lake build local : le .lake/packages/ de ce lac est vide sur cette machine, donc il n'y a pas de Mathlib à compiler contre. La preuve apportée pour ce fichier est celle qui est disponible et suffisante ici : diff commentaire-seul (ci-dessus) — une ligne de commentaire ne participe pas à l'élaboration.

Si un reviewer exige un build pour kls_lean, le geste est lake exe cache get && lake build sur une lane qui a le lac provisionné ; je le ferai sur demande plutôt que de l'annoncer sans l'avoir fait.

Portée

• Un seul sujet : trois groundings faux, une classe de défaut (la doc cède devant le pin), deux lacs.
• See #24634 — même famille (documentation Lean qui ment sur ce que le pin contient), instance distincte : Docs(lean): les pins Mathlib documentes contredisent les lakefiles (3 lakes mesures, cohorte GameTheory a mesurer) #24634 porte des numéros de version faux, ceci des capacités fausses. Pas de Part of, pour ne pas gonfler le périmètre de cette issue.
• Part of #20403 (EPIC du lake riemann200_lean).
• G-VAR-3 : second docs consécutif après Fix(docs,#24634): README galois_lean et conway_lean alignes sur leurs lakefiles #24642, sous l'exception variation-protocol G-VAR-3 : le ban absolu des genres LIGHT et l'exception MED/DEEP-distinct se recouvrent sur guard/test/docs/readme/ledger #14357 — second grain MED, et aucun fichier partagé avec Fix(docs,#24634): README galois_lean et conway_lean alignes sur leurs lakefiles #24642 (comm -12 vide sur les trois chemins).

🤖 Generated with Claude Code

[github-actions]

Avertissements consultatifs

Trivial-diff advisory (#15740, non bloquant).
genre docs dans la famille META (docs/guard/ledger/readme/test) + diff de 47 lignes changees (<= 100) + aucune exception ecrite dans le body : le litmus de la trivialite (une douzaine d'instances scannees a la suite) est credible. Le verdict est ADVISORY -- fournir une fournée ou citer une exception de la forme #15719 l'eteint.
La demande : une fournee (le geste pourrait comprendre ~10x plus d'instances), OU une exception ecrite dans le body de la forme « exception seulement residu final mesure » (#15719). Editer le body re-deroule cet organe et retire le label.

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

• TIER-INFLATION : declared LIGHT << effective LIGHT-genre (tally : declared=3 genre=5 cap=3)
• CAP-EXCEEDED-BY-GENRE : light_genre > cap partage G-VAR-2 (tally : declared=3 genre=5 cap=3)

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.

G-VAR-2 light cap reached (advisory, non bloquant).
La lane myia-po-2027:CoursIA a deja consomme son budget LIGHT du jour (axe genre G-VAR-2/3 (light-genre, quel que soit le tier declare) : #24127 (LIGHT/ledger, merge a 2026-11-04T05:01:42Z), #24129 (LIGHT/docs, merge a 2026-11-04T05:04:20Z), #24555 (MED/guard, merge a 2026-11-04T07:18:58Z), #24582 (MED/docs, merge a 2026-11-04T12:33:06Z), #24642 (MED/docs, merge a 2026-11-04T20:16:47Z)).
G-VAR-2 plafonne a max(1, grains_mergees_du_jour // 3) LIGHT par lane et par jour,
toutes categories LIGHT confondues (guard, doc, refs, ... partagent un seul budget) :
c'est un RATIO, pas un plafond plat. La decision de merge reste au coordinateur.

Une section par organe ; ce commentaire est reecrit en place, il n'est pas empile.

[github-actions]

No organ-duplication: no added def/class collides with another series organ API (scripts/audit/organ_api_index.yaml).

Detector: python scripts/audit/detect_organ_duplication.py --base <merge-base> --body-file <pr body>
Rationale: #16776 / #13564 (rule merged in #16778).