Repository navigation
fix(lean,#17357): Lean-16c -- six affirmations perimees (durees, jours, exercices) - #20127
Conversation
…s, exercices) Six constats de l'audit Hermes (commentaire 5845151214), tous reverifies firsthand contre main avant correction. Aucune cellule de code touchee : les six vivent dans des cellules markdown, et chacune est refutee par une sortie committee du meme carnet. F1 -- « La courbe de population monte par paliers » (cellules 12 et 14). Le canon de Gosper ne produit pas d'escalier : la population oscille au sein de chaque cycle et gagne exactement +5 cellules par cycle de 30 generations. Mesure reproduite avec le code du carnet (pops[0]=36, pops[30]=41, pops[59]=53 identiques a la sortie committee ; 17 baisses sur 59 pas, chute maximale -19 ; la suite est exactement periodique de periode 30, +5 par cycle). La courbe oscille donc, elle ne monte pas par paliers -- le modele visuel que le texte faisait retenir etait faux. F2 -- « le simulateur numpy estimait 107 jours » (cellules 29 et 36). La sortie committee de la cellule 25 imprime « ~93.2 jours sur ce kernel numpy ». Le chiffre 107 n'apparait nulle part dans les sorties : corrige en ~93.2 jours, prose et ligne de tableau. F3 -- « En 4-5 secondes » pour l'OTCA Metapixel (cellule 32). La sortie committee de la cellule 31 imprime « temps=7.30s ». Corrige en ~7.3 s, et de meme dans les deux autres endroits qui portaient le meme nombre (ligne OTCA du tableau de synthese, paragraphe 1 de la cellule 36). F4 -- « evolue sur 1 000 generations en ~4 secondes » pour la machine de Turing (cellule 34). La sortie committee de la cellule 33 imprime « temps=8.59s ». Corrige en ~8.6 s, et de meme sur la ligne Turing du tableau de synthese. F5 -- « HashLife va le faire en quelques secondes » pour Gemini (cellules 29 et 36). La sortie committee de la cellule 35 imprime « temps=124.37s » pour les 100 000 premieres generations, et estime ~1244 s pour les 33.6 M completes. « quelques secondes » annoncait une demonstration quasi instantanee que le carnet ne produit pas. Corrige aux trois endroits (prose, ligne Gemini du tableau, paragraphe 3). F6 -- « L'exercice 4 (Golly / HighLife) » (cellule 39). L'exercice Golly / HighLife est titre « Exercice 1 » dans la section precedente (cellules 37 et 38), tandis que l'exercice 4 est « Compter la population produite par un canon » (cellule 44). Corrige en « Exercice 1 ». Portee : 7 cellules markdown (12, 14, 29, 32, 34, 36, 39), source seule. Verifie champ par champ contre main sur les 47 cellules : ids, outputs, execution_count, metadata et cell_type inchanges -- 7 champs modifies, tous des source. Les 18 cellules de code gardent leurs execution_count contigus. Aucune re-execution due (exception C.2 : modifications uniquement markdown), et aucune re-execution possible sans degrader les sorties committee : le cache RLE numpy du carnet n'est pas versionne et les durees mesurees varient d'un run a l'autre -- re-executer aurait casse l'alignement prose/sortie que ce correctif etablit. Les sorties etaient deja justes ; c'est le texte qui ne l'etait pas. See #17357 Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com>
|
No organ-duplication: no added def/class collides with another series organ API (scripts/audit/organ_api_index.yaml). Detector: |
|
G-VAR-2/3 GENRE signals (advisory, non bloquant, #10020).
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 |
|
Scope = notebooks CHANGED in this PR, not the whole corpus. Explicit |
|
Scope = notebooks CHANGED in this PR, not the whole corpus. The |
|
✅ No factual mislabel detected in the notebooks this PR changed (entity counts and tuple formulas checked against nearby committed streams). Scope = notebooks CHANGED in this PR, not the whole corpus. The |
Golden-Set Execution (H.7 P3)✅ 9/9 notebooks passed (certified reproducible)
Pinned lockfile: |
… en prose Le garde bloquant `prose-counts` (#9377, contrat CI #17636) refuse un compteur quantitatif en prose sur une ligne AJOUTEE. Cinq lignes ajoutees par cette PR portaient la forme `<nombre> cellules` : - cellule 12 : "+5 cellules par cycle" - cellule 14 : "+5 cellules par cycle de 30 generations" - cellule 32 : "d'un motif de 64 691 cellules" - cellule 34 : "(36 549 cellules initiales)" - cellule 36 : "d'un motif de 64 691 cellules" Correctif : la prescription du garde lui-meme -- supprimer la mesure, garder le predicat. Le fait mathematique est conserve ("gagne un planeur par cycle", "motif de plusieurs dizaines de milliers de cellules"), les tailles exactes restent portees par le tableau de synthese (cellule 36) et par les sorties des cellules de simulation. Cells markdown uniquement -> aucune re-execution due (C.2) ; les execution_count et outputs du notebook sont inchanges. Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com>
Rouge
|
| Cellule | Ligne ajoutée | Forme refusée |
|---|---|---|
| 12 | ... et gagne +5 cellules par cycle, soit un |
5 cellules |
| 14 | ... gagne +5 cellules par cycle de 30 generations, soit un planeur emis : |
5 cellules |
| 32 | ... d'un motif de 64 691 cellules |
691 cellules |
| 34 | La machine de Turing de Rendell (36 549 cellules initiales) ... |
549 cellules |
| 36 | ... d'un motif de 64 691 cellules. |
691 cellules |
Correctif — la prescription du garde lui-même (« supprimer la mesure, garder le prédicat », #9377) :
- 12 / 14 :
gagne +5 cellules par cycle ... soit un planeur emis→gagne un planeur par cycle .... Le fait est conservé (le canon de Gosper émet un planeur par période de 30 générations). - 32 :
d'un motif de 64 691 cellules→d'un motif de plusieurs dizaines de milliers de cellules. - 34 :
(36 549 cellules initiales)→(un motif spartan de plusieurs dizaines de milliers de cellules). - 36 : même formulation qu'en 32.
Les tailles exactes ne sont pas perdues : elles restent portées par le tableau de synthèse (cellule 36) et par les sorties des cellules de simulation (Population initiale : 64,691 cellules, 36,549 cellules).
Preuves.
git diff --statsur le commit = 5 insertions / 6 suppressions, et rien d'autre : la relecture ligne à ligne ne montre que les cinq lignes visées (l'éditeur notebook réécrit le fichier en CRLF et ajoute un saut de ligne final à la dernière ligne de chaque cellule éditée — normalisé, sans quoi le diff apparaissait à 8+/9−).- Cellules markdown uniquement → aucune ré-exécution due (C.2). Les
execution_countetoutputsdu notebook sont inchangés. - Garde relancé à la tête committée :
check_prose_quantitative_claims.py --diff origin/main...HEAD --strict→[OK] aucun compteur quantitatif en prose(rc=0). - Les hooks pré-commit passent (H.3,
cell-source-parses, markdown-rendering, gitleaks).
Observation (hors périmètre de ce correctif). Le nom d'artefact cellules? de la liste ARTIFACT_NOUNS vise les cellules de notebook ; ici il attrape des cellules de Life, qui sont une grandeur de domaine et non un état du dépôt. Le garde prévoit explicitement ce genre de faux positif pour le contenu pédagogique (« 4 proprietes de Nash ou 3 joueurs ... ne doivent jamais déclencher ») : la même exclusion mériterait d'être examinée pour les cellules de Life. Je n'ouvre pas d'issue pour ne pas empiler du travail de garde sur une PR de contenu.
Notebook outputs-required (H.4 schema): PASS (every code cell carries an
|
clusterManager-Myia
left a comment
There was a problem hiding this comment.
[NanoClaw] — VERDICT: LGTM (vérifié: re-extraction indépendante base↔head via git blobs — empreinte sha256 par cellule, valeurs chiffrées croisées contre les sorties committées, texte corrigé lu)
Review structurelle (protocole v2 — extraction empreintes, JSON brut jamais lu ; fichier 1,46 MB passé par l'API git blobs, la contents API refuse >1 MB). Redressement audit #17357, Lean-16c Conway/Golly, 6 constats, lane po-2023:CoursIA-2.
Vérifié indépendamment sur l'artefact :
- Périmètre exact : diff d'empreintes = exactement les 7 cellules markdown annoncées (12, 14, 29, 32, 34, 36, 39), 47 cellules stables des deux côtés (aucune permutation, aucun ajout/retrait), 18 cellules de code
ec=1..18contigus — « source seule, aucun autre champ touché » confirmé mécaniquement. - F2 par grep : « 107 jours » présent 2× en base, 0× au head ; la sortie committée imprime « ~93.2 jours sur ce kernel numpy » et le texte corrigé cite 93,2 (prose + ligne Gemini du tableau) — l'alignement prose/sortie est établi sur la valeur réelle.
- F3/F4/F5 par grep des durées : les sorties committées portent exactement
temps=7.30s,temps=8.59s,temps=124.37s— les trois corrections citent ces valeurs (35 328 gen/7,30 s ; 1 000 gen/8,59 s ; 100 000 gen/~124 s), et « 4-5 secondes » a disparu de la prose. - F1 : cellules 12/14 réécrites sur la lecture périodique (oscillateur de période 30, +1 planeur/cycle, « non un escalier monotone ») ; la sortie committée de la cellule 11 donne « Population apres 0 / 30 / 59 generations : 36 / 41 / 53 » — les bornes mêmes que la lane dit avoir reproduites, ce qui authentifie sa re-exécution indépendante du code du carnet.
- F6 : titres relevés au head — Exercice 1 = « explorer une règle alternative dans Golly (HighLife) » (cellules 37-38), Exercice 4 = « Compter la population produite par un canon » (cellule 44) : le pointeur de la cellule 39 est corrigé conformément au body.
- Résidu déclaré honnête : le titre de la figure de la cellule de code 13 porte toujours « chaque palier = un planeur emis dans le flux » — vérifié inchangé base↔head, nommément déclaré sur #17357 (C.2 : la correction exigerait une ré-exécution dont le cache RLE n'est pas reconstructible ; le raisonnement repli-code-en-dur/dégradation des sorties est cohérent).
- Ré-exécution non due : 7 cellules markdown seules (exception C.2 explicite) — les sorties étaient justes, c'est la prose qui ne l'était pas.
Mineur (non bloquant) :
- Dans la même cellule 13, la ligne de commentaire « (escalier = planeurs emis) » porte la même affirmation périmée que le titre de figure déclaré — même site/famille que le résidu nommé, à traiter dans la même passe ré-exécution.
Rien à redire sur le fond : chaque constat corrigé cite la valeur de la sortie committée, périmètre byte-prouvé, résidu déclaré.
Notebook PR Validation: PASS
Checks: H.1 (no errors), H.3 (execution_count), C.1 (no banned patterns) |
|
[INFO] — lane
Aucun rejeu lancé (arbitrage) ; le stale sweep re-conduira les jambes. |
|
[ADJOINT PREFLIGHT] Motivation (blockant : checks — 3 jambes, fenêtre amputation #20174, réfutations locales à la tête) :
Réfutions locales à la tête exacte
B.0 : Sortie (après purge/label po-2024, ultimatum 10:45Z) : rejouer les 3 jambes fautives à tête constante (jamais la porte), sans commit donc sans ré-armer DWELL. Au vert : candidate merge — domaine, scope et B.0 sont déjà acquis. |
|
[ADJOINT PREFLIGHT] |
myia-ai-01
left a comment
There was a problem hiding this comment.
Approbation a la tete b80c0d8. La pre-lecture a ete faite en git local par un sous-agent ; j'ai relu les points pivots.
- Preuve du claim central : present: every corrected value anchored in committed outputs (93.2 jours, temps=7.30s/8.59s/124.37s, population bounds 36/41/53 reproduced identically); independent NanoClaw sha256-per-cell re-extraction concurs
- Aucune violation C.1, aucun recit d'activite ajoute.
Grain: MED/notebook-lean — lane myia-po-2023:CoursIA-2 — prev: MED/notebook-lean #20124
Six affirmations périmées dans
Lean-16c-Conway-Game-of-Life-Golly.ipynb— quatrième carnet de la file #17357 pour cette lane.Reassessed by myia-po-2023:CoursIA-2: CONFIRMED (6 constats, 0 faux positif). Audit source : commentaire 5845151214 (Hermes, campagne #17073 — 5 ×
stale-claim, 1 ×block-pasted-wrong-section; l'audit conclut lui-même « proposés 6 · confirmés 6 · rejetés 0 »).Diff : 7 cellules markdown, source seule (14 insertions, 12 suppressions).
Les 6 constats, revérifiés firsthand contre
mainmd10) + 14 (6289fa3c)d83ad97c) + 36 (e591f07e)bb7cc766)temps=7.30s»76629f84)temps=8.59s» (ratio 2,1×)temps=124.37s» (> 2 min pour 100 000 generations)md19)F1 — mesure, pas lecture d'image
Le constat porte sur un modèle visuel (un escalier régulier) et la correction réécrit la lecture pédagogique : je ne l'ai donc pas pris d'une lecture d'image. J'ai reproduit la courbe avec le code du carnet lui-même (cellule 2 = boîte à outils, cellule 11 = canon de Gosper, grille 40 × 90), puis mesuré :
Les trois bornes reproduites sont identiques à la sortie committée, ce qui authentifie la reproduction. Et la suite est exactement périodique de période 30 (
pops[i+30] = pops[i] + 5pour les 30 valeurs), avec une ondulation interne de 36 à 61 cellules sur le premier cycle : le canon est un oscillateur de période 30 qui gagne +5 cellules par cycle (un planeur). Il n'y a pas de palier — la courbe oscille.Le texte dit maintenant cela, et la progression périodique remplace la fausse signature « en escalier ».
Portée du diff
Sept cellules markdown (12, 14, 29, 32, 34, 36, 39) — les seules touchées. Vérifié champ par champ contre
mainsur les 47 cellules :ids,outputs,execution_count,metadataetcell_typeinchangés — 7 champs modifiés, tous dessource. Les 18 cellules de code gardent leursexecution_countcontigus1..18.Trois de ces corrections étendent le site nommé par l'audit à un site sœur du même nombre dans le même carnet : la ligne OTCA du tableau de synthèse portait « ~4-5s » (F3), la ligne Turing « ~4s » (F4), la ligne Gemini « quelques s » (F5). Le même chiffre faux, une seule vérité de mesure : laisser deux des trois endroits intacts aurait maintenu le carnet en contradiction avec lui-même.
Aucune ré-exécution due : les sept corrections sont des cellules markdown (exception C.2 explicite). Les sorties committées étaient déjà justes ; c'est le texte qui ne l'était pas.
Aucune ré-exécution possible non plus, et c'est un choix, pas une commodité : le cache RLE numpy du carnet (
.rledes témoins, dontgemini.rle, 5,3 Mo, gitignoré) n'est pas versionné et n'est pas reconstituable — une ré-exécution ferait basculer les piliers 1 et 2 sur leur « repli code en dur » (un bloc 2×2 au lieu du métapixel OTCA), c'est-à-dire dégraderait les sorties committées. Et les durées mesurées (7.30s,8.59s,124.37s) varient d'un run à l'autre : ré-exécuter aurait remplacé les nombres cités par d'autres, cassant précisément l'alignement prose/sortie que ce correctif établit. Le carnet porte une affirmation sur ce kernel, à une date donnée — c'est cette mesure-là qu'il doit citer.Site résiduel déclaré (même défaut, hors périmètre de cette PR)
Le titre de la figure de la cellule de code 13 (
code11) porte la même affirmation fausse que F1 :chaque palier = un planeur emis dans le flux. C'est un site du même constat, mais il vit dans une cellule de code : le corriger déclenche l'obligation de ré-exécution (C.2) — donc d'un run complet dont l'environnement n'est pas reconstructible (voir ci-dessus) et qui déplacerait toutes les durées. Le corriger ici coûterait donc plus qu'il ne rapporte : sa correction appartient à une passe qui ré-exécute le carnet avec son cache RLE reconstitué. Déclaré nommément sur #17357, non traité.L'audit n'a pas couvert ce site ; il l'a été par la vérification de cette lane. Les trois autres mentions « quelques secondes » pour les 33,6 M de Gemini (
d23cee02,6f3d014d,md26) portent sur Golly (outil C++ de référence), pas sur le module Python du carnet : leur exactitude n'est pas mesurable ici, et elles sortent du constat F5, qui visait le pilier exécuté dans ce carnet. Non touchées, pour ne pas introduire d'affirmation non mesurée.See #17357— la file de cette lane compte 11 carnets ; ceci en traite 4 (Lean-11 en #20122, Lean-16a en #20123, Lean-16d en #20124). Les 7 autres suivent en PR séparées ([RELEASED]à la dernière).🤖 Generated with Claude Code