[jsboige]

Grain: LIGHT/guard — lane myia-ai-01:CoursIA-2 — prev: DEEP/notebook-python #24451

La page des theoremes dupliques derive de l'arbre — elle fait echouer le job Scripts Tests (CPU) de main

Le defaut

scripts/lean/tests/test_lean_theorem_duplicates.py::test_page_generee_suivant_l_arbre compare la
page commitee docs/reference/lean-theorem-duplicates.md a la page regeneree par l'organe, et exige
qu'elles soient identiques. Or ArcPartition.lean a gagne une ligne depuis la derniere
regeneration : la page citait encore l'ancien numero de ligne, et le test echoue.

Le test est donc un ratchet de derive : il rend son propre resultat vert des que la page est
regeneree, et rouge des qu'un .lean bouge sans regeneration. C'est son role.

Ce rouge est herite de main : il reproduit sur main (verifie sur le clone de travail, arbre
main), et il bloque le job Scripts Tests (CPU) de toute PR qui touche scripts/ — dont
#24441 et #24444.

Le correctif

La regeneration canonique, pas une retouche a la main :

python scripts/lean/lean_theorem_duplicates.py --write

Le diff est d'une ligne — le numero de ligne cite, passe de l'ancien a l'actuel :

-- ... (MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/knot_lean/Knots/ArcPartition.lean:843) ...
++ ... (MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/knot_lean/Knots/ArcPartition.lean:842) ...

Aucune preuve, aucun enonce, aucun .lean n'est modifie : le contenu de la page est produit par
l'organe, a partir de l'arbre courant.

Verification

• python scripts/lean/lean_theorem_duplicates.py --check : vert apres regeneration
• python -m pytest scripts/lean/tests/test_lean_theorem_duplicates.py -q : 11 passed (contre
  1 failed, 10 passed avant, sur le meme arbre)

Portee

See #24441 et See #24444 — les deux PRs de la lane sont bloquees par ce meme job de main ; la
correction leur rendra le job vert au prochain run apres merge.

🤖 Generated with Claude Code

[github-actions]

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-03) :

• TIER-INFLATION : declared LIGHT << effective LIGHT-genre (tally : declared=1 genre=3 cap=8)
• GENRE-MISMATCH : declared genre != genre infere depuis les chemins du diff

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.

[github-actions]

Trivial-diff advisory (#15740, non bloquant).
genre guard dans la famille META (docs/guard/ledger/readme/test) + diff de 2 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.

[jsboige]

[ACTION] Doublon — la même régénération est déjà ouverte par #24458 (lane myia-po-2023:CoursIA)

J'ai reproduit le défaut avant d'ouvrir cette PR, et indépendamment : le test
scripts/lean/tests/test_lean_theorem_duplicates.py::test_page_generee_suivant_l_arbre échoue
sur main (arbre 1596350104d, dans le clone de travail) ; la page committée cite
ArcPartition.lean:843 quand l'arbre dit :842 ; et
python scripts/lean/lean_theorem_duplicates.py --write produit exactement la même correction
d'une ligne, le test passant ensuite (11 passed).

Cette PR fait donc doublon avec #24458, qui porte le même correctif sur le même fichier et
est déjà en revue. Je la ferme : faire converger deux diffs identiques sur le même fichier
n'apporte rien et risquerait un conflit de fusion.

Les PRs de la lane bloquées par ce rouge base-inherited (#24441, #24444) portent chacune la
preuve du caractère hérité et le renvoi vers la PR qui le corrige.

[jsboige]

Fermee : doublon de #24458 (meme regeneration, meme fichier).