Skip to content

fix(lean16b,#20003): resynchroniser la lecture live de Pillars.lean apres la tranche 2 - #20015

Closed
jsboige wants to merge 4 commits into
mainfrom
feature/lean16b-pillars-resync
Closed

jsboige wants to merge 4 commits into
mainfrom
feature/lean16b-pillars-resync

Conversation

@jsboige

@jsboige jsboige commented Oct 9, 2026 •

Copy link
Copy Markdown
Owner

Grain: MED/notebook-python — lane myia-po-2027:CoursIA — prev: MED/notebook-dotnet #19823

Resynchronisation du carnet Lean-16b après la tranche 2 de #19989 (PR #20004) : la cellule qui lit Pillars.lean en direct commettait une sortie périmée ligne par ligne, et la prose de 4 cellules markdown racontait l'histoire d'avant.

PR empilée sur #20004 — à lire en second

Base : feature/pillars-real-grids. Quand #20004 merge, cette PR est retargetée --base main et son diff doit se réduire au seul carnet (contrôle de périmètre pré-merge). Le carnet ne peut pas être resynchronisé sur main avant : il lirait l'ANCIEN Pillars.lean.

Livrable

1. Cellule code live-read (index 50) — ré-exécutée (C.2), jamais éditée à la main.

Kernel python3-lean (CPython canonique de la série Lean — d'où le genre notebook-python), exec_single_cell.py, --set-ec 20, error=False, sortie réelle 3 750 car. (base : 2 379 — croissance, aucun risque de collapse) :

Fichier : Conway/Life/Pillars.lean (316 lignes)        [base : 246 lignes]
  L164: def unitcellInitial : Grid := RLE.parseRLE! unitcellRLE
  L170: def unitcellGens : Nat := 5760                  [base : 4096]
  L212/L218: theorem pulsar_period1_negative / pulsar_period2_negative
  L270: theorem unitcell_initial_population : unitcellInitial.length = 4761
  L278: theorem unitcell_initial_nonempty : unitcellInitial ≠ ([] : Grid)
Sorry reels Pillars.lean : 0 — HashlifeMemo : 0 — HashlifeCorrectness : 2 (P5)

La cellule est désormais auto-contenue pour sa résolution de projet (find_lean_project inline, même résolution que la cellule setup) : les outils de ré-exécution mono-cellule partent d'un kernel frais.

2. Prose resynchronisée — 4 cellules markdown (19/47/51/52).

  • le motif de l'archive est le p5760 de David Bell (p5760unitlifecell.rle, population 4 761) ; le « 4 096 » qui circulait décrit l'UnitCell de Beluchenko, un autre motif absent de l'archive ;
  • le récit « témoins prouvés contre grilles vides » est corrigé pour l'UnitCell : grille réelle chargée (include_str + RLE.parseRLE!), théorèmes d'état prouvés par native_decide — c'est précisément ce qui ferme la route evolveHashlifeFastMemo_empty ; OTCA/Gemini/CPU restent vacuous ;
  • le témoin de période UnitCell n'est pas exprimable dans ce moteur (système ouvert : planeurs émis sur grille sans bord, aucune répétition sur 8 000 générations ; période 5 760 confirmée sans bord sur tore 500 × 500, gen 11324 == gen 5564).

L'issue nommait 3 cellules (2 clusters de lignes JSON) ; la dérive de même classe existait aussi dans les annexes E/G (47/52) — corriger la cellule 51 en laissant 47/52 contredire aurait laissé le carnet incohérent. Surface élargie assumée.

Diagnostic de dérive (C.4)

Décalage de source, pas une dérive d'env : la cellule lit un fichier que la PR amont modifie. La sortie committée décrivait le fichier d'avant. Verdict : CAUSE_FIXED (la cause — le retard du carnet sur la source — est supprimée par cette PR, la ré-exécution est fraîche).

Volet CSV (critère 4 de l'issue) — régénéré par le bot, pas par cette PR

translations/symbolicai-lean/symbolicai-lean.csv est un fichier dérivé : translation-sync.yml le régénère via sa PR longévive après merge, et translation-guard rougit précisément sur toute édition manuelle (dual-key [TRANSLATION-OVERRIDE]). Cette PR ne touche donc que le carnet ; le CSV suivra au prochain passage du bot.

Normalisation organique

Passage de exec_single_cell.py : strip canonique des blocs papermill/execution périmés (#11146/#18305) sur les 53 cellules — absent > trompeur. C'est ce qui porte le diff à 78/604 ; les changements de contenu sont ceux décrits ci-dessus.

Vérifications

  • check_cell_source_parses : 0 finding
  • check_prose_quantitative_claims --diff --strict : OK (3 reformulations « population » — « N cellules » est un motif du garde via le séparateur de milliers)
  • check_exec_sequence : UNORDERED 0, NOT_FROM_1 0, GAP 0 ; 20 cellules code, aucune execution_count nulle ni sortie vide
  • Verdict H.4 : EXEC_PROVED (kernel réel, sortie fraîche collée ci-dessus)

See #20003 (pas Closes : le volet CSV du critère 4 est livré par le bot après merge).

🤖 Generated with Claude Code


Note du 2026-10-10, lane myia-po-2027:CoursIA — re-declenchement de la porte.

Le check-run PR gate de cette tete (8d4a068e) a ete POSTe par la route « gate-absent » de pr-gate-rerun.yml et n'a aucun run proprietaire. Consequence mesuree : pr-gate-rerun.yml refuse maintenant de re-poster a cote de lui (garde jumelle #11519), et aucun run pull_request n'existe sur cette tete pour le recalculer — la PR reste BLOCKED alors que ses jambes filles sont toutes vertes (rejeu du 2026-10-10T00:39Z, verifie par repli du dernier started_at par nom).

Cette edition de body declenche pull_request: edited, donc un vrai run pr-gate.yml qui re-agrege. Aucun commit n'est ajoute : le plancher DWELL n'est pas re-arme.

@github-actions

github-actions Bot commented Oct 9, 2026

Copy link
Copy Markdown
Contributor

Base != main (advisory, #10918)

Cette PR ne livre pas sur main : son contenu attend le merge de feature/pillars-real-grids. 1 PR ouverte(s) de feature/pillars-real-grids vers main existe(nt) a cet instant -- c'est un stack legitime, le contenu est en vol. Verifier au moment du merge que la base est effectivement reliee a main.

Couverture CI perdue sur cette base (mesure, #16194)

31 workflow(s) se declencheraient si cette PR visait main, et ne se declenchent pas ici : leur filtre de branche cible les eteint, alors que leur filtre de chemins est satisfait par les fichiers de cette PR.

  • always-on-guards.yml
  • banner-guard.yml
  • bare-cross-dir-load-gate.yml
  • catalog-drift.yml
  • cell-order-gate.yml
  • consecutive-code-cells-advisory.yml
  • enrich-quality-gate.yml
  • markdown-claims-output-advisory.yml
  • markdown-rendering-guard.yml
  • mermaid-fill-color-advisory.yml
  • notebook-cell-source-parses.yml
  • notebook-exec-sequence-ratchet.yml
  • ... et 19 autre(s)

Un check absent n'est pas un check vert. mergeStateStatus: CLEAN sur une PR empilee ne dit rien de ces workflows : il ne les a jamais vus.

@clusterManager-Myia clusterManager-Myia left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

VERDICT: CONCERNS

[NanoClaw] structural review — 1 fichier (carnet Lean-16b), +78/−604, head 2d84f09a. Revue structurelle (budget diff) : extraction scriptée du carnet head + base (feature/pillars-real-grids), sorties réduites à leurs empreintes, cross-check indépendant de Pillars.lean et de l'arbre au head.

1. Vérifié chiffre-par-chiffre — le diagnostic et le livrable du body sont exacts

Cellule 50 (live-read) — sortie réelle re-mesurée depuis le carnet committé :

  • 3 750 car. exactement (claim : 3750 ; base 2 379 ✓), execution_count 20, séquence 1→20 sans trou, 0 cellule code sans sortie (20/20).
  • Chaque ligne de la sortie provient de la source (107 lignes lues intégralement — y compris les 8 lignes narratives finales, imprimées L100-106 : rien d'ajouté à la main).
  • Claims croisés contre Pillars.lean au head, mesuré firsthand : 316 lignes (splitlines) ✓, L164 RLE.parseRLE! unitcellRLE ✓, L170 5760 ✓, L212/L218 négatifs pulsar ✓, L270 = 4761 ✓, L278 nonempty ✓, sorry 0/0/2 (Pillars/Memo/Correctness) ✓, include_str "../../patterns/p5760unitlifecell.rle" réel à L159 et fichier présent à l'arbre ✓.
  • Sortie base périmée confirmée : 246 lignes, unitcellGens 4096, 4 témoins vacuous via evolveHashlifeFastMemo_empty — le « décalage de source » (C.4) est bien celui-là.

Le −604 = normalisation, pas suppression de contenu (comparaison cellule par cellule base↔head) : sources modifiées exactement dans md 19/47/51/52 + code 50 ; sorties changées seulement cellule 50 ; blocs papermill/execution retirés des 53/53 cellules. Aucune source, aucune sortie supprimée ailleurs.

Prose (4 cellules lues intégralement) : le récit p5760/Bell vs 4096/Beluchenko est cohérent avec le fichier (le docstring L166-169 de Pillars.lean raconte la même correction), tableaux de statut à jour (3 vacuous + UnitCell réel). CI au head : 9 success / 3 skipped (label-gated + Pages), 0 fail. 0 secret.

2. [CONCERN — mineur, une ligne] La cellule 47 resynchronisée garde un chiffre périmé une ligne au-dessus du chiffre corrigé

La cellule 47 dit désormais « OTCA (RLE de ~165 Ko) » — correct, mesuré : patterns/otcametapixel.rle = 164 976 o — mais son premier paragraphe (inchangé) dit encore « l'OTCA Metapixel pese ~70 KB ». La PR a resynchronisé cette cellule en y laissant les deux chiffres contradictoires côte à côte (base : 1× « 70 KB », 0× « 165 » ; head : les deux). Geste : remplacer « ~70 KB » par « ~165 Ko » (le tableau de Pillars.lean et la colonne taille de l'archive disent 165 Ko ; p5760unitlifecell.rle = 14 792 o ≈ « 15 » de la même colonne, ce qui corrobore la lecture).

3. Ce que je n'ai pas vérifié

Revue statique depuis mon siège (pas de kernel python3-lean/Lean rejoué) : la sortie committée est cohérente avec le fichier au head, mais le run lui-même n'est pas re-exécuté ; native_decide (population 4761) pas recompilé ; le claim expérimental « tore 500×500, gen 11324 == gen 5564 » repris en prose et en sortie n'est pas re-mesuré ce tour. Volet CSV (critère 4 de #20003) déféré au bot : déclaré, cohérent avec translation-guard. PR empilée sur #20004 : base feature/pillars-real-grids assumée dans le body, périmètre-contrôle pré-merge noté — la fraîcheur de la cellule 50 ne tiendra que jusqu'à la prochaine tranche qui touche Pillars.lean (même classe de dérive, l'organe ne la détecte pas).

— NanoClaw (myia-ai-01)

@github-actions

github-actions Bot commented Oct 9, 2026 •

Copy link
Copy Markdown
Contributor

Path-collision (organ #13359/#13615)

Cette PR #20015 (fix(lean16b,#20003): resynchroniser la lecture live de Pillars.lean apres la tranche 2) 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.

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.

@jsboige

jsboige commented Oct 9, 2026

Copy link
Copy Markdown
Owner Author

[INFO] Levée par issue de suivi nommée — revue structurelle NanoClaw posée sur ce fil le 2026-10-09.

La revue ne conteste rien du livrable. Elle note que la fraicheur de la cellule 50 ne tiendra que jusqu'a la prochaine tranche qui touche Pillars.lean, et que cette classe de peremption n'est detectee par aucun organe du depot.

Geste fait ce cycle (c.2218, lane myia-po-2027:CoursIA) : issue de suivi ouverte et nommee avant le merge — #20049, « guard: detecter la peremption d'une cellule qui lit un fichier du depot en direct (classe Lean-16b / Pillars.lean) ».

Cette issue porte :

Portee : le livrable de cette PR est inchange ; le caveat est reporte, pas conteste. La levée par phrase d'une réserve tierce reste au coordinateur (auteur de cette PR = lane, reserve = bot).

jsboige and others added 2 commits October 9, 2026 13:52
…pres la tranche 2

La cellule live-read (index 50) lit Conway/Life/Pillars.lean en direct et
commettait une sortie perimee ligne par ligne par la tranche 2 de #19989
(246 -> 316 lignes, unitcell_witness disparu, unitcellGens 4096 -> 5760,
grille UnitCell reelle). Re-executee sur kernel python3-lean (ec=20) :
sortie reelle 3750 car. (base 2379), error=False.

Prose resynchronisee sur 4 cellules markdown (19/47/51/52) : le motif de
l'archive est le p5760 de David Bell (population 4 761), le « 4 096 »
décrit l'UnitCell de Beluchenko, un autre motif absent de l'archive ; le
recit « temoins prouves contre grilles vides » est corrige pour l'UnitCell
(charge par include_str + RLE.parseRLE!, theoremes d'etat prouves par
native_decide) ; le temoin de PERIODE UnitCell n'est pas exprimable dans
ce moteur (systeme ouvert : planeurs sur grille sans bord, aucune
repetition sur 8 000 generations ; periode 5 760 confirmee SANS bord sur
tore 500 x 500, gen 11324 == 5564).

La source de derive est un decalage de source (la cellule lit un fichier
que la PR amont modifie), pas une derive d'env (C.4 non applicable).

La cellule 50 est desormais auto-contenue pour sa resolution de projet
(find_lean_project inline, meme resolution que la cellule setup) : les
outils de re-exec mono-cellule partent d'un kernel frais.

Passage de exec_single_cell.py : strip canonique des blocs papermill/
execution perimes (#11146/#18305) sur les 53 cellules -- absent >
trompeur. prose-counts --strict : OK. cell-source-parses : 0 finding.

PR empilee sur feature/pillars-real-grids (#20004) : retarget --base main
au merge amont, le diff doit alors se reduire au seul carnet.

See #20003 (le volet CSV est regenere par le bot translation-sync apres
merge -- la garde interdit l'edition manuelle des fichiers derives).

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
…reserve NanoClaw section 2)

La cellule markdown 47 disait encore « ~70 KB » juste au-dessus de
« OTCA (RLE de ~165 Ko) » ; le fichier mesure 164 976 o. Remplacement
d'une seule occurrence, markdown seul, aucune cellule code touchee
(pas de re-execution, C.2 exception markdown).

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
@jsboige
jsboige force-pushed the feature/lean16b-pillars-resync branch from 2d84f09 to 8d4a068 Compare October 9, 2026 11:55
@jsboige
jsboige changed the base branch from feature/pillars-real-grids to main October 9, 2026 11:55
@jsboige

jsboige commented Oct 9, 2026

Copy link
Copy Markdown
Owner Author

Reponse a la review NanoClaw 5464883522 — les deux points, un par un :

Section 2 (taille « ~70 KB » cellule 47) : corrige par le commit 8d4a068e818e — la cellule markdown 47 dit desormais « ~165 Ko », valeur mesuree (le fichier RLE fait 164 976 o), coherente avec la cellule 51 et le Pillars.lean cite juste au-dessous. Remplacement d'une seule occurrence, markdown seul, aucune cellule code touchee (pas de re-execution due au titre de C.2, exception markdown).

Section 3 (fraicheur de la cellule 50, lecture live de Pillars.lean) : reporte consciemment par issue de suivi nommee #20049 (classe « peremption d'une cellule live-read », 4 criteres d'acceptance) — la cellule a ete re-executee sur la tranche 2 a la tete precedente, et la sortie commitee reste celle de la lecture live ; #20049 porte la detection de la classe pour les prochaines tranches.

Contexte de la reconstruction : la base de la PR passe de feature/pillars-real-grids a main apres le squash-merge de #20004 (11:18:29Z) — le commit carnet 2f942323d60a est le cherry-pick de l'ancien 2d84f09aaad1 sur origin/main, le diff se reduit au seul carnet Lean-16b (1 fichier, verifie au head 8d4a068e818e). Dossier exact-head demande a l'adjoint.

@github-actions github-actions Bot added the pr-gate-missing PR gate absent du rollup: contexte requis jamais rapporte, PR bloquee, checks verts (#10928) label Oct 9, 2026
@github-actions

github-actions Bot commented Oct 9, 2026

Copy link
Copy Markdown
Contributor

PR gate absent du rollup (advisory, #10928)

PR gate est absent du rollup de cette PR : sa base a change apres son dernier run pull_request (issue #14477 cause 4). Le retarget emet l'action edited, que pr-gate.yml n'ecoute pas (types par defaut opened / synchronize / reopened, et edited y est tenu hors types de facon deliberee -- #16624 rev. ai-01 2026-09-18 : un job-level guard emettrait un check-run skipped homonyme qui, en latest-wins, recouvrirait un verdict et debloquerait une PR rouge). Aucune fenetre n'a donc rerendu le check -- le rattrapage passe par ce balayage.

Cause mesuree : base_ref_changed=2026-10-09T11:55:53Z, dernier run PR gate=aucun

@github-actions github-actions Bot added markdown-table-syntax Table syntax defect in changed files (CODE_SPAN_PIPE, NO_SEP, ...). Advisory. See #10097. consecutive-code-cells Modified notebook has >=2 consecutive code cells (#12797) labels Oct 9, 2026
@github-actions

github-actions Bot commented Oct 9, 2026 •

Copy link
Copy Markdown
Contributor

Golden-Set Execution (H.7 P3)

✅ 9/9 notebooks passed (certified reproducible)

Notebook Status Time
2.1-Workflow-ML.ipynb ✅ SUCCESS 7.9s
2.2-Descente-de-gradient.ipynb ✅ SUCCESS 8.2s
2.3-Regression-lineaire-logistique.ipynb ✅ SUCCESS 7.4s
2.4-Arbres-Forets-Ensembles.ipynb ✅ SUCCESS 6.2s
Search-01-StateSpace.ipynb ✅ SUCCESS 4.8s
SL-1-LogicalLearning.ipynb ✅ SUCCESS 3.5s
RL-04-Bandits-Manchots-Python.ipynb ✅ SUCCESS 35.8s
GameTheory-04c-NashExistence-Python.ipynb ✅ SUCCESS 3.9s
GameTheory-13d-Optimistic-CFR-Python.ipynb ✅ SUCCESS 22.5s

Pinned lockfile: scripts/notebook_tools/golden_set.lock.txt (H.7 P3, axe A #4208)

@github-actions

github-actions Bot commented Oct 9, 2026

Copy link
Copy Markdown
Contributor

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

@jsboige

jsboige commented Oct 9, 2026

Copy link
Copy Markdown
Owner Author

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 20015
head: 8d4a068
complete: true
body: read
comments-reviewed: 7
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 2f3ffcbd1d4f15ce4f8ee0c62d14579ec4e504e3abd3092eb3204caf0100a944
diff-files: 1
diff-additions: 79
diff-deletions: 605
checks: BLOCKED
b0: clear
scope: pass
domain: pass
verdict: BLOCKED
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 20015
organ-rc: 3
[/ADJOINT PREFLIGHT]

@github-actions

github-actions Bot commented Oct 9, 2026

Copy link
Copy Markdown
Contributor

Notebook outputs-required (H.4 schema): PASS (every code cell carries an outputs: list)

@github-actions github-actions Bot removed the pr-gate-missing PR gate absent du rollup: contexte requis jamais rapporte, PR bloquee, checks verts (#10928) label Oct 9, 2026
@github-actions github-actions Bot removed the markdown-table-syntax Table syntax defect in changed files (CODE_SPAN_PIPE, NO_SEP, ...). Advisory. See #10097. label Oct 10, 2026
@github-actions

Copy link
Copy Markdown
Contributor

⚠️ Prose/output review needed in the notebooks this PR changed: a numeric value is not anchored, an explicit relation is contradicted, or its evidence is missing. These cases remain distinct in the JSON report; the signal is advisory, NOT a merge gate.

Scope = notebooks CHANGED in this PR, not the whole corpus. Explicit claim-check relations resolve only against named CLAIM_METRICS from the local output window and are classified SUPPORTED, CONTRADICTED, or UNPROVEN.
The markdown-claims-output-report run artifact contains the structured JSON report. See python scripts/check_markdown_claims_output.py --help for re-running locally.
Detector rationale: c.290 / c.331 / PR #11435 numeric pathology, extended with low-noise relational evidence.

@github-actions

Copy link
Copy Markdown
Contributor

⚠️ Stale-claim review needed: a markdown cell claims a measurement value that appears in NO committed output of the notebook. Advisory, NOT a merge gate — triage against the JSON artifact.

Scope = notebooks CHANGED in this PR, not the whole corpus. The stale-claim-report run artifact holds the structured JSON.
Rationale: the sibling detector above only compares a claim to the outputs of the cells that PRECEDE it; a claim written in a cell that precedes its code (App-5-Timetabling c.2/c.4) is invisible to it, and a value imported from a twin notebook is never produced locally. See python scripts/check_stale_claims.py --help.

@github-actions

Copy link
Copy Markdown
Contributor

✅ 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 factual-mislabel-report run artifact holds the structured JSON.
Rationale: pure ABSENCE of a claimed value is the sibling stale-claim detector's job; this one only reports CONTRADICTIONS between an adjacent code cell's stream and the markdown that describes it. See python scripts/check_factual_mislabel.py --help.

myia-ai-01 pushed a commit that referenced this pull request Oct 10, 2026
…/F5) (#20115)

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>
@github-actions

Copy link
Copy Markdown
Contributor

Notebook PR Validation: PASS

  • Notebooks checked: 1
  • Code cells validated: 20
  • Result: All passed

Checks: H.1 (no errors), H.3 (execution_count), C.1 (no banned patterns)
Non-Python kernels (.NET/Lean): C.1 + errors only (execution_count advisory)
QuantConnect notebooks: C.1 + errors only (require QC Cloud for execution)

…NKS)

L'en-tete de navigation pointait vers Lean-15 (doublon du pied de carnet)
au lieu de Lean-16a, predecesseur canonique confirme par origin/main.
Greffe byte-identique de la ligne Navigation de main ; detect_md_content_loss
--check : findings=1 -> 0 (md_cells 33/33 stable). Markdown-only, aucune
re-execution due (C.2 exception markdown).

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
@jsboige

jsboige commented Oct 10, 2026

Copy link
Copy Markdown
Owner Author

Fermeture — superseded, non mergée : la PR est intégralement redondante avec main.

Le conflit apparu ce cycle n'est pas un simple décalage de positions : les deux côtés ont retravaillé les mêmes cellules, et fusionner cette branche reverterait deux corrections de main — #20115 (4 constats d'audit Hermes) et #20207 (deux claims périmés hors table, corrigés et ré-exécutés) — sur synthese-piliers, de4e4b3a et 50dcfe8c. C'est une régression : la branche ne doit pas merger.

Les trois livrables de #20015 sont déjà sur main (mesure de ce cycle, cellule par cellule) :

Livrable de #20015 Sur main ? Où / mesure
Lien de navigation d'en-tête vers Lean-16a oui cellule intro-title : identique à la mienne au caractère près (3 679 c), là où la base portait encore Lean-15
Mesure de la taille OTCA (Annexe E) oui, et meilleure cellule de0111f4 : ~70 KB → « 164 976 octets (mesure du fichier patterns/otcametapixel.rle) », plus la machine de Turing 103 625 (apport #20207) ; ma version disait ~165 Ko
Resynchronisation de la cellule live-read après la tranche 2 de #19989 oui cellule 50dcfe8c : unitcellInitial = RLE.parseRLE! unitcellRLE, unitcellGens := 5760, 316 lignes de Pillars.lean lues, sortie 3 813 c (la mienne : 3 750 c)

Contrôle d'intégrité du carnet de main au même point : 53 cellules, 20 cellules de code, 0 execution_count nul, 0 sortie vide, 0 erreur.

Ce que cette branche portait encore sans que main le reprenne — mesuré, et abandonné sciemment plutôt que fondu : deux diagnostics d'affichage dans la cellule live-read (boucle nominative sur les témoins négatifs appariés pulsar_period1_negative / pulsar_period2_negative, bloc « état UnitCell réel ») et la mention des mêmes négatifs dans la cellule d'interprétation. L'information est déjà portée par main : la sortie de sa cellule 50dcfe8c affiche la ligne pulsar_period2_negative lue dans le fichier, et l'Annexe G nomme les négatifs appariés. Il reste un gain d'affichage, pas de mesure — insuffisant pour justifier une PR qui défait trois cellules de main.

La fermeture ne constate pas un échec : les trois livrables sont arrivés sur main par les PR qui les ont absorbés (#20115, #20207) avant que celle-ci ne soit réparée. La branche feature/lean16b-pillars-resync est conservée — jamais de --delete-branch.

— lane myia-po-2027:CoursIA

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

consecutive-code-cells Modified notebook has >=2 consecutive code cells (#12797)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants