fix(density,#13410): Z3-Python-16-Meal-Planner 2 lectures chiffrees (1104 -> 1273)

MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-Python-16-Meal-Planner.ipynb

@@ -433,6 +433,14 @@
     "multiples, front de Pareto — cf. notebook 06)."
    ]
   },
+  {
+   "cell_type": "markdown",
+   "id": "f1a6b3c8",
+   "metadata": {},
+   "source": [
+    "**Lecture chiffrée — le prix de l'équilibre et l'optimum confirmé deux fois.** Trois menus se lisent ensemble : le moins cher (énumération §2 et `Optimize` §4) rend **8,50 EUR** pour 770 kcal et 27 g de protéines ; le menu équilibré (§3) rend **10,50 EUR** pour 630 kcal et 37 g ; le menu libre sans contrainte (§1) tombe à 530 kcal. L'équilibre nutritionnel se facture : **+2,00 EUR/jour** et l'abandon de 140 kcal par rapport au menu le moins cher, en échange de +10 g de protéines — un solveur ne « préfère » pas l'équilibre, il le facture. Et l'optimum de coût se lit en croisant deux méthodes indépendantes : l'énumération exhaustive (36 combinaisons filtrées sur 36) et l'`Optimize` SMT rendent le même minimum **8,50 EUR** avec le même menu (soupe de légumes + pâtes à la bolognaise + mousse au chocolat). Deux algorithmes sans aucune ligne de code en commun qui convergent vers le même chiffre : c'est la validation la plus forte disponible sur un petit domaine — et la raison pour laquelle l'énumération reste le témoin de référence tant qu'elle reste tractable."
+   ]
+  },
   {
    "cell_type": "markdown",
    "id": "cc1e46a0",
@@ -726,6 +734,14 @@
     "**Capabilite exercee (Prong-B).** La matrice booleenne `Sel[7][24]` (168 variables) est resolue en quelques centaines de millisecondes : l'optimisation SMT reste tractable a cette echelle. La frontiere de convergence est plus loin — un corpus RecipeML a ~11 000 recettes (variables `Sel[7][11000]` = 77 000 Booleens par jour) sortirait du regime d'un simple `Optimize()` et demanderait une decomposition (column-generation, Lagrangian relaxation) : c'est la limite honnete de la \"couverture bornee\" d'un solveur SMT monocall, signalee dans l'Epic #1206.\n"
    ]
   },
+  {
+   "cell_type": "markdown",
+   "id": "f1a6b3c9",
+   "metadata": {},
+   "source": [
+    "**Lecture chiffrée — quatre ordres de grandeur de temps de résolution sur un même corpus de jouet.** Les durées mesurées dessinent la hiérarchie réelle des approches : énumération des 36 combinaisons **0,06 ms** ; plan SMT booléen D=3 **2,4 ms** ; `Optimize` à coût minimal D=1 **17,7 ms** ; `Optimize` D=7 sur corpus élargi de 24 plats **349,5 ms**. L'énumération gagne partout où elle reste tractable — mais sa pente est exponentielle en le nombre de variables (Interprétation 2) quand celle du solveur suit la combinatoire contrainte. Sur ce jouet, passer de 3 à 7 jours avec corpus élargi et contrainte de variété multiplie le temps par ~145 (2,4 → 349,5 ms) — observation sur cette paire de runs, pas une loi : jours et corpus changent en même temps. La lecture pratique : le temps du solveur achète l'exactitude à l'échelle où l'énumération explose, et la fenêtre [1400, 1900] kcal avec 40 g de protéines reste résolue en un tiers de seconde à D=7."
+   ]
+  },
   {
    "cell_type": "markdown",
    "id": "6f2082b4",
@@ -904,7 +920,7 @@
     "\n",
     "← [15 - Tableaux imbriqués et grilles 2D](Z3-Python-15-Nested-Arrays-2D.ipynb) | [README Z3-Python](README.md)\n",
     "\n",
-    "---\n",
+    "***\n",
     "\n",
     "> **Suite de la track (corpus réel).** Ce notebook reste sur un corpus **jouet**. L'idiom\n",
     "> `PbEq` (pseudo-booléen natif) utilisé ici pour `exactement_un` est la clé qui rend le\n",