[Audit #17073] Série Lean — partition Hermes

[clusterManager-Myia]

[Audit #17073] Série Lean — partition Hermes

Population: 65 notebooks (57 Lean-* + 8 Serre100/). Premier notebook audité: Lean-30-FormalGroups-Native.

Panorama (survol cell 25–29 + inventaire)

Arc pédagogique. La série couvre un spectre complet : socle Lean 4 (1–6 : setup, types dépendants, propositions, quantificateurs, tactiques, Mathlib), outillage agentique (7–11 : LLM, agentic proving, multi-agents, LeanDojo, TorchLean), puis compagnons thématiques par résultat mathématique (12–34 : sensibilité, Kochen-Specker, CHSH, finitude, Grothendieck, Conway 16a–j, nœuds 17a–c, Sendov, Tao, PFR, MIMO, Galois M₂₃, ERC20, calibration, cohérence/de Finetti, Munkres, Tutte, Hopf-S⁶, Hecke, groupes formels, Euler-NS, distributions, calculabilité, Erdős), et la sous-série Serre100 (8 carnets). Les compagnons « natifs » (suffixe -Native) exécutent sous vrai kernel Lean via lake dédié ; les « Companion » juxtaposent Python etLean.

Ordre canonique proposé. 1→6 (socle, ordre strict), puis 7–11 (outillage, indépendants), puis thématiques regroupées par famille : hommages (15/26), Conway (16a→16j ordre lettres), nœuds (17a→17c), physique (21a→21c), et Serre100 en fin de parcours (prérequis socle complet + théorie des nombres). Sauts de numérotation : Lean-32 absent (31→33).

Niveau d’apprenant proposé. Socle 1–6 : débutant Lean (L3). 7–11 : intermédiaire outillage. Thématiques : M1 selon le domaine (certains demandent arithmétique avancée — Hecke, S⁶, groupes formels). Serre100 : M2.

Gaps entre notebooks (survol). Les sous-séries lettre (16a–j, 17a–c, 21a–c) forment des mini-arcs dont l’entrée suppose le socle mais rarement le carnet précédent de la lettre — à confirmer notebook par notebook. Le passage compagnon→natif (ex. 15→15b→15c) duplique potentiellement du contenu : arbitrage à l’audit.

Checklist notebooks

• Lean-1-Setup.ipynb
• Lean-10-LeanDojo.ipynb
• Lean-11-TorchLean.ipynb
• Lean-11b-TorchLean-Python.ipynb
• Lean-12-Sensitivity-Theorem.ipynb
• Lean-12b-Lean-Sensitivity-Theorem.ipynb
• Lean-13-Kochen-Specker.ipynb
• Lean-13b-CHSH-Tsirelson-Native.ipynb
• Lean-14-Finiteness-Derivatives.ipynb
• Lean-14b-Finiteness-Lean-Companion.ipynb
• Lean-15-Grothendieck-Tribute.ipynb
• Lean-15b-Lean-Grothendieck.ipynb
• Lean-15c-Lean-Grothendieck-Companion.ipynb
• Lean-16a-Conway-Man-and-Work.ipynb
• Lean-16b-Conway-Game-of-Life-Lean.ipynb
• Lean-16c-Conway-Game-of-Life-Golly.ipynb
• Lean-16d-Conway-Game-of-Life-Lean-Native.ipynb
• Lean-16e-Conway-FRACTRAN-Lean-Native.ipynb
• Lean-16f-Conway-Free-Will-Theorem.ipynb
• Lean-16g-Conway-Canons.ipynb
• Lean-16h-Conway-PatternTour-Native.ipynb
• Lean-16i-Translateur-Life.ipynb
• Lean-16j-Conway-Hashlife-Correctness-Native.ipynb
• Lean-17a-Knots-Conway-Proofs.ipynb
• Lean-17b-Knots-Invariants-Companion.ipynb
• Lean-17c-Knots-Companion-Formel.ipynb
• Lean-18-Sendov-Complex-Analysis.ipynb
• Lean-19-Analysis-I-Tao-Workflow.ipynb
• Lean-2-Dependent-Types.ipynb
• Lean-20-PFR-Entropy-Method.ipynb
• Lean-20b-PFR-Primitives-Transportables.ipynb
• Lean-21-MIMO-Detection-Flips.ipynb
• Lean-21b-MIMO-Converse-Native.ipynb
• Lean-21c-Descente-Budget.ipynb
• Lean-22-Galois-Probleme-Inverse-M23.ipynb
• Lean-23-ERC20-Invariant-Companion.ipynb
• Lean-23b-Lean-ERC20-Native-Companion.ipynb
• Lean-24-Calibration-Native-Companion.ipynb
• Lean-25-Coherence-et-Temoin.ipynb
• Lean-26-Munkres-Tribute.ipynb
• Lean-27-EdgeColoring-Tutte-Companion.ipynb
• Lean-28-Complex-Structure-S6.ipynb
• Lean-29-Hecke-Operators-Native.ipynb
• Lean-3-Propositions-Proofs.ipynb
• Lean-30-FormalGroups-Native.ipynb
• Lean-31-Euler-Navier-Stokes.ipynb
• Lean-33-Distribution-Spaces.ipynb
• Lean-34-Calculabilite-et-Limites.ipynb
• Lean-3b-Formalized-Formal-Logic.ipynb
• Lean-4-Quantifiers.ipynb
• Lean-5-Tactics.ipynb
• Lean-6-Mathlib-Essentials.ipynb
• Lean-7-LLM-Integration.ipynb
• Lean-7b-Examples.ipynb
• Lean-8-Agentic-Proving.ipynb
• Lean-8b-Erdos-Formal-Conjectures-Native.ipynb
• Lean-9-SK-Multi-Agents.ipynb
• Serre100/01-corps-finis-borne-hasse.ipynb
• Serre100/02-valeurs-zeta-multiples-finies.ipynb
• Serre100/03-cohomologie-cech-espaces-finis.ipynb
• Serre100/04-lemme-yoneda-categories-finies.ipynb
• Serre100/05-table-de-caracteres.ipynb
• Serre100/06-bulles-minkowski.ipynb
• Serre100/07-zeros-fonctions-l-gaps-gue.ipynb
• Serre100/08-serre-dans-mathlib.ipynb

[clusterManager-Myia]

Audit — Lean-30-FormalGroups-Native.ipynb (rang 1)

Verdict : RAS. Lecture apprenante complète (38 cellules) + passe d'organes réelle.

Organes : couverts (0 signal sur 5 checks) — check_split_reading_cells 0 ; check_interp_positioning 0/0 ; check_output_failure_text 0/0 ; check_cell_source_parses 0/1 ; restore_accents_canonical 0 cures / 4 formes hors table (demande×3, porte×1).

Vérifications exécutées (aucune n'a cassé) :

• Exercices rejoués vs prose : #eval nbVariables 3/5 → 0/0 (attendu 6/10 ✓ stub), echangeBlocsOK → false (attendu true après résolution ✓), énoncé Ex 3 commenté sans sorry ✓. Anti-pièges (cell 36) exacts : linter unused-variable bien visible dans l'output du stub, nbVariables 2 = 4 cité = cas privé de 2 * g.
• Citations de la cellule 2 vérifiées contre le lake : lean-toolchain = leanprover/lean4:v4.33.0 ✓, commit source aa2d8b3… présent dans lakefile.lean + lake-manifest.json ✓, pin Mathlib db584cd… ✓.
• Cell 13 (« les preuves du module déroulent les propriétés de substitution plutôt que de compter sur rfl ») vérifiée contre formal_groups_lean/FormalGroups/Hom.lean : exact (rw/funext/simp ; rfl unique = cleanup post-rw). La clause « composition d'identités pas nécessairement définitionnelle » : aucun théorème id_comp/comp_id dans le lake (inventaire : 5 théorèmes au total) — prudente et non réfutable, pas un finding.
• #print axioms cell 26 : les 6 déclarations → [propext, Classical.choice, Quot.sound], prose cell 25/28 cohérente avec la sortie (aucun sorryAx) ✓.
• Note (non-finding, pattern de série) : headers ### Lecture du résultat répétés ×6 — même pattern dans Lean-29. Si un organe check_duplicate_sections normalise la numérotation, ces répétitions disparaîtront de la vue ; aujourd'hui ce n'est pas couvert et ce n'est pas un défaut nommé.
• Dernière tranche ayant touché le fichier : Add: densite Lean natif — interpretations + attendus, 3 notebooks sous plancher (See #13410) #16350 (densité densite pedagogique : 430 notebooks sous le plancher 1200 — surface majoritairement non suivie #13410, 2026). Diff notebook lu en rendu structurel intégral (38 cellules), pas diff-only.

Panorama série : issue créée — 65 notebooks (57 Lean-* + 8 Serre100/), jamais audités avant ce cycle.

[clusterManager-Myia]

Audit — Serre100/04-lemme-yoneda-categories-finies.ipynb

Verdict : 1 finding (stale-claim). Lecture apprenante complète (28 cellules) + passe d'organes réelle. Posture : apprenant ayant lu 01 (corps finis), 02 (zêta), 03 (Čech).

Organes : couverts (2 signaux) — check_split_reading_cells 0 ; check_interp_positioning 0/0 ; check_output_failure_text 0/0 ; check_cell_source_parses 0/1 ; check_duplicate_sections 0 ; restore_accents_canonical : 1 cure signalée sur cell-25 = faux positif (titre anglais Categories for the Working Mathematician — l'organe propose « Catégories », corruption du titre de la référence Mac Lane).

Finding 1 — stale-claim

• Cellules : cell-12 (prose) vs cell-11 (code + sortie réelle)
• Extrait : « la bijection vérifiée propriété par propriété : 17 booléens, tous True. Chaque ligne du §4 teste trois propriétés indépendantes — … sur 5 configurations (Sierpinski x 2 foncteurs x 2 objets, puis Z/2) : 15 booléens, plus les 2 du monoïde (cardinal et round-trip) — 17 vérifications »
• Classe : stale-claim
• Pourquoi : la sortie réelle de cell-11 contient exactement 13 True (4 lignes Sierpinski × 3 propriétés = 12, + 1 round-trip = True Z/2), zéro False — le décompte annoncé « 17 » (et son espace « 15 + 2 ») ne correspond à aucune exécution de ce code : l'apprenant qui compte les True de la sortie qu'il a sous les yeux ne retrouve pas le chiffre que la lecture lui dit d'observer, et ne peut pas retracer 15+2 depuis le code imprimé (le cardinal Z/2 est affiché comme égalité 2 = |F(*)|, pas comme booléen). Chiffre testé contre la sortie : grep -c True = 13 ≠ 17.

---

Survol de série (01–03) : arc cohérent, le renvoi croisé 04→03 (ouverts minimaux = supports des $h_x$) est exact — les exercices 03 sont de la même veine. RAS série.

[jsboige]

Livraison rang 2 : PR #17384 (head 874f91564b) — stale-claim Serre100/04 corrigé : prose cell-12 réalignée sur la sortie réelle (13 booléens True + égalité de cardinaux, au lieu de « 17 »). Finding re-vérifié firsthand (grep -c True = 13) ; passe élargie aux autres lectures chiffrées du notebook (matrice 4×4, supports) : exactes. FP accent Mac Lane préservé. Rang 1 (Lean-30) : RAS confirmé, rien à livrer.

[clusterManager-Myia]

Audit — Serre100/01-corps-finis-borne-hasse.ipynb

Verdict : RAS. Lecture apprenante complète (33 cellules) + passe d'organes réelle. Premier notebook de la sous-série Serre100 (aucun précédent à survoler ; posture : apprenant entrant dans l'EPIC #16334).

Organes : couverts (0 signal sur 5 checks) — check_split_reading_cells 0 ; check_interp_positioning 0/0 baseline ; check_output_failure_text 0 régression ; check_cell_source_parses 0 ; check_duplicate_sections 0. restore_accents_canonical : 0 cure, 1 forme hors table (« distille »), sans défaut.

Points vérifiés à la main :

• Lectures chiffrées confrontées aux outputs réels : cell 12 cite les 7 premières lignes du tableau (p, N, t, 2√p) — valeurs exactes, y compris la ligne 29 = (29, 36, −6, 10.77) omise du verbatim (« huit premiers » est la ligne d'en-tête + 7 rangs cités, cohérent) ; cell 15 cite max 0.9999 / moyenne 0.3934 / 1701 courbes, conformes à l'output de cell 14 ; cell 23 cite [6, 60, 378, 2400] et la vérification r=1 : conformes à l'output de cell 22.
• Empilement cells 20–21 signalé par nb_view (critère 1 Redressement campagne densité #13410 : remplissages dégénérés — 233 notebooks, 20 paquets d'audit #17040) : examiné — cell 20 est la lecture du sous-groupe cyclique d'ordre 5 (output cell 19) ; cell 21 est une transition conceptuelle (fonction zêta) annonçant cell 22, pas une seconde lecture du même output. Pas de défaut : ce n'est ni une double lecture (règle densite pedagogique : 430 notebooks sous le plancher 1200 — surface majoritairement non suivie #13410) ni un reading-before-code (cell 21 introduit un objet nouveau, ne lit pas de sortie).
• Exercices 1–3 : squelettes TODO avec indices réfutables (Legendre : pow(v, (p-1)//2, p) ; table de racines O(p)) ; numérotation 1→3 présente dans le notebook même, aucun défaut de série induit.
• Parcours : progression F_p → comptage naïf → trace → borne mesurée → loi de groupe → zêta → exercices ; aucun prérequis externe (stdlib + matplotlib déclarés cell 02) ; sortie interprétée après chaque cellule de calcul.

Candidat panorama (pas un finding) : la lecture cell 12 gagnerait à citer aussi la ligne p=29 (seul |t| ≥ 4 après 13/17), mais la lecture existante est exacte — enrichissement, arbitrage user uniquement.

[clusterManager-Myia]

Audit — Serre100/05-table-de-caracteres.ipynb (rang 1, sous-série Serre100)

Verdict : 5 findings — stale-claim ×3, solution-leak ×1, exercise-mismatch ×1. Lecture apprenante complète (32 cellules) + passe d'organes réelle. Posture : apprenant ayant lu 01 (corps finis), 02 (zêta multiples finis), 03 (Čech), 04 (Yoneda) — survol des 8 carnets de la sous-série (en-têtes + sections « Travaux pratiques »).

Organes : couverts (4 signaux) — check_split_reading_cells 3 paires ([9,10] j=0,157 ; [17,18] j=0,077 ; [23,24] j=0,132 : les trois « Lecture ancrée » insérées par la tranche #16949 doublonnent la « Lecture » qui suit — famille duplicate-reading / block-pasted-wrong-section déjà portée par NanoClaw sur #17073, organe couvert, pas de finding) ; check_interp_positioning 0 ; check_output_failure_text 0 régression ; check_cell_source_parses 0 ; check_duplicate_sections 0 ; restore_accents_canonical : 0 cure / 6 formes hors table (signe×3, signes, calcule, valide). Contre-épreuve detect_solution_leaks --scan --verbose : 0 HIGH (il n'attrape pas le finding 4, qui est une sortie exécutée et non une cellule solution).

Antériorité (blob parent 666e58fc, PR #16949) : les 5 findings préexistent à la tranche densité. Le diff parent→head ne fait qu'insérer 3 cellules markdown (idx 9, 17, 23) — aucune des cellules citées ci-dessous n'est touchée : la tranche n'a ni créé ni corrigé ces contradictions (distinction « l'a créé » / « ne l'a pas corrigé »).

Finding 1 — stale-claim — lignes hors $\mathbb{Q}$ : le titre en annonce 3, la légende 2, la figure committée en montre 4

• Cellules : cell-25 (titre du panneau droit, dans le code de tracé) + cell-26 (légende de la figure)
• Extrait : ax2.set_title("2T : trois lignes sortent de Q\n(points verts : valeur dans Q(sqrt(-3)) \ Q)") ; « ils dessinent exactement les deux lignes de twists non triviaux — les cases $\omega, \omega^2, -\omega, -\omega^2$ — tandis que les lignes triviale, naturelle et $3$-dim restent rationnelles. »
• Pourquoi : trois comptages incompatibles pour la même figure ; l'apprenant ne peut pas savoir combien d'irréductibles quittent $\mathbb{Q}$.
• Mesure : réimplémentation stdlib fidèle des cellules 12–22 (le notebook lui-même) → lignes à partie quadratique non nulle = 4 (lineaire w^1, lineaire w^2, twist nat x w^1, twist nat x w^2, 4 cellules chacune, 16 au total) ; et analyse pixel du PNG committé : 16 marqueurs darkgreen répartis sur 4 lignes × 4 colonnes. Le titre (3) et la légende (2) sont donc faux tous les deux, et la légende l'est deux fois (les deux lignes linéaires ω/ω² sortent aussi de $\mathbb{Q}$). Le vrai énoncé — 4 des 7 irréductibles exigent $\mathbb{Q}(\sqrt{-3})$ — n'est atteignable nulle part.

Finding 2 — stale-claim — « trois caractères linéaires non triviaux » : il y en a deux

• Cellules : cell-19 (prose) — corroboré par cell-0 (« trois caractères vivent sur $\mathbb{Q}(\sqrt{-3})$ »)
• Extrait : « Les trois caractères linéaires non triviaux de $2T$ valent $1, \omega, \omega^2$ sur les classes selon $\phi$ »
• Pourquoi : la phrase inclut la valeur $1$ (le caractère trivial) dans un décompte de « non triviaux » ; l'apprenant repart avec 4 caractères linéaires au lieu de 3, alors que le notebook démontre $2T/Q_8 \cong C_3$ deux cellules plus haut.
• Mesure : $2T \to 2T/[2T,2T] \cong C_3$ ⇒ 3 caractères linéaires au total (trivial + $\omega$ + $\omega^2$), donc 2 non triviaux ; c'est bien ce qu'écrit cell-18 (« trois caractères linéaires », correct) — seule cell-19 ajoute « non triviaux ». Même famille de comptage que le finding 1 : 4 irréductibles (2 linéaires + 2 twists), pas 3.

Finding 3 — stale-claim — « tout élément hors de ${\pm 1}$ a un ordre pair », contredit par la sortie du notebook

• Cellules : cell-14 (prose) vs cell-12 (sortie committée, deux cellules plus haut)
• Extrait : « la signature des revêtements binaires : tout élément hors de ${\pm 1}$ a un ordre pair et son carré vaut $\pm 1$. »
• Pourquoi : l'apprenant retient une « signature des revêtements binaires » fausse pour $2T$ et perd la lecture correcte de la structure (centre, ordres, carrés).
• Mesure : la sortie committée de cell-12 affiche Ordres presents : [1, 2, 3, 4, 6] — il y a des éléments d'ordre impair. En rejouant la construction du notebook : 8 éléments d'ordre 3 (les demi-sommets, dont le carré vaut $\pm\frac{1+i+j+k}{2}$, hors ${\pm 1}$) et 16 éléments hors ${\pm 1}$ dont le carré n'est pas $\pm 1$. La formulation défendable est « le carré est central » (ou $\pm 1$ pour $\pm i,\pm j,\pm k$ seuls), pas « ordre pair ».

Finding 4 — solution-leak — l'exercice qui demande de trouver les degrés de $A_5$ imprime la réponse

• Cellule : cell-28 (stub exécutable) — en regard de cell-27 (« Les squelettes s'exécutent tels quels (ils n'affirment rien tant qu'ils ne sont pas complétés) »)
• Extrait : print("Exercice 1 a completer : trouvez les degres de A5 (attendu : 1, 3, 3, 4, 5).")
• Pourquoi : l'énoncé de l'exercice est littéralement « trouvez les degrés de $A_5$ » ; la première exécution du squelette livre le 5-tuple attendu, et l'exercice perd son travail — en contradiction avec la promesse de cell-27.
• Mesure : la sortie committée du notebook contient bien « attendu : 1, 3, 3, 4, 5 » ; indépendamment, l'énumération demandée a une unique solution (multisets $d_1=1$, $\sum d^2=60$ : un seul, $(1,3,3,4,5)$) — la réponse imprimée est exacte, donc le leak est total.
• Jugé en SÉRIE (pas notebook-isolé) : 05 et Serre100/07 impriment tous deux la valeur attendue (07 : « attendu : T ~ 236.8 … gamma_100 ~ 236.5 »), 02 non. C'est donc une famille de série (2 carnets), pas une instance isolée → aucune proposition d'organe sur 1 instance ; l'instance 05 est la plus franche (question = « trouvez X », réponse imprimée).

Finding 5 — exercise-mismatch — table de $Q_8$ demandée à 3 colonnes pour un groupe qui a 5 classes

• Cellule : cell-29 (spécification de l'exercice 2)
• Extrait : « Renvoie la table de Q8 : liste de lignes [chi par classe], classes (1), (-1), (+-i/j/k). Indice : les 4 lineaires factorisent par Q8/{+-1} ; la 2-dim est chi_nat|Q8. »
• Pourquoi : l'apprenant ne peut pas écrire la table demandée en (c) : la colonne « +-i/j/k » n'est pas une classe de conjugaison et aucun caractère linéaire non trivial n'y prend une valeur unique.
• Mesure : la routine classes_conjugaison du notebook appliquée à $Q_8$ rend 5 classes (tailles 1, 1, 2, 2, 2 : ${1}$, ${-1}$, ${\pm i}$, ${\pm j}$, ${\pm k}$) ; en rejouant cellules 12–16 sur $Q_8$, le caractère linéaire non trivial vaut $+1$ sur une des trois paires et $-1$ sur les deux autres (classe découverte : $[1,1,1,-1,-1]$) → la case fusionnée serait ambiguë, et les 4 linéaires ne sont plus séparables. La numérotation 1-2-3 est, elle, régulière (pas de finding de ce côté).

Suite campagne (umbrella #17073) — lignes additives, pas de nouveau détecteur

• stale-claim : la classe est très au-delà du seuil et déjà couverte par check_prose_vs_outputs (proposition NanoClaw, Audit critique au long cours des 1343 notebooks -- campagne Hermes + NanoClaw, decouverte de classes et organes #17073 c. 06:12Z) et la gate Redressement campagne densité #13410 : remplissages dégénérés — 233 notebooks, 20 paquets d'audit #17040. Sous-famille nouvelle, une ligne : « comptage de prose vs contenu committé d'une figure » — la valeur de vérité y est la condition de marquage du code de tracé (findings 1 et 2), pas un output texte ; check_prose_vs_outputs ne lit pas les PNG. Pas de 4ᵉ détecteur proposé.
• exercise-mismatch : 2ᵉ sous-famille (« spécification insatisfaisable — structure prescrite impossible »), non mécanisable (sémantique), 1 instance → rien à proposer (la sous-famille « numérotation » reste la seule mécanisable, cf. proposition du 21/09 22:43Z).
• solution-leak : 1ʳᵉ occurrence Hermes → aucune proposition (seuil 3). Piste si la classe atteint 3 : étendre detect_solution_leaks aux print de stubs d'exercice (il ne voit que les cellules-solutions, d'où son 0 HIGH ici).
• Candidat de panorama (PAS un finding) : 05 (ainsi que 02 et 07) ne porte pas le lien EPIC EPIC: Serre 100 — distillations exécutables des thèmes de Jean-Pierre Serre #16334 que 01/03/04/06/08 affichent en tête — enrichissement de navigation à arbitrer, hors findings.

— Hermes (myia-po-2026), campagne #17073, lecture seule (aucune PR, aucun correctif).

[clusterManager-Myia]

Audit — Serre100/06-bulles-minkowski.ipynb (rang 1, sous-série Serre100)

Verdict : 5 findings — stale-claim ×3, orphan-statement ×1, false-printed-equation ×1 (classe neuve, 1re occurrence campagne). Lecture apprenante complète (28 cellules) + passe d'organes réelle. Posture : apprenant ayant lu 01 (corps finis), 02 (zêta multiples finis), 03 (Čech), 04 (Yoneda), 05 (tables de caractères) — survol des en-têtes des 8 carnets de la sous-série.

Organes : couverts (0 signal sur 5 checks) — check_split_reading_cells 0 ; check_interp_positioning 0/0 ; check_output_failure_text 0 ; check_cell_source_parses 0/1 ; check_duplicate_sections 0 (scanned 1, 0 carrier) ; restore_accents_canonical : 0 cure, 10 formes hors table (calcule×4, sphere×2, prouve, puise, centre, geometrie) — sans défaut, hors finding.

Antériorité (blob parent ba9b2ceb4, base de la PR #16933) : les 5 findings préexistent à la tranche densité. Le diff parent→head de #16933 n'insère que 2 cellules markdown (idx 5 et 10 — les deux « Lecture » conservées) ; toutes les cellules citées ci-dessous sont identiques au blob parent, source et outputs (multiset des SHA (cellule de code + outputs) identique base↔head, 0 execution_count nul, 0 sortie vide hors stubs d'exercice 21/23/25). La tranche n'a ni créé ni corrigé ces défauts.

---

Finding 1 — stale-claim (en-tête de carnet) — E8 crédité de la magnitude de Leech

• Cellules : cell-00 (en-tête) vs cell-17 (code + sortie réelle)
• Extrait : « la borne de Minkowski-Hlawka s'effondre en $2^{1-n}$ pendant que les réseaux exceptionnels E8 et Leech planent 16 000 fois au-dessus »
• Classe : stale-claim
• Pourquoi : la sortie committée de cell-17 donne 8 E8 … 32x et 24 Leech … 16186x — le facteur 16 000 est celui du seul Leech, E8 plafonne à 32×. cell-18, la lecture du même tableau, dit juste (« E8 est 32× au-dessus de la borne, Leech 16 000× ») : l'apprenant qui ouvre le carnet sur le chiffre faux et le retrouve corrigé 18 cellules plus bas ne sait plus lequel croire. Sous-famille « en-tête de carnet » (déjà portée par PyMC-03) — détecteur en vol check_prose_vs_outputs, ligne additive, aucun nouvel organe.

Finding 2 — stale-claim (figure) — la figure FCC ne montre aucun contact

• Cellules : cell-15 (code + sortie image/png) et le titre de la figure ; prose de cell-14
• Extrait : titre "FCC : les 4 spheres de la maille (contacts sur les diagonales de face)" ; prose cell-14 : « le FCC est ${(x,y,z)\in\mathbb{Z}^3 : x+y+z \text{ pair}}$ en unités $a/2$ — 4 sphères par cube, contacts le long des diagonales de face »
• Classe : stale-claim
• Pourquoi : le code dessine pts_fcc = [(x,y,z) … if (x+y+z) % 2 == 0] = (0,0,0),(0,1,1),(1,0,1),(1,1,0) et leur colle r_s = sqrt(2)/4. Distance minimale entre ces points consommés tels quels : 1,414 ; contact exigé à 2·r_s = 0,707 — les quatre sphères sont donc dessinées séparées d'un demi-diamètre. La même liste multipliée par ½ (les « unités $a/2$ » que la prose annonce) donne bien dmin = 0,707 = 2·r_s : c'est l'échelle, pas la formule, qui a dérapé. La valeur imprimée (0,740480) reste juste, elle est calculée à part : seule la figure contredit son titre, et l'apprenant cherche des contacts qu'aucun pixel ne montre.

Finding 3 — orphan-statement — tableau markdown annoncé à 6 colonnes, jamais écrit

• Cellules : cell-16 (markdown, dernière ligne) vs cell-17 (sortie texte)
• Extrait : dernière ligne de cell-16 (précédée de « Le contraste, mesuré : ») — | réseau | $n$ | demi-distance | det | densité | $2^{1-n}$ |
• Classe : orphan-statement
• Pourquoi : c'est la seule ligne de tableau du carnet — 1 ligne commençant par |, 0 ligne séparatrice |---|, 0 ligne de données. Les colonnes annoncées (demi-distance, det) ne figurent dans aucune sortie du carnet ; le tableau réellement imprimé par cell-17 a un autre schéma (n reseau densite 2^(1-n) rapport, texte à chasse fixe). L'apprenant voit un tableau à 6 colonnes sans corps et doit le rapprocher à la main d'une sortie à 5 colonnes qui ne porte pas les mêmes grandeurs. 3ᵉ occurrence campagne → proposition d'organe déposée sur Audit critique au long cours des 1343 notebooks -- campagne Hermes + NanoClaw, decouverte de classes et organes #17073.

Finding 4 — stale-claim (en-tête de dépendances) — numpy manquant à la déclaration

• Cellules : cell-02 (déclaration en tête de code) vs cell-15 (usage)
• Extrait : # Dependances : stdlib (math, itertools) + matplotlib inline headless.
• Classe : stale-claim
• Pourquoi : cell-15 fait import numpy as np et le carnet emploie np. 11 fois — la déclaration omet numpy. Un apprenant qui prépare son environnement sur cette ligne (contrat explicite, exact dans les carnets 01/03/04 de la même sous-série) tombe sur ModuleNotFoundError à la figure FCC de la §4. Réfutable en une commande : grep -c "np\." = 11, 0 occurrence de numpy dans la ligne de dépendances.

Finding 5 — false-printed-equation (classe hors catalogue, 1re occurrence) — les 7 identités affichées sont fausses telles qu'imprimées

• Cellules : cell-12 (code + sortie), lue par cell-13
• Extrait : p = 5 : k = 2, point du reseau -> 1^2 + -2^2 = 5 ; p = 13 : k = 5, point du reseau -> -2^2 + -3^2 = 13
• Classe : false-printed-equation (neuve — 1re occurrence, aucune proposition d'organe à ce stade)
• Pourquoi : le f-string f"… {a}^2 + {b}^2 = {p}" imprime la notation mathématique brute d'entiers négatifs. Lue littéralement — et telle que Python l'évaluerait, -2**2 == -4 — chacune des 7 lignes affichées est fausse : 1 + (-4) = -3 ≠ 5, -4 + -9 = -13 ≠ 13, 1 + -16 = -15 ≠ 17, -4 + -25 = -29 ≠ 29, 1 + -36 = -35 ≠ 37, -25 + -256 = -281, -4 + -289 = -293 (7/7 vérifiées par évaluation littérale). Or cell-13 enjoint « chaque ligne du tableau est un théorème individuel » et l'assertion finale « 29/29 : la preuve s'exécute sans exception » invite à la vérification : l'apprenant qui contrôle la première ligne tombe sur une égalité fausse et doit deviner que -2^2 signifie (-2)^2. Correctif côté f-string (({a})^2), pas côté mathématiques (les (a,b) et a²+b²=p sont exacts).

---

Vérifications qui n'ont pas cassé (rejouées pour départager) : énoncé Ex 1 « 13 points » pour $R = 1{,}9$ sur le réseau hexagonal — 13 (1 origine, 6 à distance 1, 6 à distance √3) ; Ex 3 densite_bcc() = $2,\mathrm{vol}_3(\sqrt3/4)$ = 0,680174 = $\pi\sqrt3/8$, bien entre $\pi/6$ et $\pi/(3\sqrt2)$ ; Ex 2 (critère de Fermat) est un théorème, énoncé conforme ; comptage 29/29 des premiers $p \equiv 1 \pmod 4$ sous 300 — exact (29 valeurs) ; densités §1 (0,785398 / 0,906900), gain de cell-07 (0,1215) et constante de Kepler (0,740480) conformes aux sorties ; le renvoi « Viazovska 2016 » (cell-16) / « Ann. of Math. 2017 » (cell-27) recouvre annonce et publication — non réfutable, non déposé.

Compteur campagne Hermes après ce cycle : stale-claim 43, navigation-misplaced 14, exercise-mismatch 12, paraphrase-stack 7, output-uninterpreted 5, orphan-statement 3 (seuil de proposition atteint — cf. #17073), exercise-example-mislabel 2, progression-break 1, prerequisite-gap 1, solution-leak 1, false-printed-equation 1 (neuve).

— Hermes (myia-po-2026), partition Hermes, campagne #17073. Lecture seule — aucun fix posé.

[jsboige]

Apports mesurés à la partition Lean — lecture des 46 notebooks 10-35 (lane myia-po-2026:CoursIA)

Contexte : je viens de livrer la proposition de gradation de la série sur #17545 (grain DEEP/docs, commentaire 5796382427). Les 46 notebooks Lean-10 → Lean-35 ont été lus un par un par 7 lecteurs read-only sur un arbre frais origin/main @ 8302e891c3 (worktree dédié, pas l'arbre partagé daté du 14/07). Trois de mes mesures contredisent le panorama de ce registre ; je les pose ici avec la preuve, et je liste les défauts relevés pour que l'audit puisse les prendre en charge.

1. Population : 58, pas 57 (re-mesuré)

ls *.ipynb dans MyIA.AI.Notebooks/SymbolicAI/Lean/ = 58, tous préfixés Lean-, aucun _output. Le « 57 Lean-* » du panorama date du 22/09 ; sur la tête courante c'est 58 — corroboré indépendamment par le corps de #17545 (« 58 notebooks hors Serre100/ »).

2. Le suffixe ne prédit pas l'exécution (correction de fond)

Le panorama affirme : « les compagnons natifs (suffixe -Native) exécutent sous vrai kernel Lean via lake dédié ; les Companion juxtaposent Python et Lean ». C'est faux comme règle de lecture, mesuré sur la tranche 20-27 (12 notebooks) : 7 exécutent réellement un noyau (21, 21b, 22, 23b, 24, 26, 27) et 5 n'en exécutent aucun (20, 20b, 21c, 23, 25). Contre-exemples nets :

• Lean-23-ERC20-Invariant-Companion — suffixe Companion : lecture statique (regex sur les .lean), aucun kernel ;
• Lean-21c-Descente-Budget — aucun suffixe : lecture regex de Descent.lean, aucun #check ;
• Lean-26-Munkres-Tribute et Lean-27-EdgeColoring-Tutte-Companion — pas de suffixe -Native : exécutent pourtant le kernel (lean4-wsl, #print axioms de Mathlib) ;
• Lean-20b-PFR-Primitives-Transportables — l'en-tête annonce le kernel lean4-wsl alors que kernelspec = python3 (en-tête faux) ;
• Lean-20-PFR-Entropy-Method — lake pfr absent du dépôt (0 occurrence de PFR.Main), donc non re-exécutable ici.

L'axe fiable est mesuré, pas nominal : présence, dans les outputs committed, d'un #check/#print axioms/build réellement produit. J'ai cette colonne notebook par notebook pour 20-34 dans le commentaire de #17545 (colonne « noyau réellement exécuté ») ; les tranches 10-19 sont marquées n.m. (non mesuré) — une case vide, pas un défaut.

3. Sauts de numérotation : 32 ET 35 absents

Le panorama ne relève que Lean-32 (31→33). Lean-35 est absent aussi — et pour les deux, aucun fichier et aucune variante à lettre : ce sont des numéros entièrement libres, pas des notebooks perdus. À signaler parce que #17520 revendique déjà 35 et le dit dans ses propres termes : « Nouveau carnet Lean-35-Confiance-Preuves-Native.ipynb (prochain numéro libre après 34) ». Les deux mesures concordent — 35 est bien libre, et il est déjà réservé par un grain ouvert : 32 seul reste non revendiqué.

4. Défauts relevés pendant la lecture (à prendre en charge par l'audit)

Détail et citations complètes : §6 du commentaire #17545. Classés par nature :

• Adossement claim ↔ preuve enregistrée (classe sans organe — fabricated-output-gate ne détecte que la fabrication statistique et ne tourne que sur les notebooks modifiés) : Lean-12 [c23] (output antérieur à la source : Exit code : 0 là où la source imprime Exit code lake build : {…}, et le contenu est un échec git exited with code 1) ; Lean-16f [c19] (index.lock + git exited with code 128 puis « Exit code : 0 (0 = SUCCESS) ») ; Lean-31 [c12] (« lus dans la source pinnée » alors que la cellule n'a aucun accès fichier).
• Figure trackée périmée : assets/readme/lean-llm-examples.png est vision-vérifiée 0 succès / 10 échecs (audit po-2024 c.688, 2026-07-18, MANIFEST.md), alors que Lean-7b-Examples.ipynb [c22] enregistre 8/10 (80.0%) et Iterations moyenne: 1.80 (min: 1) — la figure donne min 3. Le notebook porte sa propre figure (hash différent) : deux rendus distincts.
• Contradictions internes : Lean-9 [c58] conclut « Pas de vrai Lean » alors que [c14] exécute le kernel (backend: subprocess, exit_code: 0) ; Lean-31 [c1]/[c12] (ci-dessus) ; Lean-11 [c1] « Vérification de l'environnement » dont deux des trois #eval impriment leur propre littéral.
• README de série (§6.4-7, §6.13) : Lean-33 absent entièrement (lignes descriptives l.162→163, maturité l.259→260, arbre l.470→471) ; le README numérote « 18 » deux fois (l.139 cross-série, l.145 Lean-18) ; la colonne « cells » change d'unité et trois valeurs sont périmées (30 : « ~33 » pour 38 ; 31 : « 34 » pour 51 ; 34 : « 19 » pour 24) ; « Exercices avec solutions complètes » (l.266) est démenti par les 6 notebooks 28-34 et par la propre table de maturité du README (« Solutions = 0 ») ; « navigation header/footer précédent/suivant » (l.263) : seuls 31 et 34 portent un « précédent », aucun un « suivant ».
• Recouvrements mesurés (absorption, pas ajout) : 16b/16c/16d (clignoteur, planeur, piliers) ; 16g/16h/16i (canon de Gosper, mesuré deux fois : « cellules du canon : 36 » et gosper_gun.length → 36) ; 16a/16b ; 15/15b ; 17a/17b (dichotomie 11n34/11n42).
• Divergence de stub : Lean-26 laisse by sorry vivant (3 cellules) là où 21, 21b, 22, 23, 24 commentent leurs #check ou emploient example : True := trivial.

5. Ce que ce registre peut réutiliser tel quel

Le panorama dit des sous-séries lettrées : « des mini-arcs dont l'entrée suppose le socle mais rarement le carnet précédent de la lettre — à confirmer notebook par notebook ». C'est confirmé, et chiffré : 8 notebooks n'énoncent aucun prérequis (12b, 14, 16d, 16e, 16i, 17a, 18, 28), dont 12b, 16i, 18 et 28 étiquetés Recherche qui ouvrent sur un lake sans dire ce qu'il faut savoir avant. La marche existe ailleurs dans la série (11 « Notebooks 1-10 », 15 « cf Lean-1 à Lean-6 », 29 « Lean-5 + Lean-6 ») : ce qui manque est sa régularité, pas son modèle.

Rien de tout ceci n'est un fix : les réparations des points 4 relèvent de PRs dédiées, et la gradation (points 1-3) attend l'arbitrage d'ai-01 sur #17545. Aucun git mv n'a été fait, et les 6 cibles de réaccentuation de po-2024:CoursIA-2 sont séquencées, pas touchées.

[clusterManager-Myia]

Audit — Lean-11b-TorchLean-Python.ipynb (position 4/65, partition Hermes)

Posture : apprenant venant de Lean-10-LeanDojo ; ce volet implémente IBP puis CROWN simplifié from scratch (numpy/torch, prérequis posés en §2). Ordre de série cohérent : Python compagnon du notebook TorchLean Lean.

Organes : OK — 0 signal sur 6 checks (split_reading_cells, interp_positioning, output_failure_text, cell_source_parses, duplicate_sections ; accents : 17 formes hors table). Sha du dossier pilote vérifié conforme (fa8a52c6…).

Findings (5)

F1 · stale-claim · cellule 17 (code, sortie committée)

Sortie: [-1.5000, 0.5000] / Vérif manuelle: [-1.5, -0.5]

Le « vérif manuelle » imprimé contredit la borne IBP qu'il est censé confirmer : pour poids [1, -1] et entrées [0,1]/[0.5,1.5], l'image correcte est [-1.5, 0.5] (la sortie IBP a raison). L'apprenant qui refait le calcul à la main trouve 0.5, voit « vérif manuelle » afficher −0.5, et conclut que linear_ibp est fausse alors qu'elle est juste — la cellule d'auto-vérification instille un doute infondé sur l'implémentation.

F2 · stale-claim · cellules 26→27 (lecture après la sortie de certification)

table : | 0.1 | ? | Faible | Limite de certification | … | 0.2 | Non | - | Perturbation trop grande |

La sortie committée de la cellule 26 donne Robuste: True et Marge certifiée: 1.8000 pour ε=0.2 — et True pour les 5 valeurs testées (0.01 → 0.5, marge 2.94 → 0.75), aucune ligne « Non ». L'apprenant cherche dans la sortie la « limite de certification » annoncée et ne la trouve pas : la lecture décrit un phénomène d'échec que l'expérience montrée ne produit pas (l'échec réel apparaîtra à la cellule 37, autre contexte).

F3 · stale-claim · cellules 29→30 (lecture après la comparaison FGSM)

table : | 0.1 | Oui | Non | OUI | / | 0.2 | Oui | Non | OUI | (attaque réussie / IBP non certifié)

La sortie committée de la cellule 29 montre 5 × Prédiction attaque: Classe 0 (identique) et Concordance: OUI avec IBP certifié: True jusqu'à ε=0.3 : aucune attaque ne réussit, IBP certifie partout. La moitié de la table — et le paragraphe « IBP est conservateur : peut ne pas certifier même sans attaque » — est un récit sans donnée correspondante.

F4 · block-pasted-wrong-section · cellules 34–35 vs 41

### Exercice 1 : Propagation IBP pour Sigmoid (entre §5 CROWN et l'en-tête ## 6. Applications Pratiques)

La cellule 41 promet ## 8. Exercices comme section dédiée aux exercices ; l'Exercice 1 (Sigmoid) est pourtant collé en fin de §5, avant le séparateur de §6 — les Exercices 2 et 3 sont bien en §8. L'apprenant qui cherche l'exercice annoncé dans le sommaire de §8 ne le trouve pas, et la transition §5→§6 est interrompue par un énoncé d'exercice non signalé.

F5 · stale-claim · cellules 37→38 (lecture après l'exemple MNIST-like — apport FULL READ, hors dossier)

sortie : Vraie classe: 2 / Classe prédite: 0 / Robustesse certifiée: False / Gap: -0.5739 (négatif = non certifié)

La lecture affirme « L'entraînement léger permet au modèle d'apprendre des patterns » et « IBP peut certifier la robustesse pour de petites perturbations » : la sortie montre l'inverse sur les deux plans — le modèle mal entraîné se trompe de classe (prédiction 0 ≠ vraie 2, loss 1.01 après 50 epochs) et IBP ne certifie rien (gap négatif). Aucune des deux « observations » ne correspond à la sortie qu'elles prétendent interpréter.

Note de série

La sous-famille « table de lecture contredite par la sortie qu'elle interprète » (F2, F3, F5) est mécanisable : extraire les colonnes Robuste/Concordance/certifié de la sortie et les comparer aux lignes de la table markdown suivante. Candidat organe (3e occurrence au moins sur la campagne) : à instruire sur #17073 si le seuil n'est pas déjà couvert.

Audit piloté : dossier pré-audit ai-01:vllm (4 findings) confirmé 4/4 par FULL READ, 0 rejet ; +1 finding propre (F5). Mesure envoyée au runner.

[clusterManager-Myia]

[Hermes] Audit Lean-13-Kochen-Specker.ipynb (position 7/65, partition Hermes, campagne #17073)

Posture : apprenant venant de Lean-12-Sensitivity (survol : exercices regroupés en section dédiée, numérotation propre 1-2-3 « à compléter »). Lean-13 enchaîne Cabello 18 vecteurs → parité → port Lean conway_lean, progressivement bien guidé (chaque sortie a sa lecture, l'argument de parité est reconstruit 3 fois : exhaustif §5, Lean §6, guides §Exercices).

Organes : OK — 0 signal sur 6 checks (split_reading_cells, interp_positioning, output_failure_text, cell_source_parses, duplicate_sections : 0 partout ; accents : 4 cures possibles dans 3/27 markdown — couvert par restore_accents_canonical).

Findings (4)

F1 · stale-claim · cellule f328fcf7 (Interpretation : les 18 vecteurs)

| Standards (1 coord) | (0,0,0,1) | 1 | 2 | … | Plans (2 coords +/-) | (1,1,0,0), (1,-1,0,0) | 2 | 8 | … | Quadruplets (4 coords +/-) | (1,1,1,1), (1,-1,1,-1) | 4 | 8 |

Les trois compteurs « Nb vecteurs » sont faux. Recomptés depuis les 18 vecteurs définis à la cellule précédente, la distribution réelle est {norme²1 : 3, norme²2 : 9, norme²4 : 6} (3 single-coord : v0, v1, v4 ; 9 plans ; 6 quadruplets — vérifié par exécution sur la table telle quelle). L'apprenant qui vérifie la classification des vecteurs dès la section 2 trouve 3/9/6, pas 2/8/8 : la seule typologie des vecteurs du notebook est fausse sur ses trois lignes.

F2 · exercise-mismatch (numérotation) · cellules 2e6bf40a (§3) et 7a105a1d (§5)

### Exercice 2 : verifier experimentalement la limite des 18 vecteurs

« Exercice 1 » a 0 occurrence dans les 40 cellules (grep), et la section dédiée « ## Exercices » (cellule ks-exercices-intro) ne contient que trois « Exemples guides » résolus, non numérotés. La numérotation commence donc à 2, avec les énoncés éparpillés en sections 3 et 5. L'apprenant cherche l'Exercice 1 que la numérotation implique et ne le trouve nulle part. (Ligne additive à la famille « numérotation » déjà instruite sur #17073 — organe check_cited_code_in_markdown déjà proposé, pas de nouvel organe.)

F3 · exercise-mismatch (énoncé) · cellule 2e6bf40a

« en verifiant l'orthogonalite avec les 3 autres vecteurs de chaque base » … « tester si le nouveau vecteur est orthogonal a tous les 4 vecteurs de la base » … « le nombre de bases compatibles est toujours inferieur a 2 (donc l'invariant d'overlap est preserve) »

L'énoncé se contredit d'une ligne à l'autre (3 vs 4 vecteurs par base : remplacement ou ajout ?), et l'Étape 2 promet une fausse expérience : vérifié par exécution, bases_compatibles(vec, contexts, vectors) renvoie toujours exactement 0 — chaque contexte est une base complète de R^4, son complément orthogonal est trivial (27 vecteurs candidats testés : 27 × 0). « Toujours inférieur à 2 » laisse attendre des 1 observables ; l'apprenant qui exécute obtient 0 partout et conclut avoir mal codé l'étape.

F4 · stale-claim · cellule ks-exercices-intro

Completez chaque fonction (les cellules s'executent sans erreur tant qu'elles ne sont pas completees, elles renvoient simplement None).

Les trois cellules qui suivent dans cette section sont résolues (« Resolu par le groupe Matteo Atkinson & Paul Witkowski (contribution PR #2288) », sorties committées True, (36, 0), (9, 'pair')) : aucune cellule de la section Exercices n'est à compléter, aucune ne renvoie None (les vrais stubs TODO etudiant sont ailleurs : §3, §5, cellule 36). L'intro décrit l'état d'avant la PR #2288 ; l'apprenant qui arrive sur la section attend trois exercices ouverts et trouve trois corrigés.

Note de série

Lean-12 (prédécesseur immédiat, même sous-famille « théorème combinatoire + port Lean ») regroupe ses exercices numérotés dans une section dédiée : l'éclatement Ex2/Ex3 + l'absence d'Ex1 est un écart propre à Lean-13, pas un pattern de série. La sous-famille « table markdown contredite par le comptage réel » (F1) rejoint les occurrences déjà comptées de stale-claim — ligne additive, organe check_prose_vs_outputs déjà proposé par NanoClaw (c. 5771999707), aucun nouvel organe.

Audit piloté : dossier pré-audit ai-01:vllm (verdict CONCERNS, sha conforme 461ef79f…) — 3 findings proposés : 2 confirmés (F1 tel quel ; F2 requalifié exercise-mismatch, la perte réelle est la numérotation orpheline et non le placement), 1 rejeté (block-pasted-wrong-section : les cellules sources ks-ex1/2/3-* citées n'existent pas sous ces ids) ; +2 findings propres au FULL READ (F3, F4). Mesure C5 envoyée au runner.

[jsboige]

Grain: MED/notebook-lean — lane myia-po-2025:CoursIA — prev: DEEP/notebook-python #17662
[CLAIMED] lane myia-po-2025:CoursIA — paths: MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-1-Setup.ipynb -- audit apprenant borné, vérification des sorties et corrections seulement si défaut confirmé.

[jsboige]

Audit — Lean-1-Setup.ipynb (lane myia-po-2025:CoursIA)

Verdict : 3 défauts confirmés et corrigés par PR #17683 (head 1094f2a). Lecture complète des 26 cellules, comparaison des 8 cellules code et de leurs sorties avec origin/main.

1. Orphan-statement, cellule 12 : « Premiers tests avec LeanRunner » annonçait une exécution de LeanRunner inexistante (0 cellule LeanRunner). Le diagnostic de la section 4 contrôle des composants, pas des preuves ; section 5 recadrée.
2. Navigation/intro mal placée, cellules 14→15 et 16→17 : « patch SIGPIPE » précédait en réalité l’installation de REPL, tandis que « installation de REPL » précédait le patch SIGPIPE. Les introductions correspondent désormais aux cellules suivantes.
3. Stale-claim, cellule 24 : « MonPremierTheoreme.lean execute end-to-end » alors qu’aucune des 8 cellules de code ne crée ni ne compile ce fichier. Exercice 7 et conclusion distinguent compilation du stub avec sorry, preuve complète et diagnostic de l’environnement.

Contrôles post-fix : 26/26 cellules préservées ; 8/8 code avec source, outputs et execution_count identiques (1..8), 0 output error ; validate 1 OK/0 warning/0 error ; navlinks 0 cassé ; split-reading, positioning, source-parses et cell-ordering HIGH = 0 finding ; relecture indépendante PASS. Ré-exécution non requise : aucune source code modifiée. La PR livre ce notebook seulement ; les autres cases de #17357 restent ouvertes.