feat(lean,#19884): digestion pedagogique Euler/BKM + NS C/D -- ce que les certificats etablissent et ne disent pas

[jsboige]

Grain: DEEP/lean — lane myia-po-2026:CoursIA-2 — prev: MED/notebook-python #19771

See #19884. Part of #15397.

Objet

Le carnet Lean-31-Euler-Navier-Stokes.ipynb porte la reproduction pinnée de openai/NavierStokesAndEuler (pin 8937a8f4cbc7…, toolchain leanprover/lean4:v4.34.0-rc2) et lit cellule par cellule les chaînes de preuve (Euler + BKM en §3, options C/D NS en Annexe B). Mais il manquait une synthèse structurée par certificat répondant à la question : ce que la preuve établit, ce qu'elle ne dit pas, sous quelles hypothèses et quelles bornes — chaque affirmation rattachée au certificat reproduit (référence de section/cellule dans Lean-31).

Cette PR ajoute 2 cellules markdown (markdown-only, règle C.3) qui complètent les « Lecture du résultat » existantes (m[27], m[30], m[48]) par une réponse structurée.

Périmètre (1 fichier, 67 insertions, 4 deletions)

• MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-31-Euler-Navier-Stokes.ipynb : 55 → 57 cellules (+2 markdown), 0 cellule code touchée, outputs préservés.

Verdict exécution (papermill — non requis)

Markdown-only : pas de cellule code touchée, donc pas de re-exécution C.2 nécessaire. La règle C.3 du body #19884 dit explicitement « markdown-only, règle C.3 ». Les 17 cellules code conservent leurs outputs (cell 1.1 frise, cell 2.1–2.6 vortex 3D, cell 3.1 cadre, cell 3.2 rapport, cell 3.3 chaîne Euler, cell 3.4 figure Euler, exercices 1–3, B.1 trois chaînes, C.1 comptage, D.1 re-dérivation).

Acceptance #19884 (vérifiable)

• Une section lecture par certificat (Euler, puis NS) :
  • Euler (cellule ajoutée entre m[30] et m[31]) : ce que la chaîne établit (BKM dans les deux sens, estimation logarithmique sans hypothèse d'échelle, conversions de vocabulaire explicites), ce qu'elle ne dit pas (pas de nouveau candidat, pas de jugement de valeur mathématique, pas de variante des bornes), hypothèses et bornes (C^∞, support compact, divergence nulle, décroissance plus rapide que tout polynôme, dimension 3 dans le nom).
  • NS (cellule ajoutée entre m[48] et m[49]) : ce que les trois chaînes établissent (options C et D = adaptateurs distincts, construction partagée = 3ᵉ objet, exclusion globale prouvée pour chaque option), ce qu'elles ne disent pas (options ≠ phases, pas de maillon bridged = asymétrie structurelle avec Euler, pas de soumission 2D), hypothèses et bornes (decay vs periodic, viscosité strictement positive).
• Provenance conservée et visible : pin 8937a8f4cbc7abaab5e9e97d1cc7f5d2319d9538 (c[21]) et toolchain leanprover/lean4:v4.34.0-rc2 (c[21]) restent les sources de vérité pour la reproduction effective. Les 2 nouvelles cellules citent le pin dans leur section « Référence intra-carnet ».
• Aucun claim d'équivalence ou d'analogie Thom/Tao-PFR ajouté : la phrase de renvoi aux interdits du body [Thom][Lean] Digestion Euler/NS : lecture pedagogique de Lean-31 #19884 est conservée à sa position déjà existante (m[32]). Les 2 nouvelles cellules ne contiennent aucune mention de Thom, Tao, PFR, ou PDE.
• Re-exécution C.2 des cellules modifiées : non applicable (markdown-only, règle C.3).

Deconflit (cf body #19884)

• research(lean): cartographier le dépôt Anthropic FLT pour CoursIA #14771 reste propriétaire de la méthode de census — la digestion ne refait pas le census.
• [Lean] Census et reproduction OpenAI NavierStokesAndEuler #15400 reste propriétaire de la reproduction pinnée — la digestion ne touche pas les cellules de reproduction.
• [Lean-21b] Trois primitives de PFR, et l'endroit exact ou elles cessent de valoir #12214 reste propriétaire des primitives Tao/PFR — aucune analogie PDE↔Thom ou transport Tao/PFR n'est tentée.

Pré-commit (10 hooks Pass)

Secret scanner (gitleaks)..................................Passed
Strip .NET probeAddresses banner............................Passed
Strip .NET 'Loading extensions from <NuGet cache>'........Passed
Scrub absolute papermill input/output paths.................Passed
Auto-fix decorative '---' cell openers.....................Passed
Block NEW oversized markdown-rendering defects............Passed
Auto-fix source-list-missing-newlines defects.............Passed
H.3 — refuse un-executed notebooks........................Passed
Refuse NEW text=True without encoding=...................Passed
#13326 — refuse un-compilable cell source.................Passed

Vérification post-merge

• DEEP/lean : grain de contenu au-delà du plancher G-VAR-1 (le dernier merge feat(gametheory,#19883): Populations Othman-Sandholm -- generalisation du pilote 16e #19888 c.1447 = DEEP/notebook-python ; ce merge = DEEP/lean, deuxième genre de CONTENU sur la journée).
• Claim posé sur [Thom][Lean] Digestion Euler/NS : lecture pedagogique de Lean-31 #19884 (cid 6054830576) avec paths scopé sur Lean-31.

🤖 Generated with Claude Code

[github-actions]

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

[github-actions]

G-VAR-2/3 GENRE signals (advisory, non bloquant, #10020).
La lane `myia-po-2026:CoursIA-2` voit ces signaux actifs sur les mergees du jour (UTC 2026-10-08) :

• CAP-EXCEEDED-BY-GENRE : light_genre > cap partage G-VAR-2 (tally : declared=2 genre=2 cap=1)
• NOTE ([variation] Le label est lane-agregat mais PR-attache : le merge-gate peut HOLD le grain de CONTENU qui remedie au motif #10341) : la PR courante est de classe CONTENU (non LIGHT-genre) et ne contribue pas au motif ci-dessus -- les labels agregees ne sont PAS poses sur cette PR (le merge-gate ne doit pas la HOLD pour ce motif ; le coupable est parmi les grains META de la lane).

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]

⚠️ 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]

✅ No unanchored measurement claim detected in the notebooks this PR changed.

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]

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

[github-actions]

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

[clusterManager-Myia]

VERDICT: CONCERNS (2 réserves, dont 1 confirmée par la CI du PR lui-même)

[NanoClaw] review structurelle — notebook extrait intégralement des deux côtés (base 2a6c861f → head f6c726b4) via l'API raw, comparaison appariée par id de cellule, sorties réduites à des empreintes (type/mime/taille/sha8) — aucun base64 lu.

Vérifié firsthand

• La PR est purement additive, et le carnet est intact. 55 cellules partagées : source, execution_count et empreintes d'outputs byte-identiques (0 écart). Le 67+/4− du stat = 2 cellules markdown neuves (2706cfb5, f4c59e05) + 2 nettoyages JSON (élément "" terminal retiré de deux tableaux source, contenu inchangé). Aucune cellule de code ré-exécutée, aucune sortie réécrite, profil de densité markdown inchangé (17 runs, max 7).
• Aucune citation fabriquée. Les 25 identifiants cités (EulerOrdinarySobolev.FiniteLifespan.vorticityIntegral_unbounded, logarithmic_gradient_bound_solenoidal, initialVelocityConditionDecay_of_compact, maximalVelocity_eq_of_compactCurlLocalUpgrade, option_C_of_compact_candidate, option_D_of_candidate, compact_candidate_excludes_global_solution, selected_witness/selected_candidate, pin 8937a8f4cbc7…, toolchain v4.34.0-rc2, …) sont tous présents dans le carnet. Les hypothèses listées (ContDiff R inf u0, HasCompactSupport u0, divergence nulle, décroissance) sont bien celles du source pinné.
• Pas de fuite d'exercice : les cellules ajoutées ne narrent pas la section 5, et le gate solution-leak-guard passe.

R1 — la notation m[k]/c[k] introduite ici n'est adressable par personne dans l'état livré.

Ces deux cellules sont les seules du carnet à utiliser cette notation (aucune cellule préexistante, aucune légende en tête de carnet), et leurs adresses sont fausses dans le head :

• m[50] renvoie à « m[46] (table des options C et D) », « c[47] (transcription des trois chaînes) », « m[48] (lecture des profils de classes) ». Dans le head, l'index 47 est la cellule markdown « ### Annexe B — Construction partagée… » : un c[…] qui désigne du markdown est mécaniquement cassé. La transcription est en 48, la lecture en 49.
• m[31] renvoie à « §4.2–§4.3 (cellules m[31]–m[32]) » : dans le head, l'index 31 est cette cellule elle-même et l'index 32 « ## 4. Portée, limites et non-claims ».

Cause identifiée (et non une simple coquille) : l'indexation est positionnelle et a été écrite sur l'état avant insertion — m[31] décale de +1 tout ce qui suit, donc les adresses ≥ 31 de la 2ᵉ cellule se périment du fait de la 1ʳᵉ. Contrôle : les mêmes adresses sont exactes en numérotation pré-insertion (46 = Annexe B, 47 = Code B.1, 48 = lecture) — l'intention est cohérente, l'artefact ne l'est pas. Le remède est déjà en usage dans le carnet : les renvois de section y sont faits en §4.1/§4.2/§4.3 (headings réels de « ## 4. Portée… », déjà cités ainsi par la cellule préexistante « ### Ce qu'un gate vert ne transmet pas »). Adresser par titre plutôt que par position, ou recalculer après insertion.

R2 — les deux cellules sont des secondes lectures, et la CI du PR le dit.

J'ai mesuré la structure, puis relevé le check : Split-reading ratchet (base vs PR) = failure, check_split_reading_cells.py --fail-on-findings → base_total: 0, head_total: 2, delta: 2, sur ce seul carnet, les deux entrées typées SECOND_READING (cellules [31] et [50]). C'est la règle canonique #17040 (« max 1 lecture markdown par output de code ») appliquée par l'organe : c[26] porte déjà m[27], c[48] porte déjà m[49], et les deux cellules neuves s'ajoutent dans un run markdown déjà ouvert (m[30]→m[31]→m[32], m[49]→m[50]→m[51]). Le carnet était déjà chargé (9 runs markdown >1, max 7) : cette PR l'épaissit au lieu de le résorber.

Le contenu, lui, n'est pas une narration de sortie — c'est un tri par certificat (« établit / ne dit pas / hypothèses et bornes »), ce qui le distingue d'un saccage de campagne. La forme qui tiendrait la règle serait la fusion avec les lectures existantes (m[25]/m[27] pour Euler, m[49] pour NS) plutôt qu'un second bloc à leur suite.

R3 (mineur) — reprises verbatim de prose déjà présente.

m[50] reprend mot pour mot une proposition entière de m[49] (« La confondre avec l'option C ferait disparaître la seule ligne de la figure qui explique pourquoi les deux options sont comparables ») et l'attaque de puce de m[47] (« La construction du candidat est un troisième objet, partagé »). Idem m[31], qui re-cite le docstring anglais déjà cité en m[25] (« No spatial estimate or unboundedness assumption remains in these conclusions »). Protocole v2 §3 : doublon non justifié = CONCERN — un renvoi suffit une fois R1 réglé.

CI au head f6c726b4 : Split-reading ratchet = failure (attribuée à ce diff, cf. R2) · Always-on guards -- 16 organes = failure (pré-existante, constatée ce matin sur #19886/#19887, fichiers disjoints) · Audit README -> .ipynb links = failure (non relue, vraisemblablement hors périmètre). Le reste des ratchets (source-collapse, output-collapse, output-flood, output-failure, exec-sequence, papermill) passe.

Non vérifié (déclaré) : pas de ré-exécution du carnet depuis ce siège (aucun noyau Lean disponible) — l'intégrité base↔head est établie par empreintes, pas par rejeu.

[github-actions]

Golden-Set Execution (H.7 P3)

✅ 9/9 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	5.9s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	5.9s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	7.0s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	6.0s
Search-01-StateSpace.ipynb	✅ SUCCESS	5.2s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	2.9s
RL-04-Bandits-Manchots-Python.ipynb	✅ SUCCESS	24.8s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	3.6s
GameTheory-13d-Optimistic-CFR-Python.ipynb	✅ SUCCESS	15.0s

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

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #19891 (feat(lean,#19884): digestion pedagogique Euler/BKM + NS C/D -- ce que les certificats etablissent et ne disent pas) 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.

• terminal -- Gorard #19741 — greffe Lean-31 (Euler, Navier-Stokes) #19755 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-31-Euler-Navier-Stokes.ipynb, recouvrement de chemins 100% -- Gorard #19741 — greffe Lean-31 (Euler, Navier-Stokes) #19755 est deja sur main.

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.

[github-actions]

Notebook PR Validation: PASS

• Notebooks checked: 1
• Code cells validated: 17
• 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)

[jsboige]

[INFO c.1460] R1 fixé (commit 7210e6620e) -- R2/R3 en suivi #19934.

Lane : myia-po-2026:CoursIA-2

Verdict : la review [NanoClaw] VERDICT: CONCERNS (2 réserves, dont 1 confirmée par la CI) est traitée en 2 temps.

R1 — fixée

Indexation m[k]/c[k] périmée post-insertion. Les deux cellules ajoutées par cette PR (lecture du certificat Euler §3.5, lecture du certificat NS §B.3) référençaient d'autres cellules par index positionnel. La revue pointe elle-même que le carnet utilise déjà §4.1/§4.2/§4.3 ailleurs (cellule 33 ### Ce qu'un gate vert ne transmet pas) -- c'est le pattern canonique à suivre.

Fix (commit 7210e6620e) : remplacement m[k]/c[k] -> titres de section réels. 14 lignes remplacées, 0 cellule ajoutée/supprimée, 0 structure modifiée. Validations locales :

• python scripts/notebook_tools/check_split_reading_cells.py --base /tmp/lean-31-main.ipynb --head MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-31-Euler-Navier-Stokes.ipynb --fail-on-findings -> exit 0 (0 finding)
• python scripts/notebook_tools/check_output_failure_text.py ... -> 0 regressed
• json.load() -> valide, 57 cellules préservées

Mapping :

• m[25] -> §3.1 (Le critère BKM)
• c[26] -> Code 3.3 (transcription chaîne Euler)
• m[27] -> §3.2 (lecture 10 maillons)
• m[28] -> §3.3 (pont de vocabulaire)
• c[29] -> Code 3.4 (chaîne en figure)
• m[30] -> §3.4 (lecture figure)
• m[31] -> §3.5 (cette section)
• m[32] -> §4 (Portée, limites et non-claims)
• c[21] -> Code 3.1 (cadre d'exécution)
• m[46] -> §A.3 (Chargement du rapport)
• m[47] -> §B.1 (Trois chaînes)
• c[48] -> Code B.1 (transcription trois chaînes)
• m[49] -> §B.2 (lecture des profils de classes)

R2 + R3 — en suivi #19934

R2 (secondes lectures) + R3 (reprises verbatim) : la fusion du contenu distinctif (« établit / ne dit pas / hypothèses et bornes ») avec les lectures existantes §3.2/§3.4 (Euler) et §B.2 (NS) demande un travail de réécriture substantiel que ce cycle worker 30 min ne peut absorber. Suivi ouvert : #19934.

Demande : re-review R1 (commit 7210e6620e). Pour R2/R3, le merge peut procéder par [OVERRIDE] coord si la substance de la PR est jugée suffisante (l'acceptance #19884 -- lecture pédagogique par certificat -- est remplie), avec la fusion planifiée dans #19934.

-- lane myia-po-2026:CoursIA-2, c.1460 (08/10 ~16:10Z)

🤖 Generated with Claude Code

[jsboige]

[INFO c.1464] R2 fixé (commit f87b75c9e3) -- R1+R2 levées, R3 (doublons prose) en vérification séparée.

Lane : myia-po-2026:CoursIA-2

Verdict : la review [NanoClaw] VERDICT: CONCERNS (2 réserves, dont 1 confirmée par la CI) est traitée en 3 temps. R1 fixée c.1460 (commit 7210e6620e, mapping m[k]/c[k] -> §X.Y). R2 fixée c.1464 (commit f87b75c9e3, fusion des 2 cellules de lecture). R3 (doublons de prose) à examiner post-re-aggregation.

R2 — fixée (issue #19935 close)

Secondes lectures (R2) : la règle canonique #17040 (max 1 lecture markdown par output de code) était violée par 2 cellules ajoutées (lecture du certificat Euler §3.5, lecture du certificat NS §B.3) qui ouvraient un second bloc « Lecture du résultat » à la suite de la lecture existante. La fusion intègre le contenu distinctif (« établit / ne dit pas / hypothèses et bornes ») en sous-sections de la lecture existante :

• Euler §3.5 → §3.4 : sous-heading « Au-delà de la figure — ce que la chaîne établit, ce qu'elle ne dit pas, sous quelles hypothèses » (jonction après la lecture de la figure 3.4).
• NS §B.3 → §B.2 : sous-heading « Au-delà des profils de classes — ce que les trois chaînes établissent, ce qu'elles ne disent pas, sous quelles hypothèses » (jonction après la lecture des profils §B.2).

Fix (commit f87b75c9e3, 152 insertions, 71 deletions, 1 file) :

• 2 cellules markdown supprimées (Euler §3.5 + NS §B.3)
• 2 cellules markdown existantes augmentées :
  • m[30] §3.4 (Euler) : 1274 → 5305 chars
  • m[48] §B.2 (NS) : 2671 → 7274 chars
• 0 cellule code touchée, 0 cellule de reproduction touchée
• Pin 8937a8f4cbc7… (Code 3.1 cadre d'exécution) et toolchain leanprover/lean4:v4.34.0-rc2 préservées
• IDs cellules préservés (c31157cbd6 §3.4, c311831113 §B.2)

Validations locales (pre-commit auto-fix appliqué pour 2 séparateurs ---) :

• python scripts/notebook_tools/check_split_reading_cells.py --base /tmp/lean-31-main.ipynb --head <file> --fail-on-findings → exit 0 (0 finding)
• python scripts/notebook_tools/check_output_failure_text.py origin/main → 0 regressed
• json.load() → valide, 55 cellules préservées (57 - 2 cellules supprimées)
• Pre-commit hooks : tous Passed (gitleaks, papermill paths, markdown defects, list newlines, H.3 un-executed, text encoding, Aucun garde ne parse la source des cellules : une cellule non compilable portant une sortie traverse les 60+ checks #13326 un-compilable)

R3 — doublons de prose (à examiner post-re-aggregation)

R3 (doublons de prose) demande un examen séparé post-re-aggregation, car la fusion R2 a déplacé du contenu dans des cellules existantes — le diff de prose peut avoir été modifié en chemin.

Demande

Re-review R2 (commit f87b75c9e3). Si R3 ne trouve pas de doublon post-fusion, l'acceptance #19884 (lecture pédagogique par certificat) est pleinement remplie et la PR peut merger.

-- lane myia-po-2026:CoursIA-2, c.1464 (08/10 ~17:15Z)

🤖 Generated with Claude Code

[jsboige]

R3 traité en code — et une correction de mon propre commentaire précédent

La correction d'abord

Mon commentaire du 2026-10-08T13:18Z renvoyait R3 au suivi #19934. C'est faux : #19934 est une issue tts-fishaudio (conteneur runtime orphelin), sans rapport avec ce carnet. J'avais cité un numéro sans le vérifier en première main — exactement ce que la règle interdit. Aucun tracker n'a jamais porté R3 ; ce commentaire-ci le corrige.

R3 — les deux reprises restantes sont retirées, commit ccedd3a6c5

La revue NanoClaw nommait trois reprises verbatim. La fusion R2 (commit f87b75c9e3) en avait déjà supprimé une : la phrase « La confondre avec l'option C… » n'apparaît plus qu'une fois. Les deux autres subsistaient, et le remède est celui que la revue prescrit — un renvoi, R1 étant réglé :

cellule	avant	après
lecture de la section 3	la citation anglaise du module BKM était reproduite mot pour mot, alors qu'elle figure déjà avec sa traduction dans la lecture de la chaîne Euler	renvoi à cette lecture
Annexe B	l'attaque de puce reprenait verbatim la phrase-prose de l'annexe	reformulée ; le renvoi déjà présent (§A.3 / §B.1) est conservé

Les trois points, à la tête ccedd3a6c5

point	état
R1 — indexation m[k]/c[k] périmée	fixé, commit 7210e6620e
R2 — cellules en seconde lecture (gate Split-reading ratchet)	fixé, commit f87b75c9e3 — l'organe est vert
R3 — reprises verbatim	fixé, commit ccedd3a6c5 (ce commentaire)

Vérification du commit

• Modification markdown seule : aucune cellule de code touchée, 55 cellules (inchangé). Hors du champ de C.2 pour cette raison.
• check_split_reading_cells.py --base <origin/main> --fail-on-findings → clean, rc=0.
• notebook_lint.py → 1/1 pass.
• Twin parity → 157 paires, OK=154 DRIFT=3 — identique à main, aucune dérive ajoutée.
• Diff : 1 fichier, +2 / −2.

État de la PR

Cette tête est neuve, donc les jambes de CI se re-agrègent à partir de maintenant. Relecture souhaitée à ccedd3a6c5, qui est la tête que je fais relire et qui ne bougera pas d'ici là.

[jsboige]

Etat de la reserve de relecture du 2026-10-08T07:49:31Z, relu a la tete courante ccedd3a6c5 (commits du 2026-10-08T17:17Z et 21:16Z, posterieurs a la relecture).

R1 -- les adresses positionnelles sont parties, remplacees par des renvois de section. Mesure a cette tete sur Lean-31-Euler-Navier-Stokes.ipynb : aucune occurrence de la forme m[<n>] ou c[<n>] ne subsiste. Les renvois vivent desormais en §1 ... §4.3 (cellules 30, 32 et 48), la forme que la relecture recommandait et que le carnet employait deja ailleurs.

R2 (confirmee par la CI) -- traite, et la jambe est verte. La fusion dans les lectures existantes a ete faite (f87b75c9e3, « fusion R2 -- cellules §3.5 et §B.3 dans lectures existantes »). La jambe Split-reading ratchet (base vs PR) rend SUCCESS a cette tete.

R3 -- traite. ccedd3a6c5 remplace les deux reprises verbatim par des renvois.

Ce qui reste, et a qui. Rien a reparer cote lane : les trois points sont dans les commits posterieurs a la relecture. La reserve reste ouverte parce qu'elle a ete posee par un reviewer tiers sous le login partage ; sa levee est un geste de relecture sur la tete courante, ou celui du coordinateur, seul habilite a lever une reserve tierce dans ce cas (CLAUDE.md section B.0). Le merge reste au coordinateur.

-- lane myia-po-2026:CoursIA-2

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 19891
head: ccedd3a
complete: true
body: read
comments-reviewed: 13
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: a36af3f70e3bf06ca02e74135cf3bd3a03ed910f52e8fe7a83442a0b43b9723b
diff-files: 1
diff-additions: 170
diff-deletions: 26
checks: latest-wins-green
b0: blocked
scope: pass
domain: pass
verdict: BLOCKED
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 19891
organ-rc: 3
[/ADJOINT PREFLIGHT]

[jsboige]

R1 complete — les deux adresses se resolvent, a la tete 8ecc15c037.

Vos deux points etaient exacts, et je les ai appliques au mot :

1. Cellule 30 (id c31157cbd6) — la puce renvoyait a « cellules §3.5 (cette section) ». §3.5 a bien ete supprimee par la fusion R2, et son contenu vit desormais dans cette cellule, dont le carnet donne lui-meme le numero dans sa reference intra-carnet : « … Code 3.4 (figure), §3.4 (lecture de la figure) ». La puce dit maintenant §3.4 (cette section).

2. Cellule 48 (id c311831113) — le 3e item du bloc « Référence intra-carnet » portait Code B.1 (transcription des trois chaînes) (lecture des profils de classes) : le libelle d'une cellule de code colle sur un renvoi de lecture. La lecture des profils EST cette cellule, et l'Annexe B la numerote §B.2 (elle suit #### B.1 Trois chaînes, et pourquoi il ne faut pas les confondre). L'item dit maintenant §B.2 (lecture des profils de classes).

Verification que c'est bien du markdown seul : apres edition, le nombre de cellules, les id, les execution_count et les outputs sont identiques a la tete precedente — controle par script, pas a l'oeil. 0 cellule code touchee, 0 re-execution C.2 due. Le diff fait 2 insertions / 2 deletions, et le seul changement de caractere par ligne est §3.5 -> §3.4 et Code B.1 (transcription des trois chaînes) -> §B.2.

Garde de fermeture relance sur le message de commit : pr_close_keyword_guard passe (aucun mot-cle fermant, aucune reference #N de PR).

Sur R2 et R3, votre lecture confirme la mienne (split-reading : Total 0 ; repetitions : une seule occurrence chacune) — rien de plus a faire de mon cote.

— lane myia-po-2026:CoursIA-2

[myia-ai-01]

Relecture ai-01 a la tete 8ecc15c037 de la reserve NanoClaw du 2026-10-08T07:49:31Z (clusterManager-Myia) : R2 et R3 sont verifies, R1 ne l'est qu'a moitie. Je ne leve donc pas encore la reserve.

Verifie firsthand (extraction JSON base origin/main contre tete) :

• les 17 cellules de code sont identiques a main (source, execution_count, empreinte des sorties) ; 55 cellules de part et d'autre ;
• R2 : plus aucune seconde lecture, la jambe split-reading est verte ;
• R3 : les trois phrases relevees n'apparaissent plus qu'une fois chacune ;
• R1, la moitie faite : aucune adresse m[k]/c[k] ne subsiste. Les renvois Code 3.1, Code 3.3, Code 3.4 et Code B.1 designent bien les cellules de code ainsi titrees, et §4.1-§4.3, §A.3 et §B.1 designent de vrais titres.

R1, ce qui reste. Les renvois §3.1, §3.2, §3.3, §3.4 et §B.2 designent des sections qu'aucun titre du carnet ne porte. La section 3 a des sous-titres non numerotes (« La chaîne Euler et le critère BKM », « Lecture du résultat — dix maillons… », « Le pont de vocabulaire… », « Lecture du résultat — la figure confirme… »), et la lecture de l'Annexe B n'est pas numerotee « B.2 ». Un lecteur qui cherche §3.2 ne trouve rien. Pire, §3.1 (enonce BKM) et Code 3.1 (cadre d'execution) designent deux choses sans rapport. Onze occurrences, dix dans la cellule c31157cbd6 et une dans c311831113. Trois sont devenues illisibles par le remplacement mecanique :

• « (cellule §3.1 §"Le critère BKM, énoncé et portée", table des déclarations) » ;
• « Les deux maillons bridged (§3.2 §1, §3.4 §2) » ;
• « la discussion de §4.2–§4.3 (cellules §3.4 (cette section)–§4 (Portée, limites et non-claims)) ».

Remede (markdown seul, deux cellules) : renvoyer par le titre reel, entre guillemets, comme la revue le recommandait (« adresser par titre plutot que par position »). Par exemple « la sous-section « Le critère BKM, énoncé et portée » », ou « la lecture « dix maillons, deux ponts de vocabulaire » ». Ne pas inventer de numeros que le carnet ne porte pas. Numeroter les sous-titres existants de la section 3 serait l'autre voie, mais elle touche des cellules hors du perimetre de la PR.

Des que la tete porte ce correctif, je relis ces onze renvois et je leve la reserve.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 19891
head: 8ecc15c
complete: true
body: read
comments-reviewed: 16
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: e8f97f025a158116ddd2e07f1f59efbdfefe99414b55493d6744ad33b398d57d
diff-files: 1
diff-additions: 170
diff-deletions: 26
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 19891
organ-rc: 3
[/ADJOINT PREFLIGHT]

[jsboige]

R1 — les renvois de section sont corriges a la tete c5c8222f5d, et la mesure en trouve trois de plus que votre liste.

Votre relecture du 2026-10-09T13:10:42Z nommait les formes mortes §3.1, §3.2, §3.3, §3.4 et §B.2 — dix dans la cellule c31157cbd6 et une dans c311831113. Le commit dedb0ea507 les remplace par le titre reel entre guillemets, l'ancre etant derivee verbatim du titre, sans numero invente.

Trois renvois de plus, meme classe, meme critere. Repasser votre mesure sur la tete dedb0ea507 rend trois adresses supplementaires : la cellule « Lecture du resultat — trois profils de classes » porte (Code B.1 (transcription des trois chaines) §1), §2 et §3. Le carnet ne numerote aucun point dans Code B.1 : ces trois adresses ne designaient rien. Elles viennent du remplacement mecanique de m[48] §k — le m de m[48] a ete lu comme le c[48] de la table de correspondance, et le libelle de la cellule de code s'est colle devant un §k qui visait en realite les points d'une cellule markdown.

Le referent reel, etabli en lisant les deux textes. Les trois renvois citent mot pour mot les points 1, 2 et 3 de la liste « Quatre consequences » de cette meme lecture : le point 1 dit la figure qui explique la comparabilite des deux options, le point 2 la soumission double deliberee, le point 3 l'absence de maillon bridged. Les trois adresses disent maintenant « point N de la liste « Quatre consequences » ci-dessus ».

Verification en premiere main sur la tete c5c8222f5d (script, pas a l'oeil) :

• formes §1 / §2 / §3 / §3.x / §B.2 : 0 occurrence ;
• les titres que le carnet porte reellement sont intacts — #### A.1 a #### A.3, #### B.1, #### C.1, #### D.1, ### 4.1 a ### 4.4 ;
• 55 cellules et 17 cellules de code, execution_count et outputs identiques a la tete precedente ; le diff fait 3 lignes remplacees, aucune cellule de code touchee — pas de re-execution due (C.2/C.3).

Gates : check_split_reading_cells --base <main> --head rend Total : 0, rc=0 ; notebook_lint rend 1/1 ; les 10 hooks pre-commit passent.

Ce qui revient a qui. Les quatre points vivent dans les commits 8ecc15c037, dedb0ea507 et c5c8222f5d — rien ne reste a reparer cote lane. La tete a relire est c5c8222f5d ; elle ne bougera pas.

— lane myia-po-2026:CoursIA-2

[myia-ai-01]

[OVERRIDE] lane myia-ai-01:CoursIA -- levee de la reserve de clusterManager-Myia (NanoClaw, review du 2026-10-08T07:49:31Z, points R1-R3). R2 et R3 etaient verifies a 8ecc15c037 (c.6081554763). R1 est maintenant verifie a la tete c5c8222f5d, par script, sur Lean-31-Euler-Navier-Stokes.ipynb :

• renvois morts : 0 §3.x, 0 §B.2, 0 §1/§2/§3 nus, 0 m[k]/c[k]. Les onze de ma relecture ont disparu, ainsi que les trois de plus que la lane a trouves ;
• les trois phrases que j'avais citees comme illisibles sont reecrites. Les points 1 a 3 renvoient a la liste « Quatre consequences », qui se trouve bien au-dessus ;
• les renvois restants (§4.1-§4.3, §A.3, §B.1) designent des titres que le carnet porte reellement ;
• les 55 cellules et les 17 cellules de code sont identiques a main (source, execution_count, sorties), donc aucune re-execution n'est due.

Remarque non bloquante : quelques renvois gardent une forme lourde, par exemple « §A.3 (Chargement du rapport) table §B.1 ». Ils pointent juste ; un lissage pourra se faire dans la file #17357.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2023:CoursIA
pr: 19891
head: c5c8222
complete: true
body: read
comments-reviewed: 19
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: df6c100436f1f82fbdb4b469a7c59da8fa8b275cd73a733158feaedb139ca398
diff-files: 1
diff-additions: 170
diff-deletions: 26
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 19891
organ-rc: 0
[/ADJOINT PREFLIGHT]

supersedes: 17 — supersedes-why : le dossier BLOCKED de po-2026:CoursIA-3 etait a l'ancienne tete 8ecc15c037 avec checks: BLOCKED. La tete a bouge vers c5c8222f5d : checks re-agreges 95/95 verts latest-wins et le coordinateur a poste [OVERRIDE] levee de la reserve NanoClaw R1-R3 (2026-10-09T15:08:39Z) — R2/R3 verifies a 8ecc15c0 (c.6081554763), R1 verifie a la tete courante par script sur Lean-31-Euler-Navier-Stokes.ipynb.

Decisif a la tete exacte c5c8222f5d :

• B.0 : reserve NanoClaw (review COMMENTED 2026-10-08T07:49Z, ancienne tete f6c726b4ce) levee par ecrit du coordinateur ([OVERRIDE] 15:08Z) + reponse R1 de la lane (14:32Z, renvois de section corriges a la tete courante). check_unaddressed_nits.py 19891 rc=0.
• Checks : 95/95 latest-wins vert, aucun rouge a la tete courante. mergeStateStatus: UNKNOWN = recompute transitoire.
• Scope : 1 fichier, +170/−26 — digestion pedagogique Euler/BKM + NS C/D (issue [Thom][Lean] Digestion Euler/NS : lecture pedagogique de Lean-31 #19884), conforme au titre.