renum(complexity,#17063): tranche T1 -- 05 Aaronson-Arkhipov devient l'accretion 05b (R100)

MyIA.AI.Notebooks/Complexity/Complexity-03c-ComplexityZoo-Navigation-Python.ipynb

@@ -71,7 +71,7 @@
     "[02 — Vérifier contre trouver](Complexity-02-P-NP-Reduction.ipynb),\n",
     "[04 — Décider sans connaître la suite](Complexity-04-OnlineAlgorithms-Python.ipynb),\n",
     "[04b — Conjectures online](Complexity-04b-OnlineConjectures-Secretary-KServer.ipynb),\n",
-    "[05 — Aaronson & Arkhipov](Complexity-05-AaronsonArkhipov-PermanenteBosonSampling.ipynb) et\n",
+    "[05b — Aaronson & Arkhipov](Complexity-05b-AaronsonArkhipov-PermanenteBosonSampling.ipynb) et\n",
     "[06 — Déquantification](Complexity-06-Aaronson-Dequantification-Stabilizer.ipynb).\n",
     "\n",
     "Le Zoo recense plus de 500 classes de complexité. Une table d'inclusions recopiée serait une étagère ;\n",
@@ -1013,7 +1013,7 @@
    "source": [
     "## 4. Encart — le gap Mathlib du Zoo\n",
     "\n",
-    "Le même geste que [03b](Complexity-03b-HartmanisStearns-TimeHierarchy.ipynb), [05](Complexity-05-AaronsonArkhipov-PermanenteBosonSampling.ipynb) et [06](Complexity-06-Aaronson-Dequantification-Stabilizer.ipynb) :\n",
+    "Le même geste que [03b](Complexity-03b-HartmanisStearns-TimeHierarchy.ipynb), [05b](Complexity-05b-AaronsonArkhipov-PermanenteBosonSampling.ipynb) et [06](Complexity-06-Aaronson-Dequantification-Stabilizer.ipynb) :\n",
     "confronter la formalisation du carnet à l'état de [Mathlib](https://github.com/leanprover-community/mathlib4).\n",
     "\n",
     "- **Ce qui existe** : une couche `Computability/` réelle — machines de Turing (`TuringMachine`),\n",

MyIA.AI.Notebooks/Complexity/Complexity-04b-OnlineConjectures-Secretary-KServer.ipynb

@@ -15,7 +15,7 @@
    },
    "source": [
     "# Complexity-04b — La semaine historique de l'algorithmique online : secrétaire matroïdal et k-server\n",
-    "\n**Navigation** : [Index](README.md) | [04 — Décider sans connaître la suite](Complexity-04-OnlineAlgorithms-Python.ipynb) | [05 — La permanente, frontière quantique →](Complexity-05-AaronsonArkhipov-PermanenteBosonSampling.ipynb)\n",
+    "\n**Navigation** : [Index](README.md) | [04 — Décider sans connaître la suite](Complexity-04-OnlineAlgorithms-Python.ipynb) | [05b — La permanente, frontière quantique →](Complexity-05b-AaronsonArkhipov-PermanenteBosonSampling.ipynb)\n",
     "\n",
     "**Approfondissement de [04 — Décider sans connaître la suite](Complexity-04-OnlineAlgorithms-Python.ipynb)** | [Index de la série](README.md)\n",
     "\n",

MyIA.AI.Notebooks/Complexity/Complexity-06-Aaronson-Dequantification-Stabilizer.ipynb

@@ -41,7 +41,7 @@
    },
    "source": [
     "# Complexity-06 — Déquantifier les suprématies\n",
-    "\n**Navigation** : [Index](README.md) | [05 — La permanente, frontière quantique](Complexity-05-AaronsonArkhipov-PermanenteBosonSampling.ipynb)\n",
+    "\n**Navigation** : [Index](README.md) | [05b — La permanente, frontière quantique](Complexity-05b-AaronsonArkhipov-PermanenteBosonSampling.ipynb)\n",
     "\n",
     "Gottesman–Knill comme arbitre exécutable (Aaronson–Gottesman, 2004)\n"
    ]
@@ -68,7 +68,7 @@
     "[03 — Plus de temps, plus de problèmes](Complexity-03-TimeHierarchy.ipynb),\n",
     "[03b — Hartmanis–Stearns](Complexity-03b-HartmanisStearns-TimeHierarchy.ipynb),\n",
     "[04b — conjectures online](Complexity-04b-OnlineConjectures-Secretary-KServer.ipynb),\n",
-    "[05 — Aaronson–Arkhipov](Complexity-05-AaronsonArkhipov-PermanenteBosonSampling.ipynb)) :\n",
+    "[05b — Aaronson–Arkhipov](Complexity-05b-AaronsonArkhipov-PermanenteBosonSampling.ipynb)) :\n",
     "un texte fondateur, **fait tourner**. Le geste propre à cette veine est que la thèse\n",
     "**s'exécute**. Quand une « suprématie quantique » est annoncée, la question qui installe\n",
     "ou réfute la claim n'est pas « est-ce quantique ? » mais « **dans quelle classe de\n",

MyIA.AI.Notebooks/Complexity/README.md

@@ -21,7 +21,7 @@ n'y existe pas encore, et pourquoi.
 | [`Complexity-03c-ComplexityZoo-Navigation-Python.ipynb`](Complexity-03c-ComplexityZoo-Navigation-Python.ipynb) | Recherche | approfondissement de **03 — Plus de temps, plus de problèmes** | Scott Aaronson (fondateur du Complexity Zoo, 2004 — plus de 500 classes répertoriées) ; Theodore Baker, John Gill, Robert Solovay (*Relativizations of the P=?NP Question*, 1975) | La chaîne $L \subseteq NL \subseteq P \subseteq NP$ **tournée sur instances** : atteignabilité décidée deux fois — vérificateur à 2 mots de mémoire (certificat lu une fois, accord sur 4 tailles, faux témoin amputé refusé) contre DFS dont la pile explore ~$n/3$ sommets ; 2-SAT (Kosaraju, linéaire, $n=800$) contre 3-SAT (DPLL, densité-seuil $4{,}267n$) : facteurs de croissance **mesurés** par variable (~1,10× en noeuds, ~1,16× en temps), 20 certificats sur 20 vérifiés en polynomial ; **Baker–Gill–Solovay exécuté** — monde A : oracle diagonal, 4 machines vaincues par basculement d'un seul témoin, le côté NP exhaustif confirme $L_O$ sur chaque stade ; monde B : l'oracle QBF donne $P^B = NP^B$ en une requête — la barrière de relativisation vue du jouet ; carte du Zoo à 8 arêtes classées Mesuré/Cité/Ouvert (+ carte mermaid) ; encart **gap Mathlib** : `Computability/` couvre la calculabilité, mais aucune classe à bornage — le Zoo est absent | Français |
 | [`Complexity-04-OnlineAlgorithms-Python.ipynb`](Complexity-04-OnlineAlgorithms-Python.ipynb) | Licence | — | — (socle) | Louer ou acheter des skis : balayage des seuils, pire rapport $2 - 1/B$ atteint exactement au seuil $T = B$, puis distribution randomisée dont le pire rapport **converge vers $e/(e-1) \approx 1{,}58198$** ; pagination : Belady hors ligne contre LRU et FIFO — rapport tendant vers $k$ sur le motif cyclique ($4{,}84$ à $k=5$), retombant à $1{,}47$ sur requêtes aléatoires ; secrétaire : fraction d'observation balayée, sommet **plat** autour de $1/e$ (indiscernable de $0{,}4$ à $0{,}003$ près) ; quatre énoncés séparés Mesuré/Cité ; trois exercices exécutables | Français |
 | [`Complexity-04b-OnlineConjectures-Secretary-KServer.ipynb`](Complexity-04b-OnlineConjectures-Secretary-KServer.ipynb) | Recherche | approfondissement de **04 — Décider sans connaître la suite** | Sahil Singla & Christian Coester, Elias Koutsoupias, Marek Zbysiński (les deux preprints de septembre 2026 : conjecture du secrétaire matroïdal 2007 et conjecture k-server ~1990, tombées à 24 h d'écart) | Baseline $1/e$ du secrétaire classique mesurée par Monte Carlo ($n$ = 20/100/1000) ; deux matroïdes à oracle d'indépendance (uniforme, graphique) avec optimum offline exact et compétitivité de deux stratégies online ; **work function algorithm implémenté exactement** (DP sur les $\binom{m}{2}$ configurations) : sur le cycle $C_5$, ratio WFA 1,67 sous la borne $k=2$ quand greedy explose (20 à 60 requêtes, 160 à 480 — non compétitif) ; tableau du double visage randomisation/déterminisme ; trois niveaux épistémiques Mesuré/Cité/Absent (prudence « preuve annoncée ») ; encart **gap Mathlib** (matroïdes présents, compétitivité/k-server/work functions absents) | Français |
-| [`Complexity-05-AaronsonArkhipov-PermanenteBosonSampling.ipynb`](Complexity-05-AaronsonArkhipov-PermanenteBosonSampling.ipynb) | Recherche | deviendra **05b**, approfondissement du futur 05 *Compter est plus dur que vérifier* | Scott Aaronson & Alex Arkhipov (*The Computational Complexity of Linear Optics*, 2011 — la permanente comme frontière quantique) | La définition $n!$ **exécutée** avec comptes canoniques, vérifiée contre l'énumération brute des couplages parfaits (perm(0/1)) ; **Ryser vectorisé réemployé de Sudoku-15** (`batch_perm8`, généralisé à toute taille) contre Gauss instrumenté : comptes exacts par formules fermées validées par instrumentation — à $n=20$, définition $4{,}9 \times 10^{19}$ opérations contre 5 149 pour Gauss, Ryser/det ≈ $1{,}6 \times 10^4$ en temps à $n=16$ ; #P-difficulté (Valiant 1979) maintenue au niveau **Cité**, FPRAS non négatif (Jerrum–Sinclair–Vigoda) en exception qui désigne les signes ; **BosonSampling jouet** : unitaire Haar (QR, Mezzadri), loi $\lvert\mathrm{perm}\rvert^2$ exacte sur 56/924/12 870 sorties, TV(échantillon, exact) → 0, coût d'énumération extrapolé jusqu'à ~1 an à 1 TFLOP/s pour $(20, 40)$ ; encart **gap Mathlib** — premier verdict **positif** de la série : `Matrix.permanent` existe (114 lignes, forme $n!$) face à un dossier `Determinant/` entier, mais ni Ryser ni couche complexité | Français |
+| [`Complexity-05b-AaronsonArkhipov-PermanenteBosonSampling.ipynb`](Complexity-05b-AaronsonArkhipov-PermanenteBosonSampling.ipynb) | Recherche | deviendra **05b**, approfondissement du futur 05 *Compter est plus dur que vérifier* | Scott Aaronson & Alex Arkhipov (*The Computational Complexity of Linear Optics*, 2011 — la permanente comme frontière quantique) | La définition $n!$ **exécutée** avec comptes canoniques, vérifiée contre l'énumération brute des couplages parfaits (perm(0/1)) ; **Ryser vectorisé réemployé de Sudoku-15** (`batch_perm8`, généralisé à toute taille) contre Gauss instrumenté : comptes exacts par formules fermées validées par instrumentation — à $n=20$, définition $4{,}9 \times 10^{19}$ opérations contre 5 149 pour Gauss, Ryser/det ≈ $1{,}6 \times 10^4$ en temps à $n=16$ ; #P-difficulté (Valiant 1979) maintenue au niveau **Cité**, FPRAS non négatif (Jerrum–Sinclair–Vigoda) en exception qui désigne les signes ; **BosonSampling jouet** : unitaire Haar (QR, Mezzadri), loi $\lvert\mathrm{perm}\rvert^2$ exacte sur 56/924/12 870 sorties, TV(échantillon, exact) → 0, coût d'énumération extrapolé jusqu'à ~1 an à 1 TFLOP/s pour $(20, 40)$ ; encart **gap Mathlib** — premier verdict **positif** de la série : `Matrix.permanent` existe (forme $n!$) face à un dossier `Determinant/` entier, mais ni Ryser ni couche complexité | Français |
 | [`Complexity-06-Aaronson-Dequantification-Stabilizer.ipynb`](Complexity-06-Aaronson-Dequantification-Stabilizer.ipynb) | Recherche | deviendra **06b**, approfondissement du futur 06 *Simuler un circuit quantique classiquement* | Scott Aaronson & Daniel Gottesman (*Improved Simulation of Stabilizer Circuits*, 2004 — déquantifier les suprématies par l'arbitre exécutable) | Le formalisme stabilisateur **exécuté** : table de phase et conjugaison CHP **dérivées des matrices 2×2**, jamais recopiées ; port CHP complet (rowsum, portes, mesures — déterministe par lecture GF(2), aléatoire par re-stabilisation) croisé contre l'état complet 2^n : **84 valeurs propres stabilisatrices exactes au 1e-9** (zéro bruit), distributions TV sous 6× le bruit de sondage, stim en troisième juge ; banc discriminant : bascule **mesurée** dès ~12 qubits, ratio ~1600× à n=20, échelons locaux au-dessus du plancher 2× (le mur réel est plus raide que 2^n : la mémoire aussi a une loi) ; une **seule** porte T ferme le port **et** stim (`no attribute 't'`) — la frontière est Clifford/le-reste, pas quantique/classique | Français |
 
 ## Parcours

_quarto.yml

@@ -686,7 +686,7 @@ project:
     - "MyIA.AI.Notebooks/Complexity/Complexity-03c-ComplexityZoo-Navigation-Python.ipynb"
     - "MyIA.AI.Notebooks/Complexity/Complexity-04-OnlineAlgorithms-Python.ipynb"
     - "MyIA.AI.Notebooks/Complexity/Complexity-04b-OnlineConjectures-Secretary-KServer.ipynb"
-    - "MyIA.AI.Notebooks/Complexity/Complexity-05-AaronsonArkhipov-PermanenteBosonSampling.ipynb"
+    - "MyIA.AI.Notebooks/Complexity/Complexity-05b-AaronsonArkhipov-PermanenteBosonSampling.ipynb"
     - "MyIA.AI.Notebooks/Complexity/Complexity-06-Aaronson-Dequantification-Stabilizer.ipynb"
     - "MyIA.AI.Notebooks/cross-series/socle-metadata-driven/Socle-MetadataDriven-Csharp.ipynb"
     - "MyIA.AI.Notebooks/GameTheory/GameTheory-01-Setup-Python.ipynb"

docs/grothendieckian-lens.md

@@ -94,7 +94,7 @@ Entre les séries d'enseignement elles-mêmes, de nouvelles tresses se sont nou
 
 Au-dessus des deux versants veillent les grands noms, chacun avec son Epic. Mais un nom n'entre pas dans le dépôt parce qu'on le cite : il y entre quand une série exécute ce qu'il a pensé. Serre y est entré par des diptyques où le même énoncé est calculé en Python et démontré en Lean ([Serre 100](../MyIA.AI.Notebooks/SymbolicAI/Lean/Serre100/README.md)), et par une carte qui rattache sa moitié du pont à la formalisation de Grothendieck ([`SerreMap.lean`](../MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck/SerreMap.lean)). Tegmark, par une boucle en trois temps : le cours d'apprentissage automatique exécute les diagrammes de phase du *grokking* ([2.9c](../MyIA.AI.Notebooks/ML/DataScienceWithAgents/02-ML-Cours/2.9c-Grokking-Diagrammes-Phases.ipynb)), un lake démontre les lois conservées qu'on en extrait ([`Grokking.lean`](../MyIA.AI.Notebooks/ML/learning_theory_lean/EffectiveTheory/Grokking.lean)), et ICT mesure la géométrie des concepts appris ([ICT-41](../MyIA.AI.Notebooks/IIT/ICT-Series/ICT-41-SAE-GeometrieFeatures-Python.ipynb)).
 
-Schmidhuber a un organe dans ICT ([`ict/beauty.py`](../MyIA.AI.Notebooks/IIT/ICT-Series/ict/beauty.py)) et un verdict exécuté : « le compression-progress de Schmidhuber tient » ([ICT-17b](../MyIA.AI.Notebooks/IIT/ICT-Series/ICT-17b-Grokking-CompressionProgress-Python.ipynb)). Aaronson a fait de l'écart entre permanent et déterminant un compte d'opérations, avec l'algorithme de Ryser déjà présent dans le Sudoku ([Complexity-05](../MyIA.AI.Notebooks/Complexity/Complexity-05-AaronsonArkhipov-PermanenteBosonSampling.ipynb)). Pearl a trouvé sa démonstration par la machine : deux modèles causaux qui produisent les mêmes données et prédisent des interventions opposées ([CausalBridges-01-Do-Calculus](../MyIA.AI.Notebooks/Probas/DecisionTheory/Causal-Bridges/CausalBridges-01-Do-Calculus.ipynb)). Tao a digéré et formalisé une preuve récente de la conjecture de Sendov ([Lean-18](../MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-01-Sendov-Lean-Python.ipynb)). D'autres attendent : Russell, cité partout, n'habite qu'un notebook, le jeu de l'interrupteur ([GameTheory-15](../MyIA.AI.Notebooks/GameTheory/GameTheory-15-CooperativeGames-Python.ipynb)). Les Epics le mesurent elles-mêmes : plusieurs de ces noms *hantent* encore le dépôt plus qu'ils ne l'*habitent*, et c'est en les faisant habiter que naissent les ponts.
+Schmidhuber a un organe dans ICT ([`ict/beauty.py`](../MyIA.AI.Notebooks/IIT/ICT-Series/ict/beauty.py)) et un verdict exécuté : « le compression-progress de Schmidhuber tient » ([ICT-17b](../MyIA.AI.Notebooks/IIT/ICT-Series/ICT-17b-Grokking-CompressionProgress-Python.ipynb)). Aaronson a fait de l'écart entre permanent et déterminant un compte d'opérations, avec l'algorithme de Ryser déjà présent dans le Sudoku ([Complexity-05b](../MyIA.AI.Notebooks/Complexity/Complexity-05b-AaronsonArkhipov-PermanenteBosonSampling.ipynb)). Pearl a trouvé sa démonstration par la machine : deux modèles causaux qui produisent les mêmes données et prédisent des interventions opposées ([CausalBridges-01-Do-Calculus](../MyIA.AI.Notebooks/Probas/DecisionTheory/Causal-Bridges/CausalBridges-01-Do-Calculus.ipynb)). Tao a digéré et formalisé une preuve récente de la conjecture de Sendov ([Lean-18](../MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-01-Sendov-Lean-Python.ipynb)). D'autres attendent : Russell, cité partout, n'habite qu'un notebook, le jeu de l'interrupteur ([GameTheory-15](../MyIA.AI.Notebooks/GameTheory/GameTheory-15-CooperativeGames-Python.ipynb)). Les Epics le mesurent elles-mêmes : plusieurs de ces noms *hantent* encore le dépôt plus qu'ils ne l'*habitent*, et c'est en les faisant habiter que naissent les ponts.
 
 Prenons de la hauteur. Le dépôt est un site, au sens du deuxième mouvement : les séries en sont les ouverts, les ponts les recouvrements, et l'accord sur les recouvrements la condition de recollement. Là où deux séries s'accordent — Tweety et Lean sur le même syllogisme, Infer.NET et PyMC sur la même valeur d'information — une connaissance plus globale apparaît. Là où elles divergent, ou ne se ressemblent que par la structure — la percolation et l'adoption collective, la preuve de HashLife et le saut qu'elle ne couvrait pas —, l'écart n'est pas un échec : c'est une obstruction, et elle montre où travailler. C'est une image, de grade C, et elle se déclare comme telle. Mais elle dit juste : la mer ne monte plus autour d'une seule noix, elle monte entre les séries.