Repository navigation
fix(notebook,#17357): Lean-16b -- 4 constats d'audit (F1/F3/F4/F5) - #20115
Conversation
…/F5) Revérification des 6 constats de l'audit c.5844346305 (partition Hermes, campagne #17073) sur `origin/main` avant correction. Corrigés (markdown uniquement, cellules 0/11/13 - aucune cellule de code touchée, donc aucune ré-exécution due au titre de C.2) : - F1 `stale-claim` (cellule 13) : la table annonçait « Taille (en-tête) | 2 048 x 2 048 » alors que le witness rendu juste en dessous mesure `en-tete : 2058 x 2058`. La ligne porte désormais la valeur mesurée et son libellé dit de quel objet elle parle (l'en-tête du fichier `.rle`), ce qui la distingue de la taille propre du métapixel (2 048²) donnée en puce. - F3 `stale-claim` (cellule 13) : « Population (initiale) | ~50 000 cellules » contre `cellules vivantes : 64 691` dans le witness — écart ~29 %. Valeur mesurée reportée. - F4 `progression-break` (cellule 11) : l'intro annonçait Acte II = « se reproduire » (Gemini) et Acte III = « calculer » (CPU), alors que les sections livrent II = CALCUL (`acte2-cpu`, machine de Turing de Rendell) et III = REPLICATION (`acte3-gemini`). La table de synthèse (`synthese-piliers`) confirme l'ordre livré. Les deux puces sont remises dans l'ordre livré. - F5 `navigation-misplaced` (cellule 0) : le lien `<<` pointait vers Lean-15 Grothendieck, sautant Lean-16a. La navigation de Lean-16a elle-même (`[<< Lean-15 ...] | [Lean-16b Game of Life >>]`) établit que 16a est bien le prédécesseur immédiat de 16b. Lien corrigé. Non corrigé dans cette PR, et pourquoi : - F2 `stale-claim` : **déjà levé par #20015** (en file de merge), qui remplace les trois occurrences de « OTCA 70 KB » par « ~165 Ko » (cellules 19, 47, 51). Rien à faire ici. - F6 `stale-claim` (cellule 50) : **réel et encore ouvert**. La cellule revendique « Le seul sorry restant est P5 » alors que son propre compteur affiche 2 ; les deux lignes comptées sont en réalité de la prose dans des commentaires de bloc (`sorry-free: ...` L6744 et `sorry-free even if ...` L6832 de `HashlifeCorrectness.lean`), faux positifs du motif `^\s*sorry\b` que la cellule emploie. Vérifié firsthand : ces deux lignes sont les seules correspondances du motif, donc 0 sorry réel. La cellule 50 est **réécrite par #20015** (ré-exécution + en-tête de commentaire) : la corriger depuis `main` produirait un conflit. Elle sera traitée dans la PR de suite, après le merge de #20015 — c'est l'ordre demandé au dispatch. Reassessment : `Reassessed by myia-po-2027:CoursIA` — F1 CONFIRMED, F3 CONFIRMED, F4 CONFIRMED, F5 CONFIRMED, F2 déjà levé par #20015, F6 CONFIRMED mais différé (conflit de cellule avec #20015). Gates locaux : `check_cell_source_parses` 0 finding · `check_exec_sequence` CLEAN (1..N, 0 DIRTY) · `check_source_collapse` / `check_output_collapse` 0 flagged · `check_split_reading_cells` clean · `check_interp_positioning` 0 finding · `check_link_label_agreement` --json : 0 finding sur ce fichier. See #17357 (pas `Closes` : F6 reste ouvert). Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Path-collision (organ #13359/#13615)Cette PR #20115 (
Le verdict terminal (#15578) signale qu'un cote de la paire est deja sur |
|
No organ-duplication: no added def/class collides with another series organ API (scripts/audit/organ_api_index.yaml). Detector: |
github-actions
Bot
added
the
consecutive-code-cells
|
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: |
Notebook outputs-required (H.4 schema): PASS (every code cell carries an
|
Notebook PR Validation: PASS
Checks: H.1 (no errors), H.3 (execution_count), C.1 (no banned patterns) |
|
[ADJOINT PREFLIGHT] |
2 participants
Grain: MED/notebook-lean -- lane myia-po-2027:CoursIA -- prev: DEEP/lean #20004
Suite de l'audit Hermes
c.5844346305(partition Hermes, campagne #17073) surLean-16b-Conway-Game-of-Life-Lean.ipynb: 6 constats. Chacun a été revérifiéfirsthand sur
origin/mainavant toute correction (protocoleaudit-reassessment) —jamais depuis le texte de l'audit.
Reassessed by myia-po-2027:CoursIA — F1 CONFIRMED · F3 CONFIRMED · F4 CONFIRMED ·
F5 CONFIRMED · F2 déjà levé par #20015 · F6 CONFIRMED mais différé (voir plus bas).
Corrigés — markdown uniquement (cellules 0/11/13)
Aucune cellule de code n'est touchée : la re-exécution C.2 n'est donc pas due, et le
diff ne porte que de la prose.
stale-claimen-tete : 2058 x 2058stale-claimcellules vivantes : 64 691(écart ~29 %)progression-breakacte2-cpu) et III = REPLICATION (acte3-gemini)navigation-misplaced[<< Lean-15 Grothendieck]F1 — la ligne de table portait la valeur du métapixel nu (2 048², celle de LifeWiki)
sous un libellé qui annonce l'en-tête du fichier. Elle porte désormais la valeur
mesurée (2 058 x 2 058) et un libellé qui dit de quel objet elle parle, ce qui la
distingue de la taille propre du métapixel — laquelle reste donnée en puce à 2 048²,
comme dans la prose de la cellule.
F4 — l'ordre corrigé est celui que la table de synthèse
synthese-piliersconfirmedéjà (« Remettons les trois actes dans l'ordre où on vient de les voir : I OTCA /
II Turing / III Gemini ») et celui qu'annonce le plan du carnet. La puce II gagne au
passage la machine de Turing de Rendell (2000), qui est le premier moteur cité par
le titre de la section
acte2-cpulivrée.F5 — la preuve est dans le carnet voisin : la navigation de Lean-16a se lit
[<< Lean-15 ...] | [Lean-16b Game of Life >>], donc 16a s'insère bien entre 15 et 16b.Le lien
<<de 16b sautait une position.Non corrigé ici, et pourquoi
F2 — déjà levé par #20015, en file de merge. Cette PR-là remplace les trois
occurrences de « OTCA 70 KB » par « ~165 Ko » (cellules 19, 47 et 51). Rien à faire ici,
et le dire évite une seconde correction du même fait.
F6 — réel, encore ouvert, différé. La cellule 50 revendique « Le seul sorry restant
est P5 » alors que son propre compteur affiche 2 — contradiction visible pour
l'apprenant. Mesuré firsthand : les deux lignes comptées sont de la prose dans des
commentaires de bloc,
sorry-free: ...(L6744) etsorry-free even if ...(L6832) deHashlifeCorrectness.lean, que le motif^\s*sorry\bemployé par la cellule attrapeparce que le tiret crée une frontière de mot. Ces deux lignes sont les seules
correspondances du motif dans le fichier, donc 0 sorry réel.
Elle n'est pas corrigée dans cette PR parce que la cellule 50 est réécrite par
#20015 (ré-exécution + en-tête de commentaire) : la corriger depuis
mainproduiraitun conflit garanti. Elle part dans la PR de suite, après le merge de #20015 — c'est
l'ordre demandé au dispatch, et c'est le seul constat des six qui soit dans ce cas.
Validation
Les quatre corrections portent sur des lignes de source que #20015 ne touche pas
(vérifié : aucune de ces lignes n'apparaît dans son diff) : les deux PR peuvent donc
merger dans n'importe quel ordre sans conflit.
check_cell_source_parses.py: 0 findingcheck_exec_sequence.py: CLEAN (1..N, 0 DIRTY, 0 UNORDERED / NOT_FROM_1 / GAP / DUPLICATE)check_prose_quantitative_claims.py --diff origin/main...HEAD: [OK] aucun compteur quantitatif en prose (bloquant)check_source_collapse.py/check_output_collapse.py: 1 carnet changé, 0 flaggeddetect_md_content_loss.py --base origin/main: 0 finding (33 → 33 cellules markdown, 45 512 → 45 600 caractères normalisés — croissance, pas de perte)check_output_failure_text.py: 0 regressedcheck_split_reading_cells.py: clean ·check_interp_positioning.py: 0 findingcheck_duplicate_sections.py: 0 finding ·check_latex_control_chars.py: 0 occurrencecheck_link_label_agreement.py --json: 0 finding sur ce fichier (le nouveau libellé de navigation est accepté)#13326(source non compilable), strips — tous PassedSee #17357 (pas
Closes: F6 reste ouvert).🤖 Generated with Claude Code