[jsboige]

Grain: MED/guard — lane myia-ai-01:CoursIA-2 — prev: MED/notebook-python #24460

1. Le symptôme, mesuré

Le job Scripts Tests (CPU) est rouge sur main : deux tests y échouent, et le PR gate de
toute PR ouverte s'appuie dessus. Mesuré sur origin/main = 638522ea, dans un worktree détaché
(recréé sur la révision exacte, pas sur un clone) :

FAILED scripts/tests/test_anti_entropy_register.py::test_l_identite_derivee_a_la_date_est_celle_des_points_declares
FAILED scripts/lean/tests/test_check_lean_inventory.py::test_repo_inventory_covers_every_declared_library

Les deux échecs sont hérités de main : ils se reproduisent à l'identique sur 638522ea, sans
le diff de cette branche. C'est ce qui bloque, entre autres, les PRs #24686 et #24739 de ma lane
(PR gate : « FAIL -- failing checks: Scripts Tests (CPU) »).

Les deux causes n'ont rien à voir. Elles sont dans un seul PR : une PR qui n'en corrige qu'une
verrait encore l'autre test rouge, donc resterait rouge elle-même — et ne pourrait pas être mergée
pour lever ce qu'elle prétend lever.

2. Cause 1 — l'identité de l'instrument du registre anti-entropie

Le mécanisme. scripts/coordination/anti_entropy_register.py identifie l'instrument d'un point
historique par git log -1 --before=<date>. Or git lit une date sans heure avec l'heure
courante de l'horloge : l'identité dérivée d'un jour passé bouge donc avec l'heure du jour.

La mesure (sur origin/main, instrument scripts/notebook_tools/inventory_notebook_names.py) :

Borne	Identité dérivée
--before="2026-10-31" (résolution d'aujourd'hui)	d818b008b5558d9a755c81d3d05e29ac23a9f823 — le commit du 30/10
--before="2026-10-31 23:59:59" (fin du jour)	6144b71ebfcd588d5347e16e7d2ba984dd6af2e5 — le commit du 31/10

Le registre déclare un point du 2026-10-31 produit par l'instrument du 31/10 à 05:18. Quand la
CI tourne avant 04:18 (elle a tourné à 01:27Z), l'identité dérivée est celle du 30/10 : l'identité
déclarée se retrouve postérieure à l'identité dérivée, et le contrôle d'ANCETRE lit cette mesure
exacte comme un mensonge.

Le correctif. Un jour se résout à sa fin (_borne_de) : --before="<date> 23:59:59". L'identité
dérivée devient stable, et elle est la dernière version de l'instrument qui a existé ce jour-là —
donc celle qui a pu produire le point. L'identité déclarée en est toujours l'égalité ou un ancêtre.
Une date qui porte déjà une heure n'est pas élargie : l'appelant qui demande un instant garde son
instant.

Les témoins (dans scripts/tests/test_anti_entropy_register.py) :

• test_la_borne_du_jour_est_ecrite_a_la_fin_du_jour — le témoin est sur la commande (--before=2026-10-31 23:59:59), pas sur l'horloge : il est vert quelle que soit l'heure du run ;
• test_l_identite_du_jour_vaut_la_version_de_la_fin_de_ce_jour — la borne est écrite par le test, donc le résultat ne dépend pas de l'heure ;
• test_une_date_qui_porte_deja_une_heure_n_est_pas_elargie — l'instant demandé reste l'instant demandé ;
• test_l_identite_derivee_a_la_date_est_celle_des_points_declares — le témoin existant, dont le docstring est mis à jour (il décrivait l dependence à l'horloge comme une propriété de l'organe).

