From 6e0d02cc341d2f78d75f4c5df9be11b1d273e036 Mon Sep 17 00:00:00 2001 From: jsboige Date: Sat, 24 Oct 2026 18:19:02 +0200 Subject: [PATCH 1/4] Add(notebook,#21958): Pli 6 tranche C -- jumeau anglais de ANALYSE-12 Le carnet ANALYSE-12 (comptage des couplages parfaits, pont card_eq_permanent) recoit son jumeau anglais : 20/20 cellules markdown traduites, 10/10 cellules de code byte-identiques, 10/10 sorties identiques, execution_count 1-10, metadata.papermill absent -- la convention mesuree sur la paire ANALYSE-09 FR/_en. Table du README remise coherente dans le meme geste : la ligne ANALYSE-05 y figurait deux fois a l'identique (doublon), ANALYSE-09 n'y figurait pas du tout alors que le carnet et son jumeau existent ; les trois jumeaux presents (07, 09, 12) sont desormais cites comme l'est deja celui d'ANALYSE-06. _quarto.yml n'est pas touche : liste generee, regeneree par le cron catalogue (regle HARD 5). Part of #21958 Co-Authored-By: Claude Sonnet 5.5 --- ...-12-Comptage-Matching-Lean-Python_en.ipynb | 1095 +++++++++++++++++ .../SymbolicAI/Lean/ANALYSE/README.md | 6 +- 2 files changed, 1098 insertions(+), 3 deletions(-) create mode 100644 MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-12-Comptage-Matching-Lean-Python_en.ipynb diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-12-Comptage-Matching-Lean-Python_en.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-12-Comptage-Matching-Lean-Python_en.ipynb new file mode 100644 index 00000000000..c027f336a4e --- /dev/null +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-12-Comptage-Matching-Lean-Python_en.ipynb @@ -0,0 +1,1095 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "id": "9631baea-b8fd-4526-bb86-7355c8ad920c", + "metadata": { + "papermill": { + "duration": 0.002064, + "end_time": "2026-10-22T13:21:07.060394+00:00", + "exception": false, + "start_time": "2026-10-22T13:21:07.058330+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "# ANALYSE-12: Counting perfect matchings — the permanent as a bridge, Lean on one side, enumeration on the other\n", + "\n", + "Fold 6 of the `openai/math` Origami Epic (#19898, tranche B: #21958). The ANALYSE series confronts a research statement with what the repository can prove; here the statement is a **counting** problem.\n", + "\n", + "- **Finding** a perfect matching in a bipartite graph: polynomial (flow, Hungarian assignment — the `assignment_lean` lake exhibits it, cf. `Duality.lean`).\n", + "- **Counting** perfect matchings: the `#P` class — and the matrix object that carries this count is the **permanent**, the sign-forgetting cousin of the determinant.\n", + "\n", + "Tranche A (#21962) deposited into the lake the bridge `card_eq_permanent`: the permanent (native Mathlib organ) of the 0/1 adjacency matrix **equals** the number of perfect matchings. This notebook does three things:\n", + "\n", + "1. it audits the foundation (the Mathlib organ `Matrix.permanent`, the file `Counting.lean`) and checks the signatures and axioms from the lake;\n", + "2. it cross-checks the bridge by brute-force enumeration in Python — every value Lean evaluates must come out identical from the enumeration;\n", + "3. it exercises the native negative controls (`Matrix.permanent_zero`, `Matrix.permanent_one`) as guarantees of meaning.\n", + "\n", + "**Overall epistemic status** (doctrine #19898, detailed in §7): this repository proves the local bridge; `#P`-completeness (Valiant) and the FPRAS (Jerrum–Sinclair–Vigoda) are classical theorems **cited**; the `lean/docs` skeleton published by the `openai/math` authors (family 113) is **reported, not verified here**.\n", + "\n", + "**Execution environment**: kernel `python3` (the repository venv); the Lean cells compile probes via `wsl` + `lake env lean` against the `assignment_lean` lake (toolchain v4.33.0, Mathlib pin `db584cd6d46c`) — the convention of the `-Lean-Python` series (cf. ANALYSE-06).\n", + "## Navigation\n", + "\n", + "| Previous notebook | Next notebook |\n", + "|---|---|\n", + "| [ANALYSE-11 - Transverse synthesis](ANALYSE-11-Synthese-Transverse-Digestions-Python.ipynb) | -- |\n", + "\n", + "***\n" + ] + }, + { + "cell_type": "markdown", + "id": "950ad958-51c5-4771-81eb-1140027605cd", + "metadata": { + "papermill": { + "duration": 0.001667, + "end_time": "2026-10-22T13:21:07.063982+00:00", + "exception": false, + "start_time": "2026-10-22T13:21:07.062315+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 1. The statement — counting perfect matchings (family 113)\n", + "\n", + "A bipartite graph $G = (U \\cup V, E)$ with $|U| = |V| = n$, represented by its boolean adjacency matrix $B$ ($B_{ij}$: the edge $i \\to j$ exists).\n", + "\n", + "- A **perfect matching** is a bijection $\\sigma : U \\to V$ such that every edge $(i, \\sigma(i))$ exists.\n", + "- The **permanent** of a square $n \\times n$ matrix $M$ is $\\mathrm{perm}(M) = \\sum_{\\sigma \\in S_n} \\prod_{i=1}^{n} M_{i,\\sigma(i)}$ — the sum over **all** permutations, like the determinant **without the signs**.\n", + "\n", + "On a 0/1 matrix every product equals $1$ exactly when $\\sigma$ is a covered matching: $\\mathrm{perm}(B) = \\#\\{\\text{perfect matchings}\\}$. Counting already means evaluating the permanent.\n", + "\n", + "**The class jump**: deciding whether a perfect matching exists is polynomial; counting the perfect matchings of a bipartite graph is `#P`-complete — the **founding** problem of the class (Valiant, 1979) — and yet it admits a randomised FPRAS (Jerrum–Sinclair–Vigoda, 2004). Both theorems are literature classics, cited here as such; the status of the formal skeleton published by the `openai/math` authors is treated in §7." + ] + }, + { + "cell_type": "markdown", + "id": "25821175-ac6f-4ac4-912c-9af03a96a1cd", + "metadata": { + "papermill": { + "duration": 0.001968, + "end_time": "2026-10-22T13:21:07.067670+00:00", + "exception": false, + "start_time": "2026-10-22T13:21:07.065702+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 2. The proof chain — three links, only one of them ours\n", + "\n", + "| Link | Carrier | Status in this notebook |\n", + "|---|---|---|\n", + "| 1. The organ `Matrix.permanent` exists (zero, one, transpose, diagonal…) | Mathlib at pin `v4.33.0` | **verified** (audit §3 + probes) |\n", + "| 2. The bridge `card_eq_permanent`: permanent of the adjacency = number of matchings | the `assignment_lean` lake (tranche A, #21962) | **verified** (signatures + axioms + `#eval` cross-checked in §5) |\n", + "| 3. `#P`-completeness of counting; FPRAS; SDP frontier (family 126) | classical literature / `openai/math` skeleton | **cited / reported** — never \"proved by us\" |\n", + "\n", + "The notebook's method follows the series: never confuse what the repository **proves** (links 1-2, backed by `#print axioms`) with what it **cites** (link 3). The Python cross-check of §4-§5 does not prove the bridge — it verifies that the formalisation did not pick the wrong object: every Lean value must come out identical from the brute-force enumeration." + ] + }, + { + "cell_type": "markdown", + "id": "34a72bdd-dfa4-45b8-9c1a-8218cae05f31", + "metadata": { + "papermill": { + "duration": 0.001726, + "end_time": "2026-10-22T13:21:07.071281+00:00", + "exception": false, + "start_time": "2026-10-22T13:21:07.069555+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 3. The Lean foundation — auditing the organ and the bridge\n", + "\n", + "Two preliminary checks, made **at the source**: the organ `Matrix.permanent` is indeed in Mathlib at the lake's pin (with its native controls `permanent_zero`, `permanent_one`), and the file `Counting.lean` of tranche A is present in the lake with the expected declarations." + ] + }, + { + "cell_type": "code", + "id": "a835132f-8d41-4652-93ca-51709b44afe4", + "execution_count": 1, + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-22T13:21:07.076382Z", + "iopub.status.busy": "2026-10-22T13:21:07.076107Z", + "iopub.status.idle": "2026-10-22T13:21:07.513411Z", + "shell.execute_reply": "2026-10-22T13:21:07.512275Z" + }, + "papermill": { + "duration": 0.440984, + "end_time": "2026-10-22T13:21:07.514227+00:00", + "exception": false, + "start_time": "2026-10-22T13:21:07.073243+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "toolchain du lac : leanprover/lean4:v4.33.0\n", + "\n", + "organe Mathlib — Mathlib/LinearAlgebra/Matrix/Permanent.lean :\n", + " 4370 octets\n", + "\n", + "théorèmes natifs `permanent_*` (extraits) :\n" + ] + }, + { + "name": "stdout", + "output_type": "stream", + "text": [ + " theorem permanent_diagonal {d : n → R} : permanent (diagonal d) = ∏ i, d i\n", + " theorem permanent_zero [Nonempty n] : permanent (0 : Matrix n n R) = 0\n", + " theorem permanent_one : permanent (1 : Matrix n n R) = 1\n", + " theorem permanent_isEmpty [IsEmpty n] {A : Matrix n n R} : permanent A = 1\n", + " theorem permanent_eq_one_of_card_eq_zero {A : Matrix n n R} (h : card n = 0) : permanent A = 1\n", + " theorem permanent_unique {n : Type*} [Unique n] [DecidableEq n] [Fintype n] (A : Matrix n n R) :\n" + ] + } + ], + "source": [ + "# Audit Mathlib au pin v4.33.0 (db584cd6d46c) : l'organe permanent et ses contrôles natifs.\n", + "import subprocess, os\n", + "\n", + "LAKE_DIR = (subprocess.run([\"wsl\", \"wslpath\", \"-a\", os.getcwd().replace(\"\\\\\", \"/\")],\n", + " capture_output=True, text=True, encoding=\"utf-8\", errors=\"replace\")\n", + " .stdout.strip() + \"/../../../GameTheory/assignment_lean\")\n", + "MATHLIB = LAKE_DIR + \"/.lake/packages/mathlib\"\n", + "\n", + "def wsl_sh(cmd):\n", + " return subprocess.run([\"wsl\", \"-e\", \"bash\", \"-lc\", cmd],\n", + " capture_output=True, text=True,\n", + " encoding=\"utf-8\", errors=\"replace\").stdout.strip()\n", + "\n", + "print(\"toolchain du lac :\", wsl_sh(\"cat \" + LAKE_DIR + \"/lean-toolchain\"))\n", + "print()\n", + "print(\"organe Mathlib — Mathlib/LinearAlgebra/Matrix/Permanent.lean :\")\n", + "print(\" \", wsl_sh(\"stat -c %s \" + MATHLIB + \"/Mathlib/LinearAlgebra/Matrix/Permanent.lean\"), \"octets\")\n", + "print()\n", + "print(\"théorèmes natifs `permanent_*` (extraits) :\")\n", + "for t in wsl_sh(\"grep -hE '^theorem permanent_' \" + MATHLIB\n", + " + \"/Mathlib/LinearAlgebra/Matrix/Permanent.lean | sed 's/ :=.*//' | head -6\").splitlines():\n", + " print(\" \", t.strip())" + ] + }, + { + "cell_type": "markdown", + "id": "9c90bc36-eeeb-4a1b-9813-d26c92cbc54b", + "metadata": { + "papermill": { + "duration": 0.002276, + "end_time": "2026-10-22T13:21:07.518971+00:00", + "exception": false, + "start_time": "2026-10-22T13:21:07.516695+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Reading the audit\n", + "\n", + "The organ exists at the pin: `Permanent.lean` carries the definition and a family of native theorems, including the two controls used in §6 (`permanent_zero`, `permanent_one`) and the transpose used by the bridge proof (`permanent_transpose`). The lake runs under toolchain `v4.33.0` — the pin under which tranche A was proved.\n", + "\n", + "**Organ-first** (#13564): the lake redefines neither the permanent nor its lemmas — it invokes the Mathlib organ and proves the correspondence with matchings." + ] + }, + { + "cell_type": "code", + "id": "b648ee45-46ed-4e0c-9219-a2857c6c186a", + "execution_count": 2, + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-22T13:21:07.524404Z", + "iopub.status.busy": "2026-10-22T13:21:07.524135Z", + "iopub.status.idle": "2026-10-22T13:21:07.528898Z", + "shell.execute_reply": "2026-10-22T13:21:07.528153Z" + }, + "papermill": { + "duration": 0.008375, + "end_time": "2026-10-22T13:21:07.529572+00:00", + "exception": false, + "start_time": "2026-10-22T13:21:07.521197+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "fichier : ..\\..\\..\\GameTheory\\assignment_lean\\Assignment\\Counting.lean (82 lignes)\n", + "\n", + "--- lignes 23-32 ---\n", + " 23 | /-- Matrice d'adjacence entiere d'un graphe biparti sur `Fin n × Fin n` :\n", + " 24 | `1` si l'arete existe, `0` sinon. -/\n", + " 25 | def adjMatrix (B : Matrix (Fin n) (Fin n) Bool) : Matrix (Fin n) (Fin n) ℕ :=\n", + " 26 | B.map fun b => if b then 1 else 0\n", + " 27 | \n", + " 28 | /-- L'ensemble des couplages parfaits d'un graphe biparti : les permutations\n", + " 29 | dont toutes les aretes ligne `i` vers colonne `σ i` sont presentes. -/\n", + " 30 | def perfectMatchingSet (B : Matrix (Fin n) (Fin n) Bool) :\n", + " 31 | Finset (Equiv.Perm (Fin n)) :=\n", + " 32 | Finset.univ.filter fun σ => ∀ i, B i (σ i)\n", + "\n", + "--- lignes 50-57 ---\n", + " 50 | /-- **Le pont** : le permanent (Mathlib) de la matrice d'adjacence 0/1 egale\n", + " 51 | le nombre de couplages parfaits du graphe biparti. C'est la formalisation\n", + " 52 | locale du point d'entree des familles 113 (FPRAS pour compter) et 126\n", + " 53 | (cloture SDP) d'openai/math, citees avec leur statut epistemique dans le\n", + " 54 | carnet ANALYSE-12. -/\n", + " 55 | theorem card_eq_permanent (B : Matrix (Fin n) (Fin n) Bool) :\n", + " 56 | (perfectMatchingSet B).card = (adjMatrix B).permanent := by\n", + " 57 | classical\n", + "\n", + "--- lignes 74-80 ---\n", + " 74 | /-- Corollaire du pont sur le graphe complet : le permanent de la matrice\n", + " 75 | tout-un est le factoriel de n (temoin croise avec `Fintype.card_perm`). -/\n", + " 76 | theorem permanent_complete_eq_factorial (B : Matrix (Fin n) (Fin n) Bool)\n", + " 77 | (h : ∀ i j, B i j) :\n", + " 78 | (adjMatrix B).permanent = Nat.factorial (Fintype.card (Fin n)) := by\n", + " 79 | rw [← card_eq_permanent B, card_eq_factorial B h, Finset.card_univ,\n", + " 80 | Fintype.card_perm]\n", + "\n" + ] + } + ], + "source": [ + "# Lecture du socle : Counting.lean (tranche A, #21962) — extraits numérotés.\n", + "COUNTING_WIN = os.path.join(os.getcwd(), \"..\", \"..\", \"..\",\n", + " \"GameTheory\", \"assignment_lean\", \"Assignment\", \"Counting.lean\")\n", + "lines = open(COUNTING_WIN, encoding=\"utf-8\").read().splitlines()\n", + "print(\"fichier :\", os.path.relpath(COUNTING_WIN, os.getcwd()), f\"({len(lines)} lignes)\")\n", + "print()\n", + "for a, b in [(23, 32), (50, 57), (74, 80)]:\n", + " print(f\"--- lignes {a}-{b} ---\")\n", + " for k in range(a - 1, b):\n", + " print(f\"{k + 1:3d} | {lines[k]}\")\n", + " print()" + ] + }, + { + "cell_type": "markdown", + "id": "b8655a2f-bd39-4534-919f-3cf760169746", + "metadata": { + "papermill": { + "duration": 0.002056, + "end_time": "2026-10-22T13:21:07.533743+00:00", + "exception": false, + "start_time": "2026-10-22T13:21:07.531687+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Reading the foundation\n", + "\n", + "Both local definitions bridge graphs and algebra: `adjMatrix` (0/1 <- Bool) and `perfectMatchingSet` (the covered permutations, as a `Finset`). The statement `card_eq_permanent` says exactly the announced equality; the corollary `permanent_complete_eq_factorial` confronts it with the factorial on the complete graph — a cross-witness with `Fintype.card_perm`. The proof (visible in the file) rewrites the cardinal filter as a sum of indicators and then recognises the definition of the permanent, relying on `Matrix.permanent_transpose` — no hidden computation." + ] + }, + { + "cell_type": "code", + "id": "7ce3bb41-9aca-464c-ab66-dcb67251db41", + "execution_count": 3, + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-22T13:21:07.539070Z", + "iopub.status.busy": "2026-10-22T13:21:07.538796Z", + "iopub.status.idle": "2026-10-22T13:27:26.853243Z", + "shell.execute_reply": "2026-10-22T13:27:26.852212Z" + }, + "papermill": { + "duration": 379.320169, + "end_time": "2026-10-22T13:27:26.856110+00:00", + "exception": false, + "start_time": "2026-10-22T13:21:07.535941+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "@Assignment.card_eq_permanent : ∀ {n : ℕ} (B : Matrix (Fin n) (Fin n) Bool),\n", + " (Assignment.perfectMatchingSet B).card = (Assignment.adjMatrix B).permanent\n", + "@Assignment.perfectMatchingSet : {n : ℕ} → Matrix (Fin n) (Fin n) Bool → Finset (Equiv.Perm (Fin n))\n", + "@Assignment.adjMatrix : {n : ℕ} → Matrix (Fin n) (Fin n) Bool → Matrix (Fin n) (Fin n) ℕ\n", + "@Matrix.permanent_zero : ∀ {n : Type u_1} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type u_2}\n", + " [inst_2 : CommSemiring R] [Nonempty n], Matrix.permanent 0 = 0\n", + "@Matrix.permanent_one : ∀ {n : Type u_1} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type u_2}\n", + " [inst_2 : CommSemiring R], Matrix.permanent 1 = 1\n", + "@Matrix.permanent_transpose : ∀ {n : Type u_1} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type u_2}\n", + " [inst_2 : CommSemiring R] (M : Matrix n n R), M.transpose.permanent = M.permanent\n", + "'Assignment.card_eq_permanent' depends on axioms: [propext, Classical.choice, Quot.sound]\n", + "'Matrix.permanent_transpose' depends on axioms: [propext, Classical.choice, Quot.sound]\n", + "\n", + "rc = 0\n" + ] + } + ], + "source": [ + "# Vérification formelle depuis le lac : signatures + axiomes (lake env lean).\n", + "probe1 = '''import Assignment.Counting\n", + "\n", + "#check @Assignment.card_eq_permanent\n", + "#check @Assignment.perfectMatchingSet\n", + "#check @Assignment.adjMatrix\n", + "#check @Matrix.permanent_zero\n", + "#check @Matrix.permanent_one\n", + "#check @Matrix.permanent_transpose\n", + "#print axioms Assignment.card_eq_permanent\n", + "#print axioms Matrix.permanent_transpose\n", + "'''\n", + "probe_name = \"_analyse12_probe1.lean\"\n", + "try:\n", + " with open(probe_name, \"w\", encoding=\"utf-8\", newline=\"\\n\") as f:\n", + " f.write(probe1)\n", + " probe_wsl = subprocess.run([\"wsl\", \"wslpath\", \"-a\",\n", + " (os.getcwd() + os.sep + probe_name).replace(\"\\\\\", \"/\")],\n", + " capture_output=True, text=True, encoding=\"utf-8\",\n", + " errors=\"replace\").stdout.strip()\n", + " r = subprocess.run([\"wsl\", \"-e\", \"bash\", \"-lc\",\n", + " \"cd \" + LAKE_DIR + \" && timeout 850 lake env lean \" + probe_wsl + \" 2>&1\"],\n", + " capture_output=True, text=True, encoding=\"utf-8\",\n", + " errors=\"replace\", timeout=900)\n", + " print(r.stdout)\n", + " print(\"rc =\", r.returncode)\n", + "finally:\n", + " if os.path.exists(probe_name):\n", + " os.remove(probe_name)" + ] + }, + { + "cell_type": "markdown", + "id": "1f693439-3d62-4713-831f-c71cfacab3bd", + "metadata": { + "papermill": { + "duration": 0.011385, + "end_time": "2026-10-22T13:27:26.870601+00:00", + "exception": false, + "start_time": "2026-10-22T13:27:26.859216+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Reading the `#check`s and `#print axioms`\n", + "\n", + "The signatures are the expected ones: `card_eq_permanent` speaks about the cardinality of the `Finset` of covered permutations against the permanent **of the adjacency** (a `ℕ` matrix), and Mathlib's two native controls are **argument-free** statements (`permanent 0 = 0`, `permanent 1 = 1`).\n", + "\n", + "The axioms: `card_eq_permanent` depends only on Mathlib's three standard axioms (`propext`, `Classical.choice`, `Quot.sound`) — **no `sorryAx`** (no hole), **no `Lean.ofReduceBool`** (no native decision without proof). That is the formal-integrity witness of link 2." + ] + }, + { + "cell_type": "markdown", + "id": "6c5d6815-5b22-4382-94e9-e6baa51bbbb6", + "metadata": { + "papermill": { + "duration": 0.002004, + "end_time": "2026-10-22T13:27:26.874981+00:00", + "exception": false, + "start_time": "2026-10-22T13:27:26.872977+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 4. The permanent by brute-force enumeration — the Python cross-check\n", + "\n", + "The Python path is deliberately **naive and independent** of the lake: `permanent_def` applies the definition (sum over `itertools.permutations` of products), `count_matchings` counts perfect matchings directly (boolean test of the edges). Two disjoint code paths that must return the same number — then an **exhaustive** confrontation over the whole space of 0/1 matrices for $n \\le 3$." + ] + }, + { + "cell_type": "code", + "id": "fa6a5315-aea5-4297-9d3a-62a03dc560bd", + "execution_count": 4, + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-22T13:27:26.880510Z", + "iopub.status.busy": "2026-10-22T13:27:26.880308Z", + "iopub.status.idle": "2026-10-22T13:27:26.886642Z", + "shell.execute_reply": "2026-10-22T13:27:26.886186Z" + }, + "papermill": { + "duration": 0.009362, + "end_time": "2026-10-22T13:27:26.887168+00:00", + "exception": false, + "start_time": "2026-10-22T13:27:26.877806+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "graphe témoin permanent_def count_matchings\n", + "---------------------------------------------------------\n", + "K3,3 (complet) 6 6 accord\n", + "B3 (6 arêtes) 2 2 accord\n", + "bloc K2,2 + K2,2 4 4 accord\n", + "cycle C4 2 2 accord\n", + "vide (3x3) 0 0 accord\n", + "identité I3 1 1 accord\n", + "\n", + "K3,3 = 6 — le factoriel prédit par permanent_complete_eq_factorial (lignes 74-80 ci-dessus).\n" + ] + } + ], + "source": [ + "# Le permanent par définition, le comptage direct des couplages, et une galerie de témoins.\n", + "from itertools import permutations\n", + "import math\n", + "\n", + "def permanent_def(M):\n", + " n = len(M)\n", + " return sum(math.prod(M[i][s[i]] for i in range(n)) for s in permutations(range(n)))\n", + "\n", + "def count_matchings(M):\n", + " n = len(M)\n", + " return sum(1 for s in permutations(range(n)) if all(M[i][s[i]] for i in range(n)))\n", + "\n", + "def edges_to_matrix(n, edges):\n", + " M = [[0] * n for _ in range(n)]\n", + " for i, j in edges:\n", + " M[i][j] = 1\n", + " return M\n", + "\n", + "K33 = edges_to_matrix(3, [(i, j) for i in range(3) for j in range(3)])\n", + "B3 = edges_to_matrix(3, [(0, 0), (0, 2), (1, 0), (1, 1), (2, 1), (2, 2)])\n", + "BLOC4 = edges_to_matrix(4, [(0, 0), (0, 1), (1, 0), (1, 1), (2, 2), (2, 3), (3, 2), (3, 3)])\n", + "CYC4 = edges_to_matrix(4, [(i, i) for i in range(4)] + [(i, (i + 1) % 4) for i in range(4)])\n", + "VIDE3 = edges_to_matrix(3, [])\n", + "ID3 = edges_to_matrix(3, [(i, i) for i in range(3)])\n", + "\n", + "print(f\"{'graphe témoin':<24}{'permanent_def':>14}{'count_matchings':>17}\")\n", + "print(\"-\" * 57)\n", + "for nom, M in [(\"K3,3 (complet)\", K33), (\"B3 (6 arêtes)\", B3),\n", + " (\"bloc K2,2 + K2,2\", BLOC4), (\"cycle C4\", CYC4),\n", + " (\"vide (3x3)\", VIDE3), (\"identité I3\", ID3)]:\n", + " p, c = permanent_def(M), count_matchings(M)\n", + " print(f\"{nom:<24}{p:>14}{c:>17} {'accord' if p == c else 'ÉCART'}\")\n", + "print()\n", + "print(\"K3,3 =\", math.factorial(3), \"— le factoriel prédit par permanent_complete_eq_factorial (lignes 74-80 ci-dessus).\")" + ] + }, + { + "cell_type": "markdown", + "id": "3a2fb8b0-6ae1-4807-9161-698cfbb055aa", + "metadata": { + "papermill": { + "duration": 0.002341, + "end_time": "2026-10-22T13:27:26.891816+00:00", + "exception": false, + "start_time": "2026-10-22T13:27:26.889475+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Reading the result\n", + "\n", + "The two Python paths agree on the whole gallery, and the values illustrate the theory: the complete graph returns $3! = 6$ (the lake's corollary), the **empty** graph returns $0$ (no matching — the content of `permanent_zero` in §6), the identity returns $1$ (`permanent_one`), and the block $K_{2,2} \\oplus K_{2,2}$ returns $2 \\times 2 = 4$: counting is **multiplicative over disjoint unions** — a property a polynomial \"finder\" does not need." + ] + }, + { + "cell_type": "code", + "id": "571ecf04-8d60-4e56-ac25-275e6b542927", + "execution_count": 5, + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-22T13:27:26.896737Z", + "iopub.status.busy": "2026-10-22T13:27:26.896590Z", + "iopub.status.idle": "2026-10-22T13:27:26.907998Z", + "shell.execute_reply": "2026-10-22T13:27:26.907335Z" + }, + "papermill": { + "duration": 0.014342, + "end_time": "2026-10-22T13:27:26.908530+00:00", + "exception": false, + "start_time": "2026-10-22T13:27:26.894188+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "530 matrices balayées (espace 0/1 complet pour n <= 3, transposées incluses) : 0 écart(s)\n" + ] + } + ], + "source": [ + "# Confrontation exhaustive : TOUTES les matrices 0/1 pour n <= 3, plus la symétrie\n", + "# par transposée (pendant Python de Matrix.permanent_transpose).\n", + "ecarts = 0\n", + "total = 0\n", + "for n in [1, 2, 3]:\n", + " for bits in range(2 ** (n * n)):\n", + " M = [[(bits >> (i * n + j)) & 1 for j in range(n)] for i in range(n)]\n", + " total += 1\n", + " if permanent_def(M) != count_matchings(M):\n", + " ecarts += 1\n", + " if permanent_def(M) != permanent_def([list(r) for r in zip(*M)]):\n", + " ecarts += 1\n", + "print(f\"{total} matrices balayées (espace 0/1 complet pour n <= 3, transposées incluses) : {ecarts} écart(s)\")" + ] + }, + { + "cell_type": "markdown", + "id": "d4513a33-0ff6-45bd-977f-4aa80156bcee", + "metadata": { + "papermill": { + "duration": 0.001816, + "end_time": "2026-10-22T13:27:26.912265+00:00", + "exception": false, + "start_time": "2026-10-22T13:27:26.910449+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Reading the confrontation\n", + "\n", + "Over the **complete** space of small instances (every 0/1 matrix up to $n = 3$, i.e. exhaustive enumeration rather than a sample), the equality permanent = count never wavers, and the transpose symmetry holds — the computational counterpart of `Matrix.permanent_transpose`, which the bridge proof uses. This is not a proof of the bridge (that is the role of link 2), but it is object-error detection: the formalisation counts what we think it counts." + ] + }, + { + "cell_type": "markdown", + "id": "34ea121d-2492-4dab-b8e8-18de6e0b909b", + "metadata": { + "papermill": { + "duration": 0.002846, + "end_time": "2026-10-22T13:27:26.917817+00:00", + "exception": false, + "start_time": "2026-10-22T13:27:26.914971+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 5. The bridge confronted — Lean `#eval` against Python enumeration\n", + "\n", + "The decisive test: Lean **evaluates** (`#eval`) the cardinality of `perfectMatchingSet` and the permanent of the adjacency on the concrete witnesses, then Python reads those values back and compares them with its own enumeration. The two literal matrices (`B3`, `BLOC4`) are written once on the Lean side — the notebook requires them to describe the same graphs as the edge lists of §4." + ] + }, + { + "cell_type": "code", + "id": "70c6f5b8-77a6-4ee0-8e16-fd46960a7421", + "execution_count": 6, + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-22T13:27:26.924782Z", + "iopub.status.busy": "2026-10-22T13:27:26.924485Z", + "iopub.status.idle": "2026-10-22T13:33:43.313937Z", + "shell.execute_reply": "2026-10-22T13:33:43.312988Z" + }, + "papermill": { + "duration": 376.394704, + "end_time": "2026-10-22T13:33:43.315441+00:00", + "exception": false, + "start_time": "2026-10-22T13:27:26.920737+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "2\n", + "2\n", + "4\n", + "4\n", + "\n", + "quantité Lean #eval Python verdict\n", + "card(perfectMatchingSet B3) 2 2 accord\n", + "permanent(adjMatrix B3) 2 2 accord\n", + "card(perfectMatchingSet BLOC4) 4 4 accord\n", + "permanent(adjMatrix BLOC4) 4 4 accord\n", + "\n", + "pont card_eq_permanent recoupé sur les témoins : 4/4 accords\n" + ] + } + ], + "source": [ + "# Le pont mesuré des deux côtés : #eval Lean vs énumération Python (B3, BLOC4).\n", + "B3_LEAN = \"!![true, false, true; true, true, false; false, true, true]\"\n", + "BLOC4_LEAN = (\"!![true, true, false, false; \"\n", + " \"true, true, false, false; \"\n", + " \"false, false, true, true; \"\n", + " \"false, false, true, true]\")\n", + "probe2 = f'''import Assignment.Counting\n", + "open Assignment\n", + "def B3L : Matrix (Fin 3) (Fin 3) Bool := {B3_LEAN}\n", + "def BLOC4L : Matrix (Fin 4) (Fin 4) Bool := {BLOC4_LEAN}\n", + "#eval (perfectMatchingSet B3L).card\n", + "#eval (adjMatrix B3L).permanent\n", + "#eval (perfectMatchingSet BLOC4L).card\n", + "#eval (adjMatrix BLOC4L).permanent\n", + "'''\n", + "probe_name = \"_analyse12_probe2.lean\"\n", + "try:\n", + " with open(probe_name, \"w\", encoding=\"utf-8\", newline=\"\\n\") as f:\n", + " f.write(probe2)\n", + " probe_wsl = subprocess.run([\"wsl\", \"wslpath\", \"-a\",\n", + " (os.getcwd() + os.sep + probe_name).replace(\"\\\\\", \"/\")],\n", + " capture_output=True, text=True, encoding=\"utf-8\",\n", + " errors=\"replace\").stdout.strip()\n", + " r = subprocess.run([\"wsl\", \"-e\", \"bash\", \"-lc\",\n", + " \"cd \" + LAKE_DIR + \" && timeout 850 lake env lean \" + probe_wsl + \" 2>&1\"],\n", + " capture_output=True, text=True, encoding=\"utf-8\",\n", + " errors=\"replace\", timeout=900)\n", + " print(r.stdout)\n", + " lean_vals = [int(l) for l in r.stdout.splitlines() if l.strip().isdigit()]\n", + "finally:\n", + " if os.path.exists(probe_name):\n", + " os.remove(probe_name)\n", + "\n", + "py_vals = [count_matchings(B3), permanent_def(B3), count_matchings(BLOC4), permanent_def(BLOC4)]\n", + "noms = [\"card(perfectMatchingSet B3)\", \"permanent(adjMatrix B3)\",\n", + " \"card(perfectMatchingSet BLOC4)\", \"permanent(adjMatrix BLOC4)\"]\n", + "print(f\"{'quantité':<34}{'Lean #eval':>12}{'Python':>9} verdict\")\n", + "accords = 0\n", + "for nom, lv, pv in zip(noms, lean_vals, py_vals):\n", + " ok = lv == pv\n", + " accords += ok\n", + " print(f\"{nom:<34}{lv:>12}{pv:>9} {'accord' if ok else 'ÉCART'}\")\n", + "print()\n", + "print(f\"pont card_eq_permanent recoupé sur les témoins : {accords}/4 accords\")" + ] + }, + { + "cell_type": "markdown", + "id": "d0ddbd6a-fd7d-4ba8-ab1d-9b71027b4718", + "metadata": { + "papermill": { + "duration": 0.001889, + "end_time": "2026-10-22T13:33:43.320583+00:00", + "exception": false, + "start_time": "2026-10-22T13:33:43.318694+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Reading the measured bridge\n", + "\n", + "The four quantities agree: the cardinality **computed by the Lean kernel** from the lake's set-theoretic definition and the permanent **computed by the Mathlib definition** return exactly the numbers of the Python enumeration. The bridge is not a coincidence of statements — both sides compute the same thing on independent implementations (Lean kernel against Python interpreter)." + ] + }, + { + "cell_type": "markdown", + "id": "bdae367c-2112-4dae-97f8-8224df4620c5", + "metadata": { + "papermill": { + "duration": 0.002301, + "end_time": "2026-10-22T13:33:43.325370+00:00", + "exception": false, + "start_time": "2026-10-22T13:33:43.323069+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 6. The native negative controls — `permanent_zero` and `permanent_one`\n", + "\n", + "Mathlib itself supplies the two guarantees of meaning for counting: a **null** matrix has a **null** permanent (no matching in an edgeless graph), and the **identity** matrix has a permanent **equal to 1** (exactly one perfect matching: the identity permutation). These are theorems **proved** in the organ — the notebook re-declares them as `example` (proof: the native lemma, argument-free) and confronts them with the same graphs on the Python side." + ] + }, + { + "cell_type": "code", + "id": "95f93a3e-dd84-422e-b2f2-0c55093880ef", + "execution_count": 7, + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-22T13:33:43.331125Z", + "iopub.status.busy": "2026-10-22T13:33:43.330938Z", + "iopub.status.idle": "2026-10-22T13:39:24.067451Z", + "shell.execute_reply": "2026-10-22T13:39:24.066788Z" + }, + "papermill": { + "duration": 340.741432, + "end_time": "2026-10-22T13:39:24.069207+00:00", + "exception": false, + "start_time": "2026-10-22T13:33:43.327775+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "@permanent_zero : ∀ {n : Type u_1} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type u_2} [inst_2 : CommSemiring R]\n", + " [Nonempty n], permanent 0 = 0\n", + "@permanent_one : ∀ {n : Type u_1} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type u_2} [inst_2 : CommSemiring R],\n", + " permanent 1 = 1\n", + "0\n", + "1\n", + "0\n", + "1\n", + "'Matrix.permanent_zero' depends on axioms: [propext, Classical.choice, Quot.sound]\n", + "'Matrix.permanent_one' depends on axioms: [propext, Classical.choice, Quot.sound]\n", + "\n", + "contre-épreuve Python : permanent_def(VIDE3) = 0 | count_matchings(VIDE3) = 0 | permanent_def(ID3) = 1 | count_matchings(ID3) = 1\n" + ] + } + ], + "source": [ + "# Contrôles négatifs natifs Mathlib + contre-épreuve Python (graphe vide, identité).\n", + "probe3 = '''import Assignment.Counting\n", + "open Matrix Assignment\n", + "#check @Matrix.permanent_zero\n", + "#check @Matrix.permanent_one\n", + "example : (0 : Matrix (Fin 3) (Fin 3) ℕ).permanent = 0 := Matrix.permanent_zero\n", + "example : (1 : Matrix (Fin 3) (Fin 3) ℕ).permanent = 1 := Matrix.permanent_one\n", + "#eval (adjMatrix (!![false, false, false; false, false, false; false, false, false])).permanent\n", + "#eval (adjMatrix (!![true, false, false; false, true, false; false, false, true])).permanent\n", + "#eval (perfectMatchingSet (!![false, false, false; false, false, false; false, false, false])).card\n", + "#eval (perfectMatchingSet (!![true, false, false; false, true, false; false, false, true])).card\n", + "#print axioms Matrix.permanent_zero\n", + "#print axioms Matrix.permanent_one\n", + "'''\n", + "probe_name = \"_analyse12_probe3.lean\"\n", + "try:\n", + " with open(probe_name, \"w\", encoding=\"utf-8\", newline=\"\\n\") as f:\n", + " f.write(probe3)\n", + " probe_wsl = subprocess.run([\"wsl\", \"wslpath\", \"-a\",\n", + " (os.getcwd() + os.sep + probe_name).replace(\"\\\\\", \"/\")],\n", + " capture_output=True, text=True, encoding=\"utf-8\",\n", + " errors=\"replace\").stdout.strip()\n", + " r = subprocess.run([\"wsl\", \"-e\", \"bash\", \"-lc\",\n", + " \"cd \" + LAKE_DIR + \" && timeout 850 lake env lean \" + probe_wsl + \" 2>&1\"],\n", + " capture_output=True, text=True, encoding=\"utf-8\",\n", + " errors=\"replace\", timeout=900)\n", + " print(r.stdout)\n", + "finally:\n", + " if os.path.exists(probe_name):\n", + " os.remove(probe_name)\n", + "\n", + "print(\"contre-épreuve Python : permanent_def(VIDE3) =\", permanent_def(VIDE3),\n", + " \"| count_matchings(VIDE3) =\", count_matchings(VIDE3),\n", + " \"| permanent_def(ID3) =\", permanent_def(ID3),\n", + " \"| count_matchings(ID3) =\", count_matchings(ID3))" + ] + }, + { + "cell_type": "markdown", + "id": "e6ad2332-9b17-446c-9fd6-5050d68c811d", + "metadata": { + "papermill": { + "duration": 0.002042, + "end_time": "2026-10-22T13:39:24.073968+00:00", + "exception": false, + "start_time": "2026-10-22T13:39:24.071926+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Reading the controls\n", + "\n", + "The `example`s compile: both native statements apply **as they are** to the concrete sizes (no argument to supply — they are closed equalities). The `#eval`s return `0` and `1` as expected, and the Python counter-check on the same graphs (`VIDE3`, `ID3` from §4) gives the same numbers. The axioms of both native lemmas are the three standard ones — the counting controls rest on nothing stronger than the bridge itself." + ] + }, + { + "cell_type": "markdown", + "id": "655b9ccc-7baf-4191-b9ce-e684f7c3e1a3", + "metadata": { + "papermill": { + "duration": 0.001645, + "end_time": "2026-10-22T13:39:24.077487+00:00", + "exception": false, + "start_time": "2026-10-22T13:39:24.075842+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 7. Epistemic status per family — 113, 126, 104\n", + "\n", + "Doctrine of Epic #19898: every statement inherited from `openai/math` carries its status, **per family**. Never \"OpenAI proved X, therefore X\".\n", + "\n", + "### Family 113 — counting perfect matchings (FPRAS, `#P`)\n", + "\n", + "- **Classical literature, cited**: the `#P`-completeness of counting bipartite perfect matchings (Valiant, 1979) and the existence of a randomised FPRAS (Jerrum–Sinclair–Vigoda, 2004) are published, peer-reviewed theorems, cited here at the level of their statement — this repository does not re-prove them.\n", + "- **`openai/math` (reported)**: family 113 of the authors' repository publishes a `lean/docs` skeleton for this counting thread. Status: **reported** — skeleton published by the authors, not verified by this repository.\n", + "- **What this repository proves**: the local bridge `card_eq_permanent` (link 2, standard axioms, §3) — the formal entry point of counting, not the complexity bounds.\n", + "\n", + "### Family 126 — SDP closure of the matching polytope\n", + "\n", + "- **Negative** result (no compact semidefinite lift); same reading grid: statement cited from the literature, `openai/math` skeleton **reported**, nothing verified locally beyond the bridge that defines the counted object.\n", + "\n", + "### Family 104 — on watch\n", + "\n", + "- No treatment in this fold; mentioned for the memory of the landscape." + ] + }, + { + "cell_type": "markdown", + "id": "8c477b11-ac01-4ef2-b01a-9ceca5729f9a", + "metadata": { + "papermill": { + "duration": 0.001688, + "end_time": "2026-10-22T13:39:24.080977+00:00", + "exception": false, + "start_time": "2026-10-22T13:39:24.079289+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 8. Friction and discovery path\n", + "\n", + "Three real frictions met while writing this notebook, kept because they teach the method:\n", + "\n", + "1. **Signatures are probed, not guessed.** The first draft of the `example` control applied an argument to `Matrix.permanent_zero` (`permanent_zero _`) — a `#check` probe revealed that the native statement is **closed** (`permanent 0 = 0`, no quantifier over the matrix). One probe cycle beats one failed notebook-execution cycle.\n", + "2. **The lake's entry cost is the Mathlib import.** Every `lake env lean` probe pays the import (measured: ~5 min per probe through the WSL /mnt/d mount, seconds on a lake in a native filesystem) — so the probes are **grouped** into three files rather than scattered per cell, with a timeout sized for the cold import (850 s).\n", + "3. **Two literals for one graph.** The witnesses exist on the Lean side (`!![...]` literals) and on the Python side (edge lists); the notebook enforces the discipline of writing them **side by side in the same cell** so that de-synchronisation stays visible." + ] + }, + { + "cell_type": "markdown", + "id": "14b7fe45-222b-471f-bbe3-37c148dcbc9a", + "metadata": { + "papermill": { + "duration": 0.001585, + "end_time": "2026-10-22T13:39:24.084253+00:00", + "exception": false, + "start_time": "2026-10-22T13:39:24.082668+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 9. Exercises\n", + "\n", + "Three exercises, from computation to meaning. Series convention: stubs without deliberate errors — the notebook runs end to end even when unfinished." + ] + }, + { + "cell_type": "code", + "id": "cecd3835-e44e-4fa0-9d50-83abee3fa018", + "execution_count": 8, + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-22T13:39:24.090260Z", + "iopub.status.busy": "2026-10-22T13:39:24.090081Z", + "iopub.status.idle": "2026-10-22T13:39:24.092870Z", + "shell.execute_reply": "2026-10-22T13:39:24.092346Z" + }, + "papermill": { + "duration": 0.005711, + "end_time": "2026-10-22T13:39:24.093359+00:00", + "exception": false, + "start_time": "2026-10-22T13:39:24.087648+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Exercice a completer\n" + ] + } + ], + "source": [ + "# Exercice 1 -- Ryser : le permanent par inclusion-exclusion (a completer)\n", + "# But : evaluer le permanent SANS enumerer les n! permutations -- par la formule de\n", + "# Ryser : perm(M) = (-1)^n * sum_{S sous-ensemble non vide des colonnes} (-1)^{|S|} * prod_i (sum_{j in S} M[i][j])\n", + "# Etape 1 : implementer ryser(M) avec itertools.combinations (ou un balayage de bits).\n", + "# Etape 2 : verifier que ryser coincide avec permanent_def sur TOUS les temoins du\n", + "# paragraphe 4 (K33, B3, BLOC4, CYC4, VIDE3, ID3).\n", + "# Indice : pour n <= 6, le balayage des 2^n - 1 sous-ensembles est immediat.\n", + "def ryser(M):\n", + " # TODO etudiant\n", + " return None\n", + "\n", + "print(\"Exercice a completer\")" + ] + }, + { + "cell_type": "markdown", + "id": "8556e0c3-66e0-437a-a324-e3022c71291d", + "metadata": { + "papermill": { + "duration": 0.001778, + "end_time": "2026-10-22T13:39:24.097025+00:00", + "exception": false, + "start_time": "2026-10-22T13:39:24.095247+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Exercise 2 — Union of two cycles: predict, then measure\n", + "\n", + "A 2-regular bipartite graph is a union of even cycles; each cycle $C_{2k}$ carries exactly two perfect matchings. **Before measuring**: how many perfect matchings for the union of two $C_4$ ($n = 8$)? Then build the matrix and check." + ] + }, + { + "cell_type": "code", + "id": "a1ea2700-1248-4b9e-b59a-d8acbb6fb651", + "execution_count": 9, + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-22T13:39:24.101442Z", + "iopub.status.busy": "2026-10-22T13:39:24.101256Z", + "iopub.status.idle": "2026-10-22T13:39:24.103989Z", + "shell.execute_reply": "2026-10-22T13:39:24.103477Z" + }, + "papermill": { + "duration": 0.005587, + "end_time": "2026-10-22T13:39:24.104407+00:00", + "exception": false, + "start_time": "2026-10-22T13:39:24.098820+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Exercice a completer\n" + ] + } + ], + "source": [ + "# Exercice 2 -- union de deux C4 (n=8) : PREDIRE le compte, puis MESURER (a completer)\n", + "# Etape 1 : construire la matrice 8x8 de l'union de deux cycles C4 :\n", + "# cycle 1 sur les sommets 0-3 (colonnes 0-3), cycle 2 sur les sommets 4-7 (colonnes 4-7),\n", + "# chaque cycle reliant i a i et (i+1) mod 4 dans son bloc.\n", + "# Etape 2 : noter la prediction ici (en commentaire), puis mesurer avec count_matchings\n", + "# et permanent_def -- les trois valeurs doivent coherir.\n", + "def union_deux_c4():\n", + " # TODO etudiant\n", + " return None\n", + "\n", + "print(\"Exercice a completer\")" + ] + }, + { + "cell_type": "markdown", + "id": "c2f8e71c-78d1-42a9-a128-b7330a8de5f0", + "metadata": { + "papermill": { + "duration": 0.002553, + "end_time": "2026-10-22T13:39:24.109044+00:00", + "exception": false, + "start_time": "2026-10-22T13:39:24.106491+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Exercise 3 — The limit of the bridge: negative entries\n", + "\n", + "The bridge `card_eq_permanent` lives on 0/1 adjacency matrices. What becomes of the counting interpretation when the permanent is evaluated on a matrix with arbitrary coefficients — for instance a $-1$ entry? Measure, then explain why the bridge proof (products of indicators) does not extend." + ] + }, + { + "cell_type": "code", + "id": "c8d2ce81-7c80-4095-95eb-a238572c9ed4", + "execution_count": 10, + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-22T13:39:24.115927Z", + "iopub.status.busy": "2026-10-22T13:39:24.115713Z", + "iopub.status.idle": "2026-10-22T13:39:24.119152Z", + "shell.execute_reply": "2026-10-22T13:39:24.118517Z" + }, + "papermill": { + "duration": 0.008073, + "end_time": "2026-10-22T13:39:24.120001+00:00", + "exception": false, + "start_time": "2026-10-22T13:39:24.111928+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Exercice a completer\n" + ] + } + ], + "source": [ + "# Exercice 3 -- une entree negative : le permanent compte-t-il encore ? (a completer)\n", + "M_neg = [[1, 1], [-1, 1]]\n", + "# Etape 1 : evaluer permanent_def(M_neg) et decrire le resultat (signe, valeur).\n", + "# Etape 2 : en une phrase (en commentaire), expliquer pourquoi ce nombre n'est PLUS\n", + "# un compte de couplages -- quel maillon de la preuve du pont (produits d'indicateurs 0/1)\n", + "# casse avec une entree negative ?\n", + "print(\"Exercice a completer\")" + ] + }, + { + "cell_type": "markdown", + "id": "635090bd-e354-4ddf-b572-e9cefb31a5bc", + "metadata": { + "papermill": { + "duration": 0.002482, + "end_time": "2026-10-22T13:39:24.125206+00:00", + "exception": false, + "start_time": "2026-10-22T13:39:24.122724+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 10. Conclusion\n", + "\n", + "- **What the repository now knows**: the Mathlib permanent of the adjacency matrix equals the number of perfect matchings — a bridge **proved** (tranche A), **verified** here by signatures, axioms and `#eval` cross-checked against exhaustive Python enumeration on small instances.\n", + "- **What this notebook cites without proving**: `#P`-completeness (Valiant), the FPRAS (JSV), the SDP frontier (family 126) — status per family in §7; the `openai/math` skeleton of family 113 remains **reported**.\n", + "- **What counting has over finding**: the gallery of §4 shows it on one example — counting is multiplicative over disjoint unions, it distinguishes graphs that are equally \"coverable\", and it is precisely that richness which places it in `#P` while existence remains polynomial.\n", + "\n", + "The local link is closed; the complexity frontier remains a cited statement — and that is exactly the distinction the ANALYSE series exists to hold." + ] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3 (ipykernel)", + "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/Lean/ANALYSE/README.md b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/README.md index 6155e8ae8aa..d1f8b8c274a 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/README.md +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/README.md @@ -14,13 +14,13 @@ La série principale garde son tutoriel (numéros 1 à 14) ; le présent dossier | [ANALYSE-04-PFR-Primitives-Python](ANALYSE-04-PFR-Primitives-Python.ipynb) | Trois primitives de PFR, et l'endroit exact où elles cessent de valoir — companion de digestion de ANALYSE-03 : ce qui se transporte hors du cadre d'origine (#12214) | 30 min | | [ANALYSE-05-KLS-Lean-Python](ANALYSE-05-KLS-Lean-Python.ipynb) | La conjecture KLS démontrée (Bizeul–Klartag–Lehec, arXiv:2610.05474) : énoncé (Théorème 1.1), chaîne de la preuve en cinq maillons (thin-shell, germe quadratique, localisation stochastique, suspension, critère de Song–Zhang), lac local `kls_lean` — audit Mathlib au pin, six définitions, deux théorèmes prouvés (0 sorry, `#print axioms` propre) — thin-shell en Monte-Carlo avec saturation exacte à 8n par l'exponentielle produit, banc 1-lipschitzien minorant `poincareConstant` | 45 min | | [ANALYSE-06-Sensibilite-2026-Lean](ANALYSE-06-Sensibilite-2026-Lean.ipynb) | La combinatoire booléenne 2026 d'openai/math (familles 127/132/186/192) lue depuis notre lac `Sensitivity` : Huang prouvé chez nous (`#check`/`#print axioms`), énoncés 2026 cités avec leur statut épistémique, et nos séparations sensibilité/sensibilité de bloc du module `Sensitivity.Separations`, prouvées et calculées (`#eval` natif, Pli 2 d'Origami #19898) ; jumeau anglais à code byte-identique : [ANALYSE-06-...-_en](ANALYSE-06-Sensibilite-2026-Lean_en.ipynb) | 35 min | -| [ANALYSE-07-Percolation-Critique](ANALYSE-07-Percolation-Critique.ipynb) | Percolation critique et Ising sur l'arbre d-régulier — pli 3 de la digestion Origami (#19898) : les inégalités de Harris–Kleitman `#check`ées dans notre lac `percolation_lean`, les familles 2026 **213** (criticité Benjamini–Schramm) et **236** (seuil factor-of-IID de l'Ising sur l'arbre) citées avec leur statut, et deux calculs nôtres **exacts** — la probabilité critique p_c = 1/(d-1) par Galton–Watson (point fixe non trivial 4/9, vérifiable à la main) et l'écart entre seuil de reconstruction et seuil d'aimantation | 40 min | +| [ANALYSE-07-Percolation-Critique](ANALYSE-07-Percolation-Critique.ipynb) | Percolation critique et Ising sur l'arbre d-régulier — pli 3 de la digestion Origami (#19898) : les inégalités de Harris–Kleitman `#check`ées dans notre lac `percolation_lean`, les familles 2026 **213** (criticité Benjamini–Schramm) et **236** (seuil factor-of-IID de l'Ising sur l'arbre) citées avec leur statut, et deux calculs nôtres **exacts** — la probabilité critique p_c = 1/(d-1) par Galton–Watson (point fixe non trivial 4/9, vérifiable à la main) et l'écart entre seuil de reconstruction et seuil d'aimantation ; jumeau anglais à code byte-identique : [ANALYSE-07-...-_en](ANALYSE-07-Percolation-Critique_en.ipynb) | 40 min | | [ANALYSE-08-Ramsey-VdW](ANALYSE-08-Ramsey-VdW.ipynb) | Ramsey et van der Waerden par épuisement : R(3,3)=6 et W(2,3)=9 prouvés par énumération exhaustive (survivantes 18→12→0 côté graphes, 6→0 côté progressions), le mur 2^153 où le geste meurt, et le pont probabiliste d'Erdős (#19960, pli 4 Origami #19898) | 30 min | +| [ANALYSE-09-Tuilage-Aperiodique](ANALYSE-09-Tuilage-Aperiodique.ipynb) | Famille 155 du corpus `openai/math` : un carreau de ℤ³ qui pave sans périodicité totale (contre-exemple de dimension trois). Le carnet ramène le pavage par translations à la couverture exacte que le dépôt formalise déjà (`sudoku_lean`, `ExactCover.IsExactCover`), puis mesure quatre fenêtres avec deux organes déterministes — backtracking borné `place_tiles` et rang de période `period_rank` (élimination de Gauss exacte sur ℚ) — la leçon transverse étant que la demi-fenêtre cache toute période plus longue qu'elle ; jumeau anglais à code byte-identique : [ANALYSE-09-...-_en](ANALYSE-09-Tuilage-Aperiodique_en.ipynb) | 30 min | | [Note-IA-et-preuves-2026](../Note-IA-et-preuves-2026.md) | Note transverse — les trois AI-disclosures de la résolution de KLS (octobre 2026), ce qu'elles révèlent des modes de collaboration humain-IA, et trois leçons directement applicables au dépôt (#19729 grain 3/3) | 20 min | -| [ANALYSE-05-KLS-Lean-Python](ANALYSE-05-KLS-Lean-Python.ipynb) | La conjecture KLS démontrée (Bizeul–Klartag–Lehec, arXiv:2610.05474) : énoncé (Théorème 1.1), chaîne de la preuve en cinq maillons (thin-shell, germe quadratique, localisation stochastique, suspension, critère de Song–Zhang), lac local `kls_lean` — audit Mathlib au pin, six définitions, deux théorèmes prouvés (0 sorry, `#print axioms` propre) — thin-shell en Monte-Carlo avec saturation exacte à 8n par l'exponentielle produit, banc 1-lipschitzien minorant `poincareConstant` | 45 min | | [ANALYSE-10-Reflexion-Thurston-Python](ANALYSE-10-Reflexion-Thurston-Python.ipynb) | Carnet de distillation **réflexif** : trois thèses de W. P. Thurston (*On proof and progress in mathematics*, 1994) confrontées à des données mesurées sur ce dépôt — (1) la productivité mathématique se mesure à ce que les humains portent (sorry × consommateurs de la série), (2) la fiabilité est un processus social (densité d'agents et de rôles dans les traces du prover multi-agents), (3) comprendre n'est pas produire une preuve (ratio digestion Python / formalisation Lean) | carnet long (lecture sériée recommandée) | | [ANALYSE-11-Synthese-Transverse-Digestions-Python](ANALYSE-11-Synthese-Transverse-Digestions-Python.ipynb) | Synthèse transverse des pilotes de digestion (Epic #13106, critère 6) : huit pilotes de familles différentes (Sendov, *Analysis I*, PFR, CHSH, Erdős, minima parasites, `knot_lean`, `grothendieck_lean`) confrontés à la grille en dix points, chaque case adossée à une ancre re-vérifiée à l'exécution. Ce qu'on y mesure : aucun pilote ne porte de revue humaine nommée, la dette en `sorry` ne prédit pas la couverture de la grille, et hors de cette sous-série les pilotes ne se citent pas. La canonicalisation n'est pas déclarée | 30 min | -| [ANALYSE-12-Comptage-Matching-Lean-Python](ANALYSE-12-Comptage-Matching-Lean-Python.ipynb) | Pli 6 de l'Epic Origami `openai/math` (#19898) : **compter** les couplages parfaits d'un graphe biparti, là où les trouver est polynomial. L'objet qui porte ce comptage est le **permanent** — cousin signe-ignorant du déterminant — et la tranche A (#21962) a posé dans le lac `assignment_lean` le pont `card_eq_permanent` : le permanent (organe Mathlib) de la matrice d'adjacence 0/1 égale le cardinal des couplages parfaits. Le carnet audite le socle à la source (signatures, `#print axioms`, contrôles négatifs natifs `permanent_zero` / `permanent_one`) puis recoupe **chaque** valeur évaluée par Lean contre l'énumération brute en Python : il vérifie que la formalisation ne s'est pas trompée d'objet, il ne prouve pas le pont. Le saut de classe (`#P`-complétude, Valiant 1979) et le FPRAS (Jerrum-Sinclair-Vigoda 2004) sont **cités**, jamais prouvés par nous | 30 min | +| [ANALYSE-12-Comptage-Matching-Lean-Python](ANALYSE-12-Comptage-Matching-Lean-Python.ipynb) | Pli 6 de l'Epic Origami `openai/math` (#19898) : **compter** les couplages parfaits d'un graphe biparti, là où les trouver est polynomial. L'objet qui porte ce comptage est le **permanent** — cousin signe-ignorant du déterminant — et la tranche A (#21962) a posé dans le lac `assignment_lean` le pont `card_eq_permanent` : le permanent (organe Mathlib) de la matrice d'adjacence 0/1 égale le cardinal des couplages parfaits. Le carnet audite le socle à la source (signatures, `#print axioms`, contrôles négatifs natifs `permanent_zero` / `permanent_one`) puis recoupe **chaque** valeur évaluée par Lean contre l'énumération brute en Python : il vérifie que la formalisation ne s'est pas trompée d'objet, il ne prouve pas le pont. Le saut de classe (`#P`-complétude, Valiant 1979) et le FPRAS (Jerrum-Sinclair-Vigoda 2004) sont **cités**, jamais prouvés par nous ; jumeau anglais à code byte-identique : [ANALYSE-12-...-_en](ANALYSE-12-Comptage-Matching-Lean-Python_en.ipynb) | 30 min | **Prérequis d'entrée** : le tutoriel de la série principale (numéros 1 à 6, tactiques et Mathlib). Le point d'entrée réel documenté du carnet 01 est [Search-03e-AStar-Optimality](../../../Search/Part1-Foundations/Search-03e-AStar-Optimality.ipynb) (heuristique A*, companion `search_lean`) — voir sa cellule d'ouverture. From cc5496ac1ae66649da92b3e58ecc9fb7fd6f185f Mon Sep 17 00:00:00 2001 From: jsboige Date: Sat, 24 Oct 2026 22:33:11 +0200 Subject: [PATCH 2/4] Fix(translation,#21958): ANALYSE-12 _en -- ids recopies, arete de navigation, constante 17->18 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Les trois check-runs bloquants du head 6e0d02cc, remede par remede. 1. `twin-parity-guard` STRUCTURE_DRIFT : les 30 `cell.id` du jumeau avaient ete regeneres (UUID) au lieu d'etre recopies du FR (ids courts). Recopies a l'identique dans l'ordre des cellules -- chirurgie textuelle sur les 30 lignes `"id":`, aucune re-serialisation JSON, code et sorties intacts. Garde : `check_twin_parity_changed.py --diff origin/main...HEAD` -> PASS. 2. `check-nav-chain` independent_chain sur la serie ANALYSE : le jumeau ne recevait aucun lien `.ipynb` entrant. Ajout de la ligne « **Version anglaise** : [ANALYSE-12 (en)](...) » dans la cellule 0 du FR12, convention exacte de FR06/FR09. Garde : `check_notebook_nav_chain.py --check --diff-base origin/main` -> OK, 0 NEW finding. 3. `Always-on guards` pair_count_declared : `EXPECTED_PAIR_COUNT` 17 -> 18, avec l'entree d'historique datee. La constante suit la mesure (#21391). Aucune cellule code touchee, aucune sortie modifiee, pas de re-execution due. Co-Authored-By: Claude Sonnet 5.5 --- ...YSE-12-Comptage-Matching-Lean-Python.ipynb | 1 + ...-12-Comptage-Matching-Lean-Python_en.ipynb | 60 +++++++++---------- .../tests/test_check_translation_parity.py | 5 +- 3 files changed, 35 insertions(+), 31 deletions(-) diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-12-Comptage-Matching-Lean-Python.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-12-Comptage-Matching-Lean-Python.ipynb index 08f0b34803f..18f9cc4bfcf 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-12-Comptage-Matching-Lean-Python.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-12-Comptage-Matching-Lean-Python.ipynb @@ -15,6 +15,7 @@ }, "source": [ "# ANALYSE-12 : Compter les couplages parfaits — le permanent comme pont, Lean d'un côté, énumération de l'autre\n", + "\n**Version anglaise** : [ANALYSE-12 (en)](ANALYSE-12-Comptage-Matching-Lean-Python_en.ipynb)\n", "\n", "Pli 6 de l'Epic Origami `openai/math` (#19898, tranche B : #21958). La série ANALYSE confronte un énoncé de recherche à ce que le dépôt sait prouver ; ici, l'énoncé est un problème de **comptage**.\n", "\n", diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-12-Comptage-Matching-Lean-Python_en.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-12-Comptage-Matching-Lean-Python_en.ipynb index c027f336a4e..feecc0ebd06 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-12-Comptage-Matching-Lean-Python_en.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-12-Comptage-Matching-Lean-Python_en.ipynb @@ -2,7 +2,7 @@ "cells": [ { "cell_type": "markdown", - "id": "9631baea-b8fd-4526-bb86-7355c8ad920c", + "id": "cd6024a7", "metadata": { "papermill": { "duration": 0.002064, @@ -41,7 +41,7 @@ }, { "cell_type": "markdown", - "id": "950ad958-51c5-4771-81eb-1140027605cd", + "id": "0b391856", "metadata": { "papermill": { "duration": 0.001667, @@ -67,7 +67,7 @@ }, { "cell_type": "markdown", - "id": "25821175-ac6f-4ac4-912c-9af03a96a1cd", + "id": "11921379", "metadata": { "papermill": { "duration": 0.001968, @@ -92,7 +92,7 @@ }, { "cell_type": "markdown", - "id": "34a72bdd-dfa4-45b8-9c1a-8218cae05f31", + "id": "fd28b15f", "metadata": { "papermill": { "duration": 0.001726, @@ -111,7 +111,7 @@ }, { "cell_type": "code", - "id": "a835132f-8d41-4652-93ca-51709b44afe4", + "id": "ff18b2b9", "execution_count": 1, "metadata": { "execution": { @@ -182,7 +182,7 @@ }, { "cell_type": "markdown", - "id": "9c90bc36-eeeb-4a1b-9813-d26c92cbc54b", + "id": "9ba0c7e9", "metadata": { "papermill": { "duration": 0.002276, @@ -203,7 +203,7 @@ }, { "cell_type": "code", - "id": "b648ee45-46ed-4e0c-9219-a2857c6c186a", + "id": "c7f8529e", "execution_count": 2, "metadata": { "execution": { @@ -278,7 +278,7 @@ }, { "cell_type": "markdown", - "id": "b8655a2f-bd39-4534-919f-3cf760169746", + "id": "f79a65b4", "metadata": { "papermill": { "duration": 0.002056, @@ -297,7 +297,7 @@ }, { "cell_type": "code", - "id": "7ce3bb41-9aca-464c-ab66-dcb67251db41", + "id": "82c40b38", "execution_count": 3, "metadata": { "execution": { @@ -371,7 +371,7 @@ }, { "cell_type": "markdown", - "id": "1f693439-3d62-4713-831f-c71cfacab3bd", + "id": "8b39571b", "metadata": { "papermill": { "duration": 0.011385, @@ -392,7 +392,7 @@ }, { "cell_type": "markdown", - "id": "6c5d6815-5b22-4382-94e9-e6baa51bbbb6", + "id": "b7aa8da0", "metadata": { "papermill": { "duration": 0.002004, @@ -411,7 +411,7 @@ }, { "cell_type": "code", - "id": "fa6a5315-aea5-4297-9d3a-62a03dc560bd", + "id": "4c054a81", "execution_count": 4, "metadata": { "execution": { @@ -486,7 +486,7 @@ }, { "cell_type": "markdown", - "id": "3a2fb8b0-6ae1-4807-9161-698cfbb055aa", + "id": "9aea2426", "metadata": { "papermill": { "duration": 0.002341, @@ -505,7 +505,7 @@ }, { "cell_type": "code", - "id": "571ecf04-8d60-4e56-ac25-275e6b542927", + "id": "5daaa20b", "execution_count": 5, "metadata": { "execution": { @@ -550,7 +550,7 @@ }, { "cell_type": "markdown", - "id": "d4513a33-0ff6-45bd-977f-4aa80156bcee", + "id": "3cd6363d", "metadata": { "papermill": { "duration": 0.001816, @@ -569,7 +569,7 @@ }, { "cell_type": "markdown", - "id": "34ea121d-2492-4dab-b8e8-18de6e0b909b", + "id": "baaa823d", "metadata": { "papermill": { "duration": 0.002846, @@ -588,7 +588,7 @@ }, { "cell_type": "code", - "id": "70c6f5b8-77a6-4ee0-8e16-fd46960a7421", + "id": "23fc7022", "execution_count": 6, "metadata": { "execution": { @@ -675,7 +675,7 @@ }, { "cell_type": "markdown", - "id": "d0ddbd6a-fd7d-4ba8-ab1d-9b71027b4718", + "id": "f1c622f0", "metadata": { "papermill": { "duration": 0.001889, @@ -694,7 +694,7 @@ }, { "cell_type": "markdown", - "id": "bdae367c-2112-4dae-97f8-8224df4620c5", + "id": "0153e3dd", "metadata": { "papermill": { "duration": 0.002301, @@ -713,7 +713,7 @@ }, { "cell_type": "code", - "id": "95f93a3e-dd84-422e-b2f2-0c55093880ef", + "id": "2d95fd79", "execution_count": 7, "metadata": { "execution": { @@ -791,7 +791,7 @@ }, { "cell_type": "markdown", - "id": "e6ad2332-9b17-446c-9fd6-5050d68c811d", + "id": "a8580fb8", "metadata": { "papermill": { "duration": 0.002042, @@ -810,7 +810,7 @@ }, { "cell_type": "markdown", - "id": "655b9ccc-7baf-4191-b9ce-e684f7c3e1a3", + "id": "87b00ab6", "metadata": { "papermill": { "duration": 0.001645, @@ -843,7 +843,7 @@ }, { "cell_type": "markdown", - "id": "8c477b11-ac01-4ef2-b01a-9ceca5729f9a", + "id": "20d2b45e", "metadata": { "papermill": { "duration": 0.001688, @@ -866,7 +866,7 @@ }, { "cell_type": "markdown", - "id": "14b7fe45-222b-471f-bbe3-37c148dcbc9a", + "id": "c305f36b", "metadata": { "papermill": { "duration": 0.001585, @@ -885,7 +885,7 @@ }, { "cell_type": "code", - "id": "cecd3835-e44e-4fa0-9d50-83abee3fa018", + "id": "037a177d", "execution_count": 8, "metadata": { "execution": { @@ -929,7 +929,7 @@ }, { "cell_type": "markdown", - "id": "8556e0c3-66e0-437a-a324-e3022c71291d", + "id": "873fec21", "metadata": { "papermill": { "duration": 0.001778, @@ -948,7 +948,7 @@ }, { "cell_type": "code", - "id": "a1ea2700-1248-4b9e-b59a-d8acbb6fb651", + "id": "7f3ff994", "execution_count": 9, "metadata": { "execution": { @@ -991,7 +991,7 @@ }, { "cell_type": "markdown", - "id": "c2f8e71c-78d1-42a9-a128-b7330a8de5f0", + "id": "1256aed2", "metadata": { "papermill": { "duration": 0.002553, @@ -1010,7 +1010,7 @@ }, { "cell_type": "code", - "id": "c8d2ce81-7c80-4095-95eb-a238572c9ed4", + "id": "a60f98ea", "execution_count": 10, "metadata": { "execution": { @@ -1049,7 +1049,7 @@ }, { "cell_type": "markdown", - "id": "635090bd-e354-4ddf-b572-e9cefb31a5bc", + "id": "02a4deb5", "metadata": { "papermill": { "duration": 0.002482, diff --git a/scripts/translation/tests/test_check_translation_parity.py b/scripts/translation/tests/test_check_translation_parity.py index e03eb82691c..125238896c8 100644 --- a/scripts/translation/tests/test_check_translation_parity.py +++ b/scripts/translation/tests/test_check_translation_parity.py @@ -769,7 +769,10 @@ def test_is_scannable_matches_on_relative_parts_only(tmp_path): # lignee. Le compte MESURE sur l'arbre fusionne est 17 (test_full_repo_state # _passes_parity le rend : 'found 17, declared 16'). La constante suit la # mesure, pas le recit : aucune paire n'est ajoutee par cette fusion. -EXPECTED_PAIR_COUNT = 17 +# 2026-10-24 (PR #22383) : la paire ANALYSE-12 FR/_en est ajoutee par cette PR. +# La constante suit la mesure -- l'arbre au head porte 18 paires `_en` ; +# le bump est conscient (#21391), il accompagne l'ajout, il ne le suit pas. +EXPECTED_PAIR_COUNT = 18 def _collect_parity_failures(repo_root: Path, From 11c648ca5884f87dbabfafbe5868e87fc55b4c49 Mon Sep 17 00:00:00 2001 From: jsboige Date: Sun, 25 Oct 2026 02:40:33 +0100 Subject: [PATCH 3/4] Fix(translation,#21958): ligne reciproque French version dans la Navigation du jumeau EN Le garde md-content-loss en mode translation compare les cibles de navigation du jumeau au sibling FR de la meme revision : le FR porte desormais 2 cibles (_en, ANALYSE-11) depuis cc5496ac, le jumeau n'en avait qu'une (ANALYSE-11) -> LOST_NAV_LINKS. Ajout de la ligne traduite (convention : la Version anglaise du FR a pour contrepartie la French version du jumeau), insertion textuelle, aucune re-serialisation, aucune cellule code touchee. Garde : detect_md_content_loss.py --check -> findings=0 (2 cibles de chaque cote). Co-Authored-By: Claude Sonnet 5.5 --- .../ANALYSE/ANALYSE-12-Comptage-Matching-Lean-Python_en.ipynb | 1 + 1 file changed, 1 insertion(+) diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-12-Comptage-Matching-Lean-Python_en.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-12-Comptage-Matching-Lean-Python_en.ipynb index feecc0ebd06..fad77fd5bb0 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-12-Comptage-Matching-Lean-Python_en.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-12-Comptage-Matching-Lean-Python_en.ipynb @@ -15,6 +15,7 @@ }, "source": [ "# ANALYSE-12: Counting perfect matchings — the permanent as a bridge, Lean on one side, enumeration on the other\n", + "**French version**: [ANALYSE-12 (fr)](ANALYSE-12-Comptage-Matching-Lean-Python.ipynb)\n", "\n", "Fold 6 of the `openai/math` Origami Epic (#19898, tranche B: #21958). The ANALYSE series confronts a research statement with what the repository can prove; here the statement is a **counting** problem.\n", "\n", From f72d73a4940ac261961a037bada3f7c48a53fd34 Mon Sep 17 00:00:00 2001 From: jsboige Date: Mon, 26 Oct 2026 02:44:01 +0100 Subject: [PATCH 4/4] Fix(analyse,#21958): ligne ANALYSE-09 du README -- 'quatre fenetres' -> 'quatre experiences' MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Reponse a la reserve mineure (🟡) de la review incrementale Hermes du 2026-10-26T00:49Z au head 57e40ed1 : les sorties committees montrent 9 resolutions de fenetre (2+3+2+2, sept tailles distinctes) sur 4 experiences. 'quatre experiences' est exact ; 'quatre fenetres' etait sous-specifie. Markdown seul, une ligne, aucun carnet touche. Co-Authored-By: Claude Sonnet 5.5 --- MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/README.md b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/README.md index 54916164da7..4ac3e1cfac4 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/README.md +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/README.md @@ -17,7 +17,7 @@ La série principale garde son tutoriel (numéros 1 à 14) ; le présent dossier | [ANALYSE-06-Sensibilite-2026-Lean](ANALYSE-06-Sensibilite-2026-Lean.ipynb) | La combinatoire booléenne 2026 d'openai/math (familles 127/132/186/192) lue depuis notre lac `Sensitivity` : Huang prouvé chez nous (`#check`/`#print axioms`), énoncés 2026 cités avec leur statut épistémique, et nos séparations sensibilité/sensibilité de bloc du module `Sensitivity.Separations`, prouvées et calculées (`#eval` natif, Pli 2 d'Origami #19898) ; jumeau anglais à code byte-identique : [ANALYSE-06-...-_en](ANALYSE-06-Sensibilite-2026-Lean_en.ipynb) | 35 min | | [ANALYSE-07-Percolation-Critique](ANALYSE-07-Percolation-Critique.ipynb) | Percolation critique et Ising sur l'arbre d-régulier — pli 3 de la digestion Origami (#19898) : les inégalités de Harris–Kleitman `#check`ées dans notre lac `percolation_lean`, les familles 2026 **213** (criticité Benjamini–Schramm) et **236** (seuil factor-of-IID de l'Ising sur l'arbre) citées avec leur statut, et deux calculs nôtres **exacts** — la probabilité critique p_c = 1/(d-1) par Galton–Watson (point fixe non trivial 4/9, vérifiable à la main) et l'écart entre seuil de reconstruction et seuil d'aimantation ; jumeau anglais à code byte-identique : [ANALYSE-07-...-_en](ANALYSE-07-Percolation-Critique_en.ipynb) | 40 min | | [ANALYSE-08-Ramsey-VdW](ANALYSE-08-Ramsey-VdW.ipynb) | Ramsey et van der Waerden par épuisement : R(3,3)=6 et W(2,3)=9 prouvés par énumération exhaustive (survivantes 18→12→0 côté graphes, 6→0 côté progressions), le mur 2^153 où le geste meurt, et le pont probabiliste d'Erdős (#19960, pli 4 Origami #19898) | 30 min | -| [ANALYSE-09-Tuilage-Aperiodique](ANALYSE-09-Tuilage-Aperiodique.ipynb) | Famille 155 du corpus `openai/math` : un carreau de ℤ³ qui pave sans périodicité totale (contre-exemple de dimension trois). Le carnet ramène le pavage par translations à la couverture exacte que le dépôt formalise déjà (`sudoku_lean`, `ExactCover.IsExactCover`), puis mesure quatre fenêtres avec deux organes déterministes — backtracking borné `place_tiles` et rang de période `period_rank` (élimination de Gauss exacte sur ℚ) — la leçon transverse étant que la demi-fenêtre cache toute période plus longue qu'elle ; jumeau anglais à code byte-identique : [ANALYSE-09-...-_en](ANALYSE-09-Tuilage-Aperiodique_en.ipynb) | 30 min | +| [ANALYSE-09-Tuilage-Aperiodique](ANALYSE-09-Tuilage-Aperiodique.ipynb) | Famille 155 du corpus `openai/math` : un carreau de ℤ³ qui pave sans périodicité totale (contre-exemple de dimension trois). Le carnet ramène le pavage par translations à la couverture exacte que le dépôt formalise déjà (`sudoku_lean`, `ExactCover.IsExactCover`), puis mesure quatre expériences avec deux organes déterministes — backtracking borné `place_tiles` et rang de période `period_rank` (élimination de Gauss exacte sur ℚ) — la leçon transverse étant que la demi-fenêtre cache toute période plus longue qu'elle ; jumeau anglais à code byte-identique : [ANALYSE-09-...-_en](ANALYSE-09-Tuilage-Aperiodique_en.ipynb) | 30 min | | [Note-IA-et-preuves-2026](../Note-IA-et-preuves-2026.md) | Note transverse — les trois AI-disclosures de la résolution de KLS (octobre 2026), ce qu'elles révèlent des modes de collaboration humain-IA, et trois leçons directement applicables au dépôt (#19729 grain 3/3) | 20 min | | [ANALYSE-10-Reflexion-Thurston-Python](ANALYSE-10-Reflexion-Thurston-Python.ipynb) | Carnet de distillation **réflexif** : trois thèses de W. P. Thurston (*On proof and progress in mathematics*, 1994) confrontées à des données mesurées sur ce dépôt — (1) la productivité mathématique se mesure à ce que les humains portent (sorry × consommateurs de la série), (2) la fiabilité est un processus social (densité d'agents et de rôles dans les traces du prover multi-agents), (3) comprendre n'est pas produire une preuve (ratio digestion Python / formalisation Lean) | carnet long (lecture sériée recommandée) | | [ANALYSE-11-Synthese-Transverse-Digestions-Python](ANALYSE-11-Synthese-Transverse-Digestions-Python.ipynb) | Synthèse transverse des pilotes de digestion (Epic #13106, critère 6) : huit pilotes de familles différentes (Sendov, *Analysis I*, PFR, CHSH, Erdős, minima parasites, `knot_lean`, `grothendieck_lean`) confrontés à la grille en dix points, chaque case adossée à une ancre re-vérifiée à l'exécution. Ce qu'on y mesure : aucun pilote ne porte de revue humaine nommée, la dette en `sorry` ne prédit pas la couverture de la grille, et hors de cette sous-série les pilotes ne se citent pas. La canonicalisation n'est pas déclarée | 30 min |