[jsboige]

Grain: DEEP/notebook-dotnet -- lane myia-po-2024:CoursIA-2 -- prev: DEEP/notebook-python #24361

Ce que fait cette PR

Trois carnets de la série Z3-Linq2Z3 créditent explicitement, dans leur cellule d'introduction, l'ouvrage-ancrage de la série : Yurichev, SAT/SMT by Example (édition du 12 février 2023). C'est le travail 3 de l'issue #19278 (« si un notebook reprend un exemple du livre presque tel quel, la cellule d'intro le crédite explicitement »).

Chaque crédit porte la section exacte et le folio imprimé relevés sur la copie archivée (G:\Mon Drive\MyIA\IA\Bibliographie IA\Symbolic\2023 - SAT_SMT_by_example.pdf) : l'attribution est écrite depuis l'ouvrage, pas depuis un résumé. Le crédit distingue en outre ce que le carnet reprend (le cadre d'encodage) de ce qu'il n'emprunte pas (l'instance) — c'est l'apport de cette PR sur son propre premier jet.

Carnet	Section de l'ouvrage	Folio imprimé	Ce que le carnet reprend
13_Cryptarithmetic_SMT.ipynb	§8.10 « Alphametics »	p. 276	l'instance : SEND + MORE = MONEY, mêmes lettres (S E N D M O R Y), même équation positionnelle
02_Sudoku_Theorem_vs_Array.ipynb	§8.1.2 « Simple sudoku in SMT using functions and array »	p. 212	le cadre d'encodage (domaine 1..9, une valeur par case, trois cases distinctes par bloc) — l'instance est propre au carnet
18_Einsteins_Riddle.ipynb	§8.2 « Zebra puzzle (AKA Einstein puzzle) »	p. 232	le cadre d'encodage (une variable entière par couple attribut/valeur, Distinct par groupe, voisinage encodé en différence de 1) — l'instance est propre au carnet

Mesures (firsthand, sur la copie archivée)

Instrument : PyMuPDF 1.27.2.3. Folio imprimé = index de page PDF − 1 (index 0-based ; la page 206 porte le folio 205, la page 277 porte le folio 276). Les numéros de section sont relevés sur la page : le sommaire imprimé (folio 6) et le corps divergent.

• §8.1 (p. 205) — la grille du livre est le « world's hardest sudoku ». Reconstituée par la géométrie du dessin (10 verticales et 10 horizontales de get_drawings(), chiffres positionnés par get_text("words")) :

  ..53.....
  8......2.
  .7..1.5..
  4....53..
  .1..7...6
  ..32...8.
  .6.5....9
  ..4....3.
  .....97..
  

  soit 23 indices — ceux de http://www.norvig.com/sudoku.html et du « world's hardest sudoku » de mirror.co.uk (la mention « 23 clues, from … » figure en légende, folio 232).

• La grille du carnet 02 est celle de Norvig à 30 indices (5 3 . . 7 . . . . / 6 . . 1 9 5 . . . / . 9 8 . . . . 6 . / 8 . . . 6 . . . 3 / 4 . . 8 . 3 . . 1 / 7 . . . 2 . . . 6 / . 6 . . . . 2 8 . / . . . 4 1 9 . . 5 / . . . . 8 . . 7 9), absente de l'ouvrage : recherche exhaustive sur le texte intégral, séparateurs effacés (chaîne de 81 chiffres, et chacune des 9 lignes prise isolément) → 0 occurrence ; et reconstruction de toutes les grilles 9x9 dessinées dans les 666 pages → seule la page 205 porte la grille du livre.

• §8.2 (p. 232) — l'instance du livre est le puzzle canonique : 14 indices (de « 1. There are five houses. » à « 15. The Norwegian lives next to the blue house. »), conclusion imprimée « Now, who drinks water? Who owns the zebra? », et la réponse canonique est que c'est le Japonais qui possède le zèbre. Le carnet 18 en résout une autre : 15 indices, attributs renommés (le Japonais devient l'Allemand, le zèbre devient le poisson), et la position de la verte inversée (immédiatement à gauche de la blanche, et non à droite de l'ivoire) — d'où la solution affichée « l'Allemand qui possède le poisson ».