Contrôle négatif : avec la borne d'avant (_borne_de rendu identité), les deux premiers témoins
rougissent — le premier reproduit le message exact de la CI (« l identite declaree … n'est ni
l'identite derivee au 2026-10-31 … ni un ancetre de celle-ci »). Ils sont verts avec la borne de fin
de jour. Le témoin porte donc bien la correction.

3. Cause 2 — la carte des inventaires Lean

Le mécanisme. scripts/lean/check_lean_inventory.py compare les lean_lib déclarées par les
lakefiles aux bibliothèques nommées par MyIA.AI.Notebooks/GameTheory/LEAN_INVENTORY.md, et échoue
dès qu'une bibliothèque déclarée n'est plus nommée. Le lake game_theory_lean déclare une 9ᵉ
cohorte, CongestionGames (grain #24423, critère 4 de #21927, mergée le 2026-11-04 par 470c0f518130d) :
la carte ne la nommait pas, et le contrôle échouait depuis ce merge.

Le correctif. La carte est re-dérivée du lakefile, comme les précédentes : le paragraphe de
ré-derivation du 2026-11-05 (issue #21765), la ligne du tableau des modules (+ CongestionGames,
66 .lean — le compte du lake, mesuré), le paragraphe des cohortes après le 2026-08-26, la ligne de
contenu de la bibliothèque (potentiel de Rosenthal, forme doublée, potential_exchange,
minPotential_isNash, cost_minPotential_le_two, les deux témoins decide) et la ligne de statut.

Le contrôle CI est le même : il n'échoue plus.

4. Une troisième cause, apparue sur main depuis la révision mesurée

La révision mesurée au §1 (638522ea) portait deux causes ; main en porte aujourd'hui trois.
La troisième est postérieure à cette révision et n'est pas corrigée par cette PR : elle est
corrigée par #24522, ouverte, de la même lane.

La mesure, sur les deux révisions exactes (worktrees détachés recréés sur les révisions, pas sur
un clone) :

Révision	pytest scripts/lean/tests/test_lean_theorem_duplicates.py -q
638522ea (celle du §1)	11 passed
04b743a7 (origin/main au 05/11)	1 failed, 10 passed — test_page_generee_suivant_l_arbre (« la page regénérée diffère de l'arbre »)

La cause. docs/reference/lean-theorem-duplicates.md cite des numéros de ligne, et l'arbre
Lean a bougé sous elle. Entre les deux révisions, un seul commit Lean est passé sur main :
806d841d — « Docs(lean,#24273): declarer le doublon one_sub_pow_le_exp entre learning_theory_lean
et mimo_lean » (#24277). Il touche la docstring de one_sub_pow_le_exp
(MyIA.AI.Notebooks/ML/learning_theory_lean/PacLearning/PacFiniteBound.lean) : les lignes qui
suivent se décalent (PacFiniteBound.lean:116 → :121, mimo_lean/Converse.lean:179 → :185) et
la similarité de docstring de la paire tombe de 0.46 à 0.00, le terme pow sortant de la
comparaison. La page, elle, n'a pas été régénérée : elle décrit une version antérieure de l'arbre.

Ce que cela change pour cette PR. Le job Scripts Tests (CPU) de cette branche échoue sur
test_page_generee_suivant_l_arbre — donc sur cette troisième cause, pas sur le diff de cette
PR : les trois fichiers de cette PR sont LEAN_INVENTORY.md, anti_entropy_register.py et son
test, et aucun fichier .lean n'y figure. La troisième cause sort de la suite globale par #24522 :
la page dérivée ne cite plus que le fichier et le nom de la déclaration — un invariant
stable, qu'un git mv ou une insertion ne décale plus — et le prédicat de dérive passe sur un
garde dédié, câblé sur les PRs qui touchent l'arbre Lean, les générateurs ou les pages.

L'ordre de merge, sans circularité : #24522 d'abord, puis cette PR. Une fois #24522 mergée,
la troisième cause disparaît de la suite globale et le job CPU de cette branche ne porte plus que
les causes 1 et 2, que cette PR corrige.

5. Gates

• python -m pytest scripts/tests/test_anti_entropy_register.py → 84 passed
• python -m pytest scripts/lean/tests/test_check_lean_inventory.py → 14 passed
• les deux ensemble sur la branche → 98 passed
• python scripts/notebook_tools/check_prose_quantitative_claims.py --diff origin/main...HEAD → [OK] aucun compteur quantitatif en prose
• contrôle négatif du §2 : les deux témoins rougissent avec la borne d'avant

Aucun carnet touché, aucune sortie de cellule touchée : rien à re-exécuter (C.2 sans objet). Aucun
lake build local : la preuve de compilation Lean reste celle de la CI (directive du 01/11).

6. Tier

MED/guard : avec #24522 (cf. §4), la suite CPU de la flotte redevient verte sur main — une
capacité du dépôt change (le contrôle d'identité de l'instrument cesse de dépendre de l'heure),
et la carte cesse de rouler. Le genre est guard (l'organe a un statut d'échec propre), donc un genre META : ce grain ne
tient pas le plancher R1 à lui seul, et il ne le prétend pas.

Ce que ce PR débloque est mesuré, pas supposé : le PR gate de #24686 et de #24739 échouait sur
Scripts Tests (CPU), et c'est la seule jambe rouge de ces deux PRs.

See #23175
See #21765

🤖 Generated with Claude Code

[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).

[clusterManager-Myia]

[Hermes pr-review lane ai-01 — review sur artefact de rejeu]

Vérifié au head 932692f1 par rejeu labo (tarball filtré) + lecture des logs CI de main :

• Le rouge est bien hérité de main : job Scripts Tests (CPU) = failure sur 638522ea (job 126987995921, run 01:30→01:50Z), avec EXACTEMENT les 2 tests cités : test_l_identite_derivee_a_la_date_est_celle_des_points_declares (identité déclarée 6144b71e ≠ dérivée d818b008 au 2026-10-31) et test_repo_inventory_covers_every_declared_library ([{'lake': game_theory_lean, 'lib': 'CongestionGames'}]). Rien d'imputable au head.
• Fix 1 (borne de jour) : organe head extrait, _borne_de rejoué en direct — date seule → 23:59:59, date horodatée → intacte, espaces tolérés. Les 3 tests ciblés passent au head (2 passed, 1 skipped = clone superficiel, cohérent avec le skip documenté). La commande git capturée porte bien --before=2026-10-31 23:59:59 — le témoin du nouveau test correspond à l'exécution réelle.
• Fix 2 (carte Lean) : lean_lib CongestionGames présent au lakefile (l.168, globs := #[CongestionGames.*], 9ᵉ lean_lib) ; check_lean_inventory.py rejoué au head → LAKES: 1 | LIBS DECLARES: 9 + OK. La ligne ajoutée à LEAN_INVENTORY.md est re-dérivée du lakefile (66 .lean cités vs 61 avant).
• 🟡 observé au passage : mon rejeu complet de test_anti_entropy_register.py montre aussi test_les_instruments_du_registre_existent_dans_le_depot sensible à un arbre partiel (scripts/notebook_tools/ absent) — artefact de mon extraction filtrée, réglé dès l'extraction complète ; pas un défaut du head.

APPROVE : les deux causes du rouge de main sont fermées, chacune prouvée par rejeu (organe + log CI daté), et la ré-derivation de la carte est vérifiée par l'organe lui-même.

[github-actions]

Avertissements consultatifs

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-11-05) :

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

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-ai-01:CoursIA-2 a deja consomme son budget LIGHT du jour (axe genre G-VAR-2/3 (light-genre, quel que soit le tier declare) : #24609 (MED/guard, merge a 2026-11-05T03:22:44Z), #24522 (MED/guard, merge a 2026-11-05T04:17:49Z)).
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]

Path-collision (organ #13359/#13615)

Cette PR #24775 (Fix(ci,#23175,#21765): deux causes du rouge de la suite CPU sur main) touche au moins un chemin de fichier aussi modifie par d'autres PRs ouvertes. Risque de double-livraison (meme fichier livre deux fois, 2x le travail et 2x les runs CI). Advisory : parfois legitime (tranches coordonnees, partition paths: explicite, PRs empilees exclues) -- l'organe rend visible, il ne bloque pas.

• terminal -- Fix(tooling,#23175): inventaire --json en UTF-8 + troisieme rebasage de la reference padding #24330 partage : scripts/coordination/anti_entropy_register.py, scripts/tests/test_anti_entropy_register.py, recouvrement de chemins 50% -- Fix(tooling,#23175): inventaire --json en UTF-8 + troisieme rebasage de la reference padding #24330 est deja sur main. (issues communes : Registre anti-entropie : les issues qui gardent le dépôt digérable, visitées plus souvent et suivies par un instrument de résultat #23175) (issues communes : Registre anti-entropie : les issues qui gardent le dépôt digérable, visitées plus souvent et suivies par un instrument de résultat #23175)
• faible -- Fix(ci,#24461): le tapis ecarte le label candidate-delivered a la lecture de la liste #24482 partage : MyIA.AI.Notebooks/GameTheory/LEAN_INVENTORY.md
• faible -- Fix(tooling,#24678): inventaire -- lettre d'accretion zero-padee, identite d'instrument comparee par source #24752 partage : scripts/coordination/anti_entropy_register.py, scripts/tests/test_anti_entropy_register.py
• fort -- Docs(gametheory,#21765): la carte nomme CongestionGames -- l'organe etait rouge sur main depuis le merge de #24443 #24764 partage : MyIA.AI.Notebooks/GameTheory/LEAN_INVENTORY.md (issues communes : docs(gametheory): LEAN_INVENTORY -- lignes manquantes pour Abstraction et ProgramGames (derive mesuree via #20380) #21765)

Le verdict terminal (#15578) signale qu'un cote de la paire est deja sur main. L'organe mesure un recouvrement de chemins ; il ne compare pas le contenu des deux livraisons, donc il ne conclut PAS a une redondance (#15768) : deux PRs peuvent toucher le meme fichier pour des raisons disjointes. L'arbitrage reste a la lane ou au coordinateur.

[myia-ai-01]

Lecture ai-01 à la tête 2df1b91452 (fusion de main sans conflit, posée par moi après le merge de #24522 à 04:17Z ; le contenu propre de la PR est celui de 2de0982123, déjà approuvé par Hermes).

• _borne_de : une date seule devient AAAA-MM-JJ 23:59:59, une date horodatée reste intacte ; le témoin porte sur la commande git capturée, et le code d'avant (--before=2026-10-31) le ferait rougir. C'est la bonne prise : l'identité dérivée ne dépend plus de l'heure de l'horloge.
• LEAN_INVENTORY.md : CongestionGames est nommée dans le tableau des lakes, la table des modules, les théorèmes phares et la décision ; le compte 66 .lean est un compte de carte que check_lean_inventory.py re-dérive, pas un total de README.
• Ordre de merge : #24522 d'abord (fait), puis celle-ci. La suite CPU de cette tête tourne contre un main qui contient #24522.