diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-01-Sendov-Lean-Python.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-01-Sendov-Lean-Python.ipynb index 3a979de70a..c1ec5af71d 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-01-Sendov-Lean-Python.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-01-Sendov-Lean-Python.ipynb @@ -426,6 +426,12 @@ "# Theoreme Sendov pour a = 0 : il existe zeta point critique avec |zeta| <= 1.\n", "#\n", "# Source Lean : Sendov/Interior.lean (sendov_center) + Sendov/Analytic/*\n", + "#\n", + "# Contexte dans ce carnet : voir §5 (enonce), §6 (cas 0 < |a| < 1, Code 6.1),\n", + "# §7 (cas |a| = 1, Rubinstein, Code 7.1), §8 (recollement, Code 8.1).\n", + "# Sendov se decompose en 3 cas par position de a : centre (ce §5),\n", + "# interieur (Code 6.1, §6), frontiere (Code 7.1, §7) ; le recollement\n", + "# (§8) elimine la normalisation a in [0, 1) et conclut le theoreme.\n", "\n", "import numpy as np\n", "\n", @@ -567,6 +573,12 @@ "# Source : Sendov/Analytic/LowDegree.lean (Sendov.lowJ_lt_one)\n", "# Formule : J_m(a) = integral_0^1 (a + (1-a^2)*t)^m dt\n", "# Pour 0 < a < 1 et 1 <= m <= 4 : J_m(a) < 1.\n", + "#\n", + "# Contexte dans ce carnet : voir §5 (cas du centre, Code 5.1),\n", + "# ce §6 (cas interieur 0 < |a| < 1), §7 (cas boundary |a| = 1,\n", + "# Rubinstein, Code 7.1), §8 (recollement, Code 8.1). Le branch point\n", + "# J_m(a) < 1 est la cle du cas interieur ; il s'insere dans la\n", + "# decomposition par cas (§5/§6/§7) que §8 recolle pour conclure.\n", "\n", "from scipy.integrate import quad\n", "\n", @@ -701,6 +713,13 @@ "# Pour p(z) = z^n - 1, zeros = racines n-iemes de l'unite, tous sur |z| = 1.\n", "# Points critiques = {0} (tous en 0, p'(z) = n z^{n-1}).\n", "# Distance d'un zero omega (|omega| = 1) a 0 : |omega - 0| = 1 exactement.\n", + "#\n", + "# Contexte dans ce carnet : voir §5 (cas du centre, Code 5.1), §6 (cas\n", + "# interieur 0 < |a| < 1, Code 6.1), ce §7 (cas boundary |a| = 1,\n", + "# Rubinstein), §8 (recollement, Code 8.1). Rubinstein identifie le cas\n", + "# extreme ou l'inegalite stricte < 1 echoue (egalite). Phelps-Rodriguez\n", + "# AFFIRME que c'est le seul cas d'echec, ce qui complete la preuve\n", + "# apres le recollement de §8.\n", "\n", "import cmath\n", "import numpy as np\n",