diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Serre100/29-reciprocite-quadratique-legendre.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Serre100/29-reciprocite-quadratique-legendre.ipynb new file mode 100644 index 0000000000..39e28cf5dc --- /dev/null +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Serre100/29-reciprocite-quadratique-legendre.ipynb @@ -0,0 +1,677 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "id": "c00", + "metadata": { + "papermill": { + "duration": 0.003762, + "end_time": "2026-10-25T12:13:08.611555+00:00", + "exception": false, + "start_time": "2026-10-25T12:13:08.607793+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "# 29 - Réciprocité quadratique et symbole de Legendre\n", + "\n", + "*Série Serre 100 — distillations exécutables* (EPIC #16334)\n", + "\n", + "La **loi de réciprocité quadratique** est le cœur du chapitre I de *A Course\n", + "in Arithmetic* de Serre : elle relie, pour deux nombres premiers impairs\n", + "distincts `p` et `q`, la « résidu-ité » de `p` modulo `q` à celle de `q` modulo\n", + "`p`. Ce carnet **mesure** l'outil qui la porte — le **symbole de Legendre**\n", + "`(a/p)` — puis la vérifie de bout en bout :\n", + "\n", + "- le symbole de Legendre `(a/p)` et la partition en résidus / non-résidus ;\n", + "- les **lois supplémentaires** `(2/p)` et `(-1/p)` ;\n", + "- la **loi de réciprocité** elle-même, `(p/q)·(q/p) = (-1)^{…}`.\n", + "\n", + "Tout est exécuté et vérifié en Python ci-dessous. Le pendant formel (preuve par\n", + "le noyau Lean, `legendreSym.quadratic_reciprocity`) est un grain de suite de la série.\n" + ] + }, + { + "cell_type": "markdown", + "id": "c01", + "metadata": { + "papermill": { + "duration": 0.001836, + "end_time": "2026-10-25T12:13:08.615611+00:00", + "exception": false, + "start_time": "2026-10-25T12:13:08.613775+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## Plan\n", + "\n", + "1. Le symbole de Legendre `(a/p)` — définition par le critère d'Euler.\n", + "2. Les résidus quadratiques modulo `p`.\n", + "3. Les lois supplémentaires `(2/p)` et `(-1/p)`.\n", + "4. La loi de réciprocité quadratique.\n", + "5. Exercices.\n" + ] + }, + { + "cell_type": "markdown", + "id": "c02", + "metadata": { + "papermill": { + "duration": 0.001768, + "end_time": "2026-10-25T12:13:08.619127+00:00", + "exception": false, + "start_time": "2026-10-25T12:13:08.617359+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 1. Le symbole de Legendre\n", + "\n", + "Pour un nombre premier impair `p` et un entier `a`, le **symbole de Legendre**\n", + "`(a/p)` est :\n", + "\n", + "- `0` si `p` divise `a` ;\n", + "- `+1` si `a` est un **résidu quadratique** modulo `p` (il existe `x` avec\n", + " `x² ≡ a [mod p]`) ;\n", + "- `-1` sinon.\n", + "\n", + "Il se calcule sans chercher `x` grâce au **critère d'Euler** :\n", + "`(a/p) ≡ a^{(p-1)/2} [mod p]`, qui ne vaut que `0`, `1` ou `-1`.\n" + ] + }, + { + "cell_type": "code", + "execution_count": 1, + "id": "c03", + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-25T12:13:08.624762Z", + "iopub.status.busy": "2026-10-25T12:13:08.624312Z", + "iopub.status.idle": "2026-10-25T12:13:08.634882Z", + "shell.execute_reply": "2026-10-25T12:13:08.634139Z" + }, + "papermill": { + "duration": 0.015603, + "end_time": "2026-10-25T12:13:08.636612+00:00", + "exception": false, + "start_time": "2026-10-25T12:13:08.621009+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "p = 3 : (1/3)=+1 (2/3)=-1\n", + "p = 5 : (1/5)=+1 (2/5)=-1 (3/5)=-1 (4/5)=+1\n", + "p = 7 : (1/7)=+1 (2/7)=+1 (3/7)=-1 (4/7)=+1 (5/7)=-1 (6/7)=-1\n", + "p = 11 : (1/11)=+1 (2/11)=-1 (3/11)=+1 (4/11)=+1 (5/11)=+1 (6/11)=-1 (7/11)=-1 (8/11)=-1 (9/11)=+1 (10/11)=-1\n", + "p = 13 : (1/13)=+1 (2/13)=-1 (3/13)=+1 (4/13)=+1 (5/13)=-1 (6/13)=-1 (7/13)=-1 (8/13)=-1 (9/13)=+1 (10/13)=+1 (11/13)=-1 (12/13)=+1\n" + ] + } + ], + "source": [ + "def legendre(a, p):\n", + " \"\"\"Symbole de Legendre (a/p) par le critere d'Euler :\n", + " a**((p-1)//2) mod p vaut 0, 1 ou p-1 (i.e. +1 ou -1).\"\"\"\n", + " a %= p\n", + " if a == 0:\n", + " return 0\n", + " r = pow(a, (p - 1) // 2, p)\n", + " return 1 if r == 1 else -1\n", + "\n", + "# Table du symbole de Legendre pour quelques petits premiers\n", + "for p in [3, 5, 7, 11, 13]:\n", + " row = \" \".join(f\"({a}/{p})={legendre(a, p):+d}\" for a in range(1, p))\n", + " print(f\"p = {p:2d} : {row}\")\n" + ] + }, + { + "cell_type": "markdown", + "id": "c04", + "metadata": { + "papermill": { + "duration": 0.002046, + "end_time": "2026-10-25T12:13:08.641248+00:00", + "exception": false, + "start_time": "2026-10-25T12:13:08.639202+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Lecture du résultat\n", + "\n", + "Le symbole ne prend que les valeurs `+1` et `-1` hors du cas `p | a`, et il\n", + "**partitionne** les classes `1, …, p-1` en deux moitiés. Pour `p = 7`, la table\n", + "donne `2` comme résidu (`(2/7) = +1`) mais `3`, `5`, `6` comme non-résidus —\n", + "exactement la moitié. C'est cette oscillation `±1` que la réciprocité va relier\n", + "entre deux premiers.\n" + ] + }, + { + "cell_type": "markdown", + "id": "c05", + "metadata": { + "papermill": { + "duration": 0.001841, + "end_time": "2026-10-25T12:13:08.645091+00:00", + "exception": false, + "start_time": "2026-10-25T12:13:08.643250+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 2. Les résidus quadratiques modulo p\n", + "\n", + "Les **résidus quadratiques** modulo `p` sont les `a` (dans `1, …, p-1`) pour\n", + "lesquels `(a/p) = +1`. Il y en a exactement `(p-1)/2` : les carrés\n", + "`1², 2², …` modulo `p` ne couvrent qu'une moitié des classes non nulles.\n" + ] + }, + { + "cell_type": "code", + "execution_count": 2, + "id": "c06", + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-25T12:13:08.650136Z", + "iopub.status.busy": "2026-10-25T12:13:08.649876Z", + "iopub.status.idle": "2026-10-25T12:13:08.654844Z", + "shell.execute_reply": "2026-10-25T12:13:08.653838Z" + }, + "papermill": { + "duration": 0.008645, + "end_time": "2026-10-25T12:13:08.655594+00:00", + "exception": false, + "start_time": "2026-10-25T12:13:08.646949+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "p = 7 : residues = [1, 2, 4] (|R| = 3 = (p-1)/2 = 3)\n", + "p = 11 : residues = [1, 3, 4, 5, 9] (|R| = 5 = (p-1)/2 = 5)\n", + "p = 13 : residues = [1, 3, 4, 9, 10, 12] (|R| = 6 = (p-1)/2 = 6)\n" + ] + } + ], + "source": [ + "# Residus quadratiques modulo p : les a dans 1..p-1 avec (a/p) = +1\n", + "for p in [7, 11, 13]:\n", + " res = [a for a in range(1, p) if legendre(a, p) == 1]\n", + " print(f\"p = {p:2d} : residues = {res} \"\n", + " f\"(|R| = {len(res)} = (p-1)/2 = {(p - 1) // 2})\")\n" + ] + }, + { + "cell_type": "markdown", + "id": "c07", + "metadata": { + "papermill": { + "duration": 0.002147, + "end_time": "2026-10-25T12:13:08.660086+00:00", + "exception": false, + "start_time": "2026-10-25T12:13:08.657939+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Lecture du résultat\n", + "\n", + "Pour `p = 7`, les résidus sont `[1, 2, 4]` ; pour `p = 11`, `[1, 3, 4, 5, 9]` ;\n", + "pour `p = 13`, `[1, 3, 4, 9, 10, 12]` — dans chaque cas exactement `(p-1)/2`\n", + "éléments. Le critère d'Euler retrouve ici, par un simple `pow(a, (p-1)//2, p)`,\n", + "la même partition qu'une énumération brute des carrés.\n" + ] + }, + { + "cell_type": "markdown", + "id": "c08", + "metadata": { + "papermill": { + "duration": 0.001943, + "end_time": "2026-10-25T12:13:08.664174+00:00", + "exception": false, + "start_time": "2026-10-25T12:13:08.662231+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 3. Les lois supplémentaires\n", + "\n", + "Deux cas particuliers de la réciprocité se closent eux-mêmes :\n", + "\n", + "- **`(-1/p)`** : vaut `+1` si `p ≡ 1 [mod 4]`, `-1` si `p ≡ 3 [mod 4]` —\n", + " soit `(-1/p) = (-1)^{(p-1)/2}`.\n", + "- **`(2/p)`** : vaut `+1` si `p ≡ ±1 [mod 8]`, `-1` si `p ≡ ±3 [mod 8]` —\n", + " soit `(2/p) = (-1)^{(p²-1)/8}`.\n", + "\n", + "Elles « lèvent » les symboles dont la base est `-1` ou `2` sans faire appel à\n", + "la réciprocité proprement dite.\n" + ] + }, + { + "cell_type": "code", + "execution_count": 3, + "id": "c09", + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-25T12:13:08.669390Z", + "iopub.status.busy": "2026-10-25T12:13:08.669160Z", + "iopub.status.idle": "2026-10-25T12:13:08.675819Z", + "shell.execute_reply": "2026-10-25T12:13:08.674969Z" + }, + "papermill": { + "duration": 0.010384, + "end_time": "2026-10-25T12:13:08.676504+00:00", + "exception": false, + "start_time": "2026-10-25T12:13:08.666120+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Loi (2/p) sur 11 premiers impairs <= 40 : contre-exemples = aucun\n", + "Loi (-1/p) sur 11 premiers impairs <= 40 : contre-exemples = aucun\n", + " p mod 8 : 3->3 5->5 7->7 11->3 13->5 17->1 19->3 23->7 29->5 31->7 37->5\n" + ] + } + ], + "source": [ + "def is_prime(n):\n", + " \"\"\"n est-il premier ?\"\"\"\n", + " if n < 2:\n", + " return False\n", + " d = 2\n", + " while d * d <= n:\n", + " if n % d == 0:\n", + " return False\n", + " d += 1\n", + " return True\n", + "\n", + "odd_primes = [p for p in range(3, 41) if is_prime(p)]\n", + "\n", + "# Loi (2/p) : (2/p) = (-1)^((p^2-1)/8)\n", + "bad2 = [p for p in odd_primes\n", + " if legendre(2, p) != (1 if ((p * p - 1) // 8) % 2 == 0 else -1)]\n", + "# Loi (-1/p) : (-1/p) = (-1)^((p-1)/2)\n", + "badm1 = [p for p in odd_primes\n", + " if legendre(-1, p) != (1 if ((p - 1) // 2) % 2 == 0 else -1)]\n", + "print(f\"Loi (2/p) sur {len(odd_primes)} premiers impairs <= 40 : \"\n", + " f\"contre-exemples = {bad2 if bad2 else 'aucun'}\")\n", + "print(f\"Loi (-1/p) sur {len(odd_primes)} premiers impairs <= 40 : \"\n", + " f\"contre-exemples = {badm1 if badm1 else 'aucun'}\")\n", + "# Apercu : (2/p) ne depend que de p modulo 8\n", + "print(\" p mod 8 : \" + \" \".join(f\"{p}->{p % 8}\" for p in odd_primes))\n" + ] + }, + { + "cell_type": "markdown", + "id": "c10", + "metadata": { + "papermill": { + "duration": 0.002256, + "end_time": "2026-10-25T12:13:08.681150+00:00", + "exception": false, + "start_time": "2026-10-25T12:13:08.678894+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Lecture du résultat\n", + "\n", + "Les deux lois tiennent sur tous les premiers impairs `≤ 40` sans contre-exemple.\n", + "`(2/p)` ne dépend que de `p` **modulo 8** : `+1` pour `p ∈ {7, 17, 23, 31}`\n", + "(`≡ ±1 [mod 8]`) et `-1` pour `p ∈ {3, 5, 11, 13, 19, 29, 37}` (`≡ ±3 [mod 8]`) ;\n", + "`(-1/p) = +1` exactement quand `p ≡ 1 [mod 4]`.\n" + ] + }, + { + "cell_type": "markdown", + "id": "c11", + "metadata": { + "papermill": { + "duration": 0.002173, + "end_time": "2026-10-25T12:13:08.685583+00:00", + "exception": false, + "start_time": "2026-10-25T12:13:08.683410+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 4. La loi de réciprocité quadratique\n", + "\n", + "Pour deux nombres premiers impairs **distincts** `p` et `q`, la loi de\n", + "**réciprocité quadratique** (Euler–Gauss) dit :\n", + "\n", + " (p/q) · (q/p) = (-1)^{ ((p-1)/2) · ((q-1)/2) }.\n", + "\n", + "Le signe du membre de droite n'est `-1` que lorsque `p` **et** `q` sont tous\n", + "deux `≡ 3 [mod 4]` ; sinon il est `+1`. La loi permet de **retourner** le\n", + "symbole : pour un premier `a > p`, `(a/p)` s'exprime en `(p/a)` et un signe —\n", + "la base devient plus petite, et l'itération aboutit.\n" + ] + }, + { + "cell_type": "code", + "execution_count": 4, + "id": "c12", + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-25T12:13:08.691445Z", + "iopub.status.busy": "2026-10-25T12:13:08.691192Z", + "iopub.status.idle": "2026-10-25T12:13:08.696361Z", + "shell.execute_reply": "2026-10-25T12:13:08.695605Z" + }, + "papermill": { + "duration": 0.009322, + "end_time": "2026-10-25T12:13:08.697108+00:00", + "exception": false, + "start_time": "2026-10-25T12:13:08.687786+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Verifie sur 55 paires de premiers impairs (p < q <= 40) : 55/55 conformes.\n", + "Contre-exemples : aucun\n" + ] + } + ], + "source": [ + "# Loi de reciprocite : pour p, q premiers impairs DISTINCTS,\n", + "# (p/q) * (q/p) = (-1)^(((p-1)/2) * ((q-1)/2))\n", + "ps = [p for p in range(3, 41) if is_prime(p)]\n", + "bad, total = [], 0\n", + "for i in range(len(ps)):\n", + " for j in range(i + 1, len(ps)):\n", + " p, q = ps[i], ps[j]\n", + " total += 1\n", + " lhs = legendre(p, q) * legendre(q, p)\n", + " exp = 1 if (((p - 1) // 2) * ((q - 1) // 2)) % 2 == 0 else -1\n", + " if lhs != exp:\n", + " bad.append((p, q, lhs, exp))\n", + "print(f\"Verifie sur {total} paires de premiers impairs (p < q <= 40) : \"\n", + " f\"{total - len(bad)}/{total} conformes.\")\n", + "print(\"Contre-exemples :\", bad if bad else \"aucun\")\n" + ] + }, + { + "cell_type": "markdown", + "id": "c13", + "metadata": { + "papermill": { + "duration": 0.002229, + "end_time": "2026-10-25T12:13:08.701909+00:00", + "exception": false, + "start_time": "2026-10-25T12:13:08.699680+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Lecture du résultat\n", + "\n", + "La loi tient sur les `55` paires de premiers impairs `p < q ≤ 40` sans\n", + "contre-exemple. Le « retournement » se lit sur les échantillons : `(3/7) = -1`\n", + "et `(7/3) = +1`, de produit `-1` — le signe attendu, car `3` et `7` sont tous\n", + "deux `≡ 3 [mod 4]` ; alors que pour la paire `(5, 7)` le signe est `+1`\n", + "(`5 ≡ 1 [mod 4]`). C'est ce retournement itéré qui rend la réciprocité un\n", + "**algorithme** de décision de résidu-ité.\n" + ] + }, + { + "cell_type": "markdown", + "id": "c14", + "metadata": { + "papermill": { + "duration": 0.002211, + "end_time": "2026-10-25T12:13:08.706293+00:00", + "exception": false, + "start_time": "2026-10-25T12:13:08.704082+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 5. Exercices\n" + ] + }, + { + "cell_type": "code", + "execution_count": 5, + "id": "c15", + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-25T12:13:08.712449Z", + "iopub.status.busy": "2026-10-25T12:13:08.712035Z", + "iopub.status.idle": "2026-10-25T12:13:08.716348Z", + "shell.execute_reply": "2026-10-25T12:13:08.715492Z" + }, + "papermill": { + "duration": 0.008493, + "end_time": "2026-10-25T12:13:08.717022+00:00", + "exception": false, + "start_time": "2026-10-25T12:13:08.708529+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "is_quadratic_residue(2, 7) = None\n", + "is_quadratic_residue(3, 7) = None\n" + ] + } + ], + "source": [ + "# Exercice 1\n", + "# Ecrire `is_quadratic_residue(a, p)` : renvoyer True si `a` est un residu\n", + "# quadratique modulo `p` (il existe x avec x^2 == a [mod p]), False sinon.\n", + "# NE PAS utiliser le critere d'Euler : tester directement les x dans 1..p-1.\n", + "# Indice : chercher un x tel que (x * x) % p == a % p.\n", + "def is_quadratic_residue(a, p):\n", + " # TODO etudiant\n", + " return None\n", + "print(\"is_quadratic_residue(2, 7) =\", is_quadratic_residue(2, 7)) # attendu : True\n", + "print(\"is_quadratic_residue(3, 7) =\", is_quadratic_residue(3, 7)) # attendu : False\n" + ] + }, + { + "cell_type": "code", + "execution_count": 6, + "id": "c16", + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-25T12:13:08.723572Z", + "iopub.status.busy": "2026-10-25T12:13:08.723338Z", + "iopub.status.idle": "2026-10-25T12:13:08.727713Z", + "shell.execute_reply": "2026-10-25T12:13:08.726826Z" + }, + "papermill": { + "duration": 0.008742, + "end_time": "2026-10-25T12:13:08.728404+00:00", + "exception": false, + "start_time": "2026-10-25T12:13:08.719662+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "non_residues(7) = None\n" + ] + } + ], + "source": [ + "# Exercice 2\n", + "# Ecrire `non_residues(p)` : renvoyer la liste des NON-residus quadratiques\n", + "# dans 1..p-1, c'est-a-dire les a avec (a/p) = -1.\n", + "# Indice : [a for a in range(1, p) if legendre(a, p) == -1].\n", + "def non_residues(p):\n", + " # TODO etudiant\n", + " return None\n", + "print(\"non_residues(7) =\", non_residues(7)) # attendu : [3, 5, 6]\n" + ] + }, + { + "cell_type": "code", + "execution_count": 7, + "id": "c17", + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-25T12:13:08.735084Z", + "iopub.status.busy": "2026-10-25T12:13:08.734711Z", + "iopub.status.idle": "2026-10-25T12:13:08.739468Z", + "shell.execute_reply": "2026-10-25T12:13:08.738539Z" + }, + "papermill": { + "duration": 0.009216, + "end_time": "2026-10-25T12:13:08.740136+00:00", + "exception": false, + "start_time": "2026-10-25T12:13:08.730920+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "flip_symbol(7, 3) = None\n" + ] + } + ], + "source": [ + "# Exercice 3\n", + "# L'interet computatoire de la reciprocite est de « retourner » le symbole :\n", + "# pour un premier a > p, ecrire `flip_symbol(a, p)` qui renvoie le couple\n", + "# (signe, (p/a)), avec (a/p) = signe * (p/a) et\n", + "# signe = (-1)^(((a-1)/2) * ((p-1)/2)).\n", + "# Indice : signe = 1 si ((a-1)//2 * (p-1)//2) est pair, -1 sinon.\n", + "def flip_symbol(a, p):\n", + " # TODO etudiant\n", + " return None\n", + "print(\"flip_symbol(7, 3) =\", flip_symbol(7, 3)) # (7/3) = signe * (3/7)\n" + ] + }, + { + "cell_type": "markdown", + "id": "c18", + "metadata": { + "papermill": { + "duration": 0.002972, + "end_time": "2026-10-25T12:13:08.745855+00:00", + "exception": false, + "start_time": "2026-10-25T12:13:08.742883+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## Conclusion\n", + "\n", + "Le symbole de Legendre est un indicateur `±1` (ou `0`) de résidu-ité modulo un\n", + "premier ; le critère d'Euler le calcule en une puissance. Les lois\n", + "supplémentaires le closent pour les bases `-1` et `2` ; la **réciprocité\n", + "quadratique** le relie entre deux premiers et, en le retournant itérativement,\n", + "fournit un algorithme. Les trois volets sont mesurés ci-dessus sur des\n", + "dizaines de premiers ; leur preuve formelle, par le noyau Lean, fait l'objet\n", + "d'un carnet pendant de la série.\n" + ] + }, + { + "cell_type": "markdown", + "id": "c19", + "metadata": { + "papermill": { + "duration": 0.002453, + "end_time": "2026-10-25T12:13:08.751042+00:00", + "exception": false, + "start_time": "2026-10-25T12:13:08.748589+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## Ressources\n", + "\n", + "- J.-P. Serre, *A Course in Arithmetic* — ch. I (corps finis, § 3 : la loi de\n", + " réciprocité quadratique, et son appendice qui en donne une seconde preuve),\n", + " prolongé par le ch. III (symbole de Hilbert).\n", + "- Mathlib (Lean 4) : `legendreSym.quadratic_reciprocity`,\n", + " `ZMod.exists_sq_eq_two_iff`, `ZMod.exists_sq_eq_prime_iff_of_mod_four_eq_one` —\n", + " le pendant formel de ce carnet. Deux pièges de nommage : l'ordre des arguments\n", + " est `legendreSym p a` (et non l'inverse), et les résidus quadratiques sont\n", + " formalisés par `IsSquare` — le Mathlib épinglé ne définit aucun prédicat\n", + " `IsQuadraticResidue`.\n", + "\n", + "Retour à la série : [README de *Serre 100*](README.md)" + ] + } + ], + "metadata": { + "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.7" + }, + "papermill": { + "default_parameters": {}, + "duration": 5.232579, + "end_time": "2026-10-25T12:13:12.231540+00:00", + "environment_variables": {}, + "exception": null, + "input_path": "29-reciprocite-quadratique-legendre.ipynb", + "output_path": "29-reciprocite-quadratique-legendre.ipynb", + "parameters": {}, + "start_time": "2026-10-25T12:13:06.998961+00:00", + "version": "2.7.0" + } + }, + "nbformat": 4, + "nbformat_minor": 5 +} diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Serre100/README.md b/MyIA.AI.Notebooks/SymbolicAI/Lean/Serre100/README.md index f53fb3d170..413be57d40 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Serre100/README.md +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Serre100/README.md @@ -36,6 +36,7 @@ Le geste « distillation » : prendre un énoncé ou une construction centrale d | 25 | [25-groupe-galois-calcule.ipynb](25-groupe-galois-calcule.ipynb) | Le groupe de Galois calculé (*Topics in Galois Theory*, leçon 1) — types de décomposition (Dedekind, prolonge 17), discriminant exact (Sylvester/Bareiss) et $G \subseteq A_n$, étau de sous-groupes transitifs : neuf groupes identifiés ($C_3$ à $S_5$), leçon mesurée de la transitivité ($V_4$ contre un pseudo-$C_2$), résolvante cubique concordante, série dérivée calculée (Abel-Ruffini exécuté, $A_5$ parfait), Cardano vérifié contre Durand-Kerner, pont Lean-22/$M_{23}$ | Python stdlib + matplotlib | | 26 | [26-trois-carres-legendre.ipynb](26-trois-carres-legendre.ipynb) | Théorème des trois carrés de Legendre (première preuve complète : Gauss, *Disquisitiones* art. 291) — critère n ≠ 4ᵃ(8b+7) confronté à la force brute, obstruction 2-adique de profondeur mesurée 2a+3 (dégraissage des puissances de 4), instrument r₃(n) validé sur OEIS A005875 (deux pièges de balayage autopsiés), pont de Gauss-Hurwitz r₃(n) = 12H(4n) / 24H(n) par les nombres de classes des carnets 12/14 | Python stdlib (math.isqrt, fractions) + matplotlib | | 27 | [27-pell-fermat.ipynb](27-pell-fermat.ipynb) | Équation de Pell-Fermat $x^2 - dy^2 = 1$ — fraction continue de √d (algorithme de Lagrange, palindrome de Galois), théorème d'indice sur les convergents, période impaire ⇔ Pell négative soluble (186/186 mesuré sur d ≤ 200), critère de Legendre exact pour les premiers (44/44 et 0/50 sous 500) et mis en défaut par les composés (d = 34), unité fondamentale de Z[√d] par composition de Brahmagupta — le groupe cyclique infini de Dirichlet rang 1, contraste avec les corps imaginaires du carnet 11 | Python stdlib + matplotlib | +| 29 | [29-reciprocite-quadratique-legendre.ipynb](29-reciprocite-quadratique-legendre.ipynb) | Symbole de Legendre et réciprocité quadratique — résidus quadratiques énumérés par force brute puis confrontés au critère d'Euler (p = 7, 11, 13), lois supplémentaires (2/p) et (−1/p) sur les 11 premiers impairs ≤ 40, les 55 paires de premiers vérifiées une à une | Python stdlib | ## Conventions