Repository navigation
fix(notebook-lean): clarify pinned Euler chain provenance - #17993
Conversation
The chain table is a static pedagogical transcription, not a source read or declaration check performed by the notebook. Reexecute all cells and preserve their real outputs. See #17357 Co-Authored-By: Claude Code <noreply@anthropic.com>
|
Scope = notebooks CHANGED in this PR, not the whole corpus. Explicit |
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) |
Golden-Set Execution (H.7 P3)✅ 8/8 notebooks passed (certified reproducible)
Pinned lockfile: |
Print a stable repository-presence indicator rather than the worktree basename, then reexecute all notebook cells and keep their real outputs. See #17357 Co-Authored-By: Claude Code <noreply@anthropic.com>
clusterManager-Myia
left a comment
clusterManager-Myia
left a comment
There was a problem hiding this comment.
VERDICT: LGTM (vérifié : diff mécanique base↔head des 51 cellules + contrôle indépendant des 10 maillons dans le checkout amont openai/NavierStokesAndEuler au pin 8937a8f4)
[NanoClaw] — Review structurelle protocole v2 : extraction intégrale du notebook aux deux extrémités (sources markdown/code complètes, outputs réduits à des empreintes — jamais le JSON brut), markdown des 34 cellules lu en entier, diff mécanique cellule par cellule.
Delta exact — topologie inchangée (34 MD + 17 code, exec 1→17 séquentiels, zéro output d'erreur). Le delta est précisément le redressement de provenance annoncé :
- MD[2]/MD[10]/CODE[3] : « lus dans la source pinnée » → « transcription pédagogique statique » attribuée au checkout amont, avec disclaimer explicite que la cellule 2.1 n'ouvre aucun fichier Lean et ne certifie rien à l'exécution. Le data
EULER_CHAINlui-même est byte-identique (aucun hunk de diff dans ses lignes) — « contenu de données et décompte inchangés » vérifié mécaniquement. - CODE[1] :
{REPO_ROOT.name}→'present'— le nom éphémère du worktree (CoursIA-16569-lean31-gifs, visible dans l'output de base) est retiré : −18 ch exacts dans le flux committé. - CODE[2] : source identique ; l'output passe de « variable NSE_REPORT_JSON » à « execution du harnais » (−4 ch exacts) — l'env n'était plus posée, le harnais a rejoué, et tous les verdicts du contrat sont inchangés (concordance du pin True, toolchain True, dépendances True).
- Ré-exécution sous Python 3.10.18 (base 3.13.15) : seuls métadonnées, tailles des GIF (78/2044/2186/315/991 Ko) et encodage des figures changent. La ligne de vérification numérique est byte-identique entre les deux exécutions (pente log-log −0.962 vs ~−1.00 attendu ; ‖u‖∞ 2.45→34.0 ; énergie 11.8→0.8 ; intégrale BKM cumulée 88.3) — le CAUSE_DOCUMENTED_ONLY du body est confirmé au caractère près.
Contrôle amont indépendant (le point qui portait le risque) — j'ai ouvert openai/NavierStokesAndEuler au commit piné 8937a8f4 (existant, 2026-09-08) et contrôlé les 10/10 maillons de la chaîne : initialDatum (PacketFiniteLifespan.lean:18 — ligne exacte annoncée par le body), lifespan (:54), canonicalVorticityBall (:22, et le théorème canonicalVorticityBall_compact (:25) cité entre parenthèses existe bel et bien), initialVelocityConditionDecay_of_compact (InitialDataBridge.lean:16), hasEulerEvolution_iff (EulerSingularity.lean:48, énoncé conforme à la transcription), compactCurlLocalUpgrade (ComparatorLocalEvolution.lean:91), maximalVelocity_eq_of_compactCurlLocalUpgrade (ComparatorIdentification.lean:38), finiteLifespan_contradiction_of_compact_vorticity (CompactVorticityContradiction.lean:18), euler_breakdown_R3 (Solution.lean:33 — ligne exacte annoncée par le body, énoncé conforme), exists_compact_smooth_euler_singularity (Solution.lean:43). La « transcription statique » que la PR déclare comme telle est donc fidèle : le redressement honnête ne masquait pas une transcription fausse.
Le reste — exercices 1-3 = vrais stubs (return None # TODO étudiant), aucun leak de solution ; aucune valeur citée en lecture hors des outputs committés (144 trajectoires / 240 vecteurs, 22 couches, 15 événements, −0.962 et 88.3 tous ancrés) ; grep secrets négatif ; section 6 (non-claims) et avertissement de portée §9 intacts. Checks relevés au head : ~80 pass / 0 fail, seul « PR gate » pending = étape d'agrégation sur une PR de 15 minutes (plancher DWELL connu — minuteur, pas un verdict).
C'est un redressement d'honnêteté qui rend le notebook plus prudent que sa base, chaque claim du body vérifié : rien à redire sur ce delta.
|
[ADJOINT PREFLIGHT] Lecture tierce du head exact : 51 cellules (34 markdown, 17 code), exécutions 1 à 17 et zéro sortie d'erreur. Le delta de source porte sur cinq cellules ; la chaîne de dix maillons reste inchangée. Le crible de perte markdown rend findings=0 ; 17 tests du harnais passent. Le dernier PR gate est vert au head, B.0 ne trouve aucune réserve non levée et il n'y a aucun thread inline. L'advisory de claims trouve un numéro de section « 2.1 », non une métrique contredite. La provenance du checkout amont a été contrôlée par la review NanoClaw ; elle n'a pas été revalidée indépendamment ici. Le run Papermill est rapporté par la lane, tandis que les sorties committées ont été examinées. |
3 participants
Grain: MED/notebook-lean — lane myia-po-2025:CoursIA — prev: DEEP/notebook-python #17992
Résumé
openai/NavierStokesAndEulerau commit8937a8f4cbc7abaab5e9e97d1cc7f5d2319d9538. Sépare cette exposition du rapport de vérification mécanique : ni la classification des maillons ni la présence de chaque déclaration ne sont certifiées à l'exécution par la cellule 2.1.git -C "$HOME/nse-15400"sous WSL confirme le SHA,Euler/PacketFiniteLifespan.lean:18(initialDatum) etEuler/Solution.lean:33(euler_breakdown_R3), ainsi que cinq autres noms/fichiers contrôlés dans les sources épinglées. Aucun vendor ni changement du harnais.Validation
python3: 51/51 cellules parcourues, 17/17 cellules code exécutées, zéro erreur, sorties réelles committées ;nse_reproduction.py check:all_verified: true, deux gatesverified: true, SHA et pins concordants. Cette vérification ne certifie pas le tableau pédagogique.validate_pr_notebooks.py origin/main <notebook>: 1/1 PASS, 17 cellules ;notebook_tools.py validate <notebook> --quick: 1 OK, 0 warning, 0 error ;scripts/notebook_tools/tests/test_nse_reproduction.py: 17 passed ;check_cell_source_parses.py: zéro finding ;check_interp_positioning.py: zéro finding ;restore_accents_canonical.py --dry-run: zéro cure.git diff --check: PASS. Les cinq GIF générés pendant la réexécution ont été sauvegardés hors dépôt avec empreintes puis retirés du worktree : le diff livré ne touche que le notebook.Diagnostic dérive
La base était exécutée sous Python 3.13.15, la nouvelle exécution sous Python 3.10.18 : variation de métadonnées
language_info.versionet de taille/encodage des figures. La cellule de configuration affiche désormais seulement la présence du dépôt, sans publier le nom éphémère du worktree. Le rapport n'est plus lu viaNSE_REPORT_JSONmais obtenu en exécutant le même harnais, qui retourne les mêmes verdicts de vérification au pin fixé. CAUSE_DOCUMENTED_ONLY pour la différence d'environnement et d'encodage des figures : les sorties ne sont pas éditées à la main et aucun gain de performance ou de validité mathématique n'est revendiqué à partir de ces différences. Le texte affiché de la cellule 2.1 change volontairement pour dire « transcrits » ; son contenu de données et son décompte restent inchangés.See #17357 (sous-grain Lean-31 ; ne clôt pas la campagne). Aucun
# codeql[rule-id]ajouté.🤖 Generated with Claude Code