fix(notebook,#19240): Sudoku Tranche B -- provenance allegee

MyIA.AI.Notebooks/Sudoku/Sudoku-13-SymbolicAutomata-CSharp.ipynb

@@ -2903,22 +2903,22 @@
    "source": [
     "## Annexe S10 - Pont `Microsoft.Z3` natif : l'automate symbolique, sans detour\n",
     "\n",
-    "> **Grain DEEP/notebook-dotnet, lane `myia-po-2023:CoursIA-2`, prev: `DEEP/notebook-dotnet #10450`**\n",
-    ">\n",
-    "> **Contexte :** la fiche de parite `scripts/notebook_tools/twin_pairs.d/sudoku-13-symbolicautomata.yaml` porte aujourd'hui `bridge_verdict: INTRINSIC` au motif que \"le C# (pur System.* stdlib, 0 NuGet, 18 cellules code) construit la logique d'automate symbolique from scratch\". **L'omission est la suivante** : le notebook utilise deja `Microsoft.Z3` (cellule 17, NuGet officiel, axe 1 du registre #3801), et il resout des **contraintes d'automates symboliques** dans la theorie des chaines - **uniquement en passant par le fork Automata** (cellule 21) ou par `ParseSMTLIB2String` textuel (cellule 26). Cette annexe exhibe le **constructeur d'automate symbolique directement emit en SMT-LIB 2.6 par concatenation C# depuis le notebook**, et le moteur `Microsoft.Z3` qui le resout - **sans fork Automata, sans lib externe**, juste la lib officielle Microsoft.Z3 et la theorie des chaines Z3.\n",
+    "> **Contexte** : la fiche de parite `scripts/notebook_tools/twin_pairs.d/sudoku-13-symbolicautomata.yaml` porte aujourd'hui `bridge_verdict: INTRINSIC` au motif que \"le C# (pur System.* stdlib, 0 NuGet, code from scratch, sans lib externe) construit la logique d'automate symbolique from scratch\". **L'omission est la suivante** : le notebook utilise deja `Microsoft.Z3` (cellule 17, NuGet officiel, axe 1 du registre SOTA axe-2), et il resout des **contraintes d'automates symboliques** dans la theorie des chaines - **uniquement en passant par le fork Automata** (cellule 21) ou par `ParseSMTLIB2String` textuel (cellule 26). Cette annexe exhibe le **constructeur d'automate symbolique directement emit en SMT-LIB 2.6 par concatenation C# depuis le notebook**, et le moteur `Microsoft.Z3` qui le resout - **sans fork Automata, sans lib externe**, juste la lib officielle Microsoft.Z3 et la theorie des chaines Z3.\n",
     "\n",
     "> **Ce que cette annexe prouve** : sous l'angle **axe 1 (binding .NET / NuGet officiel)**, `Microsoft.Z3` est atteignable et **rejoint des contraintes d'automates symboliques**. Le verdict precedent (\"INTRINSIC pour limite academique SFAz3+Z3 'monstre regex tronque'\") reste **valide en second niveau** (la limite SFAz3/Z3 existe, cap du temoin a ~21 caracteres sans le detour par la theorie des chaines : voir `known_differences` du yaml) mais n'est plus de premier niveau. Le triptyque devient :\n",
-    ">\n",
-    "> | Niveau | Verdict | Motif |\n",
-    "> |---|---|---|\n",
-    "> | Premier (ce qu'on ajoute) | **`RECOVERABLE-LOCAL`** | la lib `Microsoft.Z3` (NuGet, chargee par cellule 17) resout la theorie des chaines, donc la **contrainte d'automate symbolique** via `str.in_re`. Pont direct .NET -> SMT-LIB 2.6 -> temoin. |\n",
-    "> | Second (connu_differences) | plafond SFAz3+Z3 \"monstre regex tronque\" | la limite est **academique et documentee** (cap du temoin ~21 caracteres SFAz3, voir issue upstream AutomataDotNet/Automata#6), pas un workaround degrade. Ce plafond vit dans `known_differences` du yaml. |\n",
-    ">\n",
-    "> **Ce que cette annexe ne fait PAS** : remplacer la voie from-scratch (cellules 5-7) ou la voie fork Automata (cellule 21). Le from-scratch garde sa valeur pedagogique (reconnaissance de l'explosion DFA), le fork Automata reste le pont avec `&` / `~` first-class. Cette annexe est **en plus**, jamais a la place - mandat #10382 (parite lib-vs-lib).\n",
+    "\n",
+    "| Niveau | Verdict | Motif |\n",
+    "|---|---|---|\n",
+    "| Premier (ce qu'on ajoute) | **`RECOVERABLE-LOCAL`** | la lib `Microsoft.Z3` (NuGet, chargee par cellule 17) resout la theorie des chaines, donc la **contrainte d'automate symbolique** via `str.in_re`. Pont direct .NET -> SMT-LIB 2.6 -> temoin. |\n",
+    "| Second (connu_differences) | plafond SFAz3+Z3 \"monstre regex tronque\" | la limite est **academique et documentee** (cap du temoin ~21 caracteres SFAz3, voir issue upstream AutomataDotNet/Automata#6), pas un workaround degrade. Ce plafond vit dans `known_differences` du yaml. |\n",
+    "\n",
+    "> **Ce que cette annexe ne fait PAS** : remplacer la voie from-scratch (cellules 5-7) ou la voie fork Automata (cellule 21). Le from-scratch garde sa valeur pedagogique (reconnaissance de l'explosion DFA), le fork Automata reste le pont avec `&` / `~` first-class. Cette annexe est **en plus**, jamais a la place - le mandat de parite lib-vs-lib (jumeau C# / jumeau Python) reste la raison d'etre de la fiche de parite.\n",
     "\n",
     "### Lecture que cette annexe referme\n",
     "\n",
-    "Le titre du notebook est \"Le Sudoku comme Regex Symbolique\". Il a resolu la promesse via SMT-LIB 2.6 emis par fork Automata (cellule 21) ou via emmission manuelle (cellule 26). Il manquait un troisieme chemin : **construire un terme regex SMT-LIB 2.6 directement** depuis C# (StringBuilder), le passer a `Microsoft.Z3.Context.ParseSMTLIB2String` (API native), et le resoudre. Ce chemin montre que la lib Microsoft.Z3 elle-meme - sans fork Automata - tient le role de **constructeur d'automate symbolique** : la representation reguliere (`re.++`, `re.*`, `re.inter`, `re.range`) est un **terme SMT-LIB 2.6** direct, et la theorie des chaines le resout."
+    "Le titre du notebook est \"Le Sudoku comme Regex Symbolique\". Il a resolu la promesse via SMT-LIB 2.6 emis par fork Automata (cellule 21) ou via emmission manuelle (cellule 26). Il manquait un troisieme chemin : **construire un terme regex SMT-LIB 2.6 directement** depuis C# (StringBuilder), le passer a `Microsoft.Z3.Context.ParseSMTLIB2String` (API native), et le resoudre. Ce chemin montre que la lib Microsoft.Z3 elle-meme - sans fork Automata - tient le role de **constructeur d'automate symbolique** : la representation reguliere (`re.++`, `re.*`, `re.inter`, `re.range`) est un **terme SMT-LIB 2.6** direct, et la theorie des chaines le resout.\n",
+    "\n",
+    "> Provenance : Process metadata (lane, prev PR) deporte en pied de cellule. Issue de reference : #19240 (Tranche B, fille de #14446).\n"
    ]
   },
   {
@@ -3111,22 +3111,9 @@
     "\n",
     "2. **`Microsoft.Z3` resout, et le temoin est immediat.** Le solveur de chaines Z3 reconnait en millisecondes que le langage regulier decrit (sous-sequence ordonnee 1..9) est habite, et produit un temoin. La these du notebook (\"le regex, bien emis, est l'outil\") est demontree a nouveau, par une **autre** emmission de la **meme** contrainte.\n",
     "\n",
-    "3. **Pas de fork Automata, pas de cell 21.** Le Pont utilise exclusivement `Microsoft.Z3` (cellule 17, NuGet, axe 1 registre #3801), `Context.ParseSMTLIB2String` (API native) et la theorie des chaines Z3. C'est **la lib Microsoft.Z3 qui est le moteur**, pas un wrapper autour d'un autre solveur.\n",
-    "\n",
-    "### Pourquoi le verdict change de niveau\n",
-    "\n",
-    "La fiche de parite `scripts/notebook_tools/twin_pairs.d/sudoku-13-symbolicautomata.yaml` porte `bridge_verdict: INTRINSIC` au motif que \"le C# construit la logique d'automate symbolique from scratch\". **La clause \"from scratch\" est vraie en l'etat du depot avant cette annexe** : le notebook C# utilise `Microsoft.Z3` pour la **resolution** (cellule 18, `Distinct` sur 81 entiers) mais deleguait la **construction d'automate** au fork Automata (cellule 21) ou a un SMT-LIB 2.6 ecrit a la main (cellule 26). L'annexe **referme cette brèche** : la lib est bien employee pour les deux roles. Le verdict devient :\n",
-    "\n",
-    "- **Premier niveau (registre modifie)** : `RECOVERABLE-LOCAL` - la lib `Microsoft.Z3` (NuGet, axe 1 du registre #3801) resout des contraintes d'automates symboliques via la theorie des chaines. **Le C# n'est pas \"from scratch\" pour la theorie des chaines** : il l'invoque.\n",
-    "- **Second niveau (known_differences, inchange)** : la limite SFAz3+Z3 \"monstre regex tronque\" reste vraie (cap du temoin ~21 caracteres sur le chemin SFAz3 d'origine, voir issue AutomataDotNet/Automata#6). Cette limite est **academique et documentee**, pas un workaround degrade - c'est pourquoi elle vit dans `known_differences` du yaml, pas dans `bridge_verdict`.\n",
-    "\n",
-    "### Mirroir du precedent GT-17 (#10464)\n",
-    "\n",
-    "Meme structure a deux niveaux :\n",
-    "- **Premier niveau** : la lib est atteignable (axe 1 NuGet = RECOVERABLE-LOCAL).\n",
-    "- **Second niveau** : la limite \"monstre regex tronque\" est partagee par les deux jumeaux (pas un defaut de parite).\n",
+    "3. **Pas de fork Automata, pas de cell 21.** Le Pont utilise exclusivement `Microsoft.Z3` (cellule 17, NuGet, axe 1 du registre SOTA axe-2), `Context.ParseSMTLIB2String` (API native) et la theorie des chaines Z3. C'est **la lib Microsoft.Z3 qui est le moteur**, pas un wrapper autour d'un autre solveur.\n",
     "\n",
-    "From-scratch from-scratch (cellules 5-7) et fork Automata (cellule 21) restent en place. Le pont est en plus, jamais a la place."
+    "> Provenance : Les sections *Pourquoi le verdict change de niveau* et *Mirroir du precedent GT-17* sont deports au carnet de verifications (voir issue #19240).\n"
    ]
   },
   {
@@ -3234,7 +3221,7 @@
     "[Sudoku-14](Sudoku-14-BDD-CSharp.ipynb) construit ses BDD **from scratch** en\n",
     "C# pur ; cette annexe prend le chemin complémentaire : sans réimplémenter le\n",
     "moteur, elle **invoque le même `dd.autoref.BDD` que le jumeau Python** via le\n",
-    "pont .NET -> pythonnet -> CPython (axe 5 du registre #3801 : « la lib a-t-elle\n",
+    "pont .NET -> pythonnet -> CPython (axe 5 du registre SOTA axe-2 (la lib a-t-elle un binding Python ?) : « la lib a-t-elle\n",
     "un binding Python ? » — ici le pont va le chercher).\n",
     "\n",
     "Un BDD est un **automate déterministe acyclique** : chaque variable booléenne\n",
@@ -3255,7 +3242,7 @@
     "> **Prérequis d'exécution** : la variable d'environnement `PYTHONNET_PYDLL`\n",
     "> doit pointer vers une DLL CPython hébergeant `dd` épinglé (`pip install\n",
     "> dd==0.6.0`). Ce notebook ne hardcode aucun chemin machine (précédent\n",
-    "> Search-7) ; la cellule échoue explicitement si la variable est absente."
+    "> Search-7) ; la cellule échoue explicitement si la variable est absente.\n"
    ]
   },
   {

MyIA.AI.Notebooks/Sudoku/Sudoku-13-SymbolicAutomata-Python.ipynb

@@ -23,14 +23,14 @@
     "\n",
     "> **Twin Python** de [Sudoku-13-SymbolicAutomata-CSharp](Sudoku-13-SymbolicAutomata-CSharp.ipynb). Ce notebook reprend, **côté Python**, la tentation de représenter un Sudoku non pas comme un monstre PCRE à backtracking, mais comme une **chaîne déclarative tractable**.\n",
     "\n",
-    "## Complémentarité (#3801 Prong B)\n",
+    "## Complémentarité (registre SOTA axe-2, parite lib-vs-lib)\n",
     "\n",
     "| Twin | Outils | Valeur |\n",
     "|------|--------|--------|\n",
     "| C# (Resharp RE# + Microsoft.Automata + Z3.NET) | DLLs `.deploy` in-repo, intersection déclarative | la chaîne d'outils symboliques de Veanes (AutomataDotNet) |\n",
     "| **Python (z3-solver + regex + automata-lib)** | PyPI, idiomatique Python | **la récursivité `(?&rec)` du module `regex`** — capability que .NET REJETE |\n",
     "\n",
-    "**Le point de bascule** : les Sudoku-en-un-regex célèbres (Conway, ikegami PerlMonks 471168) reposent sur la **récursion `(?R)`/`(?&nom)`** — un langage **non régulier**. Le twin C# démontre (cellule 15) que `System.Text.RegularExpressions` **rejette** cette syntaxe à la construction. Le module Python [`regex`](https://pypi.org/project/regex/) la **supporte** : ce twin peut donc *exécuter* une approche récursive que le twin C# ne fait qu'évoquer. C'est la valeur complémentaire — pas un simple miroir."
+    "**Le point de bascule** : les Sudoku-en-un-regex célèbres (Conway, ikegami PerlMonks 471168) reposent sur la **récursion `(?R)`/`(?&nom)`** — un langage **non régulier**. Le twin C# démontre (cellule 15) que `System.Text.RegularExpressions` **rejette** cette syntaxe à la construction. Le module Python [`regex`](https://pypi.org/project/regex/) la **supporte** : ce twin peut donc *exécuter* une approche récursive que le twin C# ne fait qu'évoquer. C'est la valeur complémentaire — pas un simple miroir.\n"
    ]
   },
   {
@@ -1123,13 +1123,13 @@
     "\n",
     "Ce twin Python parcourt la même échelle que le twin C# — Conway -> reconnaissance -> résolution -> théorie des chaînes — mais **complète** là où le C# bute : la **récursion `(?&rec)`** du module `regex` exécute les langages non-réguliers que `System.Text.RegularExpressions` rejette. Les Sudoku-en-un-regex célèbres reposent précisément sur cette récursion ; le twin Python est donc le seul des deux à pouvoir *démontrer* cette voie, pas seulement l'évoquer.\n",
     "\n",
-    "**Bilan complémentaire (#3801 Prong B)** :\n",
+    "**Bilan complémentaire (registre SOTA axe-2)** :\n",
     "- `re` + lookaheads : reconnaissance linéaire d'une ligne/grille valide.\n",
     "- `z3-solver` : résolution (production de la grille) + théorie des chaînes (reconnaissance SMT).\n",
     "- `regex` `(?&rec)` : le seul outil des deux twins qui franchit la frontière du régulier.\n",
     "- Backtracking récursif : le contre-point robuste, compétitif sur 9x9.\n",
     "\n",
-    "> Retour au [twin C#](Sudoku-13-SymbolicAutomata-CSharp.ipynb) — où le barreau récursion est documenté comme un mur (.NET rejette `(?R)`)."
+    "> Retour au [twin C#](Sudoku-13-SymbolicAutomata-CSharp.ipynb) — où le barreau récursion est documenté comme un mur (.NET rejette `(?R)`).\n"
    ]
   }
  ],
@@ -1184,4 +1184,4 @@
  },
  "nbformat": 4,
  "nbformat_minor": 5
-}
+}