• §8.10 (p. 276) — le cryptarithme est le même : l'ouvrage imprime SEND + MORE = MONEY et l'équation 1000·S+100·E+10·N+D + 1000·M+100·O+10·R+E == 10000·M+1000·O+100·N+10·E+Y ; le carnet 13 reprend lettres et équation à l'identique.

• Date d'édition confirmée sur la page de titre : « February 12, 2023 ».

Ce que la vérification des instances change

Le crédit doit dire ce qui est repris, pas seulement cité. Confronté instance par instance à l'ouvrage, le premier jet de cette PR créditait les trois carnets comme reprenant « un exemple du livre » — vrai pour un seul.

Carnet	Crédit initial	Crédit mesuré
13	reprend l'alphamétique du livre	inchangé — l'instance est identique
02	reprend « la même grille d'exemple »	corrigé — l'encodage vient de §8.1.2 (p. 212) ; l'instance du livre (§8.1, p. 205) est une autre grille
18	reprend le puzzle Zebra	corrigé — le cadre d'encodage vient de §8.2 (p. 232) ; l'instance résolue est une variante renommée

Les cellules d'introduction des carnets 02 et 18 disent désormais cela. Le carnet 13 n'est pas modifié par cette correction : son crédit était déjà exact.

Portée

• Cellules markdown uniquement (cellule 0 de chaque carnet) : aucune cellule de code touchée, donc pas de ré-exécution due (C.2 sans objet). Les entrées, sorties et metadata sont celles de main : le diff ne porte que sur la source de la cellule d'introduction.
• python scripts/notebook_tools/check_prose_quantitative_claims.py --diff origin/main...HEAD : rc=0.
• Hooks notebooks joués à la main (les hooks pre-commit ne tournent pas dans un worktree .tmp/) : strip_probe_banner, strip_machine_paths, scrub_papermill_paths, fix_source_newlines, fix_hr_separator → 0 correction ; check_encoding_corruption, check_null_exec, check_cell_source_parses → OK ; detect_markdown_rendering --check → OK.
• Tranche 1 du même issue (mapping carnet ↔ livre dans les deux README de la série) : PR Docs(smt,#19278): confirmer le mapping carnet <-> livre Yurichev (sections et folios lus sur le PDF archivé) #24571. Les autres carnets de la série (04, 05, 14, 15, 16, 17, 20) n'y portent pas de crédit d'instance : leur correspondance avec l'ouvrage est thématique, pas d'instance — le mapping par section et folio est dans Docs(smt,#19278): confirmer le mapping carnet <-> livre Yurichev (sections et folios lus sur le PDF archivé) #24571.

Fichiers

• MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/02_Sudoku_Theorem_vs_Array.ipynb
• MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/13_Cryptarithmetic_SMT.ipynb
• MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/18_Einsteins_Riddle.ipynb

See #19278

🤖 Generated with Claude Code

[github-actions]

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

[github-actions]

Golden-Set Execution (H.7 P3)

✅ 9/9 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	5.5s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	4.5s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	5.2s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	4.3s
Search-01-StateSpace.ipynb	✅ SUCCESS	5.7s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	3.5s
RL-04-Bandits-Manchots-Python.ipynb	✅ SUCCESS	34.7s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	2.7s
GameTheory-13d-Optimistic-CFR-Python.ipynb	✅ SUCCESS	11.2s

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

[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]

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

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

[github-actions]

Notebook PR Validation: PASS

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

[clusterManager-Myia]

[NanoClaw] structural review (protocole v2 — extraction base d0383967 / head 5d4fb55b, cell-diff intégral des 3 notebooks, jamais de JSON brut en contexte)

VERDICT: LGTM (vérifié: cell-diff exhaustif 02/13/18 + ancrage de chaque affirmation interne sur le contenu des carnets)

Périmètre mesuré : 3 notebooks MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/ (02 Sudoku, 13 Cryptarithmetic, 18 Einsteins_Riddle), +15/−3. Le diff réel = ajout d'un bloc ## Source en fin de cellule d'introduction dans chacun des 3 carnets. 0 cellule code modifiée, 0 ligne supprimée (les 3 « − » sont les fins de cellule reclôturées par l'ajout) — aucune matière perdue, aucun retrait à justifier.

Ancrage des affirmations internes (gate 4bis : toute valeur citée doit se retrouver dans le carnet) :

• 02 Sudoku : « le carnet en résout une autre, à 30 indices » → ancré : la grille de cellule 21 porte exactement 30 non-zéros, et le code affiche givenCount} indices sur 81 cellules (compteur committé). « tableau de 81 cellules » → ancré (s.Cells[i*9+j], List<int> de 81). Les 23 indices / folios §8.1 p. 205 du livre = référence externe déclarée (« relevés sur l'ouvrage archivé »), non re-mesurable depuis ce siège.
• 13 Cryptarithmes : « l'exemple SEND + MORE = MONEY » → ancré (15/15/13 occurrences SEND/MORE/MONEY dans le carnet). §8.10 p. 276 = externe déclaré.
• 18 Einstein : « l'Allemand qui possède le poisson » → ancré dans les outputs committés (« >>> Reponse : le Allemand possede le Poisson (maison 4) ») ; « quinze indices au lieu de quatorze » → ancré (commentaire d'en-tête cellule 3 : « 5 maisons, 5 attributs, 15 indices ») ; « la verte immédiatement à gauche de la blanche » → ancré littéralement (t.Green == t.White - 1 dans les contraintes) ; renommages (Japonais→Allemand, zèbre→poisson) → cohérents avec la classe committée (German, pas de Japanese).

Scans : secrets = 0 (le chemin G:\Mon Drive\… cité ci-dessous n'est pas un credential) ; ec-null = sans objet (aucune cellule code touchée) ; papermill = inchangé (02 conserve ses métadonnées anciennes 2026-06-11, µs non rondes — cohérent avec cellules non ré-exécutées ; 13/18 n'en portent pas). Aucune re-exécution prétendue.

🟡 Observation mineure (non bloquante) : les 3 blocs citent la copie archivée par son chemin local Windows G:\Mon Drive\MyIA\IA\Bibliographie IA\Symbolic\2023 - SAT_SMT_by_example.pdf — exact pour l'archivage interne, mais illisible pour un étudiant hors du poste. Une référence bibliographique imprimable (auteur, édition du 12/02/2023, ISBN ou URL éditeur) en complément rendrait le crédit autosuffisant.

Review structurelle déclarée : organe C# non exécutable depuis ce siège (python/dotnet absents du conteneur, convention #16098) — la vérification porte sur les sources et outputs committés, pas sur une re-exécution.

[jsboige]

[ACTION] Rouge CI unique réparé — commit 5335e0d7da (poussé sur la branche).

Mesure : dans le log du fastlane, 54 gardes évaluées, un seul exit 1 — prose-counts (tous les autres à exit 0, y compris perimeter-review-guard, les ratchets Output-*, check-nav-chain, cell-source-parses).

La cause : la cellule ## Source du carnet 02 annonçait « L'encodage par tableau de 81 cellules » — un compteur d'artefact en prose (classe artifact de check_prose_quantitative_claims.py), que rien ne remesure et qui dérive dès qu'un tiers touche au carnet. Le carnet emploie par ailleurs « 81 propriétés » et « 81 éléments » : même mot, mais ces deux-là sont dans des phrases antérieures à cette PR, donc hors du périmètre --diff de l'organe.

La phrase devient « L'encodage par tableau d'une grille de 9 par 9 » : la taille est dite en mots, et le propos — le crédit porte sur l'encodage tableau de §8.1.2 (p. 212), pas sur l'instance — reste intact.

Vérifié sur le nouveau head : python scripts/notebook_tools/check_prose_quantitative_claims.py --diff origin/main...HEAD --strict → rc=0, « aucun compteur quantitatif en prose ».

Modification markdown seule (cellule 0 du carnet 02) : aucune cellule de code ni aucune sortie touchée, donc pas de ré-exécution due au sens de C.2/C.3 ; les hooks pre-commit du carnet (bandeau probeAddresses, chemins machine, chemins papermill, séparateurs, fins de ligne, encodage, null-exec, cell-source-parses) ont été joués à la main dans ce worktree : tous no-op, le diff reste à 1 ligne.

Le PR gate qui portait CANCELLED l'est pour une cause externe : son annotation dit STARVED -- every pending constituent is queued with no runner (pool saturated) ; son propre texte precise que « waiting cannot change the verdict until a constituent starts ; the stale sweep re-drives this gate when runners free up (#13363) ». Ce n'est pas un défaut de cette PR.