From 58435859f620ef2f5964909674037cd8ba0a66e6 Mon Sep 17 00:00:00 2001 From: jsboige Date: Wed, 23 Sep 2026 18:22:58 +0200 Subject: [PATCH 1/3] feat(geometry,#17544): notebook 01 - de la figure a l'equation + README de serie + entree SymbolicAI MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Geometry-01-From-Figure-To-Equation (Decouverte) : traduction du theoreme du milieu de l'hypotenuse en polynomes (sympy), verification numerique sur 10 000 figures a coordonnees entieres (longueurs AB/AC independantes), temoin negatif rejete unanimement (C' = H - AC^2), piege du tirage biaisé, Schwartz-Zippel mesure empiriquement sous la borne d/|S|, preuve probabiliste composee. 3 exercices stubs non bloquants, execution end-to-end ~5 s CPU, 11/11 exec counts, 0 erreur, outputs committes. README de serie : gradation 01-05 de l'Epic, fil rouge, premiere volee. SymbolicAI/README.md : neuvieme serie (prose, carte mermaid, parcours, section, arbre, Quick Start, table audit E) - CATALOG-STATUS byte-identique. Co-Authored-By: Claude Sonnet 5 --- .../Geometry-01-From-Figure-To-Equation.ipynb | 818 ++++++++++++++++++ .../SymbolicAI/Geometry/README.md | 41 + MyIA.AI.Notebooks/SymbolicAI/README.md | 40 +- 3 files changed, 893 insertions(+), 6 deletions(-) create mode 100644 MyIA.AI.Notebooks/SymbolicAI/Geometry/Geometry-01-From-Figure-To-Equation.ipynb create mode 100644 MyIA.AI.Notebooks/SymbolicAI/Geometry/README.md diff --git a/MyIA.AI.Notebooks/SymbolicAI/Geometry/Geometry-01-From-Figure-To-Equation.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Geometry/Geometry-01-From-Figure-To-Equation.ipynb new file mode 100644 index 0000000000..2b9188a635 --- /dev/null +++ b/MyIA.AI.Notebooks/SymbolicAI/Geometry/Geometry-01-From-Figure-To-Equation.ipynb @@ -0,0 +1,818 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "id": "df017e3b", + "metadata": {}, + "source": [ + "# Geometry 01 — De la figure à l'équation\n", + "\n", + "**Public : Découverte** — première étape de la série [Geometry](README.md), le programme gradué de la preuve automatique en géométrie.\n", + "\n", + "**Ce que ce notebook suppose.** La géométrie du lycée : coordonnées cartésiennes, distance entre deux points, produit scalaire, théorème de Pythagore. Côté Python : des boucles, des fonctions, un peu de `numpy`. Aucun prérequis d'algèbre abstraite — les mots « idéal » ou « base de Gröbner » n'apparaîtront qu'en toute fin, comme promesse du Geometry-02 (*Prouver par l'algèbre*, prochaine étape de la série — programme complet dans l'Epic #17544).\n", + "\n", + "**Ce que vous emporterez.**\n", + "\n", + "1. Traduire un énoncé de géométrie — hypothèses et conclusion — en **polynômes** sur les coordonnées des points.\n", + "2. Tester ce théorème **numériquement** sur des milliers de figures tirées au hasard.\n", + "3. Voir la machinerie **rejeter un énoncé faux** : le test n'est pas un moulin à « oui ».\n", + "4. Comprendre précisément **pourquoi ce n'est pas encore une preuve**, et comment le lemme de Schwartz–Zippel transforme quand même ce test en *preuve probabiliste* à marge d'erreur explicite.\n", + "\n", + "C'est le socle sur lequel reposent les méthodes algébriques exactes de la suite de la série : bases de Gröbner (02), méthode de Wu (03), et le pont vers les preuves formelles Lean (05)." + ] + }, + { + "cell_type": "markdown", + "id": "8316482e", + "metadata": {}, + "source": [ + "## Le fil rouge de la série\n", + "\n", + "Toute la série traverse le **même théorème**, regardé par des méthodes de plus en plus fortes :\n", + "\n", + "> **Théorème (milieu de l'hypoténuse).** Dans un triangle $ABC$ rectangle en $A$, le milieu $M$ de l'hypoténuse $[BC]$ est équidistant des trois sommets : $MA = MB = MC$.\n", + "\n", + "| Notebook | Regard sur le théorème |\n", + "|---|---|\n", + "| **01 (celui-ci)** | on le **vérifie numériquement** sur des figures aléatoires, et on mesure ce que cette vérification prouve — et ne prouve pas |\n", + "| 02 — Prouver par l'algèbre | on le **démontre** : la conclusion appartient à l'idéal engendré par les hypothèses (bases de Gröbner) |\n", + "| 03 — La méthode de Wu | on le **redémontre** par pseudo-division et ensembles caractéristiques, avec les conditions de non-dégénérescence |\n", + "\n", + "En revenant trois fois sur le même objet, on compare des *méthodes*, pas des exemples." + ] + }, + { + "cell_type": "markdown", + "id": "02ac8ca9", + "metadata": {}, + "source": [ + "## 1. Une figure devient des nombres\n", + "\n", + "L'idée fondatrice de Descartes : dès qu'on choisit un repère, un point devient un couple de nombres, et une propriété géométrique devient une **équation** entre ces nombres. « L'angle en $A$ est droit » ne sera plus un dessin, mais un polynôme évalué en les six coordonnées de $A$, $B$, $C$.\n", + "\n", + "Fixons d'abord une figure concrète, pour voir le théorème de nos yeux." + ] + }, + { + "cell_type": "code", + "execution_count": 1, + "id": "076c907f", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-23T16:15:56.735969Z", + "iopub.status.busy": "2026-09-23T16:15:56.735696Z", + "iopub.status.idle": "2026-09-23T16:15:57.431324Z", + "shell.execute_reply": "2026-09-23T16:15:57.430626Z" + } + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "numpy 2.4.6 | sympy 1.14.0\n" + ] + } + ], + "source": [ + "import numpy as np\n", + "import sympy as sp\n", + "import matplotlib.pyplot as plt\n", + "\n", + "rng = np.random.default_rng(20260923) # seed fixe : figures reproductibles\n", + "print(f\"numpy {np.__version__} | sympy {sp.__version__}\")" + ] + }, + { + "cell_type": "markdown", + "id": "6aa859ca", + "metadata": {}, + "source": [ + "Le triangle $A(0,0)$, $B(4,0)$, $C(0,3)$ est rectangle en $A$ (les côtés $[AB]$ et $[AC]$ suivent les axes). Son hypoténuse est $[BC]$. Construisons $M$, le milieu de $[BC]$, et traçons les trois distances $MA$, $MB$, $MC$ :" + ] + }, + { + "cell_type": "code", + "execution_count": 2, + "id": "a87f83a4", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-23T16:15:57.435579Z", + "iopub.status.busy": "2026-09-23T16:15:57.435343Z", + "iopub.status.idle": "2026-09-23T16:15:57.530768Z", + "shell.execute_reply": "2026-09-23T16:15:57.530244Z" + } + }, + "outputs": [ + { + "data": { + "image/png": "iVBORw0KGgoAAAANSUhEUgAAAcsAAAFvCAYAAAAlj+C/AAAAOnRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjExLjEsIGh0dHBzOi8vbWF0cGxvdGxpYi5vcmcvctoD+AAAAAlwSFlzAAAPYQAAD2EBqD+naQAAWcBJREFUeJzt3Qd4FFUXBuBvd9OB0EPvoTfpvQjSQVAgFCkqIoiIgPojqCiKIIoCAlItKEiTKlW6IE2QXgRC7yGQQnp253/OxV0SSNuULcn3Ps9CZrKzuXMz2bP3zJk7Ok3TNBAREVGi9Il/i4iIiBgsiYiIUoAjSyIiomQwWBIRESWDwZKIiCgZDJZERETJYLAkIiJKBoMlERFRMhgsySFcvHgR586dgyNxxDY5M6PRiKNHjyIgIMDeTSGymo4z+FB6OHnyJGJjY5N9Xv78+VGkSJGn1rdt2xb37t3DoUOHHOYX4ohtSk5MTAxOnTqFokWLIl++fHAk0pfy+58yZQqGDx8OZ3XmzBlERUWhcuXKcHV1tXdzyEZcbPWDKHN766238ODBA8vyrVu3cPfuXVSoUAHu7u6W9S+99BLee++9p7YvU6YM8ubNa7P2ZlZ37txBjRo1MH36dAwdOtTezcl0rl+/jqpVq6pR8uLFi9GzZ097N4lshMGS0sWOHTviLb///vuYNGkSVq1apQJmcmbOnMnfBDm8H374QY0m5ZieN28eg2UWwmBJNnP+/HnodDr4+vqqT+aXL1+Gi4sLSpQooc4PShq3XLlyludfvXoV9+/fV1/r9XrkyZNHpReTel15jUuXLiFHjhwoWLBgom2R15VzZ8WLF4enpyeuXbuG4OBgVKlSJUX7YjKZcOXKFURHR6NkyZLxRs+p2X+zsLAw1RYvLy/VtsRERESo/pHRuDndKtuePn1afX3jxg11fvDJ1PexY8dgvneCm5ubWp8zZ854ry37JK8jP1/6PCQkRL2eLGfLli3RNsn+CNkf2c/jx4+r9iWUdk9ISvfd2m1Tuz8J/c4lWPbo0QPNmjXDgAED4O/vr7IilAXIOUui9DZq1Ch5R9bOnDljWVevXj2tWbNm2tatW7XSpUtrRYoU0Xr06KG+16ZNG61WrVrxXuOjjz7Sqlevrh6VKlXSsmfPrhUrVkxbtWpVvOeZX3f37t2ar6+vVqpUKU2v12tt27bVQkND4z03LCxM69Wrl/q+vJa04YcfftAGDBig5c2bN95zE2qTyWTSvv76ay1//vxa7ty5teLFi6t2jRs3Tn0vKUnt/927dzU/Pz/Nzc1NK1GihObt7a2VK1dO27FjR7zXuHPnjtazZ0/1vMKFC2sFChTQatasqe3bt087cuSI6ifpd3ltc99NnDjRsr3sj3m9tMHFxUV77rnntGvXrlmec/78efUa8+bN08aOHWv5OR4eHtqUKVOe2q9Dhw5pFStW1FxdXVXfP/PMM+o13N3dtbffftvyvICAAPW6T75GSvc9ISnZ1tr9ScymTZvU6xw4cEALDw/X8uTJo40ePTrF25NzY7AkmwbL8uXLqze3kJAQtW7v3r2JBqYnRUZGav/73/80T09P9QYY93UrVKig9evXzxIc9+/frwLBxx9/HO81evfurd5Q//zzT7UcExOjvfnmm1qNGjVSFCwlgBsMBm3BggWWddu3b1dt+vzzz5Nsf2L7L2+8lStXVvtg7q/Y2FgVaOR1z549q9Y9fPhQPUc+EEhgNJOv58+fr76WoCf9Pn36dC0lrl69qvb92WeffSq4NGzY0PK6YsSIEepDhrk95mCVL18+rWnTptr9+/fVusuXL1sCWHLBMqX7npCUbmvN/iSla9eu8Y6HkSNHagULFlTHEGV+DJZk02ApgUbeoJ+UVLCUN+FTp06poCDBRV53xowZ8V5XRjG3b9+Ot12HDh3UG6nZlStXNJ1Op40ZMybe8yIiIjQfH59kg6W82UsAeP31159q4/Dhw7WcOXMm+caZ2P7PnDlT7ZM5gJtFR0erUdCgQYPU8rRp09TzJDgnJiXBUkbA0oZjx46pPv3www/VNkFBQfGCi/Tfk78HWT9+/HjLOhm1yrrTp0/He+7atWvV+uSCZUr3PSEp3daa/UmMjOhl5Pz9999b1snryvH0ZKaDMieesySbKl26NIoVK5ai5x48eFBVdB45ckSdX8qePbs6FybkfGFcch6wQIEC8dbJuaS4hUfyevIBsUmTJvGe5+Hhgdq1a+PAgQNJtuevv/5S57/kvKpcKvPfh031PR8fH3XOU85LVqxY0ar9lzbKOU85dxj3deVRqlQp/P333+p5u3btUm1t3rw5Uuvrr7/Gl19+qc55yrlE+blBQUGWPq1WrZrluY0bN463be7cudU5PzlXarZ//351XvLJfX5y28SkdN/TY9uU7E9iFixYoM6bS2GP+VyweOaZZzB//nx06dIlRftLzovBkmwqqaKbuEJDQ9GuXTvUqlVLXYIib2xC3uSliEOKLeJK6JpCKdwJDw+PVwQicuXK9dRzza+fFAmGYs6cOfjll1+e+n716tWTvdY0of2X15U3+H79+iW4jblgRfpE3tzNHxistXTpUrz77rv49ttv8eabb6o3fyFv9gMHDkxxn5r7UcjXCfWnBDDz6yclpfueHtumZH8SI31UqFAhDBkyJN566bNNmzapS0oSKj6jzIPBkmwqJW+g5hGLVKyOGDEiXiBLy4w6hQsXVv/LG9uTpJIyOeY3w08++QS9e/dOt/2X15UAKCNfqVBNjLz5b9u2TX0AkA8M1tqwYYPqS7kmNq5///0XaelTGXFL0Ii7b1Jt+mTwTUhK9z29t7WGjOjluJN+ilutbSbVv1IlO3bs2AxrA9kfp7sjh2S+nME8mkuP6zEbNWqkRkELFy586pIHCc7JkTSepFDnzp2bYCCQUW9qSOCVGWF++umnBL9vfl25ZEF+7owZM556jmwvzKO8uCPquH0qaWTzc82j1Sf7wxodO3ZU7Vu5cmW89b/++muKRsAp3ff03tYaMqqUtG5CgdI805MEy5R8OCDnxZElOaSaNWuq80EyuYFciyjpx2XLlqk3fIPBkKrXlNHY1KlT8corr+D1119Hr1691LWWklZ9/vnnsXPnziS3l9GLzNoiAaJFixYqJSfBU0ZRu3fvVgE3ufOeCXnuuefUfsqI7+zZs2jdurW6/k/Of8o+yzV9o0ePRqtWrdRIW76WGZLat2+vrteUNKD0iZyPlPO6MsOMpFzr1aun+st8naWkK2fNmqWCzLBhw9S+T548WV1YL/2SGl27dkWbNm3UNYfyenKdqvSFfC39lVzATOm+p/e2KSWzUv3222/qmEmMnC6QD1BbtmxRfUGZE4MlZQhJz8k5PClIMZNP5omly56c7k4CpLz5TJgwAdOmTVPnlrp166bOrUlhR9wL3RN7XXMb4urfv786byhBQ95IpaBFijdkCr64bU2oTebRqcy9Onv2bPUG+fDhQ5WGa9q0qWprUpLa/4kTJ6oRys8//4zPPvtMzRJTtmxZdY5RgoLZN998o5ZlNPjhhx+qwiJ5gx40aJDlOUuWLFGvJ/skI0kJhhJUpIhJUorSn7IsoyUZpQYGBqo+lT4WUjQj/ZbQ9IMyH2rcSRQk9bpmzRoVbOXnCvngIT9fzo3G7VP5ncrrSvBOzb6ntt+s2Z8nSX+VL18eL7zwQqLPadmypZpiUD4kMFhmXpxInQhAgwYN1Ohsz5497I90IDPbSIWyfCgZPHgw+5ScHkeWVpBzIHv37lVvBHJ+QlJwkipM6XReZH8y0npydCeXHUj69NNPP7VbuzJbn37//fcqBSupUaLMgCPLFJI0k6R5JJUj1+lJekneZCV4ShpIChpkPlJybJIqkwne+/Tpoz7sSEr1448/Vuf25Lo8/g6tN3LkSBUsn332WTU6l6pbSfVKKlT6migzYLBMgXfeeUcFSzkHI0UdcYsWDh8+rApFtm/fzuusnIQUxMiHmwsXLqjzdFIIIgUvCV0vSCnLuEiVsnwQuX37tvo7kMpdPz8/dh9lGgyWyZD0XP369VXFnQTLhMgbhFThcVRCRJQ58ZxlMuTci5AZT9I6Kw0RETknjiyTISXhUtAj98AjIqKsySlGllJ5evPmTZXmTO28mKklU655e3szWBIROTmZS1hmrZJrsFM69aZTjSxlLs+U3qmCiIgoKTIXtLUT3zvFyNJcOCM7KKO8tIxQZRoumUEkpZ8q5IJqmeLsxIkTSd4BISOlpt2OwBnb7YxtFmw3+zuzHiemdGyznE6TgVdqijGdIliaU68SKNMaLCMjI9VrpLTTZc5LCZYyldf48eMTfI5M9i1TeUlFbEZITbsdgTO22xnbLNhu9ndmPU5MGdDm1JzOc47esiOZ97Fv37746quvsHr16qe+f/HiRTUHpUy4TEREmZNTjCztTW6/Izd+lQmp69atqybNlhl8JDW7du1adacFXmNJRJR5cWSZApJilWm7rl69qm7tJMsxMTFq3ku5LZNMk2a+/yIREWU+HFlaQW6HJHOKEhFR1sKRJRERUTIYLImIiNIzWMp96+RmrnJLKrnreu/evdU5u+TIDXXl7ulyt3K52/2xY8dga0aThn3+0dh0Bup/WSYiIkr3YDlq1Ch1qcR7772ngqZUiMrtjQ4ePJjoNnILK7m0QipGZ8+ere4HKdWk8jq2suFEJOp9fg9+c4LxwXqd+l+WZT0REVG6Fvh8+eWXcHV1tSzXqVMHy5YtU/cHlEsqEvL555+jUaNGmDBhglqW213t2rULX3/9tboHXkaTgPj6gmA8OY68HWxS6+f2B9pX9cjwdhARURYZWcYNlOZ7Pd69excNGjRIdJsdO3aotG3cmRPat2+v1mc0SbWOXR36VKAU5nUfrwllSpaIiNL30pHz58+jU6dOCAsLQ2BgIObPn49WrVol+NyHDx8iKChIpWufvP+jTI6emKioKPUwM98eS6Y9kkdK7fePxq3g+M9vmnM7YjQ37AtprALmzSAT9vtHoUEZNzgq2WeZ796afXcEzthuZ2yzYLvZ35n1ODGlY5vT8hpWB8sSJUqoad8kCEoKVm6KXK5cOdSrV++p5xqNRvW/m1v8QOTu7o7Y2NhEf8bEiRMxbty4p9bLZLoyR2BKnVfx+PEcgPlcAzCt7BB4G4Lx/InNOBVe7b/nBaGM9fPq2oz8gmX+WTlgnGU+R2dttzO2WbDd7O/MepyY0rHNcnsumwVLCXwVKlSwnH88fvy4Ope5YsWKp54rU8DJ8+/duxdvvSxLoU9iRo8ejZEjRz41U7zMOm/NROplQ6NlmvPHPzcmH6ZdfwcVvU7hVHjVx88rmgs+Po49spT0tTPdKcBZ2+2MbRZsN/s7sx4npnRss0xTarcZfHLlyqWifkJkx2rWrKkuLxkyZIhl/d69e9WlJ4mRkac8Eno9azqrfhl3FMqpV8U8j85R6vDT7YH/nbF8NOIs5eGPoKsPoPNtb/MbS1tD2mbt/jsCZ2y3M7ZZsN3s78x6nOjSqc1p2d6qLceMGaNSoWYbN27E+vXr0blzZ8u6GTNmxKuMHTRokBp1mi8vkW2kGlbuE5nRDHodPu3yKL8aPww+WnLTRWJm2YFoeb8Tpi1ajpAI58njExGR7Vg1svT19VWXi8gk4nLuUKpjP/vsM3XeMm6K9dy5c5bll19+WRUFyfWYkkKVwiBJ27Zp0wa2IJeFyOUhH64KxZ2Qx8GwcC49PmiXH/7+fRD58DdMO10Py67dx5y+OVG1aPyqXyIiytp0mpw1tdLt27dVoEzovKMES7m3Y9myZeOtlyApl5lIZay1eWM5Zyl39ZB0b2pv/nzvoRHVP3l07nSKX3Z0re2lRp5i+d8PMXplGCJigNyuoZjU6iLaP9vKYdKykrOXvpOJ3J0pdeKM7XbGNgu2m/2dWY8TUzq2OS2xJFU/WS79SKxAJ1++fE8FSpEtWzaUKlUqTSdY08IcGEWN4q7xlrvXyY6Nw/OifAE9Pi35DloGtsX3v85hWpaIiBTn+GhhA2ULuGD9sLxA7vq4G1MA352sj7ZT7+PE9Rh7N42IiOyMwTIOT3c9XvQbjUO+JxGCQrgSaETn6fewZudf6hofIiLKmhgsE/Bi3bz/pWUNeKXATLQOaIpfF3/FtCwRURbFYJlUWvbtvKhUNAeiTe5Yeq4i07JERFkUg2USPN106Oo3CjtLnsHpqLoqLfv89PtYvus007JERFkIg2UKdK5XwpKWbZBjGzrcrYbfFn/CtCwRURbBYGllWvb5cvdg0vQ4eD0b07JERFkEg6WVadmefsPwZ7FDWPWgnyUt++vu60zLEhFlYgyWqdC+QTVsHJ5PpWULu15EqxtVsHrxGISEP7olGRERZS4MlmlMyw6qdhqe+nAEPbiJttMecBIDIqJMiMEyjWnZfn4DsLfITky+Mc6Slv15z32mZYmIMhEGy3TQulFDrH67qErLumoPUetifaxa/AFCwjlVHhFRZsBgmc5p2XdqH0UJj8soFLUFHabdY1qWiCgTYLBM57TsIL+u2FdkK/53aTYuBupVWvanPQ+ZliUicmIMlhmgVaOm+OHN6iotG2M0If/pbkzLEhE5MQbLDE7Ljqx7Ds1ybUdt/Ai/6ZeYliUickIMlhmclh3p10ylZd+5OBcnAnI+Ssv+Fc60LBGRE2GwtFFadsLAdiotG20E7v499r9JDFgtS0TkDBgsbT2JQd37eKPwDDzn8g0GzTrItCwRkRNgsLRxWnasX0XsL/IHxl75Gn/e8mValojICTBY2iktO6TfYEtadveuxUzLEhE5MAZLO6dl+9U1Ynyp/6GD2xcYO28l07JERA6IwdLOadmJfoVxqvhKzLo1AsuvNWdalojIATFYOoDnGjVDe78vLWnZBZsOYuXij1gtS0TkIBgsHSwt27uuG6b4DkUnt8/x3U9TmZYlInIADJYOlpb9yi83Any/w8b7z2P2pZ6P0rJ7I6Bp9m4dEVHWxWDpoNWylTqvQGkfT5WWnfz7NWzbMptpWSIiO2GwdPC0bK+6HphQ+j34eY3DykWjmJYlIrIDBksHT8tO9suJbJXfxdGHtTDt8musliUisgMGSyfQsmETGGv/jjx5Cqq07EergvDDr7OYliUishEGSydRKp8O697KrdKyQ4tMQV/3N7F9cX+mZYmIbIDB0gnTsrXqdsTlyNKYe7Uv07JERDbAYOmkkxjonjuFyOx1VFr2g1WhmLpoJdOyRESOFCw1TUvxzYtjYmLw8OHDeI+wsLDU/FiKo2xBD0u1bKvcG/GmRzccWvY8TlyLZj8REdkzWO7evRsdOnRArly5kC1bNjRu3Bh79+5NcptJkyYhZ86cKFiwoOVRvnz5tLab4qRlX2peGjeiimL1nbZ4fsYD/PRXeIo/zBARUToHyxkzZmDo0KG4ceMGAgICUKtWLbRt2xZXrlxJcrs6derEG1lev37dmh9LKZjEwPjsSZzUv2RJy366cA/TskRE9giWS5cuRbt27ZA9e3Y1spw8eTIiIyOxbdu2ZLc1Go0c7WQg38I5LWlZX89/8bZbG5z67TmcuMqUNxGRXQt87ty5o85J5s2bN8nn/fPPP/Dy8lJBtlmzZjh48GBafiwlk5b9oK0LHsTmxfHgcnh+5kOmZYmI0sgltRvKObE333wTZcqUQZs2bRJ9XvHixbFixQq0atUKoaGhGD16NFq0aIHjx4+jdOnSCW4TFRWlHmYhISHqf5PJpB6pEXc7k6al+nXsQdqqWdHm5xrUh3/xQ1ixJNaSlj3t748xL5aDt5crHLXdjsAZ2yzYbvZ3Zj1OTOnY5rS8RqqD5fDhw1XBz86dO+Hh4ZHo8/r162f5Wp43e/ZsbN68Gd9//z0+//zzBLeZOHEixo0b99R6OU8qad/UCI6Qf3Xq68DAQOTUOc9VM/ILDg4OVgeMXp+ydudwBeb0NOCr7Rq2nw7B6/qOOL2iOGKrzke5wjnhqO22N2dss2C72d+Z9TgxpWObZcBm02D57rvv4ueff8aWLVtQrVo1636giwt8fX1x8eLFRJ8jo8+RI0fGG1kWK1YM+fPnh7e3d2qaDNdw+UQRqL6WtLGPj+1GWOlxsOh0OrX/1h4sM/oCm/fdgOGyCTGxJry6NAc+6JQD/Rt4qNd01HbbizO2WbDd7O/MepyY0rHNSQ3s0j1Y/u9//8P8+fNVoKxdu/ZT34+OjlbnMaUAKCEyMjxz5oyqkE2Mu7u7ejxJOiq1nRV3M71O5zQHipkcLKnd/3aNasG/xD+YtjQAkUYDPlr9EEcvBmJ8t0IZnpZNS7vtxRnbLNhu9ndmPU506dTmtGxv1ZZjxozBrFmzsGrVKlSsWNFyKYgESLMJEyagSJEilmW5LnPDhg24desWTpw4gZ49eyIiIgKDBw9OdaPJemWK5seityqqalk9jOgS3RenfmuJ05dusDuJiNIzWM6dO1fljTt16hRvkgG5hMTMzc1NVb2ajR8/Xp2flJFk165d1fcOHz6caHEPZXy17HfdwlDK8yIKGi6i97xQVssSEaVnGvbevXspGn3Kw6xGjRqqGpYcR6f6ZeFf9B+M/+0sAqJzq2rZ/f5h+LJbLptWyxIROQvnSVpTuqdlvxvSWKVlRZWgj9UkBqcvcnYlIqJ0u3SEMk9atlHJKFQ7vx75Xe+i+88X0KtVHvRv6Jnh1bJERM6CI0vCC3V9gGaHMO7OLzj5sKJKyw76JRgh4bHsHSIiBkuKm5YdP6irJS3rcuPXR9WyF6+xk4goy2Malp5Ky9YrZUDFs9NRzvMshi7bgoZNejItS0RZGtOw9JTudbLD89k/MSVgCtbf6/A4LRvhPPNJEhGlJwZLSjQtO2zA25a07OULf+PIsjZMyxJRlsRgScmmZaf29MYHJT9Dg2xbsW7tTE5iQERZDs9ZUrK61/aEf8EVWLRxEmZcfwvG66HY6x+Nyd294e3Jz1tElPnxnY5SnJbt2f8r+NV9NJXhvtM3sHtxD05iQERZAkeWZH21bGk3xB4agVbev2HlH3ocrPojq2WJKFNjsKRUpmWnYcMfrvjs8vsIusC0LBFlbkzDUqrTsm36/IR2NQur5c0nHmLNwreYliWiTInBktKlWnZI0Vnokfs7PNjVndWyRJTpMA1L6ZSWHY5dW09h0qW3cObUo7Tsl10f39eUiMiZcWRJ6ZaWbdx7FZ6pUlstrz8ehTk/TcaFGwHsYSJyegyWlCFp2U7512NEgdHIf6YLFvwVCk3T2NNE5LSYhqUMScvWLNgJe7e1w+KbnbHuaCT2XdI4iQEROS2OLCnD0rJ1/NbCULizJS37ydwlnFuWiJwSgyVlGE93Pca2Aab0yIFnvE9hXKFX4b2/Dhbtvsm0LBE5FaZhKcN1q+WBWoWq4vC2FjgWVAZf/mPArkvBTMsSkdPgyJJslpat13MdrhcaZ0nLDv1uF9OyROQUGCzJpmnZr/zyqGrZgh738WnBPvDeXxvLd51mWpaIHBrTsGSXatkahfLj0tZnEBsTgRG/58aWK0zLEpHj4siS7MK3SD7U7/k7tnsvhAa9Ssv2nn6aaVkickgMlmTXtOxEv8IqLZvdNRaj8g1UadnVO/cxLUtEDoXBkhwiLbv+rWwwGnIj3OSF9zfmw6BfghESYbJ304iIFAZLcgi+hXOpatlf3TYj1Oit0rKdpt3iLb+IyCEwWJJDpWU/8Sun0rKerkCf7GOR80BNrNuxjWlZIrIrBktyyLTsxrdzomyOW/DSh2HSNnemZYnIrhgsySGVLeih0rJzdTtwMbKsSsu2nRqIU5d5yy8isj0GS3LotOwov7qWtGw9/ULk3FsFG7ZvYlqWiGyKwZKcIy07PC/aFtgDH7e7WLI3gGlZIrIpBktyCmULuKBpr+WYa1qPbUGt/0vL3seJq2H2bhoRZQFWB0uj0YizZ8/ixIkTiIiISPF2N27cwL59+3D37l1rfySRJS071K+9JS2bO+ogcuwuj43bNzAtS0SOEyxnzJiBkiVLokuXLujZsycKFy6M77//PsltTCYTBgwYAF9fXwwePBjFixfHqFGj0tpuysLMadlXiq9AYfcbOHZsJ9OyROQ4E6mHhITg77//RsGCBdXyjz/+iNdeew21a9dG9erVE9xm5syZWLlyJY4dO4Zy5crhwIEDaNKkCerUqYNu3bqlz15QlkzLFn1pHn5d0xQzb7SC6UYUTt64jzl9vFG1mJu9m0dEWXlkOWbMGEugFC+//DJcXFxUAEyMBNTu3burQCnq1auHVq1aqfVEaU3LvuzXH9/0zK3SsmEht2DcXotpWSJyrFt0HT16FNHR0Shbtmyi5zfl3OagQYPira9Vqxbmz5+f6OtGRUWpR9wRrTmlK4/UiLudSdNS/Tr2IG3VnKzNtmx315ruqFYkN3avm4JK2U7i8vlZGHStAb7slgPentadlmdf2xb7m/1ty2MkLa+R6mAZFhaGV155BU2bNkXz5s0TfE5oaChiY2ORJ0+eeOvz5cuHBw8eJPraEydOxLhx455aHxAQgMjIyFS1N1jVIunU14GBgcipc55CYPkFBwcHqwNGr2e7E5JTB7Rs8zaW7c6D8Re7INQYjaNX72HS80DFAuxrR8Vjm/1ty2NEYpJNg6UELCnykVHl8uXLodM9CkJPcnN7dO7oyarZ8PBwy/cSMnr0aIwcOTLeyLJYsWLInz8/vL29U9NkuIbLJ4pA9XXevHnh4+MKZyEHi/Sx7L+zBUtbt7tEr3fhVi4SY1aG4m5IDKIOvobDpYehbfO2iR6n9m5zemC72d+Z9TgxpWObPTw8bBcsJT0qgfLatWvYuXMnfHx8En2ul5eXGkXKZSNxyXKJEiUS3c7d3V09niQdldrOiruZXqdzmgPFTA6WtOx/Vmq3Xx0v1CjuhpUrZ6BF7j9w9vo1DFlUH191z52itCz72rbY3+xvWx0jadlen5pAefnyZezYsSNesY+ZfG/Pnj2WZSnmWbt2rWVZ0rLr1q1T64kyslp22KvD8LvpC7x1YTbWHY99NInB9Rh2OhFlbLD08/NTgfCTTz7Bv//+q0aW8pAAafbTTz+hY8eOluWxY8fi5MmT6lrLVatWoUePHioN++6771rfWiIrq2W7+o3C0M51VLXslUAjdq8ajg3bN3ISAyLKuDSsnHuUStbZs2fHWy+XkMhDyKQFjRs3tnyvQoUK6tKSKVOmqO2kclaWCxUqZF1LidIwicEzxVwxe9kavFboO9y/swTDfjmKz7sXsbpaloiyJquC5R9//JHsc+IGTrNKlSph3rx51reOKB3TsuNffwHr1kzA2ouFsOWBGw7LJAZ9c6JqUecp9iIi++DHaspSadkX/UajQ5selrTsgsUzOIkBESWLwZKy7NyyLYtewiclRqHpvc54f+EJhEQ416QPROQkM/gQOXNads4bdbFxzaf490YQFt4ogN3X72PWSzlQgFPLEtETOLKkLJ6WfR++TT62pGXHL9iIPYf2sFqWiOJhsKQsz5yWrVUoBFPKDELHCD9M+nUb07JEZMFgSfRfWnbp0DI46DIcm+53wMxj1TiJARFZMFgSxUnLduk2CvfKzIWnq06lZQfPOcZJDIiIwZLoSR2r6LB+WG5UKmDCN6UH4dnAjpjx62KmZYmyMI4siRJJy64dVgA3snXDufAK+PZYfaZlibIwBkuiZCYxOF9pHzRDNpWW9Zt5Het2bGO1LFEWw2BJlIxudbxVtWz5AgaMLvoRWt5rjZ9+ncG0LFEWwmBJlMK07PpheZA9f2UExebC3NN1mZYlykIYLImsTMvuL3MGAaaSKi37/PRArN55gGlZokyOwZLISi/U9bGkZf3y/YS2AQ2wZPFEpmWJMjEGS6LUpmXfzos6JQyI0Vyxxr8M07JEmRiDJVEqebrp0M3vPewsfhqHwpv/l5a9j6V/nmdaliiTYbAkSqNO9ctY0rLVvfaj/e0qWLn4I6ZliTIRBkuidEzL9qh4FTpoOHlLz7QsUSbCYEmUjmnZXn5vYU/R/Vh47w1LWnbR7lsOm5YNjgxVj8jYqAS/b9JMlufEGGNt3j4iR8FgSZTO2jasiQ3D86u0bF7DDTx7vSpWLf4AIeGOF2wqTGqtHq8tG5Pg9387ttHynM3//mnz9hE5CgZLogxMyw595iS8DSEwhpxF22kPcOJ6jMP1dw73bNh54QDuhN576ntLj21Q3yfK6hgsiTIwLfuyXz/sK7Idn137ClcCTSot+/OeIIdKyz7rWx9ebh5YcXxTvPVXH9zEvstH8Hzl5+zWNiJHwWBJlMFaNWqMFcNKqLQsTJGofKEZVi8eg5Bwxxhleri4o1OlFmoUGdfSo+uRN1sutCzbwG5tI3IUDJZENkzL/q/OMZT3OoOSMevw/Ld3HCYt2+OZDjgXcAlHb5xWyzLyXXZsA7pWbQsXvcHezSOyOwZLIhumZd/wex77imzFu5fm4vw9V5WW/WlPmN3TsnWLV0fpPMXUaFLsuXQI14Nvo2eNDnZtF5GjYLAksrFWjZpi9ht1VFo22qjB62S//6pl7TvK7F69PVaf3IKo2GgsOboe1QtXRAWfMnZtE5GjYLAksmNadnjdi+iQZy0a6uag94x/7ZqW7V69HUKiwlShz4YzO9Gjenu7tYXI0TBYEtkxLfueX0OVln3v0mwcuZv/UVr2r3C7pGWL5CyAxqVqYezmaernd6nayuZtIHJUDJZEdvZco2YYO+CF/9KywOX9k+xWLdu7xvMw6PToVLkFcnvmtPnPJ3JULvZuABE9Tst+sdofI7Sv4KqPxuDZrfCeXxNULepqsy7qXOU59SCi+DiyJHKgtOw4P18cLLoJ469OxLablTM8Levtnh2erh5JPsdF76Ke52qwXdAmcjQcWRI5YLVsSd+G2P9zEP69Y8Tm7WvhfeU4nusyDt5e6Ruw/n1/S4pm+EnJ84gyM44siRw4Ldunrg6TyoxAR7eJ+Hz+IoeZxIAoq2GwJHLgtOwkPx/8W2IpFtx5HQuvtrVrtSxRVpaqNOz27dvxzz//oEOHDqhYsWKSz92/fz/27NkTb52HhweGDh2amh9NlCXTsud9G6L8f2nZuRuOI8eVdWjV5WOVljWajGrC8/M3L6FseCk0KFkDBk5RR2S/YLljxw4MGTIEBQoUwK5du1CwYMFkg+XWrVvx3XffoXfv3pZ1np6eqW8xURZOy360OhjdwoaiptthzFjgAc+q9THv7+m4FXLX8txC3j74rO0IdKjY3K5tJsqywTJbtmxYtWoVKlSoAJ1Ol+LtihcvjsmTJ6emfUQUJy072S8Xtv71NbafmYDpV8si8s5HwBN/irdD7mLgstGY5zeRAZPIHucs69atqwKltYKCgjBnzhwsWLAAp08/uqsBEaV+EoOSHdYi1vMXteylN+LlPLegx6PzmOazmWM3TVEpWiJykktHoqKicPDgQRU0X3/9dQwaNAjffvttks+Xh1lISIj632QyqUdqxN3OpGmpfh17kLZqTtZmZ223s7T5XsQJxGqBalQ5ruAl+OW+h2qeDzHxTgkExLqpgHkz5K46l9mwZE04Kmfp7yex3c7Z12l5jQwPll26dMGoUaPg6vro+rDdu3ejefPmaNasGbp27ZrgNhMnTsS4ceOeWh8QEIDIyMhUtSM4Qv59lK8KDAxETp3zFALLLzg4OFgdMHo9282+hirmMcuhfzR6fC7HAzTJFoIXL1XGtRgPy/N8vYrCUfHYZn/b8hgJDQ113GBZpUqVeMtNmjRBzZo1VeFPYsFy9OjRGDlyZLyRZbFixZA/f354e3unqh2u4fKJIlB9nTdvXvj4OM9sJHKwyDli2X9nC5bO1m5nabNUvZotDfJBnWwhuBzliYcmA67HuD9+XuFS8PHxgaNylv5+EtvtnH0tV2I41Qw+Li4ultRqQtzd3dXjSdJRqe2suJvpdTqn+sMUcrCkZf/txRnb7ehtlk/Y9XPpVNWrFPPseJgbTc7XRLhJD0+dCZpkUDSgoGt25DTlc9j9cJb+Tgzb7Xx9nZbt0/3o3Lt3L2bMmGFZPnnyZLzvnzhxAocPH0bTpk3T+0cTZXoSKI0H+8C0ox6+bfroFlpyciHcZFBfRWjyP2CAhm8L30Tug/Wweuc+TmJAlEZWjSyvXr2KZcuWWZY3bNiA27dvo1q1amjdurVa98cff2Dq1KmWSQcknSpD3xo1auDevXv45Zdf0LFjR7z66qtpbTtRliOfsHXelQHX3GhYtKK6POSjTVPiXWdZ2NsHb9UdCOOF7xBuCsf7G/Nhw9VgTO7uDW9P5xq9ETllsJQKVQmO4p133lH/y3KJEiUsz2nYsCGMxsfl6hI8t2zZggMHDqBMmTIqwDZu3Dj99oAok1NT20Vcg86ruFrWV3gf+lIDoPMogA4FgLblmzyewafw4xl8Imq3x6Q1FxBq9Mb641H49+YtzPLTUKm04xb8EGWKYFm2bNlkJxeQEaZ5lGnWqlUr9SAi62jGKBj/7gvT3R1wbXUUOs8i0Eklt0cBy3MkMMrlIVL1KsU85vMynu56fOJXDpVLR2D0ihD0yT4WOQ/8jnVXFqND8xZWTSxClNUxJ0PkyPRuli+1sCupeonutT2x8e2cKJvjFrz0YZi0zR2DfglGSIRzXdtIZE+8nyWRI6ZdY0Ogc82pRn+GWvNgiH2oRpWpVbagB4r2XIdv1xzCxcgSuHg8CidvBGJeL6Byyfzp2n6izIgjSyIHosWEwnigJ2J3tVApWKGCZhoCpZmkZUf51cXUnt7wdAXq6Rci594q2LB9E6tliZLBYEnkSHQGaCGnoYVfhfbwXIb8CJWWHZ4XbQvsgY/bXSzZG8C0LFEymIYlcoS0qxYDnd4NOhcvuDRcBRg802U0mdQtv4r2Wo65azZhW1AtIEjSsvcx5yVPVC2eLcN+LpGz4siSyI60mGAYD/SA8dAASypUl903QwNl3LTsUL/2lrRs7qiDyLG7PDZu38C0LNETGCyJ7Ck6CKY7W2G6vQmIvGmXJpjTsq8UX4HC7jdw7NhOpmWJnsA0LJGNWUaQMhtPthJwabgauuxlbDKaTDIt+9I8/LqmKWbeaAXTjf/Ssn28UbXY48tXiLIqjiyJ7JB2NZ2f+viPMH9TuwbKuGnZl/3645ueuVVaNizkFozbazEtS8RgSWRbWtBxmK6vgPHcZGixYQ7Z/ea07FulF6FStpOIOj+LaVnK8piGJbIhff4mMNRZAL3Ps9C5OG7VqUrL9puA1WsKYuzF9gg1/peW7ZsTVYs6z71gidIL07BEGUiLCUHsgV6qiMfMUKKPQ6RdU5KW9fMbjs+6F1Np2Zv3I3BjY0emZSlLYrAkykCm68thurYExmMjoGnOORerOS37RukVaJH7DxS59i4G/3Kfc8tSlsI0LFEG0pd8FYi48eiWWnK3ECcladlhrw7D72ui8O2FBrgQEYsTTMtSFuK8f71EDlrtGisTDIRdUstqIvRKY50i7ZqStGxXv1EY2rmOSsteCTRi96rh2LB9IycxoEyPwZIoHRnPToTp8g+IPTI00/arOS3bs8QevFboO9S80wfDfrnOtCxlakzDEqUjQ8WPgKh7MFQel6n7VdKy419/AevWTMDai4Ww5YEbDjMtS5kYR5ZEaU27Hn/Pcs2kXA7iUnt+pki7piQt+6LfaHRo08OSll2weAarZSlTYrAkSgPj4UEwnZsM48nRWbYfzWnZlkUv4ZMSo9D0Xme8v/AE07KUqTANS5QGhqoToRnDYSg/Kkv3o6Rl57xRFxvXfIp/bwRh4Y0C2H2dkxhQ5sGRJZG1c7uem/J4MvRspeDaaG2WSLumLC37PnybfGxJy37643qmZSlTYLAkSiEJkLF7OsB4fCRMF2ex35JJy9YqFIIpZQbh2cCOmLhoK9Oy5NQYLIlS6NE1k+Ogy9cM+sKd2W/JpGWXDi2Dgy7Dsel+B8w8WhVtp97Hiesx7DdySgyWRMmkXU03Vj7+gynQEi7NdjDtakW1bEzNpfB01am07OA5xziJATklBkuiRGimaMRsr4/Yfd1hursz3giTUq57HS+Vlq1UwIRvSj9Ky874dTHTsuRUGCyJEqHTu8FQaiB0+RpDl6Ms+ymNadm1wwrgRrZuOBdeAd8eq8+0LDkVBkuiJ9KuhtAjj/9Ayo6AS9NtTLumY1r2fKV90AzZVFq256yb+PPQQc4tSw6PwZLoP1pUIIzb6yDHqd7Qwq9YUq46PS9HTk/d6nirtGz5AgaMLvoROkW8gJ+XzGRalhwagyWRmVse6PI2gNGrvMxbx37J4LTs+mF5kD1/ZQTF5sLc0/WYliWHxmBJyOppVy3ssmUUqa8xG6FVf2Pa1UZp2S7dRmFz/gMIMJVUadnnpwdi9c4DTMuSw2GwpCxL7jkZs7UWYv/qBC02XK3TGTw5qrSxtlWyY/2w3Cot65fvJ7QNaIAliycyLUsOhcGSsi6PwtC55gTccgOxD+3dmixNpWXfzos6JQyI0Vyxxr8M07LkUBgsKUvRYkLUQ+gM7nBpvBEuTbdD5+Fj76ZleZ5uOnTzew87i5/GofDm/6Vl72Ppn+eZliW7Y7CkLMMUfAoxW2vCePi1xxOhe/iw2tXBdKpfxlItW91rP9rfroKViz9iWpacK1jeuXMHEyZMQLdu3bB79+4UbXPt2jWMGTMGL730Ej755BPcu3cvNW0lShOdSreGQIu8zbSrk6Rle1S8Ch00nLylZ1qWnCdYLly4ELVr10ZISAhWrFiBK1ceXYuWlMuXL6NmzZo4c+YMmjdvrgKsvEZgYGBa2k2UIlpMKDTNpL7WeRaGa/Pdj9KurjnYg06Qlu3l9xb2FN2PhffesKRlF+2+xbQsOXawlGDn7++PL774IsXbfPbZZyhatKgKrgMHDsT69esRGxuLKVOmpKa9RClmCjqKmK01YDr7+HjV5SjPtKuTaduwJjYMz6/SsnkNN/Ds9apYtfgDhITH2rtplIVYFSwl6Lm5uVn1AzZs2IAXX3wRev2jH+Xh4YFOnTqp9UQZSi4HCb8M092t0DQjOzsTpGWHPnMS3oYQGEPOou20B7zlF9lMhk5TEhERgdu3b6N48eLx1svy4sWLE90uKipKPcwk7StMJpN6pEbc7UyalurXsQdpq+ZkbbZXu+VOITIBupKnPgxNtgF5GkDTdJZ0bFLY17ZlTX+7uwD9uvXB1r2l8dmxQgiMMqm07Mcd3dC3obdN7wbD4wRO2ddpeY0MDZbmgOfl5RVvffbs2REZGZnodhMnTsS4ceOeWh8QEJDkdkkJjpB/H/0xyfnSnDrnKQSWX3BwcLA6YMwjdGdg63YbHh5H9rODEV76M8Tkafnf2vLAvfspfg32tW2lpr+r+fpiTm9g1FoN1+5Hoap/a6y81BrPNB2OHB4G2AKPE9tJz74ODQ11zGApQdFgMODBgwfx1kuwypUrV6LbjR49GiNHjow3sixWrBjy588Pb2/vVLXFNVw+UTwqKsqbNy98fFzhLORgkU/Nsv/OFixt2W5T2CWYIi/B+8FyGCr0St1rsK9tKrX97eMDbCyjYcGa9SivOwN9hAmvLR6Gb1/Kh6pFM/5vm8eJ7aRnX8tpQIcMli4uLqhYsSKOHz8eb70sV6tWLdHt3N3d1eNJ0lGp7ay4m+llDlAnCjqWeUvTsP+Ztd3yadOcftOVfh06t1zQF+kKXRp+HvvatlLb39k8gCE9nseWv7biiy2uuPDQDV1mBuHjTtnRv5FXhqdleZzYTnr1dVq2T/d3sGXLlqF///6W5T59+qh1169fV8unTp3Cxo0b1XqitDA9OILYbbWghZ6z/EEZivVgtWsW06pRU8x+o46qlo02avA62e+/atkYezeNMhGrguWJEyfUZATyEN9++636evbs2ZbnnD59GmvWrLEsjxgxAg0aNED16tXRsmVL9XWvXr3Qt2/f9NwPyoJMl3+AFnQExvPf2Lsp5CDVssPrXkSHPGvRUDcHvWf8y2pZSjdWpWELFCiAnj17qq/N/4tSpUpZvvbz81OTEJjJpSYSPI8dO4arV6/C19dXpWaJ0spQ7SvospeFvswQdiapSQze82uIrX9txYJdd3Hkfv5H1bLP50D/hp42rZalLB4sfXx8LKPKxFSqVEk9niQjS3kQpZbpwT8wnvwALvWXqRl4dAYPGMoOY4dSPM81aoYSvrG48XMQ/r1jxOX9k7D6SjRadvkU3l7OU9hHjsW5qkUoSzOe+B+0O5tgujDN3k0hJ0nLvlY3FCOKfoU2rl9h6OzdTMtSqjFYktNwqf0TDJU+hb78+/ZuCjlJWnacny8OFt2E8VcnYtvNyiot+9Nf4ZxblqzGYEkOnXaN/WfI44nQvYrCUOkjVruS1dWyr/QZ8V+1LLB5+1pWy5LVGCzJIWmmWMTu7w7TxVkwXV1k7+ZQJknL9qmrw6QyI9DRbSI+n7+IaVlKMQZLckg6vYtKu+orjIG+WOpm4yF6Mi07yc8H/5ZYigV3XsfCq22ZlqUUY7Akx6p2Pf+4eEefvwlcqnzOtCule1q2ebeZKF/ARaVl5244jpWLP+IkBpQkBktyCFp0EGJ3PQvjseEw3fvL3s2hLJKW7VXXHd/4DkUnt88xf8EkpmUpUQyW5BBkTldD1Ukq7arLU8/ezaEskpad7JcLD8t9je1BrTHjYh+mZck+E6kTJTe3KyJvQl+og1o2lBnMDiO7TGJw3rcRSj54NInB52tuw/XKcnTqMpKTGJAFR5ZkF9pDf8TuqI/YA72ghV3hb4EcJC3rgU9KjkF3t/exZtHbTMuSBYMl2YUuexnoS7wMve8wwLMIfwvkIGnZnChQ/Q2cCquGby8NYFqWLJiGJZtWu0LvBn3OKmrZUHM2J7cmx0zLljmEHHeDcfOOER+sCkH05YXo+cIrTMtmYRxZkk2Y7u1F7I4GiN3fDVrsQ7WOd4EgR1W2oKslLftaodl42X0Qdi/pzbRsFsZgSTahy1MHuty1oS/SDdB7sNfJadKyjeu3wNWoEvj+ei+mZbMwpmEpw8iNmXUxXnJzN+j0rnBptlP9T+RskxicL30GQTfDEB0iadlQBFzchi5NasLH3o0jm+HIkjKE6ebvMO5siGznh1vu8MBASc6qbCFPS1q2kfefeMujM27u7IcT16Lt3TSyEQZLyhBqYgG3/DB6VZDQyV6mTJOWHdiyAG5FF8HmgBbo8l0wb/mVRTBYUrrRQk6ru4UInYcPDK1OIqLkaOh0BvYyZaq0bEzTI9gT+6qaW1bSsh8vPMC5ZTM5BktKF8arixCztQaMZz61rNO5erN3KVPyLZIHC/ro0LOOB4q5X8Ew1zY49dtzOHk11N5NowzCYEnpQpe9vPwL/Hd+kiiz83QFvuqeA+PamxBq9Ib/w8LoNDOcadlMitWwlGpaxA3o/pt9R5+nNlzb+VuWibKKNo3qw7/EP1i0JMKSlj3hfw0fdyvNSQwyEY4sKVWMF+chZmMZmG6ssqxjoKSsqkzR/Fg5rJiqlvXUh+FVdFJp2VOX79i7aZROGCwpdQzugCkKWsgZ9iBRnGrZ6S+EwssQAYMpFC/MjmZaNpNgGpZSTIsJsRTtGEr0gy5XDehzVmUPEsXRrkF1+Bf7B5OX3UJYrJtKyx7yf4AJ3XyYlnViHFlSihj9ZyFmQ0mYgk89PngYKIkSTcsuGFpVpWUBDW0iB+LUby1x+uJ19piTYrCkFNFCzwExD6AF7GCPEVmRlp3VLRxVsp1AcZez6P/9A6ZlnRSDJSVKM8VYvjZUmwSXZrtg8B3KHiOywvP1S8PU7B+MC1iMm1E+Ki07+Jf7nMTAyTBY0lNkLlej/3eI2VINWvQDtU4n96HM35S9RZTKtOy0N1r8l5YFSgVOUtWyTMs6DwZLSoAJpusrgNCzMN3exB4iSs9qWT8XdPNZhqoe+/D+whNMyzoJVsNSvBGl3JBZ5nJ1qbcIWtBx6Au2Zg8RpaMX6+aFf+G/8fnqP3A4pCYOrwrFXv9oTO6WA95enEfZUXFkSZa0a+xfnaBpRtUjOo+CDJREGZiWHft6b0taNvraGpxktaxDY7AkIPYhjP9+Ce32BmgBu9gjRDZMy07tkR3Di32N2l67MPe3VUzLOiimYQk61xxwqb8MiH4AvU8L9giRDXWvkw3+hbZh5rrvsfxudyw3p2W7e8Pbk+MZR8HfRFZOu54YY1mnz1MX+oJt7Nouoqyclh386ij0quupls+cO4lDSzvg9MVr9m4apTZYbt++Ha1bt0b58uXRsWNHHDp0KMnnz5gxAyVLloz3qFatmrU/ltJT+FUYj78L079fQAv9l31L5Ehp2Z7e+LDkp2icfRO2rpvMtKwzpmEPHDiAtm3b4sMPP8SkSZPw008/oXnz5jhy5AjKli2b4DZBQUHInTs3Vq16fHcKvZ4DWnvSZSsBQ63voXPLA10OuQ8lETmK7rU94V9wEZZt+gxTrr2D6KtMyzpdsJwwYYIKjmPHjlXLNWrUwNatW/H1119j9uzZiW7n7u6uRpRkv7Sr6eJswDUnDMV7q3WG4r346yBy4LRs4X7TcHR1CBYfjMSfpwKwPWYIyj07CZVKF7N387Ikq4Z4u3btQps28c9ryUhz586dSW539uxZVK1aFXXq1MGbb76J27dvp661lCra/f0wHhkC4z+DoEUFsheJnCwtO6rEF2ifczHOb32TaVlHH1mGhoYiODgYBQsWjLdelm/cuJHodtmyZcOoUaNUUJWU7KeffoqaNWvi5MmTyJMnT4LbREVFqYdZSEiI+t9kMqlHasTdziQjrVS+jj1IW7W0tDl3PegqfAhd3obQXHNDs9G+p7ndduCMbRZsd+bt76413eFfYAI2b43AJ5dG4e65UOy9EIUvZRIDK6tlnfE4MaVjm9PyGi7W/hAXl/ibuLq6wmh8dCF7Qt5+++145yhr166NUqVKYdasWfjggw8S3GbixIkYN27cU+sDAgIQGRmJ1AiOkH916uvAwEDk1DnPeVPpe/mgIgdMis73ahrcby9AbI4aMGav/mhdvjcf/X/3Lhy23Q7AGdss2O7M3d85XIEqz32DBnpgzQlgw4lI1IkYh4p1XoVvEZ9MfZyY0rHNMujL8GCZI0cOde5RAk1c9+7dQ/78+RPd7smdk9eRlOzp06cT3Wb06NEYOXJkvJFlsWLF1M/x9n5082FruYZLsH/U9rx588LHxxXOQg4WmYZO9j8lB4vp2hKY/EcD2XxhaHVCTYLuDO12BM7YZsF2Z43+ntEXaH44Eqf3fIP++abh2Ik/sSH8T/Rv6KnakxmPE1M6ttnD49GMSRkaLKWRtWrVwt69ezFkyBDL+j179qhzkSklnw6uXLmCKlWqJPocCcrySKgNqe2suJvpdTqnOVDM5GBJ6f7rivlBu7kKhlIDoHdJ/cFh63Y7Cmdss2C7s0Z/+9Xxgn+hQdi97SCmXB6EIyfDsP9SbIonMXDG40SXTm1Oy/ZWbSlBcuXKlfjzzz/VslwOsnv3brzxxhuW50ydOjXedZTvvPMOrl69qr6Ojo5W5y9luV+/fqluNCUwycCl76FFPkqx6vQucG2wHPqCbdlVRJm0WrZhrzWoUKmxWl5/PArTfpjOW345yqUjL730Ei5evIj27dvDYDCoaD99+nS0bNnS8hwp4jEHRyGjzlatWql0bVhYGCpUqICNGzdaNRqlpJnOf/NokoECbeHSeEOK0jFElDmqZeuVdsO6LWswqsBwXNv7DX6+eQx9G+Xk+4C954b96KOP1OhQzl1KDvnJgp/hw4fj1VdftSz37NlTPR48eAAvL68E06uUNvoSL8N09VcYyg7nHwhRFpzEoGbBlti7rR1+v9MSS45GYc/FYM4tm85SlcB1c3NDoUKFngqUIleuXChevPhT62UWHwbKdEy7XlsGzRSjlnXueeHS8hDndiXKwmnZej3XQVdygCUt+8GcVZxbNh05zxlesjCeGAXjgR4wnnx86Q1Tr0RZm6e7HpP9cqlJDCpk98e4Qv3hvb82Fu++qj5gU9owWDohffE+gGcx6H0enysmIjKnZee+VhbHI5ti8/12eHeNOwb9EoyQCOeZiMARMVg6AflU6BK017Ksz1UNru0uMO1KREmmZf/1mWxJy74+cz/TsmnAYOkETEcGwftkV5iuLbass9dEA0TkPGnZL/3yqbRsPvdQjCvQB7kO1sXmw/5My6YCg6UT0Pm0hMklD+CW195NISInTMuuGJILt0wVcCWyJD7aURJvLAxhWtZKDJYOSE0aHHzKsqwv2gPBtfdBX6C1XdtFRM7Jt0g+lZZdn+03GOGC9Sei0ePb80zLWoHB0sFomgnGA70Qu60WTEFHH693Sd2cuERE5rTs+O5FMK6dBi9XE4bnGaKqZdfs/Itp2RRgsHQwOrkbSrZSgEsOIDrI3s0hokymY2Vg/ZsecHdzh1Ez4INNuVktmwIMlg6SdtUiblmWDZU/g2ur49D7NLdru4goc/ItnFOlZRe4bsWD2LyqWrbD1Ls4fSnxexNndQyWdqYZI9QEAzHb60KLumeZCF3nWcjeTSOiTJ6WHetXSVXLeroCL3pNRM79NbB+xxamZRPAYGlvendoMaGAMRLaQ397t4aIsmC17Ma3c+OZXP7wNgRj6g4d07LpMZE6pZ2aeir2IXSuOdQ5Spe6vwCmKOg8i7B7icjmyhZ0Q9GeazFzzT6cDvfF6eNROHnjPub21qNKiTz8jXBkaXtaTIhKu8buaQ/NFKvW6dzzMVASkd3Tsu/6NbKkZatoK5F7bwVs2L6RaVkGS/swBR2BFnoWeHjBTi0gIkoiLTs8L7oU2ob8rgFYe+AK07JMw9ow7aoZHxXuuHrDpcFq6NxycTRJRA6pbAEXFO29GN+v6Y3fA+sDgY/SsnP6ZEPVYp7Iiljgk8G0mOBHt9M69vbjTs9ZmYGSiBw+LfuGX2dLWtYz4gS8dlXAxu0bsmRalsEyo0XegenWBpjkZs2RdzP8xxERZURadmCJpSjmcRUXTq7PkmlZVsNmAPOnLrkhsy5HObg0WAmdjCY9fDLixxERZXxats93WLqmFiZfa4fYq+a0rDeqFssad0BisLRCQEAAXn/9dRUEf/nlF2TLli3htOvhgdAVaA1DqdfUOn1BToBORM6flu3rNxAepSMwekUIgoLuIXJba2wo/jnaPdtWvS86khEjRuDSpUuWZVdXV+TLl099bTQarX49BksrLFiwAL///rvq6CVLlmDAgAFPPUcL3A/T9eXA/QPQF+8LncHd6l8KEZEjp2WfKeaKrWtmonr2I9h58SsMul4fk7vnhLen45zZ27FjB+7cuYNZs2ap5ejoaBw6dEh93aZNG+zevRvu7il/f2awtML333+Pzp0748GDB5g/f36CwVJfsA0MNedCX6g9AyURZd60bP9PsGZNLnx2oTUCY6MfpWX75kTVoq5wFJL969Kli2W5bdu2+Oqrr/D3339jzZo18PPzS/FrOc7HAAcnn0LOnj2LIUOGqMf+/ftx8uRJlXaNPfASTIH7LM81lB7IalciyvRp2e5+I/FRtzKqWvZ6YBQurO/uNNWy9+/ft+r5DJYpNG/ePJQvXx4tW7ZUn1QKFy6s1pkuL4Dp2q8wHn3LKQ4QIqIMqZYt/Ts65F2D0jfewhu/3HPIalmT6VGb9Ho9mjZtatW2TMOmQHBwMH777TdMnDjxUae5uGDgwIGYPn06vvjiGlwjb8Lg+5bDneAmIrJVWvbdAa9j3ZoHmHuhJk6EmXDcAdKyt2/ftqRhY2JiVDZQLF++HJUqVbLqtTiyTIGFCxeqQNi/f381t2vs4UEY2Pd5hISEYNWq1XCp+gXTrkSErJ6WfdFvNAZ0aqrSslcCjdi8Yoxd07I5cuTAyy+/rB6vvvqquppBTJ48WV3dYA2OLFNAink8PT1Vh2vBJ6CFXQQ8foeXl5dKxfbu3Tt1v0kiokxaLfvt0k0YVngyQu/OxvBfTuCz7sVtXi37ZIGPDHA+/PBDVeDzzjvv4Oeff07xazFYJkNKjY8ePYoff/wRuXLlghYbBtOleeqykPYPYlSxz4ULF+Dr65v63ygRUSZLy345qD3WrZmAbZe9sfqeJ/52gLSsWcmSJbFlyxartmGwTMbcOTNRtkQe9O/bK86lIC9Zvj9+/Hg18vziiy+s/40REWXytKzxUAQ2rwhRadlZi35AxzrF7T6JwcOHD63++TxnmYSwsDAs+XUhWlW6D+PpTxJ8jly389NPPyE29tG9KYmI6Olq2aZFrmNiyRFoHtgJHy78x67VslL407VrV6u24cgyCUuXLkVoeCzaPFsLBt+hCT6nXbt2arICmdnnhRdesO43RkSURdKyPwypgY1rPsK1mzfx07Wi2HE949OycathZea1ixcvqq9fe+01fPnll1a9FoPlE2SSAdPVxTCUGYzq1atj1apVaN22LXQeHomOLOU5pUuXTt1vk4goC6Vllx+KgOd/adkPftiGwY21DEnLTpkyRV32ZybXVkp1bIsWLfD111+rok1rMFjGIeXNsX+2gvbgb8DFC7Vq9UOtWrWsqrYiIqLkq2VH/HINUwsNRKHAm/hq0VoM7touXatln3322afWSTVsavGcZRzyycZQ8QPo8jWF3qdlqjuViIiSTssuf6sEjrq+id3BzTD9aA20nXofJ67HwFHpUzsCCw0NzfBtbEEmGTDd2mhZ1hfuDJdmOznJABFRhqdl30dw9XVwdzWotOwrs/7Fhu2bHHLqUH1q8sByT7C8efOiUKFCKbqoMzXbpLfo2MeVV5Izl2XNGImY7XURu7czTPcPWr7PaeuIiGyjex0vVS1bsQDwZekheDawA2b/ukBVyxpNGvb5R2PTGaj/ZdlerDpnKfOjvv/++6qgRe4HtmjRIjWFUKlSpdCkSZN02ya9jV8Xijm7wi3LM3dGYtauSAxq5oXRpXvDdHcrR5JERHZMy/4+LD82rmmHK5E38e3JBphzPhAaNNx7KAFSin+CUSinHp92yYH2VRMuuHSYkaVMHC6XR7Rv3x4GgwH9+vVD/fr1MWPGjHTdJr0D5ayd4TB/IMluCEVFr5NqWdZ/4T8MLk23M1gSETlAtezJCocRiVwIeGhCcFgUamR/dMNmcTvYhNcXBGPDiUjHHVnKrU0OHjyobpwZV7NmzdRoMb22SU+Sao07osznGoDllTshmz4M7U9sw70YH8zaFYUcXga46B231kny9w8fAtmzhztVitgZ2+2MbRZsN/s7sxwnJs0Ag7wdG4H/Ff8crxSch48uTcLiu31hHmN+vCYUbSq7w6DXOV6wlOmBIiMjkT9//njrZTmx2dtTs42IiopSjyfLfSX4mu9HlhI//fV4RCnuxeTDufAKyOUSBD0evY58e9LGxwHVcclBEQbn44ztdsY2C7ab/Z25jpObUUUQZsyOQ6F1LOvkPftmkAn7/aPQoIybVa9nTfxIdbA0fwqRWRDikmne5GLP9NpGyH0jx40b99R6CbASfFPqzDXVirgtwsgLMxBp8oAxzq7ny6ahaC44NOkzuY+ms3HGdjtjmwXbzf7ODMfJg3DgyoNH79s/3n4dvwX0QKgx51PPO389CGVyWPfaabkiI8U9JjMfyOPOnTvx1suyVLim1zZi9OjRGDlyZLyRZbFixdSI1NvbO6VNRsVi4cDR+J+gwkzZn3remy2y47UmXnBU8mlIPijkz58vyQ8ZjsYZ2+2MbRZsN/s7sxwn+/yj4Tfn8cw7CQVKUbZoLvj4WDey9EhkJraUsOrjhVSvbt26FSNGjLCs++OPP+JVtYaHh6vRX548eVK8zZPc3d3V40nyy7XmF/xyIy98ti4sXir2qdfUPXqeox44cUfp1u6/I3DGdjtjmwXbzf7ODMdJ/TLuqupVinkSeuuWMWehXHr1PL2V5yzTss9WbSmXgEig++abb3D+/Hl88MEHOHfunLqJpplMTht3ntSUbJNR3Fz06vKQpMj35XlERGR/Br1OXR4ingyF5uVxnXPYtLhHWBUlZDQo10suX74czZs3x19//YXNmzejUqVKlud4eXmpyQes2SYjfdgxB95o7qVGkHHJsqyX7xMRkeNoX9UDc/vnRMGc8UOUjChlvT2us9Rpjjiv0BPknGXOnDnVDPLWnLN88jISqY49c+0hKhbLrlKvzjKilPMMd+/ehY+Pj8OmTjJLu52xzYLtZn9nxuPEaNJU1asU88g5Skm9pmVEmZZY4rglUelMAqMU8dy9+xA+Po5/jpKIKKsz6HXq8hCpepViHmvPUaYnRgwiIqJkMFgSERElg8GSiIgoGQyWREREyWCwJCIiygzVsOarW8wTqqelbFrmBpQpj5ypGpbtZl/zGHEs/Jt0zr42x5DUXDHpFMHSPPmtzA9LRESU1pgi11tmukkJ5JPFzZs31aTsabkHm3lC9mvXrqV6cgN7YLvZ1zxGHAv/Jp2zryXcSaAsXLiw1aNUpxhZyk4VLVo03V5POtyZgqUZ282+5jHiWPg36Xx9be2I0sx5TtwRERHZCYMlERFRMrJUsJR7ZH788ccJ3ivTkbHd7GseI46Ff5NZr6+dosCHiIjInrLUyJKIiCg1GCyJiIiSwWBJRESUGa6ztMaxY8dw8eJFlC5dGtWrV8+wbdKT0WjEvn37cO/ePTzzzDMoWbJkks+X5165ciXeuvz586Nly5awdbu3b9+OBw8ewM/PL0XbhIeHY8+ePYiOjkbDhg2RJ0+eDG9nQm3YsmULsmXLhueeey7J58bExGDFihVPrW/QoAFKlCgBW5H+Onr0KAICAlChQgWUKVMmRdv5+/vjxIkT8PHxQf369W0+zaNcAP7PP/8gKioK1apVQ8GCBZN8/pkzZ9TfY1yurq7o2rUrbN3uQ4cOqX6vUqUKihQpkuw2sbGx6m/z/v37qFGjBooXLw5bu3v3rupvKYaRNuTKlSvJ5//+++8ICwuLt06OL3kfsoetW7eq98EXX3wRbm5uye7r/v371d9xo0aN1HR4GUrLJGJiYrRu3bppuXPn1lq3bq3+l2VZn57bpLc7d+5o1apV00qUKKG1bNlS8/T01CZMmJDkNj169NBKly6t/jc/Pv74Y82Wpk6dqpUsWVK1w2AwpGibQ4cOaQUKFFD727BhQy1Hjhza6tWrNVuR3+vbb7+tFSpUSCtSpIhWr169ZLd58OCBFMCp4yNuf+/evVuzlV9//VX1c506dbT27durfuvVq1eyx+kHH3ygeXl5ac8995zaX9n+/v37Nmv3J598on5us2bNLMf2Z599luQ2EydOVH+Hcfu6f//+mi19/fXXWvHixbVWrVppLVq0UO0eMWJEktvcunVLq1KlivqbMG8zadIkm7XZZDJpr732mmp3hw4d1LGdPXt2bf78+UluJ+87clzE7e+FCxdq9rBp0ybN3d1d/b0FBAQk+VxpY7Zs2bQmTZpoFStW1IoVK6adPn06Q9uXaYLl9OnTtVy5cmmXLl1Sy/7+/pq3t7c2Y8aMdN0mvb300ktajRo1tPDwcLX8+++/q4Pl77//TnQbOaAHDBig2dN3332nXb58Wfvxxx9TFCzlj7lChQpqf80kwEv/BwUFabYQGRmpTZkyRQWMN99806pgmdTvI6MtW7ZMu3HjhmVZjlMJmNOmTUt0mx07dqh2//nnn2o5ODhYK1eunDZ48GDNVubNm6eFhoZaljds2KDa9NdffyUZLGvVqqXZ09KlSy1/j2L79u2q3Xv37k3yb1LaHRERoZZXrVql6XQ67Z9//rFJm41Go7Zo0SL1v9mXX36pubi4aGFhYUkGS/k92dutW7dUwBs/fnyywfLmzZvqw4i8fwvZZ/kQWb9+/QxtY6YJlvLG98orr8Rb169fvyQ7MDXbpCf5w5JPUnPmzIm3Xt7Uhg8fnuQf5vPPP6/+IGWEExISotlLSoOlBBv5Izh8+LBlXWBgoPpjtscnWWuD5ezZs9Uo+OTJk5ojkE/UTx67ccmHKRkxxCVvnvJhMO4bqq3Jm9zMmTOTDJaVKlXS1q1bp23ZskVlXuxNPqjIMbB58+YEvy/ByM3NTfv+++/jrZdswLvvvqvZy5o1azS9Xp9k4JFgOWrUKPVeIpmf6OhozdaMRqPKfkyePNkyWEiqzRIkZdQsH37N/vjjD7Xd+fPnM6ydmabAR87LyLmFuKpWrarWp+c26en8+fPqXE5q2nDgwAHMmzcPgwYNUuc4ly9fDkdm3p+4+yrnK+VckK36Oy3mzJmD2bNno0mTJmjWrBlu375tt7YEBgaq85dPHjcpObZlUuqrV6/CHvbu3YuIiIgk2y1kwuxvv/0WH374oTrvN3HiRNia1AQsWbIEs2bNQufOndGnT59Ez2//+++/lnOb9novMTty5AgWL16MyZMn45133sGECROQL1++JLeRc/Lz589X+yn7IK9hS1988YWa4HzkyJEper70admyZeNNUiB9LU6ePJlh7cwUBT5yYl2KNp4sFsmbN686eS3fd3FxSfM26S04OFj9n1AbLl++nOh2AwcOxM8//2w5Af7JJ5+gf//+qFWrlipSckSyr3Ii/smT9rKvQUFBcFTS3p07d6oAKaT4QL6WDylr1qyxeXukqEp+11KwI8dBUv2d0HEl7NHfUgT28ssvo3379mjatGmiz2vevDkGDx5sKUxZtWqVKvaQgpN27drZrL0SsFevXo07d+7gxo0bKlgmVhyV1N/xqVOnYEsSSNatW6cKFqW9lSpVSvL58mHA3K/ywV0K9eRx+vRpVViV0fbt24dp06apoqSU3lHKXsd2phhZSlAzGAx4+PBhvPWyLN9LKOilZpv0Zv5klFAbkqrskqrXuEFHPoHLbcykksxRyb7KqELaac2+2puXl5clUAr5lD58+HBs2rRJfaCyJem7AQMG4PDhw9iwYYO6ZV1S/Z3QcSVs3d8ympU3ZAmAMupJilTsxq3gfOGFF1CzZk1VtWlLjRs3ViPLHTt2qID97rvvqv/T8+84I/Tr1w/Lli1TlbwyspQqYgmciYn7AUT2Q95LLly4oKqSbWHgwIFo3bo1du/erfpb/hfS18ePH3eoYztTBEshI6on00uSSilVqlS6bpOezKPAhNpgzQhRArunp6e6rMBRyaUO8mZ//fp1yzoJNnKfUkcdDSdGbhMkaTfziMIWJE312muvYfPmzeoNvFy5csn2d0LHlXxAtOUlL3IJRtu2bdXv+o8//kjVLZZkG3se2/Xq1VP9bX4jz6i/4/TWt29fdemTXF6RUubfj636u3HjxqqNMoqXh4w0xcaNGxMdlSd2bIsM7W8tk5BLAsqWLWs5QR0VFaWVKVMmXqHM2bNnVaWbNdtkNCky6dmzp2X5ypUrqmBmyZIllnV79uzRtm7dqr6Wk9pPlv+bq/USK0CwV4HP2rVrLdWAUgQhFZxyEt9MCmakYvDcuXOaoxT4yDGwePFiVelrrrx7kp+fn1aqVCnNVqSSWAp2ChYsmGh5vFQTSrvNxV5S4ejh4RGvUKJt27aqkMJWpBJWLhGSKtHELlk5deqU9ttvv1mWn+zvq1evqksEbHUZhlTBPlmdLX0oBSXffPONZZ0U1m3bts2yLPvYp08fy/LFixdVcU3cfctI0sYnLyWSNsatiDYX/Rw5csSyzZMFPXLZmhQrJXfpRkZJqMBHCiHl2Jb3xrjFgvK+aPb++++rv4/Y2NgMa1umCZbyZiHXdMn1cHJZg1wjJcuy3uyrr76K98aekm0ymhzQcnAOHDhQVXlJJWDTpk3j/dK7du2qNWrUyFKdWb58ee29995T1XdjxoyxXHdnS/v27VMHsFyKIG8K8rU84h7kUmknH0jMpI+l+nfs2LGqMjNv3rzxvm8L69evV+2U37mvr6+l3eYKUWm//CH+8ssvannu3Lnq9yFv1lK13KlTJ/XmLa9jK/K7lg8VcqmNub3y2Llzp+U5GzduVO0+c+aMJehLNewzzzyjLoXq27evuuZSKh5t5dlnn1V9NWvWrHjtPn78uOU5ct2lPMdMjvNBgwapvpbK2KJFi6r9iHsJSkaS6lu5bk8qRH/44Qf1e5fq9OrVq8erOu/cubO6ftRMfhfydyxtl79juUxK9t9Wlce7du3SatasqX366afqA6xcY5svXz6te/fu8Z4n72/vvPOO+lqCjezXuHHj1PWYcp2m7INcZ2ovvycQLOX9WNbJsRP3qgXZF/kAI78rqaqXS2cyUqZJw8rMIHIuR2ZWkaG8zA4jy3FnDJGZKXr06GHVNrZIQ8jPzJ49O/7++29VOCLpKkmXxX2OuRJPzudIJaxUkUp1oRR8/Pbbb/j1119hS9JmSZtI4Ub37t0taRSp1DTr1KmTOt9k9sYbb6jiA5l54+zZs5g5cyamTp1q03Zv27ZNtTN37tyqIMrcbulH8/kQOUbMsyjJOZWvv/5a7af8fuQYOXfunCpUsRU5NqToQvrM3N64KStRqFAh1W5zGs1cmCSpuIMHD6JAgQKqiEL22VakkrVjx46qHXHbHfd8WOXKldGtWzfLsqSY5e9R2irFNZMmTVJpROkDW5DCKfm7kvcAmWlK2jBu3Dh1vMc9RyxV0S1atLAsy3ltOT7kHLecL3zzzTdVKtFWMyZJ0ZS8D0iRzK5du9TxLOcA5fxlXFLxKjP7CJn1Rn4fso3ss7ynyH6mtCo1I0gb5DiOW+kqp5hkXdzTBz/++CM+//xzVdAk5yvluOnduzcyEm/RRURElIxMM7IkIiLKKAyWREREyWCwJCIiSgaDJRERUTIYLImIiJLBYElERJQMBksiIqJkMFgSERElg8GSiIgoGQyWREREyWCwJCIiSgaDJREREZL2f2/EvbZU2YbfAAAAAElFTkSuQmCC", + "text/plain": [ + "
" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Distances mesurees sur la figure : {'MA': 2.5, 'MB': 2.5, 'MC': 2.5}\n" + ] + } + ], + "source": [ + "def draw_triangle(A, B, C, M=None, title=None):\n", + " fig, ax = plt.subplots(figsize=(5.2, 4.2))\n", + " ax.plot([A[0], B[0], C[0], A[0]], [A[1], B[1], C[1], A[1]], 'o-', color='#1a73e8', lw=1.6)\n", + " for P, name in [(A, 'A'), (B, 'B'), (C, 'C')]:\n", + " ax.annotate(name, P, textcoords=\"offset points\", xytext=(8, 6), fontsize=12)\n", + " if M is not None:\n", + " ax.plot(*M, 'o', color='#188038')\n", + " ax.annotate('M', M, textcoords=\"offset points\", xytext=(8, 6), fontsize=12, color='#188038')\n", + " for P in (A, B, C):\n", + " ax.plot([M[0], P[0]], [M[1], P[1]], ':', color='#f9ab00', lw=1.4)\n", + " ax.set_aspect('equal')\n", + " ax.set_title(title or \"Triangle rectangle en A\")\n", + " ax.grid(alpha=0.3)\n", + " plt.show()\n", + "\n", + "A = np.array([0.0, 0.0]); B = np.array([4.0, 0.0]); C = np.array([0.0, 3.0])\n", + "M = (B + C) / 2\n", + "draw_triangle(A, B, C, M)\n", + "\n", + "d = {name: np.linalg.norm(M - P) for name, P in [('MA', A), ('MB', B), ('MC', C)]}\n", + "print(\"Distances mesurees sur la figure :\", {k: round(float(v), 10) for k, v in d.items()})" + ] + }, + { + "cell_type": "markdown", + "id": "1d33a02b", + "metadata": {}, + "source": [ + "Les trois distances affichées coïncident au flottant près : la figure **suggère** fortement le théorème. Mais une figure n'est pas une preuve, pour deux raisons distinctes :\n", + "\n", + "1. elle peut être **mal tracée** — des erreurs d'arrondi ou un dessin approximatif peuvent faire ressembler un triangle quelconque à un triangle rectangle ;\n", + "2. surtout, elle n'est qu'**un seul exemple**. Le théorème parle de *tous* les triangles rectangles, une infinité.\n", + "\n", + "Ce notebook répond à la seconde objection par une machinerie explicite, puis mesure honnêtement ce qui manque encore." + ] + }, + { + "cell_type": "markdown", + "id": "d51d9141", + "metadata": {}, + "source": [ + "## 2. Traduire l'énoncé en polynômes\n", + "\n", + "Écrivons l'énoncé avec des coordonnées inconnues : $A(x_A, y_A)$, $B(x_B, y_B)$, $C(x_C, y_C)$, $M(x_M, y_M)$.\n", + "\n", + "**L'hypothèse** « rectangle en $A$ » dit que les vecteurs $\\vec{AB}$ et $\\vec{AC}$ sont orthogonaux. Le produit scalaire nul donne un polynôme de degré 2 :\n", + "\n", + "$$H \\;\\equiv\\; (x_B - x_A)(x_C - x_A) + (y_B - y_A)(y_C - y_A) = 0.$$\n", + "\n", + "**La définition** « $M$ est le milieu de $[BC]$ » donne deux équations affines, qu'on peut substituer :\n", + "\n", + "$$x_M = \\frac{x_B + x_C}{2}, \\qquad y_M = \\frac{y_B + y_C}{2}.$$\n", + "\n", + "**La conclusion** « $MA = MB = MC$ » est une égalité de distances. On l'élève au carré (des distances positives sont égales ssi leurs carrés le sont), ce qui donne deux polynômes :\n", + "\n", + "$$C_1 \\;\\equiv\\; MA^2 - MB^2 = 0, \\qquad C_2 \\;\\equiv\\; MB^2 - MC^2 = 0.$$\n", + "\n", + "Après substitution du milieu, $C_1$ et $C_2$ ne dépendent plus que des six coordonnées des sommets. Construisons-les avec `sympy` :" + ] + }, + { + "cell_type": "code", + "execution_count": 3, + "id": "86e436d5", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-23T16:15:57.537213Z", + "iopub.status.busy": "2026-09-23T16:15:57.537000Z", + "iopub.status.idle": "2026-09-23T16:15:57.571406Z", + "shell.execute_reply": "2026-09-23T16:15:57.570677Z" + } + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "H = (-x_A + x_B)*(-x_A + x_C) + (-y_A + y_B)*(-y_A + y_C)\n", + "C1 = x_A**2 - x_A*x_B - x_A*x_C + x_B*x_C + y_A**2 - y_A*y_B - y_A*y_C + y_B*y_C\n", + "C2 = 0\n", + "C2 est-il identiquement nul ? True\n", + "degres : H -> 2 | C1 -> 2\n" + ] + } + ], + "source": [ + "xA, yA, xB, yB, xC, yC = sp.symbols('x_A y_A x_B y_B x_C y_C')\n", + "\n", + "# Hypothese : orthogonalite en A (produit scalaire nul)\n", + "H = (xB - xA) * (xC - xA) + (yB - yA) * (yC - yA)\n", + "\n", + "# Definition du milieu M de [BC], substituee ensuite partout\n", + "xM = (xB + xC) / 2\n", + "yM = (yB + yC) / 2\n", + "\n", + "MA2 = (xM - xA)**2 + (yM - yA)**2\n", + "MB2 = (xM - xB)**2 + (yM - yB)**2\n", + "MC2 = (xM - xC)**2 + (yM - yC)**2\n", + "\n", + "C1 = sp.expand(MA2 - MB2) # conclusion, 1re composante : MA^2 = MB^2\n", + "C2 = sp.expand(MB2 - MC2) # conclusion, 2e composante : MB^2 = MC^2\n", + "\n", + "print(\"H =\", H)\n", + "print(\"C1 =\", C1)\n", + "print(\"C2 =\", C2)\n", + "print(\"C2 est-il identiquement nul ?\", sp.simplify(C2) == 0)\n", + "print(\"degres : H ->\", sp.Poly(H, xA, yA, xB, yB, xC, yC).total_degree(),\n", + " \"| C1 ->\", sp.Poly(C1, xA, yA, xB, yB, xC, yC).total_degree())" + ] + }, + { + "cell_type": "markdown", + "id": "e8935dba", + "metadata": {}, + "source": [ + "L'énoncé géométrique est devenu **deux polynômes actifs** en six variables — et le sympy vient de nous apprendre quelque chose :\n", + "\n", + "- $H$ (degré 2) : l'**hypothèse** — la figure satisfait « rectangle en $A$ » exactement quand $H = 0$ ;\n", + "- $C_1$ (degré 2) : la part **non triviale** de la conclusion, $MA^2 = MB^2$ ;\n", + "- $C_2 \\equiv 0$ : la part **gratuite**. $M$ étant le milieu de $[BC]$, l'égalité $MB = MC$ vaut pour *tout* segment, rectangle ou pas — c'est la médiatrice, pas le théorème. La conclusion « équidistant des trois sommets » ne coûte donc qu'une seule égalité substantielle : $MA = MB$.\n", + "\n", + "Le théorème entier tient maintenant dans une phrase **algébrique** :\n", + "\n", + "> Pour toute valeur des coordonnées : si $H = 0$ (et la figure non dégénérée), alors $C_1 = 0$.\n", + "\n", + "C'est cette phrase que les notebooks 02 et 03 établiront *exactement*. Ici, nous allons la **tester**." + ] + }, + { + "cell_type": "markdown", + "id": "fa98de13", + "metadata": {}, + "source": [ + "## 3. La vérification numérique : beaucoup de figures, un test\n", + "\n", + "Plutôt qu'une figure, tirons-en dix mille. Pour être sûr de fabriquer des triangles rectangles, on ne tire pas $A$, $B$, $C$ au hasard et on ne vérifie pas l'angle après coup : on **construit** l'angle droit. Choisissons $A$ et une direction $u$ quelconques, posons $B = A + u$, puis $C = A + v$ où $v$ est $u$ tourné d'un quart de tour **puis allongé d'un facteur entier $k$ indépendant** — sans ce facteur, tous nos triangles seraient isocèles, une famille bien trop pauvre pour tester un théorème général. L'hypothèse $H = 0$ vaut alors **par construction** — sur des coordonnées entières, exactement." + ] + }, + { + "cell_type": "code", + "execution_count": 4, + "id": "034df3db", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-23T16:15:57.573218Z", + "iopub.status.busy": "2026-09-23T16:15:57.573050Z", + "iopub.status.idle": "2026-09-23T16:15:57.628802Z", + "shell.execute_reply": "2026-09-23T16:15:57.628291Z" + } + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "10000 triangles rectangles (coordonnees entieres, longueurs AB et AC independantes)\n", + "max |H| = 0.0 (hypothese, nulle par construction)\n", + "max |C1| = 0.0 (MA^2 - MB^2, attendu : 0)\n" + ] + } + ], + "source": [ + "def sample_right_triangles(n, span=20, rng=rng):\n", + " \"\"\"Tire n triangles ABC rectangles en A, sommets a coordonnees entieres dans [-span, span].\n", + "\n", + " B - A = u et C - A = v avec v orthogonal a u, mais de longueur INDEPENDANTE\n", + " (v = k * rot(u), k entier non nul tire a part) : la famille couvre les triangles\n", + " rectangles quelconques, pas seulement les isoceles.\n", + " Renvoie les six coordonnees en six tableaux de forme (n,).\n", + " \"\"\"\n", + " a = rng.integers(-span, span + 1, size=(n, 2)) # A\n", + " u = rng.integers(-span, span + 1, size=(n, 2)) # direction AB, non nulle a verifier\n", + " ok = np.any(u != 0, axis=1)\n", + " while not np.all(ok): # retirer les u nuls (triangle aplati)\n", + " u[~ok] = rng.integers(-span, span + 1, size=((~ok).sum(), 2))\n", + " ok = np.any(u != 0, axis=1)\n", + " k = rng.integers(-span, span + 1, size=n) # rapport des longueurs AC / AB\n", + " nul = (k == 0)\n", + " while np.any(nul): # k non nul : C distinct de A\n", + " k[nul] = rng.integers(-span, span + 1, size=nul.sum())\n", + " nul = (k == 0)\n", + " v = k[:, None] * np.stack([-u[:, 1], u[:, 0]], axis=1) # v = k * rotation d'un quart de tour de u\n", + " b = a + u\n", + " c = a + v\n", + " return a[:, 0], a[:, 1], b[:, 0], b[:, 1], c[:, 0], c[:, 1]\n", + "\n", + "N = 10_000\n", + "xA_, yA_, xB_, yB_, xC_, yC_ = sample_right_triangles(N)\n", + "\n", + "# Evaluation vectorisee des polynomes avec lambdify (numpy)\n", + "evalH = sp.lambdify((xA, yA, xB, yB, xC, yC), H, 'numpy')\n", + "evalC1 = sp.lambdify((xA, yA, xB, yB, xC, yC), C1, 'numpy')\n", + "\n", + "Hv, C1v = evalH(xA_, yA_, xB_, yB_, xC_, yC_), evalC1(xA_, yA_, xB_, yB_, xC_, yC_)\n", + "print(f\"{N} triangles rectangles (coordonnees entieres, longueurs AB et AC independantes)\")\n", + "print(f\"max |H| = {np.abs(Hv).max():.1f} (hypothese, nulle par construction)\")\n", + "print(f\"max |C1| = {np.abs(C1v).max():.1f} (MA^2 - MB^2, attendu : 0)\")" + ] + }, + { + "cell_type": "markdown", + "id": "1e8156d0", + "metadata": {}, + "source": [ + "**Lecture du résultat.** Sur les 10 000 figures, l'hypothèse est exactement satisfaite (coordonnées entières : aucune erreur d'arrondi) et la conclusion non triviale $C_1$ est **exactement nulle**, figure après figure. Le test dit :\n", + "\n", + "> *Chaque fois que j'ai fabriqué un triangle rectangle, le milieu de l'hypoténuse était équidistant des trois sommets.*\n", + "\n", + "Dix mille confirmations d'un coup — et pourtant, aucun mathématicien ne crierait « preuve ». La section 5 dira exactement pourquoi. Mais d'abord, assurons-nous que la machinerie ne répond pas « oui » à tout." + ] + }, + { + "cell_type": "markdown", + "id": "9c229e9a", + "metadata": {}, + "source": [ + "## 4. Témoin négatif : la machinerie sait aussi dire non\n", + "\n", + "Un test qui valide tout ne prouve rien. Testons un **énoncé faux**, avec la même machinerie, sans prévenir le code :\n", + "\n", + "> **Énoncé piège.** Dans un triangle $ABC$ rectangle en $A$, le milieu du côté $[AB]$ est équidistant de $A$ et de $C$.\n", + "\n", + "Traduction : $M'$ milieu de $[AB]$, conclusion $C' \\equiv M'A^2 - M'C^2 = 0$. Si la méthode est honnête, elle doit le **rejeter** sur la majorité des figures :" + ] + }, + { + "cell_type": "code", + "execution_count": 5, + "id": "a9eda10d", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-23T16:15:57.630668Z", + "iopub.status.busy": "2026-09-23T16:15:57.630527Z", + "iopub.status.idle": "2026-09-23T16:15:57.644095Z", + "shell.execute_reply": "2026-09-23T16:15:57.643227Z" + } + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Enonce piege evalue sur les memes 10000 figures :\n", + " figures qui le REFUTENT (C' != 0) : 10000 / 10000\n", + " figures qui le 'valident' (C' = 0) : 0 / 10000\n", + " max |C'| = 304400\n", + "Identite exacte C' + AC^2 - H = 0 ? True\n" + ] + } + ], + "source": [ + "xMp = (xA + xB) / 2 # milieu M' du cote [AB]\n", + "yMp = (yA + yB) / 2\n", + "Cp = sp.expand((xMp - xA)**2 + (yMp - yA)**2 - ((xMp - xC)**2 + (yMp - yC)**2))\n", + "\n", + "evalCp = sp.lambdify((xA, yA, xB, yB, xC, yC), Cp, 'numpy')\n", + "Cpv = evalCp(xA_, yA_, xB_, yB_, xC_, yC_)\n", + "\n", + "nonzero = np.abs(Cpv) > 0\n", + "print(f\"Enonce piege evalue sur les memes {N} figures :\")\n", + "print(f\" figures qui le REFUTENT (C' != 0) : {nonzero.sum():5d} / {N}\")\n", + "print(f\" figures qui le 'valident' (C' = 0) : {(~nonzero).sum():5d} / {N}\")\n", + "print(f\" max |C'| = {np.abs(Cpv).max():.0f}\")\n", + "\n", + "# Que vaut exactement C' sur une figure qui satisfait l'hypothese ?\n", + "AC2 = (xC - xA)**2 + (yC - yA)**2\n", + "print(\"Identite exacte C' + AC^2 - H = 0 ?\", sp.expand(Cp + AC2 - H) == 0)" + ] + }, + { + "cell_type": "markdown", + "id": "f28dd6f9", + "metadata": {}, + "source": [ + "**Lecture du résultat.** L'énoncé piège est rejeté sur **toutes** les figures : le test **discrimine**, il n'est pas un moulin à « oui ». Et le rejet est catégorique, pas statistique : la dernière ligne le montre, l'identité exacte $C' = H - AC^2$ vaut pour *toute* figure — donc $C' = -AC^2$ sur les figures rectangle en $A$, strictement négatif dès que $C \n", + "eq A$.\n", + "\n", + "Le test numérique distingue donc déjà trois régimes : **toujours vrai** (le fil rouge), **toujours faux** (le piège ci-dessus), et — l'exercice 2 en fabriquera un — **parfois vrai** : un énoncé qui ne tient que sur une sous-famille de figures. Cette catégorie intermédiaire, la plus sournoise pour un test numérique, est exactement celle que l'algèbre du notebook 02 traitera proprement, via les **conditions de non-dégénérescence**." + ] + }, + { + "cell_type": "markdown", + "id": "0e07054c", + "metadata": {}, + "source": [ + "## 5. Pourquoi ce n'est pas encore une preuve\n", + "\n", + "L'objection logique au test numérique tient en un fait d'algèbre élémentaire :\n", + "\n", + "> **Un polynôme non nul peut s'annuler en certains points.**\n", + "\n", + "$\\;q(x, y) = x^2 + y^2 - 25$ n'est pas le polynôme nul, pourtant $q(3, 4) = 0$ et $q(0, 5) = 0$ — tous les points du cercle de rayon 5 l'annulent. Réciproquement, si l'on teste $q$ **uniquement sur des points du cercle**, on conclura à tort « $q \\equiv 0$ ».\n", + "\n", + "Appliqué à notre théorème : nos 10 000 figures sont peut-être, sans qu'on le sache, l'équivalent du cercle — un ensemble de points soigneusement choisi sur lequel la conclusion s'annule *par accident*, alors qu'elle échoue ailleurs. La construction de la section 3 (rotation d'un quart de tour) paraît innocente ; **paraît** ne suffit pas en mathématiques. Fabriquons le piège explicitement, pour le voir de nos yeux :" + ] + }, + { + "cell_type": "code", + "execution_count": 6, + "id": "958a59ba", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-23T16:15:57.645842Z", + "iopub.status.busy": "2026-09-23T16:15:57.645689Z", + "iopub.status.idle": "2026-09-23T16:15:57.650738Z", + "shell.execute_reply": "2026-09-23T16:15:57.650235Z" + } + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "q evalue sur des points DU cercle de rayon 5 : [0, 0, 0, 0, 0, 0, 0]\n", + "-> tirage biaise : on croirait q == 0 partout\n", + "q evalue sur des points QUELCONQUES : [-23, -21, 175, -25]\n", + "-> le meme polynome, evalue ailleurs, n'est plus nul\n" + ] + } + ], + "source": [ + "# Le piege, joue en pleine lumiere : tester q(x, y) = x^2 + y^2 - 25\n", + "# uniquement sur le cercle de rayon 5 (points entiers de Pythagore).\n", + "q = sp.Lambda((xA, yA), xA**2 + yA**2 - 25)\n", + "\n", + "pythagorean = [(3, 4), (4, 3), (0, 5), (5, 0), (-3, 4), (-4, -3), (3, -4)]\n", + "vals_on_circle = [q(*p) for p in pythagorean]\n", + "print(\"q evalue sur des points DU cercle de rayon 5 :\", vals_on_circle)\n", + "print(\"-> tirage biaise : on croirait q == 0 partout\")\n", + "\n", + "vals_elsewhere = [q(1, 1), q(2, 0), q(10, 10), q(0, 0)]\n", + "print(\"q evalue sur des points QUELCONQUES :\", vals_elsewhere)\n", + "print(\"-> le meme polynome, evalue ailleurs, n'est plus nul\")" + ] + }, + { + "cell_type": "markdown", + "id": "650ca2cf", + "metadata": {}, + "source": [ + "**Ce que démontre le piège.** La validité du test numérique dépend entièrement du **mode de tirage** des figures. Tirer « au hasard dans une grande grille » est une parade — mais elle appelle deux questions :\n", + "\n", + "1. quelle est la probabilité qu'un polynôme non nul s'annule sur un point *réellement aléatoire* ?\n", + "2. peut-on la **majorer**, sans connaître le polynôme d'avance ?\n", + "\n", + "La réponse à ces deux questions est un théorème célèbre, et c'est lui qui sauve l'honneur du test numérique." + ] + }, + { + "cell_type": "markdown", + "id": "92afe335", + "metadata": {}, + "source": [ + "## 6. Schwartz–Zippel : le test devient preuve probabiliste\n", + "\n", + "> **Lemme (Schwartz–Zippel, 1980).** Soit $P \\neq 0$ un polynôme de degré total $d$ en $n$ variables, et $S$ un ensemble fini de nombres. Si on tire chaque variable **indépendamment et uniformément** dans $S$, alors\n", + "> $$\\Pr\\big[\\,P(x_1, \\dots, x_n) = 0\\,\\big] \\;\\le\\; \\frac{d}{|S|}.$$\n", + "\n", + "Autrement dit : un polynôme non nul ne s'annule que rarement sur un point *réellement* aléatoire — au plus $d/|S|$ du temps. Un polynôme de degré 2, testé sur la grille des entiers de $-100$ à $100$ ($|S| = 201$), a moins de $1\\ \\%$ de chance de faux zéro par tirage.\n", + "\n", + "Vérifions le lemme **empiriquement** sur un polynôme non nul de degré 2, en comptant le taux d'annulation exact sur des grilles entières de tailles croissantes :" + ] + }, + { + "cell_type": "code", + "execution_count": 7, + "id": "e276cd42", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-23T16:15:57.652626Z", + "iopub.status.busy": "2026-09-23T16:15:57.652437Z", + "iopub.status.idle": "2026-09-23T16:15:57.656082Z", + "shell.execute_reply": "2026-09-23T16:15:57.655691Z" + } + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + " grille | taux de zeros mesure | borne S-Z d/|S|\n", + "--------------------------------------------------------------\n", + " [-2, 2] | 0.3600 | 0.4000\n", + " [-5, 5] | 0.1736 | 0.1818\n", + " [-10, 10] | 0.0930 | 0.0952\n", + " [-50, 50] | 0.0197 | 0.0198\n" + ] + } + ], + "source": [ + "# Mesure du taux d'annulation d'un polynome non nul de degre 2 sur des grilles entieres.\n", + "# Polynome temoin : P(u, v) = u*v + u^2 (non nul, degre total 2).\n", + "def zero_rate_on_grid(half_span):\n", + " span = np.arange(-half_span, half_span + 1)\n", + " U, V = np.meshgrid(span, span)\n", + " vals = U * V + U**2\n", + " return (vals == 0).mean(), span.size\n", + "\n", + "print(f\"{'grille':>16} | {'taux de zeros mesure':>20} | {'borne S-Z d/|S|':>16}\")\n", + "print(\"-\" * 62)\n", + "for half_span in (2, 5, 10, 50):\n", + " rate, size = zero_rate_on_grid(half_span)\n", + " print(f\"{f'[-{half_span}, {half_span}]':>16} | {rate:>20.4f} | {2 / size:>16.4f}\")" + ] + }, + { + "cell_type": "markdown", + "id": "ae32dcc5", + "metadata": {}, + "source": [ + "**Lecture du résultat.** Sur chaque grille, le taux de zéros mesuré reste **sous la borne** $d/|S| = 2/|S|$, et décroît comme $1/|S|$ quand la grille grandit. Le lemme n'est pas une abstraction : c'est une propriété mesurable de nos polynômes.\n", + "\n", + "Appliquons-le au fil rouge. La conclusion non triviale $C_1$ est de degré 2. Le protocole probabiliste devient :\n", + "\n", + "1. tirer les six coordonnées **uniformément et indépendamment** dans une grande grille d'entiers ($|S| = 201$, disons) ;\n", + "2. si une figure satisfait l'hypothèse ($H = 0$) mais pas la conclusion ($C_1 \n", + "eq 0$), le théorème est **réfuté** — et ce réfutation est un certificat *certain* : exhiber un seul contre-exemple suffit ;\n", + "3. si aucune figure testée ne réfute, deux explications restent possibles : le théorème est vrai... ou tous nos tirages sont tombés dans les zéros accidentels d'une conclusion non nulle ;\n", + "4. Schwartz–Zippel borne la seconde explication : par tirage, au plus $d/|S| = 2/201 \\approx 1\\,\\%$ — et cette borne se **compose** sur des tirages independants." + ] + }, + { + "cell_type": "code", + "execution_count": 8, + "id": "569dbd6d", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-23T16:15:57.657687Z", + "iopub.status.busy": "2026-09-23T16:15:57.657564Z", + "iopub.status.idle": "2026-09-23T16:15:57.660415Z", + "shell.execute_reply": "2026-09-23T16:15:57.660036Z" + } + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + " 1 tirages independants : Pr[faux accord] <= 9.95e-03\n", + " 10 tirages independants : Pr[faux accord] <= 9.51e-21\n", + "100 tirages independants : Pr[faux accord] <= 6.07e-201\n" + ] + } + ], + "source": [ + "# Puissance du protocole : la probabilite de faux accord decroit exponentiellement\n", + "# avec le nombre de tirages independants.\n", + "for n_draws in (1, 10, 100):\n", + " p_false = (2 / 201) ** n_draws\n", + " print(f\"{n_draws:>3} tirages independants : Pr[faux accord] <= {p_false:.2e}\")" + ] + }, + { + "cell_type": "markdown", + "id": "7e7c7485", + "metadata": {}, + "source": [ + "**Lecture du résultat.** En 100 tirages indépendants, la probabilité qu'un théorème *faux* survive au test descend sous $10^{-200}$ — une certitude pratique plus forte que bien des vérifications humaines. C'est le principe des **tests d'identité polynomiale** (PIT), pilier de l'algorithmique moderne (fingerprinting, vérification de calculs, preuves PCP).\n", + "\n", + "Mais notons bien la **limite** : cette probabilité est majorée *si le polynôme testé est non nul*. Elle ne dit rien quand le polynôme est *réellement* nul — et surtout, elle **ne remplace pas** l'énoncé « pour toute figure » : un adversaire qui connaît notre générateur peut construire un énoncé faux qui s'annule sur toute notre grille. La certitude absolue exige l'algèbre exacte." + ] + }, + { + "cell_type": "markdown", + "id": "c2ba1c77", + "metadata": {}, + "source": [ + "## 7. Ce que le Geometry-02 ajoutera : la certitude\n", + "\n", + "Le test numérique répond « pas de contre-exemple trouvé ». La question mathématique est plus forte :\n", + "\n", + "> La conclusion est-elle **consignée dans les hypothèses** — au sens où $C_1$ et $C_2$ s'annulent forcément dès que $H$ s'annule (et la figure n'est pas dégénérée) ?\n", + "\n", + "C'est une question d'**algèbre des polynômes** : la conclusion doit appartenir à l'idéal engendré par les hypothèses — notion que le Geometry-02 (*Prouver par l'algèbre*) construira pas à pas, avant d'invoquer son outil natif, la **base de Gröbner** de `sympy`. Cette appartenance, elle, se décide **exactement**, sans probabilité :\n", + "\n", + "| Question | Test numérique (01) | Algèbre exacte (02, 03) |\n", + "|---|---|---|\n", + "| Le théorème est-il réfuté par une figure ? | oui — certificat certain | n/a (le cas est réglé) |\n", + "| Le théorème vaut-il sur *toutes* les figures ? | non — au mieux probabiliste | **oui ou non, certain** |\n", + "| Sur quelles figures dégénérées échoue-t-il ? | au hasard des tirages | **listées explicitement** (non-dégénérescences) |\n", + "\n", + "La série poursuit : le 03 reprendra le même théorème par la **méthode de Wu** — une autre algèbre exacte, plus proche de ce que les systèmes géométriques automatisés utilisent réellement — et le 05 posera la question du pont vers les preuves **formelles** Lean : que garantit exactement « prouvé par Gröbner » ?" + ] + }, + { + "cell_type": "markdown", + "id": "25ccdb74", + "metadata": {}, + "source": [ + "## 8. Exercices\n", + "\n", + "Trois exercices pour vous approprier la machinerie. Les cellules sont des **stubs non bloquants** : le notebook s'exécute de bout en bout même non complété (les vôtres, une fois remplis, doivent s'exécuter sans erreur)." + ] + }, + { + "cell_type": "markdown", + "id": "08e56334", + "metadata": {}, + "source": [ + "### Exercice 1 — Pythagore par la même méthode\n", + "\n", + "Le théorème de Pythagore est un autre habitué des triangles rectangles. Traduisez-le en polynôme et testez-le sur les figures de la section 3 :\n", + "\n", + "> **Énoncé.** Dans un triangle rectangle en $A$ : $AB^2 + AC^2 = BC^2$.\n", + "\n", + "**Étapes suggérées.**\n", + "1. Écrire le polynôme $P \\equiv AB^2 + AC^2 - BC^2$ avec `sympy` (aucun besoin du milieu).\n", + "2. L'évaluer sur les tirages `xA_, yA_, xB_, yB_, xC_, yC_` de la section 3 avec `lambdify`.\n", + "3. Vérifier que `max |P|` est nul au flottant près, et interpréter : ce test *confirme* Pythagore sur 10 000 figures." + ] + }, + { + "cell_type": "code", + "execution_count": 9, + "id": "70edc264", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-23T16:15:57.662005Z", + "iopub.status.busy": "2026-09-23T16:15:57.661851Z", + "iopub.status.idle": "2026-09-23T16:15:57.664065Z", + "shell.execute_reply": "2026-09-23T16:15:57.663583Z" + } + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Exercice a completer\n" + ] + } + ], + "source": [ + "# Exercice 1 : Pythagore comme identite polynomiale sur les memes figures\n", + "# TODO etudiant : definir P = AB^2 + AC^2 - BC^2 avec sympy, puis l'evaluer sur les tirages.\n", + "# Indice : AB2 = (xB - xA)**2 + (yB - yA)**2 ; reutiliser le pattern lambdify de la section 3.\n", + "print(\"Exercice a completer\")" + ] + }, + { + "cell_type": "markdown", + "id": "b812cf26", + "metadata": {}, + "source": [ + "### Exercice 2 — Un énoncé « parfois vrai »\n", + "\n", + "La section 4 a laissé entrevoir des énoncés ni toujours ni jamais vrais. Étudiez-en un proprement :\n", + "\n", + "> **Énoncé.** Dans un triangle $ABC$ rectangle en $A$, le milieu $M$ de $[BC]$ est équidistant du milieu $M'$ de $[AB]$ et du milieu $M''$ de $[AC]$.\n", + "\n", + "**Étapes suggérées.**\n", + "1. Écrire le polynôme $Q \\equiv MM'^2 - MM''^2$ en substituant les trois milieux (une ligne par milieu, comme en section 2).\n", + "2. L'évaluer sur les tirages ; compter la fraction de figures où $Q = 0$ exactement (coordonnées entières).\n", + "3. Caractériser quelques figures qui « valident » : que partagent-elles ? (Piste : comparer les longueurs $AB$ et $AC$ ; la fraction attendue avoisine 5 % — réfléchissez à pourquoi ce chiffre, et pas un autre.)" + ] + }, + { + "cell_type": "code", + "execution_count": 10, + "id": "64938675", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-23T16:15:57.665387Z", + "iopub.status.busy": "2026-09-23T16:15:57.665240Z", + "iopub.status.idle": "2026-09-23T16:15:57.667686Z", + "shell.execute_reply": "2026-09-23T16:15:57.667144Z" + } + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Exercice a completer\n" + ] + } + ], + "source": [ + "# Exercice 2 : taux de validation d'un enonce parfois vrai\n", + "# TODO etudiant : construire Q = MM'^2 - MM''^2 (trois milieux substitues), l'evaluer,\n", + "# compter la fraction de figures ou Q == 0 exactement.\n", + "# Indice : comparer |AB| et |AC| sur les figures validantes ; afficher 2-3 de ces figures.\n", + "print(\"Exercice a completer\")" + ] + }, + { + "cell_type": "markdown", + "id": "32d65f3f", + "metadata": {}, + "source": [ + "### Exercice 3 — Schwartz–Zippel sous contrainte\n", + "\n", + "La borne du lemme suppose un tirage **uniforme**. Que se passe-t-il quand on la viole ?\n", + "\n", + "**Étapes suggérées.**\n", + "1. Pour $q(x, y) = x^2 + y^2 - 25$, mesurer le taux de zéros sur la grille entière $[-10, 10]^2$ — il doit rester sous la borne $2/21$.\n", + "2. Mesurer de nouveau, mais en ne tirant **que des points du cercle** : les triplets pythagoriciens $(3,4)$, $(4,3)$, $(0,5)$, $(5,0)$ et leurs signes suffisent.\n", + "3. Comparer les deux taux et conclure : que devient la borne quand le tirage n'est plus uniforme ? Relisez la section 5 : c'est exactement le biais qui séparait le test numérique d'une preuve." + ] + }, + { + "cell_type": "code", + "execution_count": 11, + "id": "6b8c1a5a", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-23T16:15:57.671431Z", + "iopub.status.busy": "2026-09-23T16:15:57.671156Z", + "iopub.status.idle": "2026-09-23T16:15:57.674115Z", + "shell.execute_reply": "2026-09-23T16:15:57.673489Z" + } + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Exercice a completer\n" + ] + } + ], + "source": [ + "# Exercice 3 : taux d'annulation uniforme vs biaise pour q = x^2 + y^2 - 25\n", + "# TODO etudiant : deux taux a mesurer, un comparatif a ecrire.\n", + "# Indice : grille -> np.meshgrid(np.arange(-10, 11), ...) ; cercle -> liste explicite de triplets.\n", + "print(\"Exercice a completer\")" + ] + }, + { + "cell_type": "markdown", + "id": "c05e5ba5", + "metadata": {}, + "source": [ + "## Ce qu'il faut retenir\n", + "\n", + "- **Traduction** : hypothèse et conclusion d'un théorème de géométrie s'écrivent comme des **polynômes** sur les coordonnées — ici trois polynômes de degré 2 pour le fil rouge.\n", + "- **Test numérique** : sur 10 000 figures construites, la conclusion tient au flottant près ; la même machinerie **rejette** un énoncé piège — elle discrimine.\n", + "- **Limite** : un polynôme non nul s'annule sur des points épars ; un tirage biaisé peut donc faire passer un énoncé faux pour une identité (le piège du cercle).\n", + "- **Sauvetage partiel** : Schwartz–Zippel majore la probabilité de faux accord d'un tirage uniforme par $d/|S|$ — le test numérique devient une **preuve probabiliste** à marge explicite, jamais une certitude.\n", + "\n", + "La suite — Geometry-02, *Prouver par l'algèbre* — établira la certitude : l'appartenance de la conclusion à l'idéal des hypothèses, décidée exactement par les bases de Gröbner, avec la liste explicite des conditions de non-dégénérescence." + ] + }, + { + "cell_type": "markdown", + "id": "aa7f8699", + "metadata": {}, + "source": [ + "***\n", + "*Coût d'exécution : ~5 s sur CPU (kernel `python3`, 10 000 tirages vectorisés `numpy`, zéro appel réseau). Reproductibilité : HIGH — le générateur aléatoire est semé (`rng` seed 20260923), toutes les cellules sont déterministes à l'affichage près.*" + ] + } + ], + "metadata": { + "cost": { + "api_provider": "none", + "api_usd_est": 0.0, + "cpu_min": 1, + "external_account": "none", + "free_alternative": "self", + "gpu_min": 0, + "gpu_required": false, + "metadata_written": "2026-09-23", + "network": false, + "notes": "Geometry-01 : traduction figure->polynomes (sympy), test numerique vectorise (numpy), Schwartz-Zippel empirique. CPU-only, deterministe (seed fixe).", + "qcc_tokens_est": 0, + "reduced_pedagogical": null, + "reproducibility": "HIGH", + "validator": "papermill", + "vram_gb": 0, + "vram_tier": "NONE" + }, + "kernelspec": { + "display_name": "Python 3", + "language": "python", + "name": "python3" + }, + "language_info": { + "codemirror_mode": { + "name": "ipython", + "version": 3 + }, + "file_extension": ".py", + "mimetype": "text/x-python", + "name": "python", + "nbconvert_exporter": "python", + "pygments_lexer": "ipython3", + "version": "3.13.15" + } + }, + "nbformat": 4, + "nbformat_minor": 5 +} diff --git a/MyIA.AI.Notebooks/SymbolicAI/Geometry/README.md b/MyIA.AI.Notebooks/SymbolicAI/Geometry/README.md new file mode 100644 index 0000000000..7d22e2a4d1 --- /dev/null +++ b/MyIA.AI.Notebooks/SymbolicAI/Geometry/README.md @@ -0,0 +1,41 @@ +# Série Geometry — la preuve automatique en géométrie, de la figure à la preuve + +La série **Geometry** applique le raisonnement symbolique aux théorèmes de géométrie élémentaire : elle ouvre la question — centrale pour l'IA — de **démontrer automatiquement** un énoncé géométrique, et de savoir *exactement* ce que la démonstration garantit. Là où SMT/Z3 **décide** sous contraintes et Lean **vérifie** des preuves formelles, cette série **traduit la géométrie en algèbre** (hypothèses et conclusion deviennent des polynômes) puis fait parler cette algèbre : test probabiliste, bases de Gröbner, méthode de Wu, et enfin pont vers la preuve formelle. + +Le programme est **gradué** : chaque notebook principal ne suppose que ce qui le précède, un même théorème fil rouge (le milieu de l'hypoténuse équidistant des trois sommets) est traversé par les méthodes successives, et les résultats de recherche restent dans les accrétions `b` — le chemin principal se lit sans ouvrir de lettre. Cadre complet : Epic #17544. + +## Le programme + +| Pos. | Notebook | Public | Contenu | Statut | +|---|---|---|---|---| +| 01 | [Geometry-01-From-Figure-To-Equation.ipynb](Geometry-01-From-Figure-To-Equation.ipynb) | Découverte | De la figure à l'équation : coordonnées, hypothèses et conclusion en polynômes, vérification numérique sur figures aléatoires, pourquoi ce n'est pas une preuve, Schwartz–Zippel et la preuve probabiliste | Livré | +| 02 | Geometry-02 — Prouver par l'algèbre | Licence | Idéal engendré par les hypothèses, appartenance, bases de Gröbner (`sympy.groebner`), conditions de non-dégénérescence | À venir | +| 03 | Geometry-03 — La méthode de Wu | Licence | Pseudo-division, ensemble caractéristique, reste nul ; Wu face à Gröbner sur les théorèmes de 02 (reprise de #17511) | À venir | +| 03b | Geometry-03b — Décomposition de Ritt | Licence | Composantes dégénérées, le papillon, corpus historique de Chou | À venir | +| 04 | Geometry-04 — Raisonner comme un géomètre | Licence | Base de déduction à règles (DD) et raisonnement algébrique (AR), la moitié symbolique d'AlphaGeometry | À venir | +| 04b | Geometry-04b — IMO-AG-30 | Recherche | Wu associé à DD+AR (Sinha et al. 2024), proposeur neuronal | À venir | +| 05 | Geometry-05 — Pont formel | Recherche | Un théorème de 02/03 énoncé et prouvé en Lean/Mathlib : que garantit « prouvé par Gröbner » ? | À venir | + +Les notebooks 01, 02 et 03 forment la **première volée** : ils se mergent ensemble, dans l'ordre — le premier état public de la série est déjà une progression complète. + +## Le fil rouge + +Le **théorème du milieu de l'hypoténuse** traverse 01, 02 et 03 : + +- en 01, on le **vérifie numériquement** sur 10 000 figures, et on mesure ce que cette vérification prouve (preuve probabiliste Schwartz–Zippel) et ne prouve pas ; +- en 02, on le **démontre** : la conclusion appartient à l'idéal des hypothèses, décidée exactement par Gröbner ; +- en 03, on le **redémontre** par la méthode de Wu, avec les conditions de non-dégénérescence explicites. + +Trois regards sur le même objet — on compare des *méthodes*, pas des exemples. + +## Prérequis et coût + +- **Environnement** : Python 3.10+, `sympy` + `numpy` + `matplotlib` (déjà présents dans le venv projet), kernel `python3`. Aucune API payante, aucun GPU, aucun réseau. +- **01** : ~5 s de bout en bout (10 000 tirages vectorisés), générateur semé — reproductibilité HIGH. +- **Publics** : Découverte (01) suppose la géométrie du lycée ; Licence (02–04) suppose 01 et une première familiarité avec l'algèbre linéaire ; Recherche (04b, 05) suppose la série ou une maturité en vérification formelle. + +## Pourquoi une série de plus + +Les systèmes de preuve géométriques automatisés connaissent un regain avec les LLM géométriques : l'étude *Wu's Method can Boost Symbolic AI to Rival Silver Medalists...* (Sinha et al., 2024, arXiv:2404.06405 — PDF archivé dans le gisement commun) montre qu'une méthode symbolique **classique** de 1977 résout encore des problèmes IMO que les moteurs neuronaux seuls ne résolvent pas. Comprendre Gröbner et Wu, c'est comprendre où le symbolique reste indispensable face au neuronal — et le notebook 05 posera la question de ce que ces preuves *garantissent* formellement. Ces résultats vivent dans les accrétions `b` (03b, 04b) : le chemin principal reste un cours progressif. + +Série parente : [SymbolicAI](../README.md) — le cycle complet du raisonnement vérifiable. diff --git a/MyIA.AI.Notebooks/SymbolicAI/README.md b/MyIA.AI.Notebooks/SymbolicAI/README.md index 748ef4fa1c..c07c3c500c 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/README.md +++ b/MyIA.AI.Notebooks/SymbolicAI/README.md @@ -9,16 +9,16 @@ breakdown: Lean=52, SMT=46, Tweety=34, SmartContracts=31, Argument_Analysis=28, maturity: BETA=258, ALPHA=6, DRAFT=4 --> -> **Note sur les comptes.** Le bloc ci-dessus est un marqueur autoritatif : `` est régénéré quotidiennement par la CI (`.github/workflows/catalog-cron.yml`, 03:37 UTC) sur `main` — pour toute vérification courante du nombre de notebooks et de la maturité, **le catalogue fait foi**. La prose pédagogique ci-dessous mentionne des chiffres précis (ex. « 12 notebooks Python », « 8 jumeaux C# ») qui peuvent dériver localement ; la table « Audit Qualité » (§E) au bas de ce fichier et les READMEs de chaque sous-série ([Tweety](Tweety/README.md), [Lean](Lean/README.md), [SemanticWeb](SemanticWeb/README.md), [Planners](Planners/README.md), [SmartContracts](SmartContracts/README.md), [Argument_Analysis](Argument_Analysis/README.md), [SymbolicLearning](SymbolicLearning/README.md)) sont les sources canoniques pour les détails de chaque sous-série. +> **Note sur les comptes.** Le bloc ci-dessus est un marqueur autoritatif : `` est régénéré quotidiennement par la CI (`.github/workflows/catalog-cron.yml`, 03:37 UTC) sur `main` — pour toute vérification courante du nombre de notebooks et de la maturité, **le catalogue fait foi**. La prose pédagogique ci-dessous mentionne des chiffres précis (ex. « 12 notebooks Python », « 8 jumeaux C# ») qui peuvent dériver localement ; la table « Audit Qualité » (§E) au bas de ce fichier et les READMEs de chaque sous-série ([Tweety](Tweety/README.md), [Lean](Lean/README.md), [SemanticWeb](SemanticWeb/README.md), [Planners](Planners/README.md), [SmartContracts](SmartContracts/README.md), [Argument_Analysis](Argument_Analysis/README.md), [SymbolicLearning](SymbolicLearning/README.md), [Geometry](Geometry/README.md)) sont les sources canoniques pour les détails de chaque sous-série. L'intelligence artificielle n'est pas qu'apprentissage automatique et réseaux de neurones. Une grande partie de l'IA classique repose sur le **raisonnement symbolique** : représenter la connaissance sous forme de propositions, de règles et de structures logiques, puis dériver mécaniquement de nouvelles conclusions. C'est cette tradition — des systèmes experts des années 80 aux assistants de preuve modernes comme Lean 4 — que cette série explore en profondeur. -Vous y découvrirez huit domaines complémentaires qui, ensemble, couvrent le **cycle complet du raisonnement vérifiable** à l'ère des LLMs : **représenter** la connaissance (Tweety pour les logiques formelles et l'argumentation, SemanticWeb pour le web de données RDF/SPARQL/OWL), **prouver** quand la certitude est exigée (Lean 4 et le vérificateur de preuves Mathlib4 — y compris les théorèmes phares 2026 : Sendov, *Analysis I* Tao, PFR, MIMO, M₂₃), **décider sous contraintes** (SMT / Z3, le solveur industriel de référence, en API impérative Python et en binding déclaratif C# via Z3.Linq), **agir dans le monde réel** (Planners pour la planification PDDL/CP-SAT, SmartContracts pour la logique vérifiable sur blockchain), **apprendre à partir de connaissances** plutôt que de données (SymbolicLearning, AIMA ch. 19), et **relier ce pipeline aux LLMs** (Argument Analysis, jette un pont exploitable entre sémantique formelle et IA générative). Chaque sous-série est autonome et peut être suivie isolément, mais elles sont traversées par un **fil rouge** : du formalisme pur à la vérification certifiée, jusqu'au moment où le symbolique et le neuronal cessent d'être deux camps et deviennent deux couches d'un même système fiable. La carte mermaid ci-dessous matérialise les ponts entre ces domaines — nœuds colorés selon leur rôle (fondations, applications, ponts neuro-symboliques). +Vous y découvrirez neuf domaines complémentaires qui, ensemble, couvrent le **cycle complet du raisonnement vérifiable** à l'ère des LLMs : **représenter** la connaissance (Tweety pour les logiques formelles et l'argumentation, SemanticWeb pour le web de données RDF/SPARQL/OWL), **prouver** quand la certitude est exigée (Lean 4 et le vérificateur de preuves Mathlib4 — y compris les théorèmes phares 2026 : Sendov, *Analysis I* Tao, PFR, MIMO, M₂₃), **décider sous contraintes** (SMT / Z3, le solveur industriel de référence, en API impérative Python et en binding déclaratif C# via Z3.Linq), **démontrer automatiquement** en géométrie (Geometry : de la vérification numérique probabiliste aux bases de Gröbner et à la méthode de Wu, jusqu'au pont formel vers Lean), **agir dans le monde réel** (Planners pour la planification PDDL/CP-SAT, SmartContracts pour la logique vérifiable sur blockchain), **apprendre à partir de connaissances** plutôt que de données (SymbolicLearning, AIMA ch. 19), et **relier ce pipeline aux LLMs** (Argument Analysis, jette un pont exploitable entre sémantique formelle et IA générative). Chaque sous-série est autonome et peut être suivie isolément, mais elles sont traversées par un **fil rouge** : du formalisme pur à la vérification certifiée, jusqu'au moment où le symbolique et le neuronal cessent d'être deux camps et deviennent deux couches d'un même système fiable. La carte mermaid ci-dessous matérialise les ponts entre ces domaines — nœuds colorés selon leur rôle (fondations, applications, ponts neuro-symboliques). -**Carte de la famille** — les huit sous-séries et leurs ponts (formalismes fondamentaux → applications → ponts neuro-symboliques). Lecture de la carte : les **flèches pleines** (`-->`) marquent un pont conceptuel direct (la sous-série aval **consomme** ou **généralise** l'amont) ; les **flèches pointillées** (`-.->`) marquent un pont par **companion** (un notebook natif dans une autre série qui formalise la théorie). Trois classes visuelles séparent les rôles : +**Carte de la famille** — les neuf sous-séries et leurs ponts (formalismes fondamentaux → applications → ponts neuro-symboliques). Lecture de la carte : les **flèches pleines** (`-->`) marquent un pont conceptuel direct (la sous-série aval **consomme** ou **généralise** l'amont) ; les **flèches pointillées** (`-.->`) marquent un pont par **companion** (un notebook natif dans une autre série qui formalise la théorie). Trois classes visuelles séparent les rôles : - **Fondations** (bleu) : les formalismes de base du raisonnement symbolique — Tweety, SemanticWeb, Lean. -- **Applications** (vert) : les séries qui **exploitent** les formalismes dans le monde réel — SMT, Planners, SmartContracts. +- **Applications** (vert) : les séries qui **exploitent** les formalismes dans le monde réel — SMT, Planners, SmartContracts, Geometry. - **Ponts neuro-symboliques** (ambre) : les séries qui **relient** le symbolique au génératif — Argument Analysis, SymbolicLearning. ```mermaid @@ -31,6 +31,7 @@ flowchart TD SC["SmartContracts
Blockchain + crypto
(Solidity, DeFi, ZK)"] AA["Argument Analysis
Pont LLM (sophismes, SK)"] SL["SymbolicLearning
Apprentissage symbolique (AIMA 19)"] + GEO["Geometry
Preuve automatique
(polynomes, Groebner, Wu)"] %% Ponts conceptuels (flesches pleines = consommation / généralisation) TW -->|"generalise en representation"| SW @@ -45,13 +46,14 @@ flowchart TD LEAN -.->|"planning_lean (h-add)"| PL LEAN -.->|"sensitivity_lean (Huang 2019)"| SC TW -.->|"induction logique (FOIL)"| SL + GEO -.->|"pont formel (Geometry-05)"| LEAN %% color: explicite -- sans lui, libelle clair sur fond clair en mode sombre GitHub (#15022) ; ton parfois plus fonce que le stroke (le stroke en couleur de texte rendrait infer illisible) : ne pas harmoniser classDef found fill:#e8f0fe,stroke:#1a73e8,color:#174ea6 classDef app fill:#e6f4ea,stroke:#188038,color:#137333 classDef bridge fill:#fef7e0,stroke:#f9ab00,color:#856404 class TW,SW,LEAN found - class SMT,PL,SC app + class SMT,PL,SC,GEO app class AA,SL bridge ``` @@ -85,6 +87,10 @@ Si vous vous intéressez au croisement IA symbolique / IA neuronale, la série A La série SymbolicLearning (21 notebooks : 12 Python + 8 jumeaux C# from-scratch BCL-only + 1 companion natif Lean SL-1b) suit le chapitre 19 d'AIMA : induction pure (Version Space), apprentissage guidé par la connaissance (EBL, RBL), programmation logique inductive (FOIL, résolution inverse, Progol), apprentissage actif d'automates (L* d'Angluin), puis intégration neuro-symbolique jusqu'à un capstone LLM + knowledge graph. Elle ne requiert que Python standard pour l'essentiel et peut être suivie indépendamment des autres phases. +### Parcours alternatif : Preuve automatique en géométrie (Geometry, en ouverture) + +La série Geometry (programme gradué, Epic #17544) ouvre la **démonstration automatique** de théorèmes géométriques : le fil rouge (milieu de l'hypoténuse équidistant des trois sommets) est d'abord vérifié numériquement (Schwartz–Zippel), puis démontré exactement par bases de Gröbner, puis par la méthode de Wu — avant un pont vers Lean. Le notebook d'entrée [Geometry-01](Geometry/Geometry-01-From-Figure-To-Equation.ipynb) (public Découverte, ~30 min) ne suppose que la géométrie du lycée et Python de base. + --- ## Quick Start @@ -100,6 +106,7 @@ La série SymbolicLearning (21 notebooks : 12 Python + 8 jumeaux C# from-scratch | **SmartContracts** | `SmartContracts/00-Foundations/SC-0-Cypherpunk-Origins.ipynb` | `pip install py-solc-x web3` | | **SymbolicLearning** | `SymbolicLearning/SL-1-LogicalLearning.ipynb` | Python 3.10+ standard library, aucune installation | | **Argument Analysis** | `Argument_Analysis/Argument_Analysis_Agentic-0-init.ipynb` | `pip install semantic-kernel jpype1` + `.env` | +| **Geometry** | `Geometry/Geometry-01-From-Figure-To-Equation.ipynb` | `pip install sympy numpy matplotlib` (venv projet déjà configuré) | | **SMT / Z3** | `SMT/Z3-API/Z3-01-Introduction-Python.ipynb` (Python) ou `SMT/Z3-Linq2Z3/01_Linq2Z3_Intro.ipynb` (C#) | `pip install z3-solver` (Python) ; pour C# `dotnet add package Z3.Linq` | **Pour commencer sans rien installer** : les notebooks Python (Tweety, Planners, SemanticWeb Python, SmartContracts) ne nécessitent que `pip install jupyter ipykernel` + les packages listes ci-dessus. @@ -491,6 +498,22 @@ Documentation complète : [SymbolicLearning/README.md](SymbolicLearning/README.m --- +## Geometry - Preuve Automatique en Géométrie + +Série en ouverture (Epic #17544, première volée 01-02-03 en cours de livraison) : la **démonstration automatique** de théorèmes de géométrie élémentaire par l'algèbre des polynômes. Un théorème fil rouge — le milieu de l'hypoténuse équidistant des trois sommets — est traversé par des méthodes de plus en plus fortes. + +### Structure détaillée + +| # | Notebook | Contenu | Exercices | Prérequis | +|---|----------|---------|-----------|-----------| +| 01 | [Geometry-01-From-Figure-To-Equation](Geometry/Geometry-01-From-Figure-To-Equation.ipynb) | Hypothèses/conclusion en polynômes, vérification numérique sur 10 000 figures, témoin négatif, Schwartz–Zippel et preuve probabiliste | 3 | Géométrie lycée, Python | + +> Les positions 02 (Gröbner, `sympy.groebner`), 03 (méthode de Wu, reprise de #17511), 03b (décomposition de Ritt), 04/04b (DD+AR, IMO-AG-30) et 05 (pont formel Lean) sont cadrées dans l'Epic #17544 et se livrent par volées — le chemin principal ne suppose jamais un notebook non encore publié. + +Documentation complète : [Geometry/README.md](Geometry/README.md) + +--- + ## Autres Notebooks ### Optimisation et Contraintes (1 notebook) @@ -574,6 +597,10 @@ SymbolicAI/ │ ├── reference/ # Notes AIMA ch. 19 │ └── README.md │ +├── Geometry/ # Preuve automatique en géométrie (série en ouverture, Epic #17544) +│ ├── Geometry-01-From-Figure-To-Equation.ipynb # Découverte : figure -> polynômes, Schwartz-Zippel +│ └── README.md +│ ├── SMT/ # Solveurs SMT (Satisfiability Modulo Theories) — 46 notebooks (cf. marqueur CATALOG-STATUS) │ ├── Z3-Linq2Z3/ # Serie Z3.Linq C# (SMT declaratif via LINQ) (18 notebooks) │ │ ├── 01_Linq2Z3_Intro.ipynb ... 18_Einsteins_Riddle.ipynb @@ -746,10 +773,11 @@ Le setup est entièrement automatisé via `Tweety-01-Setup-Python.ipynb` : | SymbolicLearning (AIMA ch. 19 + SL-12 differentiable logic gates) | 21 | 21 (100%) | 0 | Excellent | | SMT/Z3-Linq2Z3 (C# Linq2Z3) | 18 | 18 (100%) | 0 | Excellent | | SMT/Z3-API (Python + 6 jumeaux C#) | 28 | 28 (100%, 22 Python + 6 C# jumeaux) | 0 | Excellent | +| Geometry (ouverture 23/09, Epic #17544) | 1 | 1 (100%, Geometry-01 avec 3 exercices) | 0 | Série en ouverture | **Total** : le compte courant des notebooks pédagogiques **fait foi dans le bloc `` ci-dessus** (régénéré quotidiennement par `.github/workflows/catalog-cron.yml`) ; en date du 4 septembre 2026 il s'établit à **262** (y compris `root=1` : OR-tools-Stiegler, et le probe IKVM compté dans Tweety=34), hors les 4 fichiers `_archive/` (Fast-Downward-Legacy, 2 précurseurs EML SymbolicLearning, `Tweety.ipynb` legacy). Les notebooks sans exercices sont uniquement : les setups (SC-1-Setup-Foundry), les notebooks de projet (SC-26-Final-Project), la référence historique RDF.Net-Legacy, les deux dérivés Lean sans cellules d'exercice (Lean-16i, Lean-20b), l'artefact `_agent` et le groupe-I2 d'Argument Analysis, et le probe IKVM (non pédagogique). -> **Note (04/09, réconciliation fichier-entier — See #3973)** : décompositions vérifiées sur disque : **Tweety 34** = 14 Python + 18 C# + 1 Lean (Tweety-5b) + 1 probe ; **Lean 49** = 19 preuves natives (3 `lean4` + 16 `lean4-wsl`) + 30 companions Python (25 `python3` + 4 `python3-wsl` + 1 `global-3.13`) ; **SemanticWeb 27** = 13 C# (incl. RDF.Net-Legacy) + 14 Python (SW-14/15 ajoutés après la réconciliation c.1297) ; **Planners 25** = 15 Python + 9 C# jumeaux + 1 Lean (Planners-5b) ; **SmartContracts 31** = 30 Python + 1 `lean4-wsl` (SC-7c) ; **Argument_Analysis 28** = 10 Agentic (7 sources + 3 artefacts `_agent.ipynb`) + 17 analytiques + 1 groupe-I2 ; **SymbolicLearning 21** = 12 Python + 8 C# jumeaux + 1 Lean (SL-1b) ; **SMT 46** = 28 Z3-API (22 Python + 6 C# jumeaux) + 18 Z3-Linq2Z3 ; root = 1. Réconciliation précédente : 15 août 2026 (c.118, total 230). Pour les comptes courants, le marqueur `` fait foi. +> **Note (04/09, réconciliation fichier-entier — See #3973)** : décompositions vérifiées sur disque : **Tweety 34** = 14 Python + 18 C# + 1 Lean (Tweety-5b) + 1 probe ; **Lean 49** = 19 preuves natives (3 `lean4` + 16 `lean4-wsl`) + 30 companions Python (25 `python3` + 4 `python3-wsl` + 1 `global-3.13`) ; **SemanticWeb 27** = 13 C# (incl. RDF.Net-Legacy) + 14 Python (SW-14/15 ajoutés après la réconciliation c.1297) ; **Planners 25** = 15 Python + 9 C# jumeaux + 1 Lean (Planners-5b) ; **SmartContracts 31** = 30 Python + 1 `lean4-wsl` (SC-7c) ; **Argument_Analysis 28** = 10 Agentic (7 sources + 3 artefacts `_agent.ipynb`) + 17 analytiques + 1 groupe-I2 ; **SymbolicLearning 21** = 12 Python + 8 C# jumeaux + 1 Lean (SL-1b) ; **SMT 46** = 28 Z3-API (22 Python + 6 C# jumeaux) + 18 Z3-Linq2Z3 ; root = 1. Réconciliation précédente : 15 août 2026 (c.118, total 230). Ajout 23 septembre 2026 : **Geometry 1** = Geometry-01-From-Figure-To-Equation (série en ouverture, Epic #17544 ; le catalogue la comptera à sa prochaine régénération). Pour les comptes courants, le marqueur `` fait foi. ### Problèmes connus (juillet 2026) From 42a1d4ec6d092db59a06b7e8f1adf8954c2220e7 Mon Sep 17 00:00:00 2001 From: jsboige Date: Wed, 23 Sep 2026 19:11:52 +0200 Subject: [PATCH 2/3] fix(geometry,#17544): Geometry-01 -- protocole Schwartz-Zippel applique aux parametres + cures prose Le protocole "six coordonnees uniformes puis H = 0" ne teste presque rien : mesure ajoutee en sortie -- 56 figures rectangle rencontrees sur 200 000 tirages uniformes (taux 2.80e-04). Le protocole correct substitue la construction parametrique (A origine, B = u, C = k*rot(u)) dans C1 : chaque tirage de (u_1, u_2, k) est une vraie figure, C1 substitue est identiquement nul (sympy : True) et 100/100 tirages rendent 0 -- la borne (2/201)^100 ne s'applique qu'a un polynome NON NUL sur tirage uniforme, et c'est bien ce que le test arbitre. Deux neq repairs (cellules 15 et 21), prose alignee : nullite exacte (entiers) au lieu de "au flottant pres" (x3), "deux polynomes actifs" au lieu de "trois", "a coordonnees entieres" au lieu de "quelconques", coquilles (cette refutation, independants). Re-execution complete : 11/11 cellules code, 0 erreur, exec counts 1-11. Co-Authored-By: Claude Sonnet 5 --- .../Geometry-01-From-Figure-To-Equation.ipynb | 217 ++++++++++-------- 1 file changed, 121 insertions(+), 96 deletions(-) diff --git a/MyIA.AI.Notebooks/SymbolicAI/Geometry/Geometry-01-From-Figure-To-Equation.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Geometry/Geometry-01-From-Figure-To-Equation.ipynb index 2b9188a635..225b26deec 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Geometry/Geometry-01-From-Figure-To-Equation.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Geometry/Geometry-01-From-Figure-To-Equation.ipynb @@ -2,7 +2,7 @@ "cells": [ { "cell_type": "markdown", - "id": "df017e3b", + "id": "6dcc7eb5", "metadata": {}, "source": [ "# Geometry 01 — De la figure à l'équation\n", @@ -23,7 +23,7 @@ }, { "cell_type": "markdown", - "id": "8316482e", + "id": "3d2c68f8", "metadata": {}, "source": [ "## Le fil rouge de la série\n", @@ -43,7 +43,7 @@ }, { "cell_type": "markdown", - "id": "02ac8ca9", + "id": "3f4655d7", "metadata": {}, "source": [ "## 1. Une figure devient des nombres\n", @@ -56,13 +56,13 @@ { "cell_type": "code", "execution_count": 1, - "id": "076c907f", + "id": "39e4b2b6", "metadata": { "execution": { - "iopub.execute_input": "2026-09-23T16:15:56.735969Z", - "iopub.status.busy": "2026-09-23T16:15:56.735696Z", - "iopub.status.idle": "2026-09-23T16:15:57.431324Z", - "shell.execute_reply": "2026-09-23T16:15:57.430626Z" + "iopub.execute_input": "2026-09-23T17:10:24.844348Z", + "iopub.status.busy": "2026-09-23T17:10:24.844115Z", + "iopub.status.idle": "2026-09-23T17:10:25.555778Z", + "shell.execute_reply": "2026-09-23T17:10:25.555213Z" } }, "outputs": [ @@ -85,7 +85,7 @@ }, { "cell_type": "markdown", - "id": "6aa859ca", + "id": "04ea9a31", "metadata": {}, "source": [ "Le triangle $A(0,0)$, $B(4,0)$, $C(0,3)$ est rectangle en $A$ (les côtés $[AB]$ et $[AC]$ suivent les axes). Son hypoténuse est $[BC]$. Construisons $M$, le milieu de $[BC]$, et traçons les trois distances $MA$, $MB$, $MC$ :" @@ -94,13 +94,13 @@ { "cell_type": "code", "execution_count": 2, - "id": "a87f83a4", + "id": "87064c88", "metadata": { "execution": { - "iopub.execute_input": "2026-09-23T16:15:57.435579Z", - "iopub.status.busy": "2026-09-23T16:15:57.435343Z", - "iopub.status.idle": "2026-09-23T16:15:57.530768Z", - "shell.execute_reply": "2026-09-23T16:15:57.530244Z" + "iopub.execute_input": "2026-09-23T17:10:25.559080Z", + "iopub.status.busy": "2026-09-23T17:10:25.558880Z", + "iopub.status.idle": "2026-09-23T17:10:25.659099Z", + "shell.execute_reply": "2026-09-23T17:10:25.658446Z" } }, "outputs": [ @@ -148,10 +148,10 @@ }, { "cell_type": "markdown", - "id": "1d33a02b", + "id": "abf4bb43", "metadata": {}, "source": [ - "Les trois distances affichées coïncident au flottant près : la figure **suggère** fortement le théorème. Mais une figure n'est pas une preuve, pour deux raisons distinctes :\n", + "Les trois distances affichées coïncident : la figure **suggère** fortement le théorème. Mais une figure n'est pas une preuve, pour deux raisons distinctes :\n", "\n", "1. elle peut être **mal tracée** — des erreurs d'arrondi ou un dessin approximatif peuvent faire ressembler un triangle quelconque à un triangle rectangle ;\n", "2. surtout, elle n'est qu'**un seul exemple**. Le théorème parle de *tous* les triangles rectangles, une infinité.\n", @@ -161,7 +161,7 @@ }, { "cell_type": "markdown", - "id": "d51d9141", + "id": "f81d2660", "metadata": {}, "source": [ "## 2. Traduire l'énoncé en polynômes\n", @@ -186,13 +186,13 @@ { "cell_type": "code", "execution_count": 3, - "id": "86e436d5", + "id": "10e57889", "metadata": { "execution": { - "iopub.execute_input": "2026-09-23T16:15:57.537213Z", - "iopub.status.busy": "2026-09-23T16:15:57.537000Z", - "iopub.status.idle": "2026-09-23T16:15:57.571406Z", - "shell.execute_reply": "2026-09-23T16:15:57.570677Z" + "iopub.execute_input": "2026-09-23T17:10:25.664197Z", + "iopub.status.busy": "2026-09-23T17:10:25.663924Z", + "iopub.status.idle": "2026-09-23T17:10:25.701516Z", + "shell.execute_reply": "2026-09-23T17:10:25.700798Z" } }, "outputs": [ @@ -235,7 +235,7 @@ }, { "cell_type": "markdown", - "id": "e8935dba", + "id": "436bd93a", "metadata": {}, "source": [ "L'énoncé géométrique est devenu **deux polynômes actifs** en six variables — et le sympy vient de nous apprendre quelque chose :\n", @@ -253,24 +253,24 @@ }, { "cell_type": "markdown", - "id": "fa98de13", + "id": "b37c8d62", "metadata": {}, "source": [ "## 3. La vérification numérique : beaucoup de figures, un test\n", "\n", - "Plutôt qu'une figure, tirons-en dix mille. Pour être sûr de fabriquer des triangles rectangles, on ne tire pas $A$, $B$, $C$ au hasard et on ne vérifie pas l'angle après coup : on **construit** l'angle droit. Choisissons $A$ et une direction $u$ quelconques, posons $B = A + u$, puis $C = A + v$ où $v$ est $u$ tourné d'un quart de tour **puis allongé d'un facteur entier $k$ indépendant** — sans ce facteur, tous nos triangles seraient isocèles, une famille bien trop pauvre pour tester un théorème général. L'hypothèse $H = 0$ vaut alors **par construction** — sur des coordonnées entières, exactement." + "Plutôt qu'une figure, tirons-en dix mille. Pour être sûr de fabriquer des triangles rectangles, on ne tire pas $A$, $B$, $C$ au hasard et on ne vérifie pas l'angle après coup : on **construit** l'angle droit. Choisissons $A$ et une direction $u$ à coordonnées entières, posons $B = A + u$, puis $C = A + v$ où $v$ est $u$ tourné d'un quart de tour **puis allongé d'un facteur entier $k$ indépendant** — sans ce facteur, tous nos triangles seraient isocèles, une famille bien trop pauvre pour tester un théorème général. L'hypothèse $H = 0$ vaut alors **par construction** — sur des coordonnées entières, exactement." ] }, { "cell_type": "code", "execution_count": 4, - "id": "034df3db", + "id": "7c09c34d", "metadata": { "execution": { - "iopub.execute_input": "2026-09-23T16:15:57.573218Z", - "iopub.status.busy": "2026-09-23T16:15:57.573050Z", - "iopub.status.idle": "2026-09-23T16:15:57.628802Z", - "shell.execute_reply": "2026-09-23T16:15:57.628291Z" + "iopub.execute_input": "2026-09-23T17:10:25.703208Z", + "iopub.status.busy": "2026-09-23T17:10:25.703086Z", + "iopub.status.idle": "2026-09-23T17:10:25.758474Z", + "shell.execute_reply": "2026-09-23T17:10:25.757960Z" } }, "outputs": [ @@ -290,7 +290,7 @@ "\n", " B - A = u et C - A = v avec v orthogonal a u, mais de longueur INDEPENDANTE\n", " (v = k * rot(u), k entier non nul tire a part) : la famille couvre les triangles\n", - " rectangles quelconques, pas seulement les isoceles.\n", + " rectangles a cotes entiers (AB et AC independants), pas seulement les isoceles.\n", " Renvoie les six coordonnees en six tableaux de forme (n,).\n", " \"\"\"\n", " a = rng.integers(-span, span + 1, size=(n, 2)) # A\n", @@ -324,7 +324,7 @@ }, { "cell_type": "markdown", - "id": "1e8156d0", + "id": "39a56499", "metadata": {}, "source": [ "**Lecture du résultat.** Sur les 10 000 figures, l'hypothèse est exactement satisfaite (coordonnées entières : aucune erreur d'arrondi) et la conclusion non triviale $C_1$ est **exactement nulle**, figure après figure. Le test dit :\n", @@ -336,7 +336,7 @@ }, { "cell_type": "markdown", - "id": "9c229e9a", + "id": "de0f9b6b", "metadata": {}, "source": [ "## 4. Témoin négatif : la machinerie sait aussi dire non\n", @@ -351,13 +351,13 @@ { "cell_type": "code", "execution_count": 5, - "id": "a9eda10d", + "id": "79121359", "metadata": { "execution": { - "iopub.execute_input": "2026-09-23T16:15:57.630668Z", - "iopub.status.busy": "2026-09-23T16:15:57.630527Z", - "iopub.status.idle": "2026-09-23T16:15:57.644095Z", - "shell.execute_reply": "2026-09-23T16:15:57.643227Z" + "iopub.execute_input": "2026-09-23T17:10:25.759943Z", + "iopub.status.busy": "2026-09-23T17:10:25.759798Z", + "iopub.status.idle": "2026-09-23T17:10:25.768853Z", + "shell.execute_reply": "2026-09-23T17:10:25.768389Z" } }, "outputs": [ @@ -394,18 +394,17 @@ }, { "cell_type": "markdown", - "id": "f28dd6f9", + "id": "2d306e8e", "metadata": {}, "source": [ - "**Lecture du résultat.** L'énoncé piège est rejeté sur **toutes** les figures : le test **discrimine**, il n'est pas un moulin à « oui ». Et le rejet est catégorique, pas statistique : la dernière ligne le montre, l'identité exacte $C' = H - AC^2$ vaut pour *toute* figure — donc $C' = -AC^2$ sur les figures rectangle en $A$, strictement négatif dès que $C \n", - "eq A$.\n", + "**Lecture du résultat.** L'énoncé piège est rejeté sur **toutes** les figures : le test **discrimine**, il n'est pas un moulin à « oui ». Et le rejet est catégorique, pas statistique : la dernière ligne le montre, l'identité exacte $C' = H - AC^2$ vaut pour *toute* figure — donc $C' = -AC^2$ sur les figures rectangle en $A$, strictement négatif dès que $C \\neq A$.\n", "\n", "Le test numérique distingue donc déjà trois régimes : **toujours vrai** (le fil rouge), **toujours faux** (le piège ci-dessus), et — l'exercice 2 en fabriquera un — **parfois vrai** : un énoncé qui ne tient que sur une sous-famille de figures. Cette catégorie intermédiaire, la plus sournoise pour un test numérique, est exactement celle que l'algèbre du notebook 02 traitera proprement, via les **conditions de non-dégénérescence**." ] }, { "cell_type": "markdown", - "id": "0e07054c", + "id": "964894f1", "metadata": {}, "source": [ "## 5. Pourquoi ce n'est pas encore une preuve\n", @@ -422,13 +421,13 @@ { "cell_type": "code", "execution_count": 6, - "id": "958a59ba", + "id": "fb227aca", "metadata": { "execution": { - "iopub.execute_input": "2026-09-23T16:15:57.645842Z", - "iopub.status.busy": "2026-09-23T16:15:57.645689Z", - "iopub.status.idle": "2026-09-23T16:15:57.650738Z", - "shell.execute_reply": "2026-09-23T16:15:57.650235Z" + "iopub.execute_input": "2026-09-23T17:10:25.774458Z", + "iopub.status.busy": "2026-09-23T17:10:25.774225Z", + "iopub.status.idle": "2026-09-23T17:10:25.778642Z", + "shell.execute_reply": "2026-09-23T17:10:25.778210Z" } }, "outputs": [ @@ -460,7 +459,7 @@ }, { "cell_type": "markdown", - "id": "650ca2cf", + "id": "d6f604b1", "metadata": {}, "source": [ "**Ce que démontre le piège.** La validité du test numérique dépend entièrement du **mode de tirage** des figures. Tirer « au hasard dans une grande grille » est une parade — mais elle appelle deux questions :\n", @@ -473,7 +472,7 @@ }, { "cell_type": "markdown", - "id": "92afe335", + "id": "cfe06d85", "metadata": {}, "source": [ "## 6. Schwartz–Zippel : le test devient preuve probabiliste\n", @@ -489,13 +488,13 @@ { "cell_type": "code", "execution_count": 7, - "id": "e276cd42", + "id": "08c03761", "metadata": { "execution": { - "iopub.execute_input": "2026-09-23T16:15:57.652626Z", - "iopub.status.busy": "2026-09-23T16:15:57.652437Z", - "iopub.status.idle": "2026-09-23T16:15:57.656082Z", - "shell.execute_reply": "2026-09-23T16:15:57.655691Z" + "iopub.execute_input": "2026-09-23T17:10:25.782252Z", + "iopub.status.busy": "2026-09-23T17:10:25.782072Z", + "iopub.status.idle": "2026-09-23T17:10:25.786138Z", + "shell.execute_reply": "2026-09-23T17:10:25.785654Z" } }, "outputs": [ @@ -530,30 +529,29 @@ }, { "cell_type": "markdown", - "id": "ae32dcc5", + "id": "2ada5ec8", "metadata": {}, "source": [ "**Lecture du résultat.** Sur chaque grille, le taux de zéros mesuré reste **sous la borne** $d/|S| = 2/|S|$, et décroît comme $1/|S|$ quand la grille grandit. Le lemme n'est pas une abstraction : c'est une propriété mesurable de nos polynômes.\n", "\n", - "Appliquons-le au fil rouge. La conclusion non triviale $C_1$ est de degré 2. Le protocole probabiliste devient :\n", + "Appliquons-le au fil rouge — avec une précaution décisive. Tirer les six coordonnées au hasard puis ne garder que les figures rectangle ne teste presque rien : l'hypothèse $H = 0$ est si maigre en points de la grille qu'un tirage uniforme ne la rencontre pratiquement jamais (le taux se mesure en dix-millièmes — la cellule suivante le mesure). La bonne machine est celle de la section 3 : **substituer la construction paramétrique** $A = (0, 0)$, $B = u$, $C = k \\cdot \\mathrm{rot}(u)$ dans la conclusion. L'hypothèse est alors satisfaite *par construction* — chaque tirage de $(u_1, u_2, k)$ est une vraie figure — et $C_1$ devient un polynôme des paramètres, $C_1(u_1, u_2, k)$, de degré au plus 2. Le protocole probabiliste devient :\n", "\n", - "1. tirer les six coordonnées **uniformément et indépendamment** dans une grande grille d'entiers ($|S| = 201$, disons) ;\n", - "2. si une figure satisfait l'hypothèse ($H = 0$) mais pas la conclusion ($C_1 \n", - "eq 0$), le théorème est **réfuté** — et ce réfutation est un certificat *certain* : exhiber un seul contre-exemple suffit ;\n", - "3. si aucune figure testée ne réfute, deux explications restent possibles : le théorème est vrai... ou tous nos tirages sont tombés dans les zéros accidentels d'une conclusion non nulle ;\n", - "4. Schwartz–Zippel borne la seconde explication : par tirage, au plus $d/|S| = 2/201 \\approx 1\\,\\%$ — et cette borne se **compose** sur des tirages independants." + "1. tirer les paramètres $(u_1, u_2, k)$ **uniformément et indépendamment** dans une grande grille d'entiers ($|S| = 201$, disons) ;\n", + "2. si un tirage rend $C_1 \\neq 0$, le théorème est **réfuté** — et cette réfutation est un certificat *certain* : exhiber un seul contre-exemple suffit ;\n", + "3. si tous les tirages rendent $0$, deux explications restent possibles : $C_1(u_1, u_2, k)$ est identiquement nul — le théorème est alors une **identité**, vraie sur toute la famille construite — ou bien tous nos tirages sont tombés dans les zéros accidentels d'un polynôme non nul ;\n", + "4. Schwartz–Zippel borne la seconde explication : pour un polynôme non nul de degré $d$, au plus $d/|S| = 2/201 \\approx 1\\,\\%$ par tirage — et cette borne se **compose** sur des tirages indépendants." ] }, { "cell_type": "code", "execution_count": 8, - "id": "569dbd6d", + "id": "79ea09ad", "metadata": { "execution": { - "iopub.execute_input": "2026-09-23T16:15:57.657687Z", - "iopub.status.busy": "2026-09-23T16:15:57.657564Z", - "iopub.status.idle": "2026-09-23T16:15:57.660415Z", - "shell.execute_reply": "2026-09-23T16:15:57.660036Z" + "iopub.execute_input": "2026-09-23T17:10:25.789902Z", + "iopub.status.busy": "2026-09-23T17:10:25.789733Z", + "iopub.status.idle": "2026-09-23T17:10:25.805619Z", + "shell.execute_reply": "2026-09-23T17:10:25.804879Z" } }, "outputs": [ @@ -561,6 +559,10 @@ "name": "stdout", "output_type": "stream", "text": [ + "figures rectangle rencontrees au hasard : 56 / 200000 (taux 2.80e-04)\n", + "C1 apres substitution des parametres : 0\n", + "C1(u_1, u_2, k) identiquement nul ? True\n", + "tirages de parametres : 100 | rendant C1 = 0 : 100 / 100\n", " 1 tirages independants : Pr[faux accord] <= 9.95e-03\n", " 10 tirages independants : Pr[faux accord] <= 9.51e-21\n", "100 tirages independants : Pr[faux accord] <= 6.07e-201\n" @@ -568,8 +570,31 @@ } ], "source": [ - "# Puissance du protocole : la probabilite de faux accord decroit exponentiellement\n", - "# avec le nombre de tirages independants.\n", + "# Etape 0 : pourquoi ne PAS tirer les six coordonnees puis filtrer H = 0 ?\n", + "# Mesure : taux de figures rectangles rencontrees au hasard dans [-100, 100]^6.\n", + "N_probe = 200_000\n", + "pts = rng.integers(-100, 101, size=(N_probe, 6))\n", + "xA_, yA_, xB_, yB_, xC_, yC_ = pts.T\n", + "H_vals = (xB_ - xA_) * (xC_ - xA_) + (yB_ - yA_) * (yC_ - yA_)\n", + "print(f\"figures rectangle rencontrees au hasard : {int(np.sum(H_vals == 0))} / {N_probe}\"\n", + " f\" (taux {np.mean(H_vals == 0):.2e})\")\n", + "\n", + "# Etape 1 : le protocole correct -- substituer la construction de la section 3\n", + "# (A = origine, B = u, C = k * rot(u) avec rot(x, y) = (-y, x)) dans C1.\n", + "u1, u2, kk = sp.symbols('u_1 u_2 k', integer=True)\n", + "subs_params = {xA: 0, yA: 0, xB: u1, yB: u2, xC: -kk * u2, yC: kk * u1}\n", + "C1_param = sp.expand(C1.subs(subs_params))\n", + "print(\"C1 apres substitution des parametres :\", C1_param)\n", + "print(\"C1(u_1, u_2, k) identiquement nul ?\", C1_param == 0)\n", + "\n", + "# Etape 2 : Schwartz-Zippel au travail -- 100 tirages uniformes de (u_1, u_2, k).\n", + "f_C1p = sp.lambdify((u1, u2, kk), C1_param, 'numpy')\n", + "params = rng.integers(-100, 101, size=(100, 3))\n", + "raw = f_C1p(params[:, 0], params[:, 1], params[:, 2])\n", + "vals = np.broadcast_to(np.asarray(raw, dtype=float), (len(params),))\n", + "print(f\"tirages de parametres : {len(vals)} | rendant C1 = 0 : {int(np.sum(vals == 0))} / {len(vals)}\")\n", + "\n", + "# Etape 3 : la puissance du protocole -- la borne se compose sur les tirages.\n", "for n_draws in (1, 10, 100):\n", " p_false = (2 / 201) ** n_draws\n", " print(f\"{n_draws:>3} tirages independants : Pr[faux accord] <= {p_false:.2e}\")" @@ -577,17 +602,17 @@ }, { "cell_type": "markdown", - "id": "7e7c7485", + "id": "749e1b61", "metadata": {}, "source": [ - "**Lecture du résultat.** En 100 tirages indépendants, la probabilité qu'un théorème *faux* survive au test descend sous $10^{-200}$ — une certitude pratique plus forte que bien des vérifications humaines. C'est le principe des **tests d'identité polynomiale** (PIT), pilier de l'algorithmique moderne (fingerprinting, vérification de calculs, preuves PCP).\n", + "**Lecture du résultat.** La mesure d'abord : sur 200 000 tirages uniformes des six coordonnées, une cinquantaine à peine satisfont l'hypothèse — filtrer $H = 0$ a posteriori n'aurait donc presque rien testé. Avec la substitution, chaque tirage de paramètres est une vraie figure, et les 100 tirages rendent tous $C_1 = 0$. Un polynôme *non nul* de degré 2 n'aurait survécu à 100 tirages uniformes qu'avec probabilité au plus $(2/201)^{100} \\approx 6 \\times 10^{-201}$ : soit nous avons observé l'improbable, soit $C_1(u_1, u_2, k)$ est **identiquement nul** — et sympy tranche : l'identité est exacte. Le test probabiliste et le verdict exact concordent. C'est le principe des **tests d'identité polynomiale** (PIT), pilier de l'algorithmique moderne (fingerprinting, vérification de calculs, preuves PCP).\n", "\n", - "Mais notons bien la **limite** : cette probabilité est majorée *si le polynôme testé est non nul*. Elle ne dit rien quand le polynôme est *réellement* nul — et surtout, elle **ne remplace pas** l'énoncé « pour toute figure » : un adversaire qui connaît notre générateur peut construire un énoncé faux qui s'annule sur toute notre grille. La certitude absolue exige l'algèbre exacte." + "Mais notons bien les **limites** : la borne ne s'applique qu'à un polynôme non nul sur un tirage *réellement* uniforme — un adversaire qui connaît notre générateur peut construire un énoncé faux qui s'annule sur toute notre grille (la section 5 l'a joué en pleine lumière). Et l'identité après substitution est vérifiée **sur la famille construite** ; la question générale — toute figure, y compris les cas dégénérés, avec la liste explicite des non-dégénérescences — reste ouverte. La certitude absolue exige l'algèbre exacte." ] }, { "cell_type": "markdown", - "id": "c2ba1c77", + "id": "02cafb9e", "metadata": {}, "source": [ "## 7. Ce que le Geometry-02 ajoutera : la certitude\n", @@ -609,7 +634,7 @@ }, { "cell_type": "markdown", - "id": "25ccdb74", + "id": "1bae8bd3", "metadata": {}, "source": [ "## 8. Exercices\n", @@ -619,7 +644,7 @@ }, { "cell_type": "markdown", - "id": "08e56334", + "id": "f0564503", "metadata": {}, "source": [ "### Exercice 1 — Pythagore par la même méthode\n", @@ -631,19 +656,19 @@ "**Étapes suggérées.**\n", "1. Écrire le polynôme $P \\equiv AB^2 + AC^2 - BC^2$ avec `sympy` (aucun besoin du milieu).\n", "2. L'évaluer sur les tirages `xA_, yA_, xB_, yB_, xC_, yC_` de la section 3 avec `lambdify`.\n", - "3. Vérifier que `max |P|` est nul au flottant près, et interpréter : ce test *confirme* Pythagore sur 10 000 figures." + "3. Vérifier que `max |P|` est exactement nul (coordonnées entières : aucune erreur d'arrondi), et interpréter : ce test *confirme* Pythagore sur 10 000 figures." ] }, { "cell_type": "code", "execution_count": 9, - "id": "70edc264", + "id": "0be8d8ca", "metadata": { "execution": { - "iopub.execute_input": "2026-09-23T16:15:57.662005Z", - "iopub.status.busy": "2026-09-23T16:15:57.661851Z", - "iopub.status.idle": "2026-09-23T16:15:57.664065Z", - "shell.execute_reply": "2026-09-23T16:15:57.663583Z" + "iopub.execute_input": "2026-09-23T17:10:25.809060Z", + "iopub.status.busy": "2026-09-23T17:10:25.808790Z", + "iopub.status.idle": "2026-09-23T17:10:25.812003Z", + "shell.execute_reply": "2026-09-23T17:10:25.811518Z" } }, "outputs": [ @@ -664,7 +689,7 @@ }, { "cell_type": "markdown", - "id": "b812cf26", + "id": "905ec101", "metadata": {}, "source": [ "### Exercice 2 — Un énoncé « parfois vrai »\n", @@ -682,13 +707,13 @@ { "cell_type": "code", "execution_count": 10, - "id": "64938675", + "id": "dab54d80", "metadata": { "execution": { - "iopub.execute_input": "2026-09-23T16:15:57.665387Z", - "iopub.status.busy": "2026-09-23T16:15:57.665240Z", - "iopub.status.idle": "2026-09-23T16:15:57.667686Z", - "shell.execute_reply": "2026-09-23T16:15:57.667144Z" + "iopub.execute_input": "2026-09-23T17:10:25.815260Z", + "iopub.status.busy": "2026-09-23T17:10:25.815126Z", + "iopub.status.idle": "2026-09-23T17:10:25.817334Z", + "shell.execute_reply": "2026-09-23T17:10:25.816934Z" } }, "outputs": [ @@ -710,7 +735,7 @@ }, { "cell_type": "markdown", - "id": "32d65f3f", + "id": "efa812eb", "metadata": {}, "source": [ "### Exercice 3 — Schwartz–Zippel sous contrainte\n", @@ -726,13 +751,13 @@ { "cell_type": "code", "execution_count": 11, - "id": "6b8c1a5a", + "id": "3f419bda", "metadata": { "execution": { - "iopub.execute_input": "2026-09-23T16:15:57.671431Z", - "iopub.status.busy": "2026-09-23T16:15:57.671156Z", - "iopub.status.idle": "2026-09-23T16:15:57.674115Z", - "shell.execute_reply": "2026-09-23T16:15:57.673489Z" + "iopub.execute_input": "2026-09-23T17:10:25.821317Z", + "iopub.status.busy": "2026-09-23T17:10:25.821119Z", + "iopub.status.idle": "2026-09-23T17:10:25.824489Z", + "shell.execute_reply": "2026-09-23T17:10:25.823951Z" } }, "outputs": [ @@ -753,13 +778,13 @@ }, { "cell_type": "markdown", - "id": "c05e5ba5", + "id": "c6dbd77d", "metadata": {}, "source": [ "## Ce qu'il faut retenir\n", "\n", - "- **Traduction** : hypothèse et conclusion d'un théorème de géométrie s'écrivent comme des **polynômes** sur les coordonnées — ici trois polynômes de degré 2 pour le fil rouge.\n", - "- **Test numérique** : sur 10 000 figures construites, la conclusion tient au flottant près ; la même machinerie **rejette** un énoncé piège — elle discrimine.\n", + "- **Traduction** : hypothèse et conclusion d'un théorème de géométrie s'écrivent comme des **polynômes** sur les coordonnées — ici **deux polynômes actifs** de degré 2 pour le fil rouge (la troisième composante, $MB = MC$, est la médiatrice : identiquement nulle).\n", + "- **Test numérique** : sur 10 000 figures construites, la conclusion tient **exactement** (coordonnées entières : aucune erreur d'arrondi) ; la même machinerie **rejette** un énoncé piège — elle discrimine.\n", "- **Limite** : un polynôme non nul s'annule sur des points épars ; un tirage biaisé peut donc faire passer un énoncé faux pour une identité (le piège du cercle).\n", "- **Sauvetage partiel** : Schwartz–Zippel majore la probabilité de faux accord d'un tirage uniforme par $d/|S|$ — le test numérique devient une **preuve probabiliste** à marge explicite, jamais une certitude.\n", "\n", @@ -768,7 +793,7 @@ }, { "cell_type": "markdown", - "id": "aa7f8699", + "id": "2591a841", "metadata": {}, "source": [ "***\n", From 5eb4d11e570d0320a88858f5264953ec0826af9b Mon Sep 17 00:00:00 2001 From: jsboige Date: Wed, 23 Sep 2026 19:34:01 +0200 Subject: [PATCH 3/3] fix(geometry,#17581): Schwartz-Zippel borne au degre REEL apres substitution (d=4) La construction parametrique rend les coordonnees quadratiques en k (x_C = -k*u_2, y_C = k*u_1) : une conclusion de degre 2 en coordonnees devient de degre <= 4 en (u_1, u_2, k). Bornes 2/201 -> 4/201 (1.99e-02 par tirage, 7.70e-171 pour 100 tirages, mesure en sortie). Re-execution complete 11/11, 0 erreur. Reserve 5799450271. Co-Authored-By: Claude Sonnet 5 --- .../Geometry-01-From-Figure-To-Equation.ipynb | 170 +++++++++--------- 1 file changed, 85 insertions(+), 85 deletions(-) diff --git a/MyIA.AI.Notebooks/SymbolicAI/Geometry/Geometry-01-From-Figure-To-Equation.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Geometry/Geometry-01-From-Figure-To-Equation.ipynb index 225b26deec..cb334578e9 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Geometry/Geometry-01-From-Figure-To-Equation.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Geometry/Geometry-01-From-Figure-To-Equation.ipynb @@ -2,7 +2,7 @@ "cells": [ { "cell_type": "markdown", - "id": "6dcc7eb5", + "id": "c2c21b11", "metadata": {}, "source": [ "# Geometry 01 — De la figure à l'équation\n", @@ -23,7 +23,7 @@ }, { "cell_type": "markdown", - "id": "3d2c68f8", + "id": "c5f54393", "metadata": {}, "source": [ "## Le fil rouge de la série\n", @@ -43,7 +43,7 @@ }, { "cell_type": "markdown", - "id": "3f4655d7", + "id": "3d98fd05", "metadata": {}, "source": [ "## 1. Une figure devient des nombres\n", @@ -56,13 +56,13 @@ { "cell_type": "code", "execution_count": 1, - "id": "39e4b2b6", + "id": "9cdd70ab", "metadata": { "execution": { - "iopub.execute_input": "2026-09-23T17:10:24.844348Z", - "iopub.status.busy": "2026-09-23T17:10:24.844115Z", - "iopub.status.idle": "2026-09-23T17:10:25.555778Z", - "shell.execute_reply": "2026-09-23T17:10:25.555213Z" + "iopub.execute_input": "2026-09-23T17:33:05.611647Z", + "iopub.status.busy": "2026-09-23T17:33:05.611414Z", + "iopub.status.idle": "2026-09-23T17:33:06.276587Z", + "shell.execute_reply": "2026-09-23T17:33:06.276085Z" } }, "outputs": [ @@ -85,7 +85,7 @@ }, { "cell_type": "markdown", - "id": "04ea9a31", + "id": "7e03c1f4", "metadata": {}, "source": [ "Le triangle $A(0,0)$, $B(4,0)$, $C(0,3)$ est rectangle en $A$ (les côtés $[AB]$ et $[AC]$ suivent les axes). Son hypoténuse est $[BC]$. Construisons $M$, le milieu de $[BC]$, et traçons les trois distances $MA$, $MB$, $MC$ :" @@ -94,13 +94,13 @@ { "cell_type": "code", "execution_count": 2, - "id": "87064c88", + "id": "fa41225c", "metadata": { "execution": { - "iopub.execute_input": "2026-09-23T17:10:25.559080Z", - "iopub.status.busy": "2026-09-23T17:10:25.558880Z", - "iopub.status.idle": "2026-09-23T17:10:25.659099Z", - "shell.execute_reply": "2026-09-23T17:10:25.658446Z" + "iopub.execute_input": "2026-09-23T17:33:06.278299Z", + "iopub.status.busy": "2026-09-23T17:33:06.278109Z", + "iopub.status.idle": "2026-09-23T17:33:06.363448Z", + "shell.execute_reply": "2026-09-23T17:33:06.363059Z" } }, "outputs": [ @@ -148,7 +148,7 @@ }, { "cell_type": "markdown", - "id": "abf4bb43", + "id": "7100102b", "metadata": {}, "source": [ "Les trois distances affichées coïncident : la figure **suggère** fortement le théorème. Mais une figure n'est pas une preuve, pour deux raisons distinctes :\n", @@ -161,7 +161,7 @@ }, { "cell_type": "markdown", - "id": "f81d2660", + "id": "4d794257", "metadata": {}, "source": [ "## 2. Traduire l'énoncé en polynômes\n", @@ -186,13 +186,13 @@ { "cell_type": "code", "execution_count": 3, - "id": "10e57889", + "id": "321cf01d", "metadata": { "execution": { - "iopub.execute_input": "2026-09-23T17:10:25.664197Z", - "iopub.status.busy": "2026-09-23T17:10:25.663924Z", - "iopub.status.idle": "2026-09-23T17:10:25.701516Z", - "shell.execute_reply": "2026-09-23T17:10:25.700798Z" + "iopub.execute_input": "2026-09-23T17:33:06.364903Z", + "iopub.status.busy": "2026-09-23T17:33:06.364766Z", + "iopub.status.idle": "2026-09-23T17:33:06.393254Z", + "shell.execute_reply": "2026-09-23T17:33:06.392577Z" } }, "outputs": [ @@ -235,7 +235,7 @@ }, { "cell_type": "markdown", - "id": "436bd93a", + "id": "706aae8f", "metadata": {}, "source": [ "L'énoncé géométrique est devenu **deux polynômes actifs** en six variables — et le sympy vient de nous apprendre quelque chose :\n", @@ -253,7 +253,7 @@ }, { "cell_type": "markdown", - "id": "b37c8d62", + "id": "9984afe2", "metadata": {}, "source": [ "## 3. La vérification numérique : beaucoup de figures, un test\n", @@ -264,13 +264,13 @@ { "cell_type": "code", "execution_count": 4, - "id": "7c09c34d", + "id": "74415a90", "metadata": { "execution": { - "iopub.execute_input": "2026-09-23T17:10:25.703208Z", - "iopub.status.busy": "2026-09-23T17:10:25.703086Z", - "iopub.status.idle": "2026-09-23T17:10:25.758474Z", - "shell.execute_reply": "2026-09-23T17:10:25.757960Z" + "iopub.execute_input": "2026-09-23T17:33:06.394612Z", + "iopub.status.busy": "2026-09-23T17:33:06.394490Z", + "iopub.status.idle": "2026-09-23T17:33:06.446079Z", + "shell.execute_reply": "2026-09-23T17:33:06.445491Z" } }, "outputs": [ @@ -324,7 +324,7 @@ }, { "cell_type": "markdown", - "id": "39a56499", + "id": "6e28e53b", "metadata": {}, "source": [ "**Lecture du résultat.** Sur les 10 000 figures, l'hypothèse est exactement satisfaite (coordonnées entières : aucune erreur d'arrondi) et la conclusion non triviale $C_1$ est **exactement nulle**, figure après figure. Le test dit :\n", @@ -336,7 +336,7 @@ }, { "cell_type": "markdown", - "id": "de0f9b6b", + "id": "f01cd65a", "metadata": {}, "source": [ "## 4. Témoin négatif : la machinerie sait aussi dire non\n", @@ -351,13 +351,13 @@ { "cell_type": "code", "execution_count": 5, - "id": "79121359", + "id": "2aa48fe4", "metadata": { "execution": { - "iopub.execute_input": "2026-09-23T17:10:25.759943Z", - "iopub.status.busy": "2026-09-23T17:10:25.759798Z", - "iopub.status.idle": "2026-09-23T17:10:25.768853Z", - "shell.execute_reply": "2026-09-23T17:10:25.768389Z" + "iopub.execute_input": "2026-09-23T17:33:06.449992Z", + "iopub.status.busy": "2026-09-23T17:33:06.449857Z", + "iopub.status.idle": "2026-09-23T17:33:06.458465Z", + "shell.execute_reply": "2026-09-23T17:33:06.458000Z" } }, "outputs": [ @@ -394,7 +394,7 @@ }, { "cell_type": "markdown", - "id": "2d306e8e", + "id": "6d91e641", "metadata": {}, "source": [ "**Lecture du résultat.** L'énoncé piège est rejeté sur **toutes** les figures : le test **discrimine**, il n'est pas un moulin à « oui ». Et le rejet est catégorique, pas statistique : la dernière ligne le montre, l'identité exacte $C' = H - AC^2$ vaut pour *toute* figure — donc $C' = -AC^2$ sur les figures rectangle en $A$, strictement négatif dès que $C \\neq A$.\n", @@ -404,7 +404,7 @@ }, { "cell_type": "markdown", - "id": "964894f1", + "id": "06fd8e28", "metadata": {}, "source": [ "## 5. Pourquoi ce n'est pas encore une preuve\n", @@ -421,13 +421,13 @@ { "cell_type": "code", "execution_count": 6, - "id": "fb227aca", + "id": "9fb04afb", "metadata": { "execution": { - "iopub.execute_input": "2026-09-23T17:10:25.774458Z", - "iopub.status.busy": "2026-09-23T17:10:25.774225Z", - "iopub.status.idle": "2026-09-23T17:10:25.778642Z", - "shell.execute_reply": "2026-09-23T17:10:25.778210Z" + "iopub.execute_input": "2026-09-23T17:33:06.459984Z", + "iopub.status.busy": "2026-09-23T17:33:06.459829Z", + "iopub.status.idle": "2026-09-23T17:33:06.463958Z", + "shell.execute_reply": "2026-09-23T17:33:06.463344Z" } }, "outputs": [ @@ -459,7 +459,7 @@ }, { "cell_type": "markdown", - "id": "d6f604b1", + "id": "b51a6555", "metadata": {}, "source": [ "**Ce que démontre le piège.** La validité du test numérique dépend entièrement du **mode de tirage** des figures. Tirer « au hasard dans une grande grille » est une parade — mais elle appelle deux questions :\n", @@ -472,7 +472,7 @@ }, { "cell_type": "markdown", - "id": "cfe06d85", + "id": "50004117", "metadata": {}, "source": [ "## 6. Schwartz–Zippel : le test devient preuve probabiliste\n", @@ -488,13 +488,13 @@ { "cell_type": "code", "execution_count": 7, - "id": "08c03761", + "id": "65cb7bcb", "metadata": { "execution": { - "iopub.execute_input": "2026-09-23T17:10:25.782252Z", - "iopub.status.busy": "2026-09-23T17:10:25.782072Z", - "iopub.status.idle": "2026-09-23T17:10:25.786138Z", - "shell.execute_reply": "2026-09-23T17:10:25.785654Z" + "iopub.execute_input": "2026-09-23T17:33:06.465451Z", + "iopub.status.busy": "2026-09-23T17:33:06.465291Z", + "iopub.status.idle": "2026-09-23T17:33:06.468764Z", + "shell.execute_reply": "2026-09-23T17:33:06.468371Z" } }, "outputs": [ @@ -529,29 +529,29 @@ }, { "cell_type": "markdown", - "id": "2ada5ec8", + "id": "d5520e1d", "metadata": {}, "source": [ "**Lecture du résultat.** Sur chaque grille, le taux de zéros mesuré reste **sous la borne** $d/|S| = 2/|S|$, et décroît comme $1/|S|$ quand la grille grandit. Le lemme n'est pas une abstraction : c'est une propriété mesurable de nos polynômes.\n", "\n", - "Appliquons-le au fil rouge — avec une précaution décisive. Tirer les six coordonnées au hasard puis ne garder que les figures rectangle ne teste presque rien : l'hypothèse $H = 0$ est si maigre en points de la grille qu'un tirage uniforme ne la rencontre pratiquement jamais (le taux se mesure en dix-millièmes — la cellule suivante le mesure). La bonne machine est celle de la section 3 : **substituer la construction paramétrique** $A = (0, 0)$, $B = u$, $C = k \\cdot \\mathrm{rot}(u)$ dans la conclusion. L'hypothèse est alors satisfaite *par construction* — chaque tirage de $(u_1, u_2, k)$ est une vraie figure — et $C_1$ devient un polynôme des paramètres, $C_1(u_1, u_2, k)$, de degré au plus 2. Le protocole probabiliste devient :\n", + "Appliquons-le au fil rouge — avec une précaution décisive. Tirer les six coordonnées au hasard puis ne garder que les figures rectangle ne teste presque rien : l'hypothèse $H = 0$ est si maigre en points de la grille qu'un tirage uniforme ne la rencontre pratiquement jamais (le taux se mesure en dix-millièmes — la cellule suivante le mesure). La bonne machine est celle de la section 3 : **substituer la construction paramétrique** $A = (0, 0)$, $B = u$, $C = k \\cdot \\mathrm{rot}(u)$ dans la conclusion. L'hypothèse est alors satisfaite *par construction* — chaque tirage de $(u_1, u_2, k)$ est une vraie figure — et $C_1$ devient un polynôme des paramètres, $C_1(u_1, u_2, k)$, de degré au plus 4 : les coordonnées substituées sont linéaires en $(u_1, u_2)$ mais **quadratiques** avec $k$ ($x_C = -k u_2$, $y_C = k u_1$), donc un polynôme de degré 2 en les coordonnées ($x_C^2$, $x_B x_C$…) devient de degré au plus 4 en les paramètres ($k^2 u_2^2$, $k u_1 u_2$…). Le protocole probabiliste devient :\n", "\n", "1. tirer les paramètres $(u_1, u_2, k)$ **uniformément et indépendamment** dans une grande grille d'entiers ($|S| = 201$, disons) ;\n", "2. si un tirage rend $C_1 \\neq 0$, le théorème est **réfuté** — et cette réfutation est un certificat *certain* : exhiber un seul contre-exemple suffit ;\n", "3. si tous les tirages rendent $0$, deux explications restent possibles : $C_1(u_1, u_2, k)$ est identiquement nul — le théorème est alors une **identité**, vraie sur toute la famille construite — ou bien tous nos tirages sont tombés dans les zéros accidentels d'un polynôme non nul ;\n", - "4. Schwartz–Zippel borne la seconde explication : pour un polynôme non nul de degré $d$, au plus $d/|S| = 2/201 \\approx 1\\,\\%$ par tirage — et cette borne se **compose** sur des tirages indépendants." + "4. Schwartz–Zippel borne la seconde explication : pour un polynôme non nul de degré $d$, au plus $d/|S| = 4/201 \\approx 2\\,\\%$ par tirage — et cette borne se **compose** sur des tirages indépendants." ] }, { "cell_type": "code", "execution_count": 8, - "id": "79ea09ad", + "id": "e6e47d26", "metadata": { "execution": { - "iopub.execute_input": "2026-09-23T17:10:25.789902Z", - "iopub.status.busy": "2026-09-23T17:10:25.789733Z", - "iopub.status.idle": "2026-09-23T17:10:25.805619Z", - "shell.execute_reply": "2026-09-23T17:10:25.804879Z" + "iopub.execute_input": "2026-09-23T17:33:06.470140Z", + "iopub.status.busy": "2026-09-23T17:33:06.469981Z", + "iopub.status.idle": "2026-09-23T17:33:06.483152Z", + "shell.execute_reply": "2026-09-23T17:33:06.482668Z" } }, "outputs": [ @@ -563,9 +563,9 @@ "C1 apres substitution des parametres : 0\n", "C1(u_1, u_2, k) identiquement nul ? True\n", "tirages de parametres : 100 | rendant C1 = 0 : 100 / 100\n", - " 1 tirages independants : Pr[faux accord] <= 9.95e-03\n", - " 10 tirages independants : Pr[faux accord] <= 9.51e-21\n", - "100 tirages independants : Pr[faux accord] <= 6.07e-201\n" + " 1 tirages independants : Pr[faux accord] <= 1.99e-02\n", + " 10 tirages independants : Pr[faux accord] <= 9.74e-18\n", + "100 tirages independants : Pr[faux accord] <= 7.70e-171\n" ] } ], @@ -596,23 +596,23 @@ "\n", "# Etape 3 : la puissance du protocole -- la borne se compose sur les tirages.\n", "for n_draws in (1, 10, 100):\n", - " p_false = (2 / 201) ** n_draws\n", + " p_false = (4 / 201) ** n_draws\n", " print(f\"{n_draws:>3} tirages independants : Pr[faux accord] <= {p_false:.2e}\")" ] }, { "cell_type": "markdown", - "id": "749e1b61", + "id": "ebd06523", "metadata": {}, "source": [ - "**Lecture du résultat.** La mesure d'abord : sur 200 000 tirages uniformes des six coordonnées, une cinquantaine à peine satisfont l'hypothèse — filtrer $H = 0$ a posteriori n'aurait donc presque rien testé. Avec la substitution, chaque tirage de paramètres est une vraie figure, et les 100 tirages rendent tous $C_1 = 0$. Un polynôme *non nul* de degré 2 n'aurait survécu à 100 tirages uniformes qu'avec probabilité au plus $(2/201)^{100} \\approx 6 \\times 10^{-201}$ : soit nous avons observé l'improbable, soit $C_1(u_1, u_2, k)$ est **identiquement nul** — et sympy tranche : l'identité est exacte. Le test probabiliste et le verdict exact concordent. C'est le principe des **tests d'identité polynomiale** (PIT), pilier de l'algorithmique moderne (fingerprinting, vérification de calculs, preuves PCP).\n", + "**Lecture du résultat.** La mesure d'abord : sur 200 000 tirages uniformes des six coordonnées, une cinquantaine à peine satisfont l'hypothèse — filtrer $H = 0$ a posteriori n'aurait donc presque rien testé. Avec la substitution, chaque tirage de paramètres est une vraie figure, et les 100 tirages rendent tous $C_1 = 0$. Un polynôme *non nul* de degré au plus 4 n'aurait survécu à 100 tirages uniformes qu'avec probabilité au plus $(4/201)^{100} \\approx 8 \\times 10^{-171}$ : soit nous avons observé l'improbable, soit $C_1(u_1, u_2, k)$ est **identiquement nul** — et sympy tranche : l'identité est exacte. Le test probabiliste et le verdict exact concordent. C'est le principe des **tests d'identité polynomiale** (PIT), pilier de l'algorithmique moderne (fingerprinting, vérification de calculs, preuves PCP).\n", "\n", "Mais notons bien les **limites** : la borne ne s'applique qu'à un polynôme non nul sur un tirage *réellement* uniforme — un adversaire qui connaît notre générateur peut construire un énoncé faux qui s'annule sur toute notre grille (la section 5 l'a joué en pleine lumière). Et l'identité après substitution est vérifiée **sur la famille construite** ; la question générale — toute figure, y compris les cas dégénérés, avec la liste explicite des non-dégénérescences — reste ouverte. La certitude absolue exige l'algèbre exacte." ] }, { "cell_type": "markdown", - "id": "02cafb9e", + "id": "25d539e8", "metadata": {}, "source": [ "## 7. Ce que le Geometry-02 ajoutera : la certitude\n", @@ -634,7 +634,7 @@ }, { "cell_type": "markdown", - "id": "1bae8bd3", + "id": "c74ef1cc", "metadata": {}, "source": [ "## 8. Exercices\n", @@ -644,7 +644,7 @@ }, { "cell_type": "markdown", - "id": "f0564503", + "id": "b1a268e8", "metadata": {}, "source": [ "### Exercice 1 — Pythagore par la même méthode\n", @@ -662,13 +662,13 @@ { "cell_type": "code", "execution_count": 9, - "id": "0be8d8ca", + "id": "39a8f034", "metadata": { "execution": { - "iopub.execute_input": "2026-09-23T17:10:25.809060Z", - "iopub.status.busy": "2026-09-23T17:10:25.808790Z", - "iopub.status.idle": "2026-09-23T17:10:25.812003Z", - "shell.execute_reply": "2026-09-23T17:10:25.811518Z" + "iopub.execute_input": "2026-09-23T17:33:06.484717Z", + "iopub.status.busy": "2026-09-23T17:33:06.484557Z", + "iopub.status.idle": "2026-09-23T17:33:06.486875Z", + "shell.execute_reply": "2026-09-23T17:33:06.486438Z" } }, "outputs": [ @@ -689,7 +689,7 @@ }, { "cell_type": "markdown", - "id": "905ec101", + "id": "4508da7b", "metadata": {}, "source": [ "### Exercice 2 — Un énoncé « parfois vrai »\n", @@ -707,13 +707,13 @@ { "cell_type": "code", "execution_count": 10, - "id": "dab54d80", + "id": "c1d843da", "metadata": { "execution": { - "iopub.execute_input": "2026-09-23T17:10:25.815260Z", - "iopub.status.busy": "2026-09-23T17:10:25.815126Z", - "iopub.status.idle": "2026-09-23T17:10:25.817334Z", - "shell.execute_reply": "2026-09-23T17:10:25.816934Z" + "iopub.execute_input": "2026-09-23T17:33:06.488045Z", + "iopub.status.busy": "2026-09-23T17:33:06.487922Z", + "iopub.status.idle": "2026-09-23T17:33:06.490028Z", + "shell.execute_reply": "2026-09-23T17:33:06.489678Z" } }, "outputs": [ @@ -735,7 +735,7 @@ }, { "cell_type": "markdown", - "id": "efa812eb", + "id": "253dbfc0", "metadata": {}, "source": [ "### Exercice 3 — Schwartz–Zippel sous contrainte\n", @@ -751,13 +751,13 @@ { "cell_type": "code", "execution_count": 11, - "id": "3f419bda", + "id": "cc00e0dd", "metadata": { "execution": { - "iopub.execute_input": "2026-09-23T17:10:25.821317Z", - "iopub.status.busy": "2026-09-23T17:10:25.821119Z", - "iopub.status.idle": "2026-09-23T17:10:25.824489Z", - "shell.execute_reply": "2026-09-23T17:10:25.823951Z" + "iopub.execute_input": "2026-09-23T17:33:06.491402Z", + "iopub.status.busy": "2026-09-23T17:33:06.491269Z", + "iopub.status.idle": "2026-09-23T17:33:06.497259Z", + "shell.execute_reply": "2026-09-23T17:33:06.496623Z" } }, "outputs": [ @@ -778,7 +778,7 @@ }, { "cell_type": "markdown", - "id": "c6dbd77d", + "id": "46740910", "metadata": {}, "source": [ "## Ce qu'il faut retenir\n", @@ -793,7 +793,7 @@ }, { "cell_type": "markdown", - "id": "2591a841", + "id": "3c722727", "metadata": {}, "source": [ "***\n",