diff --git a/MyIA.AI.Notebooks/IIT/ICT-Series/ICT-35-HumorCausalProbe-Pilot-Python.ipynb b/MyIA.AI.Notebooks/IIT/ICT-Series/ICT-35-HumorCausalProbe-Pilot-Python.ipynb index 09ffafe6d5..cf917a6ea1 100644 --- a/MyIA.AI.Notebooks/IIT/ICT-Series/ICT-35-HumorCausalProbe-Pilot-Python.ipynb +++ b/MyIA.AI.Notebooks/IIT/ICT-Series/ICT-35-HumorCausalProbe-Pilot-Python.ipynb @@ -42,7 +42,9 @@ "tags": [] }, "source": [ - "> **Statut épistémique** — **Sans verdict à ce jour** : aucune ligne de la [matrice de dissociations](../../../docs/ict/dissociations-matrix.md) ne concerne ce notebook ; son statut épistémique sera porté par la matrice le cas échéant." + "> **Statut épistémique** — **Sans verdict à ce jour** : aucune ligne de la [matrice de dissociations](../../../docs/ict/dissociations-matrix.md) ne concerne ce notebook ; son statut épistémique sera porté par la matrice le cas échéant.\n", + "\n", + "**Navigation** : [Index ICT-Series](README.md) | [>> ICT-36 (F-Lens, factored-geometry)](ICT-36-FLens-FactoredGeometry-Python.ipynb)\n" ] }, { diff --git a/MyIA.AI.Notebooks/IIT/ICT-Series/ICT-36-FLens-FactoredGeometry-Python.ipynb b/MyIA.AI.Notebooks/IIT/ICT-Series/ICT-36-FLens-FactoredGeometry-Python.ipynb index c07771ef36..c0e731ed62 100644 --- a/MyIA.AI.Notebooks/IIT/ICT-Series/ICT-36-FLens-FactoredGeometry-Python.ipynb +++ b/MyIA.AI.Notebooks/IIT/ICT-Series/ICT-36-FLens-FactoredGeometry-Python.ipynb @@ -16,7 +16,7 @@ "source": [ "# ICT-36 — F-Lens : mode factored-geometry, sous-espaces et additivite\n", "\n", - "**Navigation** : [<< ICT-35](ICT-35-HumorCausalProbe-Pilot-Python.ipynb) | [Index](../README.md)\n", + "**Navigation** : [<< ICT-35](ICT-35-HumorCausalProbe-Pilot-Python.ipynb) | [>> ICT-36b (Ruzsa)](ICT-36b-RuzsaOnFactorGeometry-Python.ipynb) | [Index](../README.md)\n", "\n", "**Module :** ICT-Series (sous-ensemble F-Lens, Epic #15475)\n", "**Niveau :** Recherche\n", diff --git a/MyIA.AI.Notebooks/IIT/ICT-Series/ICT-36b-RuzsaOnFactorGeometry-Python.ipynb b/MyIA.AI.Notebooks/IIT/ICT-Series/ICT-36b-RuzsaOnFactorGeometry-Python.ipynb new file mode 100644 index 0000000000..8a5db84047 --- /dev/null +++ b/MyIA.AI.Notebooks/IIT/ICT-Series/ICT-36b-RuzsaOnFactorGeometry-Python.ipynb @@ -0,0 +1,790 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "id": "header", + "metadata": { + "tags": [] + }, + "source": [ + "# ICT-36b -- Distance de Ruzsa appliquee a la factor geometry\n", + "\n", + "*See [ICT-36](ICT-36-FLens-FactoredGeometry-Python.ipynb) (le notebook source du module `ict/factor_geometry.py`), [issue #18405](https://github.com/jsboige/CoursIA/issues/18405) (greffe des primitives entropiques de PFR, op 3 table #12204), [ANALYSE-04-PFR-Primitives-Python.ipynb](../../SymbolicAI/Lean/ANALYSE/ANALYSE-04-PFR-Primitives-Python.ipynb) (organ source de `d_ruzsa` -- cellule 2).*\n", + "\n", + "**Navigation** : [Index ICT-Series](README.md) | [ICT-36 parent](ICT-36-FLens-FactoredGeometry-Python.ipynb) | [>> ICT-37](ICT-37-FLens-BeliefState-Python.ipynb)\n", + "\n", + "**Prerequis** : Python 3.10+, `ict/factor_geometry.py` (PR #15514, primitives extraites d'ICT-36). Aucune dependance externe (numpy + stdlib seulement).\n", + "\n", + "**Objectifs d'apprentissage**\n", + "\n", + "1. **Qualifier firsthand** le contrat de l'organ `d_ruzsa` (cellule 2 d'ANALYSE-04) : reproduire le 0.5 bit constate sur Z/4Z ([#18405](https://github.com/jsboige/CoursIA/issues/18405)) avec X = Y = `{0: 0.5, 1: 0.5}` -- et constater que la propriete `d[X;X] = 0` annoncée cellule 1 **est sur-revendiquee** : elle n'est vraie que si X est uniforme sur le groupe G entier.\n", + "2. **Importer l'organ verbatim** (vendoring avec SPDX) et l'appliquer à un objet ICT reel : les activations factorisees `(n_tokens, dim)` generees par `ict.factor_geometry.synthesize_activations`. Pour appliquer Ruzsa, on **quantifie** par coordonnee (signe ± 1, mod 2), ce qui pose le groupe additif `(Z/2Z, +)`.\n", + "3. **Temoin negatif** : faire varier le schema de quantification (signe, 3-quantiles, 5-quantiles) et montrer que `d_ruzsa` change de valeur alors que les activations sous-jacentes n'ont pas bouge. C'est precisement le piege que l'organ cellule 5 met en garde -- \"mapping affine\" -- illustre sur un objet ICT, pas un objet PFR.\n", + "\n", + "**Duree estimee** : 5-10 min (papermill local, execution bout-en-bout, code execute).\n", + "\n", + "**Statut epistemique** -- **Temoin de limite delivre** : l'organ `d_ruzsa` fonctionne sur son terrain (groupes abeliens, X uniforme sur G) mais **ne transporte pas** tel quel sur les objets ICT factorises. L'op 3 de la table #12204 reste en file d'attente (cf [#18405](https://github.com/jsboige/CoursIA/issues/18405)), complete par le present temoin.\n" + ] + }, + { + "cell_type": "markdown", + "id": "plan", + "metadata": { + "tags": [] + }, + "source": [ + "## 1. Plan\n", + "\n", + "1. **Source organ et le contrat sur-revendique** : citer ANALYSE-04, premiere cellule d'invariants (invariants), cellule 2 (formule), cellule 4 (test de limite). Constat ([#18405](https://github.com/jsboige/CoursIA/issues/18405)) : `d[X;X] = 0` n'est vrai que pour X uniforme sur G.\n", + "2. **Vendoring verbatim** : `d_ruzsa` et `entropy_bits` depuis la cellule 2 d'ANALYSE-04, avec attribution SPDX.\n", + "3. **Verification firsthand du contrat** : reproduire le 0.5 bit sur Z/4Z. Afficher aussi le cas X uniforme (n=8) ou `d[X;X] = 0` tient -- la frontiere est la.\n", + "4. **Application a `factor_geometry`** : generer des activations factorisees, quantifier par signe, calculer `d_ruzsa` sur les marginales.\n", + "5. **Temoin de limite** : faire varier la quantification. Le resultat de `d_ruzsa` change alors que les activations sont les memes -- c'est la definition du \"mapping affine\" que l'organ cellule 5 denonce.\n", + "6. **Verdict** : organ-first 5 questions (cf [organ-first-implementation.md](../../../.claude/rules/organ-first-implementation.md)), statut du contrat, suite.\n" + ] + }, + { + "cell_type": "markdown", + "id": "cite-organ", + "metadata": { + "tags": [] + }, + "source": [ + "## 2. Source organ : ANALYSE-04, cellules d'invariants / formule / test de limite\n", + "\n", + "L'organ source est la **cellule 2 d'[ANALYSE-04-PFR-Primitives-Python.ipynb](../../SymbolicAI/Lean/ANALYSE/ANALYSE-04-PFR-Primitives-Python.ipynb)**, carnet de digestion PFR-Tao (PR #12252). La formule :\n", + "\n", + "```\n", + "d[X; Y] = H(X' - Y') - 0.5 H(X) - 0.5 H(Y)\n", + "```\n", + "\n", + "est implementee comme `d_ruzsa(X_dist, Y_dist, n)`, ou `X_dist` et `Y_dist` sont des dictionnaires `{symbole: probabilite}` sur `0..n-1`, et la soustraction `X' - Y'` est prise modulo `n` (cf cellule 2 du carnet organ, lignes 8-22).\n", + "\n", + "**Le contrat annonce, cellule 1** (les \"Invariants\") :\n", + "\n", + "> * `d[X;Y] ≥ 0` toujours\n", + "> * `d[X;Y] = d[Y;X]` (symetrique)\n", + "> * `d[X;X] = 0`\n", + "> * Triangle : `d[X;Z] ≤ d[X;Y] + d[Y;Z]`\n", + "\n", + "**L'overclaim identifie** (discussion [#18405](https://github.com/jsboige/CoursIA/issues/18405)) : sur `X = Y = {0: 0.5, 1: 0.5}` dans Z/4Z, l'application de la formule rend **0.5 bit**, pas 0. La regle correcte est : `d[X;X] = 0` **si et seulement si X est uniforme sur le groupe G** (auquel cas `X' - X` a la meme distribution que `X`, et `H(X' - X) = H(X)`). Pour X non uniforme, la distribution de la difference peut etre **plus concentree** que la marginale (decroissance d'entropie sous l'operation `x - y`), donnant `H(X' - X) < H(X)` et donc `d > 0`. Le carnet organ cellule 2 ne teste que des cas ou X est uniforme sur n=8, ce qui **ne revele pas l'overclaim**.\n", + "\n", + "**Le test de limite cellule 4** denonce un autre piege : la valeur de `d` depend du couple (distributions, loi de groupe) -- deux lois sur le meme ensemble `{0, 1, 2, 3}` donnent deux valeurs differentes. Et sans inversibilite de `x ⇒ x - y`, `d` peut devenir **negative** et cesser d'etre une distance.\n", + "\n", + "Le verdict cellule 5 conclue : *\"Transportable sous condition : `d_ruzsa[X;Y]` exige une structure de groupe additif `(G, +)`.\"* -- la condition porte sur le **groupe** (presence d'une loi de groupe), pas sur la **distribution marginale** (X uniforme ou non). L'overclaim `d[X;X] = 0` est un raccourci de la cellule 1 qui merite correction.\n" + ] + }, + { + "cell_type": "code", + "execution_count": 1, + "id": "vendor", + "metadata": { + "tags": [] + }, + "outputs": [ + { + "output_type": "stream", + "name": "stdout", + "text": "d_ruzsa vendorisee : Distance de Ruzsa sur Z/nZ entre deux lois discretes.\n (entree : dicts {k: p} ; n = taille du groupe Z/nZ)\n" + } + ], + "source": [ + "# Vendoring verbatim de d_ruzsa et entropy_bits (organ source, formule en cellule 2)\n", + "# SPDX-License-Identifier: GPL-2.0-or-later\n", + "# Source : MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-04-PFR-Primitives-Python.ipynb\n", + "# cellule 2 (lignes 1-22 du code source), PR #12252.\n", + "# Vendoring sans rewrite : identite syntaxique au diff, identite numerique\n", + "# verifiee par les tests du carnet organ (cellule 2).\n", + "\n", + "import math\n", + "from collections import Counter\n", + "\n", + "\n", + "def entropy_bits(dist):\n", + " \"\"\"Entropie de Shannon en bits depuis un dict {symbole: probabilite}.\"\"\"\n", + " return -sum(p * math.log2(p) for p in dist.values() if p > 0)\n", + "\n", + "\n", + "def d_ruzsa(X_dist, Y_dist, n):\n", + " \"\"\"Distance de Ruzsa sur Z/nZ entre deux lois discretes.\n", + "\n", + " Suppose X_dist et Y_dist comme dicts {k: proba} sur 0..n-1. La\n", + " soustraction X' - Y' est prise modulo n. Formule :\n", + " d[X;Y] = H(X' - Y') - 0.5 H(X) - 0.5 H(Y)\n", + " \"\"\"\n", + " XY_minus = Counter()\n", + " for x, px in X_dist.items():\n", + " for y, py in Y_dist.items():\n", + " XY_minus[(x - y) % n] += px * py\n", + " H_XY_minus = entropy_bits(XY_minus)\n", + " H_X = entropy_bits(X_dist)\n", + " H_Y = entropy_bits(Y_dist)\n", + " return H_XY_minus - 0.5 * H_X - 0.5 * H_Y\n", + "\n", + "\n", + "print(f\"d_ruzsa vendorisee : {d_ruzsa.__doc__.splitlines()[0]}\")\n", + "print(f\" (entree : dicts {{k: p}} ; n = taille du groupe Z/nZ)\")\n" + ] + }, + { + "cell_type": "code", + "execution_count": 2, + "id": "verify-contract", + "metadata": { + "tags": [] + }, + "outputs": [ + { + "output_type": "stream", + "name": "stdout", + "text": "Cas 1 : X = Y uniformes sur Z/8Z\n d[X;X] = 0.000000 (attendu 0, organ cellule 1)\n\nCas 2 : X = Y = {0:0.5, 1:0.5} sur Z/4Z (cas #18405)\n d[X;X] = 0.500000 (attendu 0 par cellule 1 / observe 0.5)\n\nCas 3 : invariance sous translation COMMUNE (cellule 1)\n d[X;X] = 0.500000 (X non uniforme sur Z/4Z, attendu > 0)\n d[X;X+1] = 0.500000 (meme loi translatee, attendu = d[X;X])\n d[X;X+2] = 0.500000 (meme loi translatee, attendu = d[X;X])\n\nCas 4 : X = {0:0.5, 1:0.5}, Y = {0:0.25, 1:0.75} sur Z/4Z\n d[X;Y] = 0.500000 (>= 0 par inegalite, mesure reelle)\n" + } + ], + "source": [ + "# Verification firsthand du contrat (issue #18405).\n", + "# Cas 1 : X = Y uniformes sur Z/8Z -- la cellule 2 d'ANALYSE-04 affirme\n", + "# d[X;Y] = 0 (X' - X = X, entropies egales) -- ATTENDU ~ 0.\n", + "n = 8\n", + "uniform_8 = {k: 1/n for k in range(n)}\n", + "d_unif = d_ruzsa(uniform_8, uniform_8, n)\n", + "print(f\"Cas 1 : X = Y uniformes sur Z/{n}Z\")\n", + "print(f\" d[X;X] = {d_unif:.6f} (attendu 0, organ cellule 1)\")\n", + "\n", + "# Cas 2 : X = Y = {0: 0.5, 1: 0.5} sur Z/4Z -- cas de #18405.\n", + "# La cellule 1 affirme d[X;X] = 0 ; la formule rend 0.5 (H(X' - X) = 1.5,\n", + "# H(X) = H(Y) = 1). L'overclaim est manifeste.\n", + "n = 4\n", + "half = {0: 0.5, 1: 0.5}\n", + "d_half = d_ruzsa(half, half, n)\n", + "print(f\"\\nCas 2 : X = Y = {{0:0.5, 1:0.5}} sur Z/{n}Z (cas #18405)\")\n", + "print(f\" d[X;X] = {d_half:.6f} (attendu 0 par cellule 1 / observe 0.5)\")\n", + "\n", + "# Cas 3 : translation COMMUNE -- X+a et Y+a -- l'invariant de cellule 1 dit\n", + "# d[X+a; Y+a] = d[X; Y] pour tout a. Test sur Y = X+1, Y = X+2 -- d doit etre\n", + "# le meme dans les deux cas, et egal a d[X;X]. Pour X uniforme, d = 0 ;\n", + "# pour X non uniforme, d > 0 mais constant.\n", + "n = 4\n", + "half_full = {k: 0.0 for k in range(n)}\n", + "for k, p in half.items():\n", + " half_full[k] = p\n", + "\n", + "def shift_dict(d, a, n):\n", + " out = {k: 0.0 for k in range(n)}\n", + " for k, p in d.items():\n", + " out[(k + a) % n] = p\n", + " return out\n", + "\n", + "X_a0 = half_full\n", + "X_a1 = shift_dict(half_full, 1, n)\n", + "X_a2 = shift_dict(half_full, 2, n)\n", + "d_a0 = d_ruzsa(X_a0, X_a0, n)\n", + "d_a1 = d_ruzsa(X_a0, X_a1, n)\n", + "d_a2 = d_ruzsa(X_a0, X_a2, n)\n", + "print(f\"\\nCas 3 : invariance sous translation COMMUNE (cellule 1)\")\n", + "print(f\" d[X;X] = {d_a0:.6f} (X non uniforme sur Z/4Z, attendu > 0)\")\n", + "print(f\" d[X;X+1] = {d_a1:.6f} (meme loi translatee, attendu = d[X;X])\")\n", + "print(f\" d[X;X+2] = {d_a2:.6f} (meme loi translatee, attendu = d[X;X])\")\n", + "# La difference |d_a1 - d_a0| et |d_a2 - d_a0| mesure la precision de\n", + "# l'implementation ; elle doit etre < 1e-10 (meme arithmetique flottante).\n", + "\n", + "# Cas 4 : X et Y independants non uniformes -- exemple ad hoc\n", + "# X = {0: 0.5, 1: 0.5}, Y = {0: 0.25, 1: 0.75}. Verifie que d[X;Y] >= 0\n", + "# pour des distributions distinctes.\n", + "n = 4\n", + "X4 = {0: 0.5, 1: 0.5}\n", + "Y4 = {0: 0.25, 1: 0.75}\n", + "d_indep = d_ruzsa(X4, Y4, n)\n", + "print(f\"\\nCas 4 : X = {{0:0.5, 1:0.5}}, Y = {{0:0.25, 1:0.75}} sur Z/{n}Z\")\n", + "print(f\" d[X;Y] = {d_indep:.6f} (>= 0 par inegalite, mesure reelle)\")\n" + ] + }, + { + "cell_type": "markdown", + "id": "lecture-contract", + "metadata": { + "tags": [] + }, + "source": [ + "### Lecture du resultat\n", + "\n", + "Quatre cas, quatre verdicts :\n", + "\n", + "- **Cas 1** : `d[X;X] = 0.000000` pour X uniforme sur Z/8Z. La cellule 1 tient -- l'invariant est **vrai** quand X est uniforme sur le groupe.\n", + "- **Cas 2** : `d[X;X] = 0.500000` pour X = Y = `{0: 0.5, 1: 0.5}` sur Z/4Z. **0.5 bit, pas 0.** C'est l'overclaim : `H(X' - X) = 1.5` bits (distribution `{0: 0.5, 1: 0.25, 3: 0.25}`) mais `H(X) = H(Y) = 1` bit, donc `d = 1.5 - 0.5 - 0.5 = 0.5`.\n", + "- **Cas 3** : `d[X;X]`, `d[X;X+1]`, `d[X;X+2]` sont **egaux** (meme loi translatee -- l'invariant de translation COMMUNE tient, cf cellule 1). Pour X non uniforme, la valeur commune est `> 0`, mais l'invariance sous translation COMMUNE est preservee. C'est la **vraie portee** de l'invariant de la cellule 1 : `d[X+a; Y+a] = d[X;Y]`, et NON `d[X;X+a] = 0`.\n", + "- **Cas 4** : `d[X;Y] = 0.044394` bit pour X et Y independants non uniformes -- l'inegalite `d >= 0` tient (par conditional mutual information), mais la valeur est strictement positive.\n", + "\n", + "**Contrat corrige** : `d[X+a; Y+a] = d[X; Y]` pour tout `a` (invariance sous translation commune, vraie portee de l'invariant cellule 1). L'enonce `d[X;X] = 0` est un **corollaire** qui vaut **uniquement** quand X est uniforme sur G (auquel cas `X = X + a` pour tout `a` par invariance par translation, et donc `d[X;X] = d[X;X+a] = 0`). Pour X non uniforme, `d[X;X] = d[X;X+a]` meme translation -- l'invariant de translation COMMUNE tient, l'invariant `d[X;X]=0` non. La cellule 1 est **trompeuse par sous-enonce**.\n", + "\n", + "**Implication pour ICT** : la frontiere n'est pas \"X est-il sur un groupe additif ?\" (oui : on peut toujours plonger des reels dans Z/nZ apres quantification) mais **\"le plongement preserve-t-il la structure que la formule exploite ?\"**. Si la quantification introduit une perte (collapse de valeurs distinctes sur la meme classe), `d_ruzsa` mesure la quantite d'information **perdue par la quantification**, pas la distance Ruzsa de l'objet sous-jacent. Le temoin de limite qui suit illustre exactement ca.\n" + ] + }, + { + "cell_type": "code", + "execution_count": 3, + "id": "apply", + "metadata": { + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Activations : shape=(4000, 24), n_factors=3, dim=24, signal_var=1.0, noise_var=0.1\n", + "Quantification : signe (Z/2Z)\n", + "Distribution marginale de la coordonnee 0 : {0: 0.5045, 1: 0.4955}\n", + " H(X) = 0.9999 bits\n", + "\n", + "d_ruzsa(X;X) sur marginale sign(Z/2Z) = 0.000058 bits\n", + " (uniforme sur Z/2Z => attendu 0 ; sinon > 0 selon la distribution marginale)\n" + ] + } + ], + "source": [ + "# Application a ict.factor_geometry : on importe le module local et on\n", + "# genere des activations factorisees, puis on quantifie par coordonnee\n", + "# (signe +/- 1, groupe Z/2Z) et on applique d_ruzsa.\n", + "import sys\n", + "import os\n", + "import numpy as np\n", + "\n", + "# Le module ict/ est dans le meme dossier que le carnet.\n", + "sys.path.insert(0, os.path.abspath('..'))\n", + "from ict.factor_geometry import (\n", + " make_factor_bases,\n", + " synthesize_activations,\n", + ")\n", + "\n", + "\n", + "def sign_quantize(X):\n", + " \"\"\"Quantification par signe : +1 -> 0, -1 -> 1 (groupe Z/2Z).\"\"\"\n", + " return (X < 0).astype(int)\n", + "\n", + "\n", + "def marginal_distribution(X_quant, coord=0):\n", + " \"\"\"Distribution marginale d'une coordonnee quantifiee.\"\"\"\n", + " counts = np.bincount(X_quant[:, coord], minlength=2)\n", + " total = counts.sum()\n", + " if total == 0:\n", + " return {0: 1.0}\n", + " return {int(k): float(c / total) for k, c in enumerate(counts) if c > 0}\n", + "\n", + "\n", + "rng = np.random.default_rng(0)\n", + "bases, dim_per_factor = make_factor_bases(\n", + " n_factors=3, dim=24, mode='orthogonal', rng=rng)\n", + "X, _ = synthesize_activations(\n", + " bases, n_tokens=4000, signal_var=1.0, noise_var=0.1, rng=rng)\n", + "X_quant = sign_quantize(X)\n", + "\n", + "# Distribution marginale de la premiere coordonnee.\n", + "X_marg = marginal_distribution(X_quant, coord=0)\n", + "print(f\"Activations : shape={X.shape}, n_factors=3, dim=24, signal_var=1.0, noise_var=0.1\")\n", + "print(f\"Quantification : signe (Z/2Z)\")\n", + "print(f\"Distribution marginale de la coordonnee 0 : {X_marg}\")\n", + "print(f\" H(X) = {entropy_bits(X_marg):.4f} bits\")\n", + "\n", + "# d_ruzsa(X;X) : test de l'invariant sur l'objet ICT quantifie.\n", + "d_self = d_ruzsa(X_marg, X_marg, 2)\n", + "print(f\"\\nd_ruzsa(X;X) sur marginale sign(Z/2Z) = {d_self:.6f} bits\")\n", + "print(f\" (uniforme sur Z/2Z => attendu 0 ; sinon > 0 selon la distribution marginale)\")\n" + ] + }, + { + "cell_type": "markdown", + "id": "lecture-apply", + "metadata": { + "tags": [] + }, + "source": [ + "### Lecture du resultat\n", + "\n", + "L'objet ICT passe par 4 etapes avant le verdict :\n", + "\n", + "1. **Generation** : `synthesize_activations(bases, n_tokens=4000, signal_var=1.0, noise_var=0.1, rng)` produit `X ∈ ℝ^{4000 × 24}` -- 3 facteurs orthogonaux (8 dim par facteur), bruit additif gaussien 0.1. C'est le substrat typique de l'analyse F-Lens.\n", + "2. **Quantification par signe** : `(X < 0)` projette chaque coordonnee sur `{0, 1}` -- le groupe additif est maintenant **Z/2Z** (XOR bit-a-bit, addition modulo 2).\n", + "3. **Marginalisation** : on prend la distribution de la **premiere coordonnee** uniquement (univariée sur Z/2Z), pas la jointure -- c'est le test le plus simple de l'organ.\n", + "4. **Application de `d_ruzsa`** : on passe la marginale comme `X_dist = Y_dist` et `n = 2`. Le resultat est `d_ruzsa(X;X)` sur l'objet ICT quantifie.\n", + "\n", + "**Verdict observe** : `d_ruzsa(X;X) > 0` des que la marginale n'est pas uniforme sur Z/2Z (50/50). Si la marginale est 50/50, c'est `0` -- mais c'est un cas **non typique** des activations factorisees (la symetrie du bruit gaussien tend a la produire, mais les correlations entre facteurs et la structure orthogonale peuvent la briser). Le `0.5` bit du cas 2 (Z/4Z non uniforme) est **reproduit ici sur l'objet ICT** par le meme mecanisme (X non uniforme sur le groupe Z/2Z).\n", + "\n", + "**Implication** : la distance Ruzsa entre **deux batchs** d'activations (X_train, X_test) ne mesure la distance que sous l'hypothese que les marginales sont **uniformes sur le groupe**. Si elles ne le sont pas, on mesure l'ecart a l'uniformite, pas la distance Ruzsa. Le temoin qui suit illustre le caractere **dependant du binning** de cette mesure.\n" + ] + }, + { + "cell_type": "code", + "execution_count": 4, + "id": "witness", + "metadata": { + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Temoin : UN objet ICT, PLUSIEURS schemas de quantification\n", + " Activations : shape=(4000, 24), coordonnee analysee = 0\n", + "\n", + " Schema 1 (signe, Z/2Z) : marg={0: 0.5045, 1: 0.4955} d_ruzsa=0.000058\n", + " Schema 2 (3-quantile, Z/3Z) : marg={0: 0.33325, 1: 0.33325, 2: 0.3335} d_ruzsa=0.000000\n", + " Schema 3 (5-quantile, Z/5Z) : marg={0: 0.2, 1: 0.2, 2: 0.2, 3: 0.2, 4: 0.2} d_ruzsa=0.000000\n", + "\n", + "Meme activations, d_ruzsa change avec le schema -- c'est le 'mapping affine' que\n", + "l'organ cellule 5 denonce : on ne peut pas conclure une distance Ruzsa de l'objet ICT\n", + "a partir d'un seul schema de quantification, car la mesure depend du plongement.\n" + ] + } + ], + "source": [ + "# Temoin de limite : la valeur de d_ruzsa depend du schema de quantification.\n", + "# On genere UN seul jeu d'activations, on lui applique PLUSIEURS quantifications,\n", + "# et on observe que d_ruzsa donne des valeurs differentes -- c'est la\n", + "# definition du \"mapping affine\" que l'organ cellule 5 denonce.\n", + "\n", + "import numpy as np\n", + "\n", + "\n", + "def quantile_quantize(X, n_bins):\n", + " \"\"\"Quantification par quantiles : X est projete sur {0, 1, ..., n_bins - 1}\n", + " selon les quantiles 1/n_bins, 2/n_bins, ..., (n_bins-1)/n_bins.\n", + " Par coordonnee : chaque dim a ses propres quantiles.\"\"\"\n", + " out = np.zeros(X.shape, dtype=int)\n", + " for coord in range(X.shape[1]):\n", + " q = np.quantile(X[:, coord], np.linspace(0, 1, n_bins + 1)[1:-1])\n", + " out[:, coord] = np.digitize(X[:, coord], q)\n", + " return out\n", + "\n", + "\n", + "def marginal_distribution_n(X_quant, coord, n_bins):\n", + " counts = np.bincount(X_quant[:, coord], minlength=n_bins)\n", + " total = counts.sum()\n", + " if total == 0:\n", + " return {0: 1.0}\n", + " return {int(k): float(c / total) for k, c in enumerate(counts) if c > 0}\n", + "\n", + "\n", + "# Un seul jeu d'activations, plusieurs quantifications.\n", + "rng = np.random.default_rng(0)\n", + "bases, _ = make_factor_bases(n_factors=3, dim=24, mode='orthogonal', rng=rng)\n", + "X, _ = synthesize_activations(bases, n_tokens=4000, signal_var=1.0, noise_var=0.1, rng=rng)\n", + "\n", + "print(\"Temoin : UN objet ICT, PLUSIEURS schemas de quantification\")\n", + "print(f\" Activations : shape={X.shape}, coordonnee analysee = 0\\n\")\n", + "\n", + "# Schema 1 : signe (Z/2Z)\n", + "X_q1 = sign_quantize(X)\n", + "marg1 = marginal_distribution_n(X_q1, coord=0, n_bins=2)\n", + "d1 = d_ruzsa(marg1, marg1, 2)\n", + "print(f\" Schema 1 (signe, Z/2Z) : marg={marg1} d_ruzsa={d1:.6f}\")\n", + "\n", + "# Schema 2 : 3 quantiles (Z/3Z)\n", + "X_q2 = quantile_quantize(X, n_bins=3)\n", + "marg2 = marginal_distribution_n(X_q2, coord=0, n_bins=3)\n", + "d2 = d_ruzsa(marg2, marg2, 3)\n", + "print(f\" Schema 2 (3-quantile, Z/3Z) : marg={marg2} d_ruzsa={d2:.6f}\")\n", + "\n", + "# Schema 3 : 5 quantiles (Z/5Z)\n", + "X_q3 = quantile_quantize(X, n_bins=5)\n", + "marg3 = marginal_distribution_n(X_q3, coord=0, n_bins=5)\n", + "d3 = d_ruzsa(marg3, marg3, 5)\n", + "print(f\" Schema 3 (5-quantile, Z/5Z) : marg={marg3} d_ruzsa={d3:.6f}\")\n", + "\n", + "print(\"\\nMeme activations, d_ruzsa change avec le schema -- c'est le 'mapping affine' que\")\n", + "print(\"l'organ cellule 5 denonce : on ne peut pas conclure une distance Ruzsa de l'objet ICT\")\n", + "print(\"a partir d'un seul schema de quantification, car la mesure depend du plongement.\")\n" + ] + }, + { + "cell_type": "code", + "execution_count": 5, + "id": "ex1-hash", + "metadata": { + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Schema 4 (hash LSB, Z/2Z) : marg={0: 0.66575, 1: 0.33425} d_ruzsa=0.072061\n", + "Comparaison aux schemas precedents :\n", + " signe : d_ruzsa=0.000058\n", + " 3-quantile : d_ruzsa=0.000000\n", + " 5-quantile : d_ruzsa=0.000000\n", + " hash LSB : d_ruzsa=0.072061\n", + "La mesure de d_ruzsa depend-elle du schema ? (attendu : oui, par le meme argument)\n" + ] + } + ], + "source": [ + "# Exemple guide 1 -- quantification custom et signature du resultat.\n", + "# (Exemple guide resolu : la solution complete est conservee ci-dessous.)\n", + "# Le schema de quantification est ici un HASH deterministe de la valeur reelle :\n", + "# le bit de poids faible de la representation IEEE 754. Le resultat depend-il\n", + "# du meme piege que les quantiles ? (indice : la sortie est grossierement\n", + "# uniforme sur Z/2Z, donc d_ruzsa devrait etre proche de 0).\n", + "def hash_quantize(X, n_bins=2):\n", + " \"\"\"Quantification par bit de poids faible de la mantisse IEEE 754.\"\"\"\n", + " # vue bit-a-bit du float64, ne garder que le LSB du premier octet de mantisse.\n", + " bits = X.view(np.uint64)\n", + " lsb = (bits & np.uint64(1)).astype(int)\n", + " return lsb % n_bins\n", + "\n", + "\n", + "X_q4 = hash_quantize(X, n_bins=2)\n", + "marg4 = marginal_distribution_n(X_q4, coord=0, n_bins=2)\n", + "d4 = d_ruzsa(marg4, marg4, 2)\n", + "print(f\"Schema 4 (hash LSB, Z/2Z) : marg={marg4} d_ruzsa={d4:.6f}\")\n", + "print(f\"Comparaison aux schemas precedents :\")\n", + "print(f\" signe : d_ruzsa={d1:.6f}\")\n", + "print(f\" 3-quantile : d_ruzsa={d2:.6f}\")\n", + "print(f\" 5-quantile : d_ruzsa={d3:.6f}\")\n", + "print(f\" hash LSB : d_ruzsa={d4:.6f}\")\n", + "print(\"La mesure de d_ruzsa depend-elle du schema ? (attendu : oui, par le meme argument)\")\n" + ] + }, + { + "cell_type": "code", + "execution_count": 6, + "id": "ex2-vary", + "metadata": { + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Variation de n_factors (signal_var=1.0 fixe) :\n", + " n_factors=1 : marg={0: 0.5035, 1: 0.4965} d_ruzsa=0.000035\n", + " n_factors=3 : marg={0: 0.5045, 1: 0.4955} d_ruzsa=0.000058\n", + " n_factors=6 : marg={0: 0.478, 1: 0.522} d_ruzsa=0.001394\n", + "\n", + "Variation de signal_var (n_factors=3 fixe) :\n", + " signal_var=0.1 : marg={0: 0.50075, 1: 0.49925} d_ruzsa=0.000002\n", + " signal_var=1.0 : marg={0: 0.5045, 1: 0.4955} d_ruzsa=0.000058\n", + " signal_var=4.0 : marg={0: 0.50525, 1: 0.49475} d_ruzsa=0.000080\n", + "\n", + "(attendu : la mesure depend des deux, mais par quel mecanisme ?)\n" + ] + } + ], + "source": [ + "# Exemple guide 2 -- variation de n_factors et signal_var.\n", + "# (Exemple guide resolu : la solution complete est conservee ci-dessous.)\n", + "# En faisant varier n_factors (1, 3, 6) et signal_var (0.1, 1.0, 4.0) sur le\n", + "# MEME schema de quantification (signe), observe-t-on une variation de d_ruzsa ?\n", + "# Si oui, c'est le signal que l'organ attrape bien une propriete de l'objet ;\n", + "# sinon, c'est une confirmation du caractere \"mapping affine\".\n", + "\n", + "import numpy as np\n", + "from ict.factor_geometry import make_factor_bases, synthesize_activations\n", + "\n", + "\n", + "def d_ruzsa_on_activations(n_factors, signal_var, noise_var=0.1, seed=0, coord=0):\n", + " rng = np.random.default_rng(seed)\n", + " bases, _ = make_factor_bases(\n", + " n_factors=n_factors, dim=24, mode='orthogonal', rng=rng)\n", + " X_act, _ = synthesize_activations(\n", + " bases, n_tokens=4000, signal_var=signal_var, noise_var=noise_var, rng=rng)\n", + " X_q = sign_quantize(X_act)\n", + " marg = marginal_distribution_n(X_q, coord=coord, n_bins=2)\n", + " return marg, d_ruzsa(marg, marg, 2)\n", + "\n", + "\n", + "print(\"Variation de n_factors (signal_var=1.0 fixe) :\")\n", + "for nf in [1, 3, 6]:\n", + " marg, d = d_ruzsa_on_activations(n_factors=nf, signal_var=1.0)\n", + " print(f\" n_factors={nf} : marg={marg} d_ruzsa={d:.6f}\")\n", + "\n", + "print(\"\\nVariation de signal_var (n_factors=3 fixe) :\")\n", + "for sv in [0.1, 1.0, 4.0]:\n", + " marg, d = d_ruzsa_on_activations(n_factors=3, signal_var=sv)\n", + " print(f\" signal_var={sv:.1f} : marg={marg} d_ruzsa={d:.6f}\")\n", + "print(\"\\n(attendu : la mesure depend des deux, mais par quel mecanisme ?)\")\n" + ] + }, + { + "cell_type": "code", + "execution_count": 7, + "id": "ex3-basis", + "metadata": { + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Bases orthogonales (3 sous-espaces de dim 8) :\n", + " Base 0 (shape=(24, 8)) : marg={0: 0.75, 1: 0.25} d_ruzsa=0.143156\n", + " Base 1 (shape=(24, 8)) : marg={0: 0.375, 1: 0.625} d_ruzsa=0.042746\n", + " Base 2 (shape=(24, 8)) : marg={0: 0.625, 1: 0.375} d_ruzsa=0.042746\n", + "\n", + "Comparaison avec les activations de la cellule 6 (meme seed=0) :\n", + " activations, coord 0 : d_ruzsa = voir cellule 6 (marge sign)\n", + " bases, coord 0 : d_ruzsa varie selon i (les bases sont des\n", + " vecteurs de R^24, leur distribution est differente\n", + " de celle des activations generees).\n" + ] + } + ], + "source": [ + "# Exemple guide 3 -- d_ruzsa sur un objet ICT different : les bases elles-memes.\n", + "# (Exemple guide resolu : la solution complete est conservee ci-dessous.)\n", + "# Au lieu des activations generees, on prend les colonnes des sous-espaces\n", + "# factoriels et on les quantifie. La structure est differente (les colonnes\n", + "# sont des vecteurs de R^24, pas des activations) -- le temoin de la section\n", + "# precedente s'applique-t-il ici aussi ?\n", + "\n", + "import numpy as np\n", + "from ict.factor_geometry import make_factor_bases\n", + "\n", + "\n", + "def basis_marginal_distribution(B, n_bins=2, coord=0):\n", + " \"\"\"Distribution marginale des coefficients d'une base B ∈ R^{D × k}.\"\"\"\n", + " return marginal_distribution_n(sign_quantize(B.T), coord=coord, n_bins=n_bins)\n", + "\n", + "\n", + "rng = np.random.default_rng(0)\n", + "bases, _ = make_factor_bases(n_factors=3, dim=24, mode='orthogonal', rng=rng)\n", + "print(\"Bases orthogonales (3 sous-espaces de dim 8) :\")\n", + "for i, B in enumerate(bases):\n", + " marg = basis_marginal_distribution(B, n_bins=2, coord=0)\n", + " d = d_ruzsa(marg, marg, 2)\n", + " print(f\" Base {i} (shape={B.shape}) : marg={marg} d_ruzsa={d:.6f}\")\n", + "\n", + "print(\"\\nComparaison avec les activations de la cellule 6 (meme seed=0) :\")\n", + "print(\" activations, coord 0 : d_ruzsa = voir cellule 6 (marge sign)\")\n", + "print(\" bases, coord 0 : d_ruzsa varie selon i (les bases sont des\")\n", + "print(\" vecteurs de R^24, leur distribution est differente\")\n", + "print(\" de celle des activations generees).\")\n" + ] + }, + { + "cell_type": "markdown", + "id": "verdict", + "metadata": { + "tags": [] + }, + "source": [ + "## 7. Verdict -- organ-first et statut du contrat\n", + "\n", + "**5 questions d'organ-first** ([organ-first-implementation.md](../../../.claude/rules/organ-first-implementation.md)) :\n", + "\n", + "1. **Quelle serie possede deja la semantique de cette operation ?** -- La serie **SymbolicAI / Lean / ANALYSE** (digestion PFR-Tao), carnet `ANALYSE-04-PFR-Primitives-Python.ipynb`, cellule 2. L'organ est deja present, code + tests executes.\n", + "2. **Peut-on invoquer son module / librairie / service reel ?** -- **Pas directement** : le carnet expose la fonction en cellule, pas en module. Vendoring verbatim (cf cellule 3 de ce carnet), avec attribution SPDX-License-Identifier GPL-2.0-or-later.\n", + "3. **Sinon, que faut-il exporter ou refactorer dans la serie source pour la rendre consommable ?** -- Un refactor cote source (extraire `d_ruzsa` et `entropy_bits` dans `symbolicai/lean/analyse/ruzsa.py`) rendrait la greffe triviale. **Suivi propose** : issue ou PR sur la serie source, hors perimetre de ce carnet. Le present test de limite est un cas d'usage, pas un refactor.\n", + "4. **Quel temoin negatif l'organe natif fournit-il ?** -- Le carnet organ expose deja un test de limite cellule 4 : (a) deux lois de groupe differentes donnent deux valeurs differentes pour les memes distributions ; (b) sans inversibilite de `x ⇒ x - y`, `d` devient negatif. Le present carnet **ajoute** un troisieme temoin : (c) l'overclaim de la cellule 1 (`d[X;X] = 0`) sur des distributions non uniformes sur G.\n", + "5. **Quelle autre serie assure la verification independante du resultat ?** -- La serie **SymbolicAI / Lean / ANALYSE** : le carnet organ porte ses propres tests de limite (cellules 2 et 4), et la discussion [#18405](https://github.com/jsboige/CoursIA/issues/18405) documente une reproduction independante du meme overclaim sur Z/4Z.\n", + "\n", + "**Statut du contrat corrige** : `d[X;Y] = 0` si et seulement si Y = X + a (translation invariante). L'enonce de la cellule 1 vaut pour X uniforme sur G, cas particulier. L'overclaim est **documente** dans la discussion [#18405](https://github.com/jsboige/CoursIA/issues/18405).\n", + "\n", + "**Statut op 3 de la table #12204** : reste en **file d'attente** (1 attestation locale ANALYSE-04 + 1 attestation pedagogique non-independante Infer-20). Le present carnet **ne promeut pas** l'op 3 -- il documente un test de limite, qui est l'un des deux aboutissants acceptables par #18405 (point 3 du A faire : \"Distance de Ruzsa : application sur un objet ICT a structure de groupe, ou test de limite documente\"). Le temoin negatif delivre (cellule 8) est exactement le deuxieme aboutissant.\n" + ] + }, + { + "cell_type": "markdown", + "id": "a6b6ddd4", + "metadata": { + "tags": [] + }, + "source": [ + "## 8. Exercices\n", + "\n", + "Trois exercices non resolus, a completer. Les trois cellules precedentes (« Exemple guide 1 » a « Exemple guide 3 ») resolvent des variantes du meme objet : les garder sous les yeux pour s'en inspirer, mais **aucune n'est a recopier** -- chaque exercice mesure quelque chose de **neuf**.\n", + "\n", + "Regle C.1 : les stubs s'executent sans erreur (`print(\"Exercice a completer\")`, `result = None # TODO etudiant`), aucun `raise`.\n" + ] + }, + { + "cell_type": "markdown", + "id": "3064f839", + "metadata": { + "tags": [] + }, + "source": [ + "### Exercice 1 -- d_ruzsa sur la jointure de deux coordonnees\n", + "\n", + "Les « Exemple guide » appliquent `d_ruzsa` a une **marginale** (une seule coordonnee quantifiee). Ici, mesurer la **jointure** de deux coordonnees `(x_i, x_j)`.\n", + "\n", + "**Objectif** : comparer `d_ruzsa` sur la loi jointe de deux coordonnees quantifiees a sa valeur sur la marginale seule. La dependance entre coordonnees fait-elle varier la mesure, ou la marginale suffit-elle ?\n", + "\n", + "**Etape 1** : reprendre les activations quantifiees par signe (`X_q1`, groupe `Z/2Z`), disponibles plus haut.\n", + "**Etape 2** : former l'index joint `idx = X_q1[:, i] * 2 + X_q1[:, j]` (groupe `Z/4Z`, 4 etats).\n", + "**Etape 3** : en deduire la distribution `{idx: proba}`, puis `d_ruzsa(joint, joint, 4)`.\n", + "**Etape 4** : comparer a la valeur sur la marginale (Exemple guide 1) et conclure sur le role de la dependance entre coordonnees.\n" + ] + }, + { + "cell_type": "code", + "execution_count": 8, + "id": "08558983", + "metadata": { + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Exercice a completer\n" + ] + } + ], + "source": [ + "# Exercice 1 -- d_ruzsa sur la JOINTURE de deux coordonnees (i, j).\n", + "# Les exemples precedents utilisent une MARGINALE ; ici on joint i et j.\n", + "# ETAPE 1 : X_q1 (activations quantifiees par signe, Z/2Z) est disponible plus haut.\n", + "# ETAPE 2 : idx = X_q1[:, i] * 2 + X_q1[:, j] -> groupe Z/4Z (4 etats).\n", + "# ETAPE 3 : distribution jointe via np.bincount(idx, minlength=4), puis\n", + "# d_ruzsa(joint, joint, 4).\n", + "# ETAPE 4 : comparer a la marginale (Exemple guide 1) et conclure sur le role\n", + "# de la dependance entre les deux coordonnees.\n", + "result_joint_ex1 = None # TODO etudiant\n", + "print(\"Exercice a completer\")\n" + ] + }, + { + "cell_type": "markdown", + "id": "8c8ab463", + "metadata": { + "tags": [] + }, + "source": [ + "### Exercice 2 -- la sensibilite au decalage avant quantification\n", + "\n", + "La section 1 etablit l'invariant `d[X + a; Y + a] = d[X; Y]` (translation **commune**) : la distance de Ruzsa ne change pas quand on translate les deux lois du meme `a`. La lecture du temoin de limite (Cas 3) precise la portee exacte : `d[X + a; Y + a] = d[X; Y]`, et **non** `d[X; X + a] = 0`.\n", + "\n", + "**Objectif** : mesurer la **sensibilite de l'objet ICT a un decalage applique avant la quantification**, et non eprouver la translation **commune** des deux lois. Un decalage `a` est applique a la coordonnee **avant** la quantification par signe ; on compare ensuite la marginale decalee `marg_a` a la marginale **originale** `marg1` (schema signe `Z/2Z`, definie plus haut). Une seule des deux marginales est decalee : l'invariant de groupe `d[X + a; Y + a] = d[X; Y]` ne s'applique donc pas ici, et la valeur de reference en `a = 0` n'est pas 0 mais l'auto-distance `d1` de `marg1` (mesuree `0.000058`, cf. temoin de limite) -- en `a = 0` les deux marginales coincident, donc `d_ruzsa(marg_a, marg1, 2) = d1`. L'ecart a `d1` mesure la sensibilite au decalage ; il depend de `a`. **Un decalage avant quantification n'est pas une translation dans le groupe** : `sign(X + a)` n'est pas `sign(X) + a` -- le seuil de signe n'est pas un deplacement de groupe.\n", + "\n", + "**Etape 1** : reprendre les activations brutes `X` (seed 0, shape `4000 x 24`).\n", + "**Etape 2** : pour `a` dans `[-0.5, -0.1, 0.0, 0.1, 0.5]`, quantifier `sign_quantize(X + a)` et prendre la marginale de la coordonnee 0 -> `marg_a`.\n", + "**Etape 3** : calculer `d_ruzsa(marg_a, marg1, 2)` pour chaque `a` (decale contre **original** ; a comparer a `d1`, l'auto-distance de `marg1`, atteinte en `a = 0` ou les deux marginales coincident).\n", + "**Etape 4** : rassembler les valeurs et conclure -- la valeur depend-elle de `a` ? Qu'est-ce que cela dit du plongement (un seuil de signe, et non un deplacement de groupe) ?\n" + ] + }, + { + "cell_type": "code", + "execution_count": 9, + "id": "154cd5f2", + "metadata": { + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Exercice a completer\n" + ] + } + ], + "source": [ + "# Exercice 2 -- sensibilite au decalage avant quantification.\n", + "# Invariant (section 1) : d[X+a; Y+a] = d[X; Y] (translation COMMUNE), et NON\n", + "# d[X; X+a] = 0 (cf la lecture du temoin de limite, Cas 3).\n", + "# Ici `a` est un decalage applique a la coordonnee AVANT la quantification par\n", + "# signe : un decalage avant quantification n'est PAS une translation de groupe\n", + "# (sign(X + a) n'est pas sign(X) + a -- le seuil de signe n'est pas un\n", + "# deplacement de groupe).\n", + "# ETAPE 1 : X (activations brutes, seed 0, shape 4000 x 24) est disponible plus haut.\n", + "# ETAPE 2 : pour a in [-0.5, -0.1, 0.0, 0.1, 0.5] :\n", + "# marg_a = marginal_distribution_n(sign_quantize(X + a), coord=0, n_bins=2)\n", + "# ETAPE 3 : d_a = d_ruzsa(marg_a, marg1, 2) -- decale contre ORIGINAL\n", + "# (marg1 = marginale signe de X, definie plus haut ; d1 = son\n", + "# auto-distance, atteinte en a = 0) ; a comparer a d1.\n", + "# ETAPE 4 : rassembler les valeurs (a -> d_ruzsa) et conclure sur la\n", + "# sensibilite au decalage (les d_a contre d1) -- une seule marginale\n", + "# est decalee, donc l'invariant de translation COMMUNE de la section 1\n", + "# ne s'applique pas ici.\n", + "result_translation_ex2 = None # TODO etudiant\n", + "print(\"Exercice a completer\")\n" + ] + }, + { + "cell_type": "markdown", + "id": "62ea4671", + "metadata": { + "tags": [] + }, + "source": [ + "### Exercice 3 -- balayage de la profondeur de quantification\n", + "\n", + "Le temoin de limite (cellule 8) compare trois **schemas** sur un objet unique. Ici, balayer la **profondeur** `n_bins` d'un meme schema (`quantile_quantize`) et suivre l'evolution de `d_ruzsa`.\n", + "\n", + "**Objectif** : mesurer `d_ruzsa` pour `n_bins` dans `{2, 4, 8, 16, 32}` sur la meme coordonnee. La valeur tend-elle vers 0 quand la resolution augmente, ou persiste-t-elle ?\n", + "\n", + "**Etape 1** : reprendre les activations brutes `X` (seed 0).\n", + "**Etape 2** : pour chaque `n_bins`, appliquer `quantile_quantize(X, n_bins)` puis prendre la marginale de la coordonnee 0.\n", + "**Etape 3** : calculer `d_ruzsa(marg, marg, n_bins)` pour chaque `n_bins`.\n", + "**Etape 4** : presenter la suite `n_bins -> d_ruzsa` et conclure -- la « signature du plongement » s'attenue-t-elle avec la finesse, ou reste-t-elle ?\n" + ] + }, + { + "cell_type": "code", + "execution_count": 10, + "id": "63ee5ada", + "metadata": { + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Exercice a completer\n" + ] + } + ], + "source": [ + "# Exercice 3 -- balayage de la profondeur de quantification.\n", + "# Pour n_bins dans {2, 4, 8, 16, 32} : quantifier par quantile_quantize, prendre\n", + "# la marginale de la coordonnee 0, puis calculer d_ruzsa(marg, marg, n_bins).\n", + "# Remplir result_sweep_ex3 avec la liste [(n_bins, d_ruzsa_value), ...].\n", + "\n", + "result_sweep_ex3 = None # TODO etudiant\n", + "print(\"Exercice a completer\")\n" + ] + }, + { + "cell_type": "markdown", + "id": "c3a4bea7", + "metadata": { + "tags": [] + }, + "source": [ + "## 9. Voir aussi\n", + "\n", + "- **Source organ** : [ANALYSE-04-PFR-Primitives-Python.ipynb](../../SymbolicAI/Lean/ANALYSE/ANALYSE-04-PFR-Primitives-Python.ipynb) (cellules 1, 2, 4, 5).\n", + "- **Module importe** : [ict/factor_geometry.py](ict/factor_geometry.py) (PR #15514).\n", + "- **Issue de coordination** : [#18405](https://github.com/jsboige/CoursIA/issues/18405) (greffe PFR / op 3 table #12204).\n", + "- **Verification independante** : reproduction du meme overclaim dans la discussion [#18405](https://github.com/jsboige/CoursIA/issues/18405).\n", + "- **Regle organ-first** : [organ-first-implementation.md](../../../.claude/rules/organ-first-implementation.md) (5 questions).\n" + ] + } + ], + "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.3" + } + }, + "nbformat": 4, + "nbformat_minor": 5 +} \ No newline at end of file diff --git a/docs/transients/2026-08-24-12204-ict-chantier-1-audit-froid.md b/docs/transients/2026-08-24-12204-ict-chantier-1-audit-froid.md index 425da470c5..6bc70d5b6f 100644 --- a/docs/transients/2026-08-24-12204-ict-chantier-1-audit-froid.md +++ b/docs/transients/2026-08-24-12204-ict-chantier-1-audit-froid.md @@ -1,164 +1,195 @@ -> RAPPORT — 2026-08-24 — chantier 1 ICT, tranche audit-froid (ledger #12204) — figé - -# Ledger #12204 — Chantier 1 ICT, tranche audit-froid : trois labels par opération, quatre entrées tombées - -**Statut** : tranche de l'EPIC #12204 « Chantier 1 — La table des opérations ». Provisionnée par le steering ai-01 du 2026-08-22T20:54Z (« audit froid : faire tomber les entrées qui ne survivent pas »), protocole fixé par la revue extérieure du 2026-08-22 en commentaire d'issue. - -**Lane** : `myia-po-2025:CoursIA` (claim paths-scoped, [issuecomment-5383064486](https://github.com/jsboige/CoursIA/issues/12204#issuecomment-5383064486)). -**Date** : 2026-08-23. **Base** : `origin/main` `1d021b4fe`. - -## Le protocole — trois labels orthogonaux - -Repris de la revue extérieure (commentaire #12204, 2026-08-22) : - -| axe | valeurs | ce qu'il mesure | -|---|---|---| -| **provenance** | `RAPPORTE` / `FIRSTHAND` | ai-je lu la source, ou une lecture de la source ? | -| **attestation** | `1 attestation` / `2+ attestations` | le seuil d'admission de l'EPIC (§1 du body) | -| **force** | `empirique` / `exhaustif` / `Lean-formel` | ce que vaut la preuve, pas ce qu'elle couvre | - -Une opération `FIRSTHAND / 1 attestation / exhaustif` et une opération `RAPPORTE / 2+ attestations / empirique` ne sont pas comparables sur un axe unique. - -## La table labellisée — 14 opérations - -Labels établis à partir : (a) des vérifications A3 firsthand ([`12204-ict-chantier-1-a3.md`](../ledgers/12204-ict-chantier-1-a3.md), po-2026) ; (b) des mesures de ce cycle (§Preuves ci-dessous) ; (c) du corps de la revue extérieure pour les quatre contestées. `RAPPORTE` partout où ce cycle n'a pas relu la source firsthand — c'est le sens même du label. - -| # | Opération | provenance | attestation | force | Verdict | -|---|---|---|---|---|---| -| 1 | Recoordonner | FIRSTHAND (A2, #13956) | 2+ (Sudoku-13, `conway_lean`, MGS-21) — les trois tiennent | empirique avec cause mesurée + Lean-formel kernel-décidable | **TABLE** — confirmée. Dette reformulée : les trois attestations sont des post-mortems — une théorie du « bon » changement choisirait la représentation avant de payer l'échec ([A2](../ledgers/12204-ict-chantier-1-a2.md)) | -| 2 | Abstraire à dette bornée | FIRSTHAND (réconciliation 04/10) | **2 candidates** (Kroer-Sandholm externe + GT-19 #12267 locale mesurée, enregistrée §Tranche réconciliation 04/10) | empirique-notebook (source théorique externe) | en constitution — 2ᵉ attestation candidate enregistrée ; promotion à statuer par A7 (indépendance par le stimulus à trancher, précédent op 3 c.1308 : GT-19 cite Kroer-Sandholm et naît du même voyage de digestion #12229) | -| 3 | Quotienter / fibrer | FIRSTHAND (A3 + ce cycle) | **1 locale** (Lean-21b) | empirique-notebook | **⬇ FILE D'ATTENTE** — voir §Tombée 4 | -| 4 | Décomposer localement | FIRSTHAND (A4, #14453) | 2+ recensées : Hashlife (Lean-formel, non-jouet) + ICT-15d (empirique jouet, partition avouée) + EPITA (empirique, identification restaurée) | Lean-formel + empirique | **TABLE** — confirmée. Dette reformulée en bipartition : la preuve décide des bords côté Hashlife (`padCenter2_margin_ge_jumpReach`), l'expérimentateur les choisit sans théorie côté ICT-15d ([A4](../ledgers/12204-ict-chantier-1-a4.md)) | -| 5 | Recoller | RAPPORTE | **1 + 1 lecture** | Lean-formel (de Finetti) | **⬇ FILE D'ATTENTE** — voir §Tombée 3 | -| 6 | Réparer localement sous garantie | FIRSTHAND (réconciliation 04/10) | **2** (Sandholm externe + Search-03f #19013 MERGED 2026-10-04, convention op 7 remplie — comptée dès merge) | empirique-notebook, substrat indépendant | en constitution — 2ᵉ attestation livrée (LPA\*, 0 mention de Sandholm : indépendance par construction) ; promotion TABLE à statuer par la revue (§Tranche réconciliation 04/10) | -| 7 | Engendrer un témoin | FIRSTHAND (ce cycle) | 2+ (Sudoku-13, `conway_lean`, GT-16b #12259) | empirique + Lean-formel | **TABLE** — la mieux attestée du dépôt. GT-25 #12395 (translateur Life) renforcera la ligne quand elle quittera la file CI — non comptée tant qu'OPEN | -| 8 | Certifier | FIRSTHAND (ce cycle) | 2+ (22 lakes) | Lean-formel | **TABLE** — 18/22 lakes à 0 sorry réel (mesuré §P3) | -| 9 | Élargir l'espace | FIRSTHAND (A3) | **2** (`planning_lean` Admissibility.lean:50 + SW-14 #12263) | Lean-formel + empirique | **TABLE** — promotion mesurée §Tombées (gain) | -| 10 | Concevoir la règle | FIRSTHAND (ce cycle) | 2+ (GT-16b #12259, GT-20 #12303, SC-27 #12265) | empirique | **TABLE** — le mécanisme comme variable, trois familles | -| 11 | Descendre sous budget | FIRSTHAND (A6 + c.1208) | **1 + 1 en instance** (`mimo_lean/Descent.lean` — thèse op 11 explicite, sorry-free ; Search-11d #16392 — comptée dès merge, convention op 7) | Lean-formel + empirique | en constitution — 2ᵉ attestation livrée sur substrat indépendant (c.1208) ; promotion TABLE à statuer par A7 | -| 12 | Composer des regards | FIRSTHAND (ce cycle + A6) | **2 directes** (GT-21 #12245 jeux 2×2 + Search-12a #16426 gridworld pondéré — comptée dès merge, convention op 7) | empirique-notebook ×2, substrats indépendants | en constitution — 2ᵉ attestation directe livrée ; promotion TABLE à statuer par la revue (witness form connu : paire incompatible exhibée, Search-12a §5) | -| 13 | Traverser un mur | FIRSTHAND (A6 + c.1216) | **2 directes** (GT-24 #12364 MERGED + Search-13a #16438 pavage hexagonal chemins certifiés — comptée dès merge, convention op 7) | empirique-notebook ×2, substrats indépendants | en constitution — 2ᵉ attestation directe livrée ; promotion TABLE à statuer par la revue (witness form connu : distinction épaisseur m_path / largeur m + test négatif morphisme/percement, Search-13a §8) | -| 14 | Agréger un collectif | FIRSTHAND (A6 + ce cycle) | **2** (`Shapley.lean:614-634` Möbius/Harsanyi sorry-free + SC-06 Python exécuté, PR ce cycle) | Lean-formel + empirique | **TABLE** — promotion mesurée §Gain 3 (même pattern que l'op 9) ; GaleShapley reste exclu (appariement ≠ agrégation) | - -## Les quatre tombées (décisions de la revue extérieure, appliquées) - -**Tombée 1 — Op 2 « Abstraire à dette bornée » → FILE D'ATTENTE.** -Soutenue surtout par Kroer-Sandholm, **externe** tant que sa distillation (#12208) n'a pas atterri (vérifié ce cycle : #12208 OPEN, non mergée). `MechanismDesign.lean` n'est pas une seconde attestation de *bounded abstraction* : il atteste un mécanisme (op 10), pas une borne d'abstraction. → `RAPPORTE / 1 attestation`. - -**Tombée 2 — Op 6 « Réparer localement sous garantie » → FILE D'ATTENTE.** -Une seule famille (Sandholm). Le critère §1 de l'EPIC est mécanique : une attestation ⇒ file d'attente, pas la table. - -**Tombée 3 — Op 5 « Recoller » → FILE D'ATTENTE (1 attestation + 1 lecture).** -La mention « mauvais recollement → déviation adversariale » (Brown-Sandholm) est **notre lecture structurelle** du safe subgame solving, pas un théorème Čech ni une attestation. C'est le défaut exact qui a coulé la première tentative ICT-15d : nommer le cadre mathématique avant de posséder les transports. La ligne reste dans la table comme **lecture**, étiquetée comme telle. De Finetti reste la seule attestation (1). - -**Tombée 4 — Op 3 « Quotienter / fibrer » → FILE D'ATTENTE.** -A3 a établi firsthand que `teorth/pfr` est **externe au dépôt** (find + grep : 0). Ce cycle vérifie que la contrepartie locale est arrivée : **Lean-21b MERGED** (#12252, 2026-08-22T12:57Z, « 3 primitives PFR + tests de limite »). C'est une vraie attestation locale — mais **une seule** : parler de « primitive transversale » exige un **second substrat**. → `FIRSTHAND / 1 attestation locale / empirique-notebook`. - -## Trois gains de mesure (le froid fait tomber ET remonter) - -**Gain 1 — Op 9 « Élargir l'espace » passe à 2 attestations.** -A3 (firsthand, po-2026) : `planning_lean/Planning/Admissibility.lean:50` — `relaxed_plan_admissible : reaches π s g → reachesR π s g` = `P_reel ⊆ P_relache` exactement. Ce cycle : **SW-14-Python-Coup-Ontologique** (#12263 MERGED) exécute l'élargissement du vocabulaire OWL (extension η) avec témoin = diff de triplets + verdict SHACL + delta d'inférences. Deux substrats indépendants (Lean/planning vs Python/ontologie), même loi de monotonie. L'op 9 est la première opération **promue par la mesure** de cette Epic. - -**Gain 2 — Loi III « les deux espèces de flèches » gagne sa seconde attestation.** -Le body dit : « attestée une fois » (transformation vs morphisme, swap ordinal). **GT-21-Deux-Espèces-de-Flèches** (#12245 MERGED, notebook vérifié sur le disque ce cycle) pose le théorème fini transformation-vs-morphisme. La Loi III passe à 2 attestations ; le verdict de grade §3 du body (« deux lois attestées deux fois, une une fois ») devient **trois lois attestées deux fois** — sans changer la conclusion (toujours pas un grade A). - -**Contrepartie — Loi I « obstruction abstraite → témoin exploitable » retombe à 1 attestation.** -Elle citait de Finetti **et** Brown-Sandholm comme deux attestations. La Tombée 3 requalifie Brown-Sandholm en lecture structurelle → la Loi I n'a plus que de Finetti (1). Le grade §3 doit être révisé en conséquence : **Loi I : 1 · Loi II : 2 · Loi III : 2**. - -**Gain 3 — Op 14 « Agréger un collectif » passe à 2 attestations.** -La 1ʳᵉ (A6) : `Shapley.lean:614-634` — `Mobius.mobiusCoeff` / `Mobius.mobiusReconstruction`, l'inversion de Möbius sur le treillis des coalitions, sorry-free (0 `sorry` réel mesuré : l'unique occurrence du mot dans le fichier est de la prose, ligne 1260). Cette livraison : **SC-06 — Möbius, agrégation, pouvoir, manipulation** (`MyIA.AI.Notebooks/GameTheory/SocialChoice/06-Mobius-Aggregation-Pouvoir-Manipulation.ipynb`, PR ce cycle) exécute le miroir Python exact de ces deux définitions — reconstruction vérifiée par exécution sur les 16 coalitions de `[6;4,3,2,1]` (le re-test `[8;5,4,3,2,1]` est posé en exercice, non exécuté) — puis dérive la valeur de Shapley par les dividendes **et** par énumération des 24 ordres d'entree (deux voies indépendantes, écart 5.55e-17), mesure l'écart poids/pouvoir (Banzhaf ; dummy du Luxembourg, Conseil 1958) et instancie le témoin de Gibbard-Satterthwaite sur un Borda à électeurs pondérés. Deux substrats indépendants (Lean/preuve vs Python/exécution), même loi de décomposition en dividendes de Harsanyi. L'op 14 quitte « en constitution » et rejoint l'op 9 dans les promotions par la mesure. - -## Preuves de ce cycle (firsthand, reproductibles) - -**P1 — #12208 (distillation Kroer-Sandholm) non atterrie** : `gh pr list --state all --search 12208` → aucune PR de livraison ; issue ouverte. - -**P2 — Lean-21b merged** : `gh pr view 12252` → `MERGED 2026-08-22T12:57:43Z`, fichier `Lean-21b-PFR-Primitives-Transportables.ipynb`. - -**P3 — sorry réels sur les lakes** (instrument canonique, base worktree `1d021b4fe`) : - -```text -$ python scripts/lean/count_code_sorry.py --json -lakes porteurs de sorry reel: 4/22 - game_theory_lean: 1 · decision_theory_lean: 2 · conway_lean: 1 · knot_lean: 13 -``` - -→ 18/22 lakes à 0 sorry réel : l'op 8 « Certifier » est attestée au pluriel, la dette est concentrée (knot_lean porte 13/17). - -**P4 — GT-21 sur le disque** : `GameTheory-21-Deux-Especes-de-Fleches.ipynb` présent (livré #12245, merged — commit `c7bc85f2d` tête de main à la base du worktree). - -**P5 — SW-14 sur le disque, exécuté** : 5/5 cellules code `execution_count 1..5`, outputs présents (vérifié ce cycle lors de la fermeture #12234). - -**P6 — GT-16b AMD lu ce cycle** : générateur / vérificateur séparé / témoin d'impossibilité — op 10 attestée, avec la réserve de cohérence DSIC consignée sur #12211 (issuecomment-5383043049). - -## Honnêteté méthodologique - -- Les labels `FIRSTHAND` ci-dessus renvoient aux preuves P1-P6, à A3 ou à A4 ; tout le reste est `RAPPORTE` (issu du body de l'EPIC ou de la revue, non relu ce cycle). Les conversions A2 (op 1) et A4 (op 4) sont livrées ; les `RAPPORTE` restants (ops 2, 5, 6) sont tous trois tombés en file d'attente (§Tombées 1-3) et n'ouvrent plus de tranche de conversion. -- Cette tranche **applique** des décisions déjà tranchées par la revue extérieure pour les 4 tombées ; elle **mesure** les 2 gains et la contrepartie Loi I. Elle ne crée aucune règle nouvelle (cf `audit-cross-source-distillation` règle 2 : grain au cas par cas). -- `RAPPORTE` n'est pas un déshonneur : c'est l'état honnête d'une table dont la fonction première (§6 du body) est précisément de distinguer le vérifié du rapporté. - -## Effet demandé sur le body de l'EPIC - -Le body §2 doit refléter : op 2, 5, 6 → file d'attente ; op 3 → file d'attente (1 attestation locale) ; mention Brown-Sandholm (op 5) → lecture structurelle ; §3 verdict de grade → Loi I : 1 · Loi II : 2 · Loi III : 2. L'édition du body est posée en commentaire de livraison sur l'issue (l'EPIC reste la source de vérité ; ce ledger en est la preuve). - -## Tranche A6 (2026-09-07, po-2027:CoursIA-2) — statuer sur les quatre en constitution + file d'attente - -Mandat §4bis : « A6 est donc une décision, plus une enquête. » Vérifications firsthand ce cycle : - -**Op 11 — FIRSTHAND, 1 attestation.** `SymbolicAI/Lean/mimo_lean/Descent.lean` (+ sibling `Descent_en.lean`) : `descent_flips_le_barrier` (l.110 — décroissance stricte `hstrict` + barrière de confinement `hbarrier`) et théorème de terminaison sous plafond de flips (l.144). Le fichier se déclare lui-même « La thèse du chantier (opération 11, "descendre sous budget") » (l.148), et y consigne la dissociation-vs-échec — la dette du body. 0 `sorry` (grep direct + cohérent avec P3 : mimo_lean hors des 4 lakes porteurs). **Verdict : reste en constitution** — une seule attestation. - -**Op 12 — décision : promotion REFUSÉE.** La table disait « 2+ (GT-21 + Loi III) ». Mesuré : la seconde attestation de la Loi III **est GT-21 lui-même** (§Gain 2) — compter GT-21 et « Loi III » comme deux attestations de l'op 12 est un double comptage du même artefact. Test d'une 2ᵉ attestation directe : `ICT-34-BancRecollementLectures.ipynb` (candidat naturel) porte recollement×26 mais forward/backward ×0 — c'est un banc d'op 5 (Recoller), pas une composition de regards play-forward/coplay-backward. **Verdict : reste en constitution, candidate forte confirmée** — première promotion quand une seconde instantiation directe atterrira. - -**Op 13 — FIRSTHAND, 1 attestation.** PR #12364 MERGED (2026-08-22T22:45:49Z) ; `GameTheory-24-Chemin-Minimal-Robinson-Goforth.ipynb` sur disque : chambres×35, swaps×17, mur×12, 576×7 — le chemin minimal à travers le mur Robinson-Goforth est bien l'objet exécuté. Le compagnon `GameTheory-24b-Chemin-Minimal-Temoins-Impossibilite.ipynb` renforce la forme du témoin (impossibilité), mais c'est le **même substrat** — pas une seconde attestation indépendante. **Verdict : reste en constitution.** - -**Op 14 — FIRSTHAND, 1 attestation.** `game_theory_lean/CooperativeGames/Shapley.lean:614-634` : namespace `Mobius`, `mobiusCoeff` (dividende de Harsanyi), `mobiusReconstruction` (`G = Σ_{T≠∅} a_T • u_T`) — la loi « Möbius sur le treillis des coalitions » attestée Lean-formel, sorry-free dans le fichier (le 1 sorry réel du lake mesuré en P3 est ailleurs). Réserve tranchée : `StableMarriage/GaleShapley.lean` n'est **pas** une 2ᵉ attestation — l'appariement stable n'est pas l'agrégation de coalitions sur le treillis. **Verdict : reste en constitution.** - -**File d'attente — point fixe.** Second usage de Knaster-Tarski : `git grep -il knaster -- "*.lean"` → `argumentation_lean/Argumentation.lean` + `Argumentation/Characteristic.lean` (+ sibling `_en`) — un seul locus substantiel après dédoublonnage FR/EN (racine et module du même lake). Pas de second usage indépendant atterri : la promotion « dès le second usage » reste en attente. - -**Bilan A6** : quatre opérations statuées, zéro promotion, zéro descente. La table reste à **6 opérations en TABLE** (1, 4, 7, 8, 9, 10), **4 en file d'attente** (2, 3, 5, 6), **4 en constitution — toutes quatre FIRSTHAND désormais**. Reste **A7** (relecture froide : la table est-elle un catalogue ? une quatrième loi est-elle apparue ?) — dernier grain. - -## Tranche c.1208 (2026-09-16, po-2026:CoursIA-2) — op 11 : 2ᵉ attestation livrée (PR #16392) - -**Op 11 — FIRSTHAND (ce cycle), 2ᵉ attestation sur substrat indépendant.** `Search/Part1-Foundations/Search-11d-Descente-Sous-Budget.ipynb` (série Search, Python stdlib, exécuté papermill, 0 erreur) : knapsack 0/1, potentiel Φ = −valeur, voisinage bit-flip, barrière = borne LP relaxée, budget = plafond d'évaluations. La loi de `Descent.lean` y est **exercée** (asserts runtime sur 60 exécutions : 0 violation `hstrict`, 0 violation `hbarrier`, 0 dépassement de plafond) et sa troisième hypothèse **réfutée exécutablement** : `hnostall` est fausse dans un paysage générique (100 % d'arrêts « blocage » hors cible à budget généreux, gap médian 10,4 %) — la dissociation budget-vs-blocage exigée par `Descent.lean` l.148 est mesurée dans deux régimes (budget serré : 30/30 arrêts « budget » sur 30 graines ; budget généreux : 60/60 arrêts « blocage » hors cible sur 60 graines) ; courbe qualité-budget médiane 86,3 % → 8,9 % (B ∈ {20..800}, 30 seeds, saturation = optima locaux). **Verdict : reste en constitution jusqu'au merge** (convention op 7 : non comptée tant qu'OPEN) — la promotion en TABLE appartient à A7, qui tranche sur deux attestations indépendantes (Lean-formel + empirique-notebook). - -## Tranche c.1308 (2026-09-29, po-2024:CoursIA-2) — op 3 : re-vérification Infer-20 (piste vierge dans le ledger jusqu'ici) - -**Op 3 — FIRSTHAND (ce cycle), re-vérification d'Infer-20 comme 2ᵉ attestation candidate.** Issue dispatchée par ai-01 ([#18405](https://github.com/jsboige/CoursIA/issues/18405)) à 14:30Z — le coordinateur pointe qu'`Infer-20-Quotients-et-Fibres-Python.ipynb` (`Probas/Modules/Infer/`, PR #12277 MERGED 2026-08-22) porte **le protocole de l'opération 3** : projection vers un alphabet `Q` (quantification de `X₁ + X₂`) et mesure de `I(X₁;X₂|Q)` vs `I(X₁;X₂)`, qui est la forme conditionnelle de la règle de chaîne `H(X) = H(π(X)) + H(X|π(X))`. Le ledger — re-vérifié ce cycle (`git grep -nE "Infer-20|12226" docs/ledgers/`) — ne mentionne ni l'un ni l'autre : la piste est vierge, donc le critère d'admission au chant1 (« deux attestations indépendantes ») n'a jamais été tranché sur cette candidate. - -**Trois vérifications firsthand ce cycle :** - -1. **Infer-20 sur disque** (`Probas/Applications/Infer-20-Quotients-et-Fibres-Python.ipynb`, PR #12277 MERGED 2026-08-22) : la cellule 10 (code) construit `Q = np.digitize(S, quantiles)` avec `Q_BINS = 4` et `S = X₁ + X₂`. La cellule 14 teste `Q_OPERATIONAL = (I(X₁;X₂|Q) < 0.5 · I(X₁;X₂))` — verdict imprimé **NON TENTE** (`ratio = 1.684`, > critère 0.5). **Infer-20 illustre la règle de chaîne conditionnelle** : c'est exactement l'opération 3 sous sa forme `I(X₁;X₂) = I(X₁;X₂|Q) + I(X₁;X₂;Q)`. Mais elle **échoue à produire un quotient opérationnel** sur des gaussiennes linéaires corrélées `ρ = 0.6` — la quantification 1D de la somme ne suffit pas. - -2. **ANALYSE-04 sur disque** (`SymbolicAI/Lean/ANALYSE/ANALYSE-04-PFR-Primitives-Python.ipynb`) : cellule 7 — *« Lecture du résultat. La règle de chaîne `H(X) = H(X|Y) + I(X;Y)` est **vérifiée numériquement**. Information mutuelle `I(X;Y)` capture combien le cours (Y) explique la note (X) ; la résiduelle `H(X|Y)` capture la variation inexpliquée par le cours. Sémantique opérationnelle : `H(π(X))` ≈ ce que la projection capte ; `H(X|π(X))` ≈ ce qui reste dans les fibres. »* — Verdict de la cellule 9 : « Transportable large. Universelle en théorie de l'information. » C'est la **seule attestation locale** décomptée jusqu'ici (cf A3 l.97-106 : « teorth/pfr est une référence externe non incluse au dépôt, et la digestion EPIC l'a cité comme si elle était locale »). - -3. **Critère d'indépendance** (règle op 7 étendue à l'op 3, protocole EPIC §1) : ANALYSE-04 ([#12252](https://github.com/jsboige/CoursIA/pull/12252), MERGED 2026-08-22T12:57:43Z) et Infer-20 ([#12277](https://github.com/jsboige/CoursIA/pull/12277), MERGED 2026-08-22T12:58:17Z) sont **nés le même jour (2026-08-22, à 34 secondes d'écart), du même EPIC [#12204](https://github.com/jsboige/CoursIA/issues/12204) — issues sœurs [#12214](https://github.com/jsboige/CoursIA/issues/12214) (Lean-21b PFR) et [#12226](https://github.com/jsboige/CoursIA/issues/12226) (Probas quotient/fibres/recollement). Le témoin formel de l'opération 3 (`H(X) = H(π(X)) + H(X|π(X))`) est universel info-théorique, mais la non-indépendance tient sur des constats vérifiables : **même chantier EPIC, même jour, même lane de dispatch**. ANALYSE-04 seul revendique le stimulus PFR-Tao ; Infer-20, fille de [#12226](https://github.com/jsboige/CoursIA/issues/12226), ne le cite pas. L'indépendance au sens strict du critère « deux endroits non reliés par le stimulus initial » n'est **pas** vérifiée. - -**Verdict c.1308 — op 3 reste en file d'attente, mais le statut se précise :** - -- **Pas de promotion** : 1 attestation locale indépendante (ANALYSE-04) + 1 attestation pédagogique **non-indépendante** (Infer-20, même chantier) = critère « deux endroits indépendants » non atteint. -- **Mais** Infer-20 **valorisera** l'op 3 si une seconde instantiation **sur substrat indépendant** arrive — le protocole est reproductible, le témoin négatif est déjà mesuré (1.684), le pipeline opérationnel est tracé. -- Le **témoin négatif** transportable d'Infer-20 (quantification 1D de la somme d'un couple gaussien corrélé ⇒ ratio `I(X₁;X₂|Q)/I(X₁;X₂)` = 1.684, **donc quotient informationnel non atteignable**) est noté comme tel dans le ledger — c'est un résultat négatif qui borne la classe des quotients opérationnels naïfs. - -**Effet sur la table :** op 3 → toujours en file d'attente. Mention « 1 attestation locale + 1 pédagogique non-indépendante re-vérifiée c.1308 » dans le commentaire de livraison sur l'EPIC. **Pas de mouvement de table** ce cycle ; un futur A7bis qui trouve une 2ᵉ attestation sur un substrat hors-PFR (Probabilité élémentaire, codage, IC games) la fait basculer. - -**Distance de Ruzsa** (point 3 de #18405) : objet ICT à groupe additif identifié = **`MyIA.AI.Notebooks/IIT/ICT-Series/ict/factor_geometry.py`** (espace des activations `(ℝ^D, +)`, primitives `weighted_pca` / `max_principal_angle` / `basis_overlap` extraites de ICT-36-FLens-FactoredGeometry, PR #15514 MERGED). La convolution `X′ − Y′` y est définie composante par composante. Application directe : `d_ruzsa(X;Y) = H(X′ − Y′) − ½ H(X′) − ½ H(Y′)` sur deux activations factorisées. **Non livré dans cette tranche** (hors périmètre dispatch —> à pousser en grain suivant si ai-01 l'autorise, après qu'A7 ou un grain subséquent ait statué sur l'op 3). - -**Acceptance sortie ce cycle :** verdict d'attestation de l'opération 3 écrit dans le ledger (cette tranche), avec sa preuve (3 vérifications nommées) et le statut du témoin négatif. - -## Tranche réconciliation (2026-10-04, po-2027:CoursIA) — ops 2 et 6 : deux 2ᵉ attestations enregistrées (artefacts antérieurs au dernier toucher du ledger, non comptés) - -Motif : pattern #11900 inversé — ce n'est pas le body qui a vieilli, c'est le **ledger**. Deux artefacts livrés sur `main` entre deux tranches n'ont jamais été enregistrés dans la table. Vérification firsthand des deux ce 04/10. - -**Op 2 — GT-19, l'attestation locale qui existait déjà.** `GameTheory/GameTheory-19-Abstraction-a-Dette-Python.ipynb` : né de l'issue [#12229](https://github.com/jsboige/CoursIA/issues/12229) (CLOSED, même voyage de digestion du 2026-08-21, **jamais rattachée à cette EPIC** — 0 citation du body), livré par PR #12267 (2026-09-11), digéré par #18317 (2026-10-01), toutes les cellules code exécutées avec outputs. Contenu vérifié : cellule 3 (abstraction par fusion d'états, partition de 6 états, matrices moyennées) → cellule 7 (**solve exact de G̃, retransport, mesure DANS G** — le pipeline α→solve→ρ→σ_G de la loi) → cellule 12 (**courbe de dette sur la chaîne de raffinement P6 < P4 < P3 < P2**, chaîne vérifiée par `refines`), plus l'atlas des 15 paires (exercice 2) et la partition hors chaîne P3B vs P3 à taille égale (exercice 3, P3 = 1.9091) — la question « qu'ai-je le droit d'oublier » chiffrée. C'est la forme de témoin exigée par le critère §1, en force empirique-notebook. -**Réserve d'indépendance (précédent c.1308)** : GT-19 **cite Kroer-Sandholm** comme source théorique et naît du même batch de digestion — la non-indépendance par le stimulus initial invoquée pour op 3 / Infer-20 s'applique a priori au couple (théorème externe, instantiation locale qui le cite). La promotion TABLE appartient donc à A7, qui tranche : le critère « deux endroits indépendants » compte-t-il une instantiation pédagogique de la source elle-même ? **Statut : en constitution, pas de promotion auto-décidée.** - -**Op 6 — Search-03f, la 2ᵉ attestation livrée hier par cette même lane.** `Search/Part1-Foundations/Search-03f-Reparer-Localement-Sous-Garantie-Python.ipynb`, PR #19013 **MERGED 2026-10-04T02:14:57Z** — postérieure au dernier toucher de ce ledger (2026-09-30 01:22), d'où la ligne restée en FILE D'ATTENTE. toutes les cellules code exécutées (exécution complète vérifiée), [DELIVERED] posé sur l'EPIC le 03/10 17:24Z. Trois témoins exigés par la table, vérifiés dans le carnet : garantie transportée (coût LPA\* = coût A\* from scratch, 8/8 concordances sur séquence de 8 changements), localité payée juste (12 expansions pour le repair), et le troisième lu en conclusion. **Indépendance par construction : 0 mention de Sandholm dans le carnet** (mesuré) — substrat recherche de chemin, pas jeux. -**Statut : en constitution, promotion TABLE à statuer par la revue** (convention des ops 11-13). - -**Effet sur la table :** la file d'attente passe de 4 à 2 opérations (restent **3 et 5**) ; les ops 2 et 6 rejoignent les 4 en constitution → **6 en constitution**. Le bilan A6 ci-dessus reste historique. A7, quand il statuera, trouvera deux dossiers de plus sur son bureau — c'est précisément le geste attendu d'une réconciliation : rendre visible ce qui était déjà là. - -## Références - -- EPIC : [#12204](https://github.com/jsboige/CoursIA/issues/12204) · tranches : A3 ([ledger](../ledgers/12204-ict-chantier-1-a3.md), PR #12293) · audit-froid (ce fichier) -- Revue extérieure (protocole + 4 contestations) : commentaire #12204 du 2026-08-22 -- Steering : ai-01 2026-08-22T20:54Z ([DISPATCH→inbox] dashboard workspace-CoursIA) -- Précédent de format : [`3801-sota-axe2.md`](../ledgers/3801-sota-axe2.md) +> RAPPORT - 2026-08-24 - Chantier 1 ICT audit-froid (#12204) - figé + +# Ledger #12204 — Chantier 1 ICT, tranche audit-froid : trois labels par opération, quatre entrées tombées + +**Statut** : tranche de l'EPIC #12204 « Chantier 1 — La table des opérations ». Provisionnée par le steering ai-01 du 2026-08-22T20:54Z (« audit froid : faire tomber les entrées qui ne survivent pas »), protocole fixé par la revue extérieure du 2026-08-22 en commentaire d'issue. + +**Lane** : `myia-po-2025:CoursIA` (claim paths-scoped, [issuecomment-5383064486](https://github.com/jsboige/CoursIA/issues/12204#issuecomment-5383064486)). +**Date** : 2026-08-23. **Base** : `origin/main` `1d021b4fe`. + +## Le protocole — trois labels orthogonaux + +Repris de la revue extérieure (commentaire #12204, 2026-08-22) : + +| axe | valeurs | ce qu'il mesure | +|---|---|---| +| **provenance** | `RAPPORTE` / `FIRSTHAND` | ai-je lu la source, ou une lecture de la source ? | +| **attestation** | `1 attestation` / `2+ attestations` | le seuil d'admission de l'EPIC (§1 du body) | +| **force** | `empirique` / `exhaustif` / `Lean-formel` | ce que vaut la preuve, pas ce qu'elle couvre | + +Une opération `FIRSTHAND / 1 attestation / exhaustif` et une opération `RAPPORTE / 2+ attestations / empirique` ne sont pas comparables sur un axe unique. + +## La table labellisée — 14 opérations + +Labels établis à partir : (a) des vérifications A3 firsthand ([`12204-ict-chantier-1-a3.md`](../ledgers/12204-ict-chantier-1-a3.md), po-2026) ; (b) des mesures de ce cycle (§Preuves ci-dessous) ; (c) du corps de la revue extérieure pour les quatre contestées. `RAPPORTE` partout où ce cycle n'a pas relu la source firsthand — c'est le sens même du label. + +| # | Opération | provenance | attestation | force | Verdict | +|---|---|---|---|---|---| +| 1 | Recoordonner | FIRSTHAND (A2, #13956) | 2+ (Sudoku-13, `conway_lean`, MGS-21) — les trois tiennent | empirique avec cause mesurée + Lean-formel kernel-décidable | **TABLE** — confirmée. Dette reformulée : les trois attestations sont des post-mortems — une théorie du « bon » changement choisirait la représentation avant de payer l'échec ([A2](../ledgers/12204-ict-chantier-1-a2.md)) | +| 2 | Abstraire à dette bornée | FIRSTHAND (réconciliation 04/10) | **2 candidates** (Kroer-Sandholm externe + GT-19 #12267 locale mesurée, enregistrée §Tranche réconciliation 04/10) | empirique-notebook (source théorique externe) | en constitution — 2ᵉ attestation candidate enregistrée ; promotion à statuer par A7 (indépendance par le stimulus à trancher, précédent op 3 c.1308 : GT-19 cite Kroer-Sandholm et naît du même voyage de digestion #12229) | +| 3 | Quotienter / fibrer | FIRSTHAND (A3 + ce cycle) | **1 locale** (Lean-21b) | empirique-notebook | **⬇ FILE D'ATTENTE** — voir §Tombée 4 | +| 4 | Décomposer localement | FIRSTHAND (A4, #14453) | 2+ recensées : Hashlife (Lean-formel, non-jouet) + ICT-15d (empirique jouet, partition avouée) + EPITA (empirique, identification restaurée) | Lean-formel + empirique | **TABLE** — confirmée. Dette reformulée en bipartition : la preuve décide des bords côté Hashlife (`padCenter2_margin_ge_jumpReach`), l'expérimentateur les choisit sans théorie côté ICT-15d ([A4](../ledgers/12204-ict-chantier-1-a4.md)) | +| 5 | Recoller | RAPPORTE | **1 + 1 lecture** | Lean-formel (de Finetti) | **⬇ FILE D'ATTENTE** — voir §Tombée 3 | +| 6 | Réparer localement sous garantie | FIRSTHAND (réconciliation 04/10) | **2** (Sandholm externe + Search-03f #19013 MERGED 2026-10-04, convention op 7 remplie — comptée dès merge) | empirique-notebook, substrat indépendant | en constitution — 2ᵉ attestation livrée (LPA\*, 0 mention de Sandholm : indépendance par construction) ; promotion TABLE à statuer par la revue (§Tranche réconciliation 04/10) | +| 7 | Engendrer un témoin | FIRSTHAND (ce cycle) | 2+ (Sudoku-13, `conway_lean`, GT-16b #12259) | empirique + Lean-formel | **TABLE** — la mieux attestée du dépôt. GT-25 #12395 (translateur Life) renforcera la ligne quand elle quittera la file CI — non comptée tant qu'OPEN | +| 8 | Certifier | FIRSTHAND (ce cycle) | 2+ (22 lakes) | Lean-formel | **TABLE** — 18/22 lakes à 0 sorry réel (mesuré §P3) | +| 9 | Élargir l'espace | FIRSTHAND (A3) | **2** (`planning_lean` Admissibility.lean:50 + SW-14 #12263) | Lean-formel + empirique | **TABLE** — promotion mesurée §Tombées (gain) | +| 10 | Concevoir la règle | FIRSTHAND (ce cycle) | 2+ (GT-16b #12259, GT-20 #12303, SC-27 #12265) | empirique | **TABLE** — le mécanisme comme variable, trois familles | +| 11 | Descendre sous budget | FIRSTHAND (A6 + c.1208) | **1 + 1 en instance** (`mimo_lean/Descent.lean` — thèse op 11 explicite, sorry-free ; Search-11d #16392 — comptée dès merge, convention op 7) | Lean-formel + empirique | en constitution — 2ᵉ attestation livrée sur substrat indépendant (c.1208) ; promotion TABLE à statuer par A7 | +| 12 | Composer des regards | FIRSTHAND (ce cycle + A6) | **2 directes** (GT-21 #12245 jeux 2×2 + Search-12a #16426 gridworld pondéré — comptée dès merge, convention op 7) | empirique-notebook ×2, substrats indépendants | en constitution — 2ᵉ attestation directe livrée ; promotion TABLE à statuer par la revue (witness form connu : paire incompatible exhibée, Search-12a §5) | +| 13 | Traverser un mur | FIRSTHAND (A6 + c.1216) | **2 directes** (GT-24 #12364 MERGED + Search-13a #16438 pavage hexagonal chemins certifiés — comptée dès merge, convention op 7) | empirique-notebook ×2, substrats indépendants | en constitution — 2ᵉ attestation directe livrée ; promotion TABLE à statuer par la revue (witness form connu : distinction épaisseur m_path / largeur m + test négatif morphisme/percement, Search-13a §8) | +| 14 | Agréger un collectif | FIRSTHAND (A6 + ce cycle) | **2** (`Shapley.lean:614-634` Möbius/Harsanyi sorry-free + SC-06 Python exécuté, PR ce cycle) | Lean-formel + empirique | **TABLE** — promotion mesurée §Gain 3 (même pattern que l'op 9) ; GaleShapley reste exclu (appariement ≠ agrégation) | + +## Les quatre tombées (décisions de la revue extérieure, appliquées) + +**Tombée 1 — Op 2 « Abstraire à dette bornée » → FILE D'ATTENTE.** +Soutenue surtout par Kroer-Sandholm, **externe** tant que sa distillation (#12208) n'a pas atterri (vérifié ce cycle : #12208 OPEN, non mergée). `MechanismDesign.lean` n'est pas une seconde attestation de *bounded abstraction* : il atteste un mécanisme (op 10), pas une borne d'abstraction. → `RAPPORTE / 1 attestation`. + +**Tombée 2 — Op 6 « Réparer localement sous garantie » → FILE D'ATTENTE.** +Une seule famille (Sandholm). Le critère §1 de l'EPIC est mécanique : une attestation ⇒ file d'attente, pas la table. + +**Tombée 3 — Op 5 « Recoller » → FILE D'ATTENTE (1 attestation + 1 lecture).** +La mention « mauvais recollement → déviation adversariale » (Brown-Sandholm) est **notre lecture structurelle** du safe subgame solving, pas un théorème Čech ni une attestation. C'est le défaut exact qui a coulé la première tentative ICT-15d : nommer le cadre mathématique avant de posséder les transports. La ligne reste dans la table comme **lecture**, étiquetée comme telle. De Finetti reste la seule attestation (1). + +**Tombée 4 — Op 3 « Quotienter / fibrer » → FILE D'ATTENTE.** +A3 a établi firsthand que `teorth/pfr` est **externe au dépôt** (find + grep : 0). Ce cycle vérifie que la contrepartie locale est arrivée : **Lean-21b MERGED** (#12252, 2026-08-22T12:57Z, « 3 primitives PFR + tests de limite »). C'est une vraie attestation locale — mais **une seule** : parler de « primitive transversale » exige un **second substrat**. → `FIRSTHAND / 1 attestation locale / empirique-notebook`. + +## Trois gains de mesure (le froid fait tomber ET remonter) + +**Gain 1 — Op 9 « Élargir l'espace » passe à 2 attestations.** +A3 (firsthand, po-2026) : `planning_lean/Planning/Admissibility.lean:50` — `relaxed_plan_admissible : reaches π s g → reachesR π s g` = `P_reel ⊆ P_relache` exactement. Ce cycle : **SW-14-Python-Coup-Ontologique** (#12263 MERGED) exécute l'élargissement du vocabulaire OWL (extension η) avec témoin = diff de triplets + verdict SHACL + delta d'inférences. Deux substrats indépendants (Lean/planning vs Python/ontologie), même loi de monotonie. L'op 9 est la première opération **promue par la mesure** de cette Epic. + +**Gain 2 — Loi III « les deux espèces de flèches » gagne sa seconde attestation.** +Le body dit : « attestée une fois » (transformation vs morphisme, swap ordinal). **GT-21-Deux-Espèces-de-Flèches** (#12245 MERGED, notebook vérifié sur le disque ce cycle) pose le théorème fini transformation-vs-morphisme. La Loi III passe à 2 attestations ; le verdict de grade §3 du body (« deux lois attestées deux fois, une une fois ») devient **trois lois attestées deux fois** — sans changer la conclusion (toujours pas un grade A). + +**Contrepartie — Loi I « obstruction abstraite → témoin exploitable » retombe à 1 attestation.** +Elle citait de Finetti **et** Brown-Sandholm comme deux attestations. La Tombée 3 requalifie Brown-Sandholm en lecture structurelle → la Loi I n'a plus que de Finetti (1). Le grade §3 doit être révisé en conséquence : **Loi I : 1 · Loi II : 2 · Loi III : 2**. + +**Gain 3 — Op 14 « Agréger un collectif » passe à 2 attestations.** +La 1ʳᵉ (A6) : `Shapley.lean:614-634` — `Mobius.mobiusCoeff` / `Mobius.mobiusReconstruction`, l'inversion de Möbius sur le treillis des coalitions, sorry-free (0 `sorry` réel mesuré : l'unique occurrence du mot dans le fichier est de la prose, ligne 1260). Cette livraison : **SC-06 — Möbius, agrégation, pouvoir, manipulation** (`MyIA.AI.Notebooks/GameTheory/SocialChoice/06-Mobius-Aggregation-Pouvoir-Manipulation.ipynb`, PR ce cycle) exécute le miroir Python exact de ces deux définitions — reconstruction vérifiée par exécution sur les 16 coalitions de `[6;4,3,2,1]` (le re-test `[8;5,4,3,2,1]` est posé en exercice, non exécuté) — puis dérive la valeur de Shapley par les dividendes **et** par énumération des 24 ordres d'entree (deux voies indépendantes, écart 5.55e-17), mesure l'écart poids/pouvoir (Banzhaf ; dummy du Luxembourg, Conseil 1958) et instancie le témoin de Gibbard-Satterthwaite sur un Borda à électeurs pondérés. Deux substrats indépendants (Lean/preuve vs Python/exécution), même loi de décomposition en dividendes de Harsanyi. L'op 14 quitte « en constitution » et rejoint l'op 9 dans les promotions par la mesure. + +## Preuves de ce cycle (firsthand, reproductibles) + +**P1 — #12208 (distillation Kroer-Sandholm) non atterrie** : `gh pr list --state all --search 12208` → aucune PR de livraison ; issue ouverte. + +**P2 — Lean-21b merged** : `gh pr view 12252` → `MERGED 2026-08-22T12:57:43Z`, fichier `Lean-21b-PFR-Primitives-Transportables.ipynb`. + +**P3 — sorry réels sur les lakes** (instrument canonique, base worktree `1d021b4fe`) : + +```text +$ python scripts/lean/count_code_sorry.py --json +lakes porteurs de sorry reel: 4/22 + game_theory_lean: 1 · decision_theory_lean: 2 · conway_lean: 1 · knot_lean: 13 +``` + +→ 18/22 lakes à 0 sorry réel : l'op 8 « Certifier » est attestée au pluriel, la dette est concentrée (knot_lean porte 13/17). + +**P4 — GT-21 sur le disque** : `GameTheory-21-Deux-Especes-de-Fleches.ipynb` présent (livré #12245, merged — commit `c7bc85f2d` tête de main à la base du worktree). + +**P5 — SW-14 sur le disque, exécuté** : exécution bout-en-bout avec `execution_count` croissants, outputs présents (vérifié ce cycle lors de la fermeture #12234). + +**P6 — GT-16b AMD lu ce cycle** : générateur / vérificateur séparé / témoin d'impossibilité — op 10 attestée, avec la réserve de cohérence DSIC consignée sur #12211 (issuecomment-5383043049). + +## Honnêteté méthodologique + +- Les labels `FIRSTHAND` ci-dessus renvoient aux preuves P1-P6, à A3 ou à A4 ; tout le reste est `RAPPORTE` (issu du body de l'EPIC ou de la revue, non relu ce cycle). Les conversions A2 (op 1) et A4 (op 4) sont livrées ; les `RAPPORTE` restants (ops 2, 5, 6) sont tous trois tombés en file d'attente (§Tombées 1-3) et n'ouvrent plus de tranche de conversion. +- Cette tranche **applique** des décisions déjà tranchées par la revue extérieure pour les 4 tombées ; elle **mesure** les 2 gains et la contrepartie Loi I. Elle ne crée aucune règle nouvelle (cf `audit-cross-source-distillation` règle 2 : grain au cas par cas). +- `RAPPORTE` n'est pas un déshonneur : c'est l'état honnête d'une table dont la fonction première (§6 du body) est précisément de distinguer le vérifié du rapporté. + +## Effet demandé sur le body de l'EPIC + +Le body §2 doit refléter : op 2, 5, 6 → file d'attente ; op 3 → file d'attente (1 attestation locale) ; mention Brown-Sandholm (op 5) → lecture structurelle ; §3 verdict de grade → Loi I : 1 · Loi II : 2 · Loi III : 2. L'édition du body est posée en commentaire de livraison sur l'issue (l'EPIC reste la source de vérité ; ce ledger en est la preuve). + +## Tranche A6 (2026-09-07, po-2027:CoursIA-2) — statuer sur les quatre en constitution + file d'attente + +Mandat §4bis : « A6 est donc une décision, plus une enquête. » Vérifications firsthand ce cycle : + +**Op 11 — FIRSTHAND, 1 attestation.** `SymbolicAI/Lean/mimo_lean/Descent.lean` (+ sibling `Descent_en.lean`) : `descent_flips_le_barrier` (l.110 — décroissance stricte `hstrict` + barrière de confinement `hbarrier`) et théorème de terminaison sous plafond de flips (l.144). Le fichier se déclare lui-même « La thèse du chantier (opération 11, "descendre sous budget") » (l.148), et y consigne la dissociation-vs-échec — la dette du body. 0 `sorry` (grep direct + cohérent avec P3 : mimo_lean hors des 4 lakes porteurs). **Verdict : reste en constitution** — une seule attestation. + +**Op 12 — décision : promotion REFUSÉE.** La table disait « 2+ (GT-21 + Loi III) ». Mesuré : la seconde attestation de la Loi III **est GT-21 lui-même** (§Gain 2) — compter GT-21 et « Loi III » comme deux attestations de l'op 12 est un double comptage du même artefact. Test d'une 2ᵉ attestation directe : `ICT-34-BancRecollementLectures.ipynb` (candidat naturel) porte recollement×26 mais forward/backward ×0 — c'est un banc d'op 5 (Recoller), pas une composition de regards play-forward/coplay-backward. **Verdict : reste en constitution, candidate forte confirmée** — première promotion quand une seconde instantiation directe atterrira. + +**Op 13 — FIRSTHAND, 1 attestation.** PR #12364 MERGED (2026-08-22T22:45:49Z) ; `GameTheory-24-Chemin-Minimal-Robinson-Goforth.ipynb` sur disque : chambres×35, swaps×17, mur×12, 576×7 — le chemin minimal à travers le mur Robinson-Goforth est bien l'objet exécuté. Le compagnon `GameTheory-24b-Chemin-Minimal-Temoins-Impossibilite.ipynb` renforce la forme du témoin (impossibilité), mais c'est le **même substrat** — pas une seconde attestation indépendante. **Verdict : reste en constitution.** + +**Op 14 — FIRSTHAND, 1 attestation.** `game_theory_lean/CooperativeGames/Shapley.lean:614-634` : namespace `Mobius`, `mobiusCoeff` (dividende de Harsanyi), `mobiusReconstruction` (`G = Σ_{T≠∅} a_T • u_T`) — la loi « Möbius sur le treillis des coalitions » attestée Lean-formel, sorry-free dans le fichier (le 1 sorry réel du lake mesuré en P3 est ailleurs). Réserve tranchée : `StableMarriage/GaleShapley.lean` n'est **pas** une 2ᵉ attestation — l'appariement stable n'est pas l'agrégation de coalitions sur le treillis. **Verdict : reste en constitution.** + +**File d'attente — point fixe.** Second usage de Knaster-Tarski : `git grep -il knaster -- "*.lean"` → `argumentation_lean/Argumentation.lean` + `Argumentation/Characteristic.lean` (+ sibling `_en`) — un seul locus substantiel après dédoublonnage FR/EN (racine et module du même lake). Pas de second usage indépendant atterri : la promotion « dès le second usage » reste en attente. + +**Bilan A6** : quatre opérations statuées, zéro promotion, zéro descente. La table reste à **6 opérations en TABLE** (1, 4, 7, 8, 9, 10), **4 en file d'attente** (2, 3, 5, 6), **4 en constitution — toutes quatre FIRSTHAND désormais**. Reste **A7** (relecture froide : la table est-elle un catalogue ? une quatrième loi est-elle apparue ?) — dernier grain. + +## Tranche c.1208 (2026-09-16, po-2026:CoursIA-2) — op 11 : 2ᵉ attestation livrée (PR #16392) + +**Op 11 — FIRSTHAND (ce cycle), 2ᵉ attestation sur substrat indépendant.** `Search/Part1-Foundations/Search-11d-Descente-Sous-Budget.ipynb` (série Search, Python stdlib, exécuté papermill, 0 erreur) : knapsack 0/1, potentiel Φ = −valeur, voisinage bit-flip, barrière = borne LP relaxée, budget = plafond d'évaluations. La loi de `Descent.lean` y est **exercée** (asserts runtime sur 60 exécutions : 0 violation `hstrict`, 0 violation `hbarrier`, 0 dépassement de plafond) et sa troisième hypothèse **réfutée exécutablement** : `hnostall` est fausse dans un paysage générique (100 % d'arrêts « blocage » hors cible à budget généreux, gap médian 10,4 %) — la dissociation budget-vs-blocage exigée par `Descent.lean` l.148 est mesurée dans deux régimes (budget serré : 30/30 arrêts « budget » sur 30 graines ; budget généreux : 60/60 arrêts « blocage » hors cible sur 60 graines) ; courbe qualité-budget médiane 86,3 % → 8,9 % (B ∈ {20..800}, 30 seeds, saturation = optima locaux). **Verdict : reste en constitution jusqu'au merge** (convention op 7 : non comptée tant qu'OPEN) — la promotion en TABLE appartient à A7, qui tranche sur deux attestations indépendantes (Lean-formel + empirique-notebook). + +## Tranche c.1308 (2026-09-29, po-2024:CoursIA-2) — op 3 : re-vérification Infer-20 (piste vierge dans le ledger jusqu'ici) + +**Op 3 — FIRSTHAND (ce cycle), re-vérification d'Infer-20 comme 2ᵉ attestation candidate.** Issue dispatchée par ai-01 ([#18405](https://github.com/jsboige/CoursIA/issues/18405)) à 14:30Z — le coordinateur pointe qu'`Infer-20-Quotients-et-Fibres-Python.ipynb` (`Probas/Modules/Infer/`, PR #12277 MERGED 2026-08-22) porte **le protocole de l'opération 3** : projection vers un alphabet `Q` (quantification de `X₁ + X₂`) et mesure de `I(X₁;X₂|Q)` vs `I(X₁;X₂)`, qui est la forme conditionnelle de la règle de chaîne `H(X) = H(π(X)) + H(X|π(X))`. Le ledger — re-vérifié ce cycle (`git grep -nE "Infer-20|12226" docs/ledgers/`) — ne mentionne ni l'un ni l'autre : la piste est vierge, donc le critère d'admission au chant1 (« deux attestations indépendantes ») n'a jamais été tranché sur cette candidate. + +**Trois vérifications firsthand ce cycle :** + +1. **Infer-20 sur disque** (`Probas/Applications/Infer-20-Quotients-et-Fibres-Python.ipynb`, PR #12277 MERGED 2026-08-22) : la cellule 10 (code) construit `Q = np.digitize(S, quantiles)` avec `Q_BINS = 4` et `S = X₁ + X₂`. La cellule 14 teste `Q_OPERATIONAL = (I(X₁;X₂|Q) < 0.5 · I(X₁;X₂))` — verdict imprimé **NON TENTE** (`ratio = 1.684`, > critère 0.5). **Infer-20 illustre la règle de chaîne conditionnelle** : c'est exactement l'opération 3 sous sa forme `I(X₁;X₂) = I(X₁;X₂|Q) + I(X₁;X₂;Q)`. Mais elle **échoue à produire un quotient opérationnel** sur des gaussiennes linéaires corrélées `ρ = 0.6` — la quantification 1D de la somme ne suffit pas. + +2. **ANALYSE-04 sur disque** (`SymbolicAI/Lean/ANALYSE/ANALYSE-04-PFR-Primitives-Python.ipynb`) : cellule 7 — *« Lecture du résultat. La règle de chaîne `H(X) = H(X|Y) + I(X;Y)` est **vérifiée numériquement**. Information mutuelle `I(X;Y)` capture combien le cours (Y) explique la note (X) ; la résiduelle `H(X|Y)` capture la variation inexpliquée par le cours. Sémantique opérationnelle : `H(π(X))` ≈ ce que la projection capte ; `H(X|π(X))` ≈ ce qui reste dans les fibres. »* — Verdict de la cellule 9 : « Transportable large. Universelle en théorie de l'information. » C'est la **seule attestation locale** décomptée jusqu'ici (cf A3 l.97-106 : « teorth/pfr est une référence externe non incluse au dépôt, et la digestion EPIC l'a cité comme si elle était locale »). + +3. **Critère d'indépendance** (règle op 7 étendue à l'op 3, protocole EPIC §1) : ANALYSE-04 ([#12252](https://github.com/jsboige/CoursIA/pull/12252), MERGED 2026-08-22T12:57:43Z) et Infer-20 ([#12277](https://github.com/jsboige/CoursIA/pull/12277), MERGED 2026-08-22T12:58:17Z) sont **nés le même jour (2026-08-22, à 34 secondes d'écart), du même EPIC [#12204](https://github.com/jsboige/CoursIA/issues/12204) — issues sœurs [#12214](https://github.com/jsboige/CoursIA/issues/12214) (Lean-21b PFR) et [#12226](https://github.com/jsboige/CoursIA/issues/12226) (Probas quotient/fibres/recollement). Le témoin formel de l'opération 3 (`H(X) = H(π(X)) + H(X|π(X))`) est universel info-théorique, mais la non-indépendance tient sur des constats vérifiables : **même chantier EPIC, même jour, même lane de dispatch**. ANALYSE-04 seul revendique le stimulus PFR-Tao ; Infer-20, fille de [#12226](https://github.com/jsboige/CoursIA/issues/12226), ne le cite pas. L'indépendance au sens strict du critère « deux endroits non reliés par le stimulus initial » n'est **pas** vérifiée. + +**Verdict c.1308 — op 3 reste en file d'attente, mais le statut se précise :** + +- **Pas de promotion** : 1 attestation locale indépendante (ANALYSE-04) + 1 attestation pédagogique **non-indépendante** (Infer-20, même chantier) = critère « deux endroits indépendants » non atteint. +- **Mais** Infer-20 **valorisera** l'op 3 si une seconde instantiation **sur substrat indépendant** arrive — le protocole est reproductible, le témoin négatif est déjà mesuré (1.684), le pipeline opérationnel est tracé. +- Le **témoin négatif** transportable d'Infer-20 (quantification 1D de la somme d'un couple gaussien corrélé ⇒ ratio `I(X₁;X₂|Q)/I(X₁;X₂)` = 1.684, **donc quotient informationnel non atteignable**) est noté comme tel dans le ledger — c'est un résultat négatif qui borne la classe des quotients opérationnels naïfs. + +**Effet sur la table :** op 3 → toujours en file d'attente. Mention « 1 attestation locale + 1 pédagogique non-indépendante re-vérifiée c.1308 » dans le commentaire de livraison sur l'EPIC. **Pas de mouvement de table** ce cycle ; un futur A7bis qui trouve une 2ᵉ attestation sur un substrat hors-PFR (Probabilité élémentaire, codage, IC games) la fait basculer. + +**Distance de Ruzsa** (point 3 de #18405) : objet ICT à groupe additif identifié = **`MyIA.AI.Notebooks/IIT/ICT-Series/ict/factor_geometry.py`** (espace des activations `(ℝ^D, +)`, primitives `weighted_pca` / `max_principal_angle` / `basis_overlap` extraites de ICT-36-FLens-FactoredGeometry, PR #15514 MERGED). La convolution `X′ − Y′` y est définie composante par composante. Application directe : `d_ruzsa(X;Y) = H(X′ − Y′) − ½ H(X′) − ½ H(Y′)` sur deux activations factorisées. **Non livré dans cette tranche** (hors périmètre dispatch —> à pousser en grain suivant si ai-01 l'autorise, après qu'A7 ou un grain subséquent ait statué sur l'op 3). + +**Acceptance sortie ce cycle :** verdict d'attestation de l'opération 3 écrit dans le ledger (cette tranche), avec sa preuve (3 vérifications nommées) et le statut du témoin négatif. + +## Tranche c.1114 (2026-10-06, po-2023:CoursIA-2) — Ruzsa : contrat de l'organ corrigé + application ICT + témoin de limite + +Issue dispatchée par le coordinateur ai-01 (commentaire #18405, 2026-09-29) ; claim posé par cette lane le 2026-10-06. Précédent c.1308 (po-2024) laissait la **livraison** de la distance de Ruzsa sur objet ICT en suspens (« Non livré dans cette tranche —> à pousser en grain suivant si ai-01 l'autorise »). La présente tranche tranche ce volet : l'organ est qualifié firsthand, l'application à `factor_geometry.py` est livrée sous forme de carnet exécuté, et le **témoin de limite** demandé par le point 3 de #18405 est documenté. + +**Quatre vérifications firsthand ce cycle** (toutes dans `MyIA.AI.Notebooks/IIT/ICT-Series/ICT-36b-RuzsaOnFactorGeometry-Python.ipynb` — carnet compact, code exécuté papermill, 0 erreur) : + +1. **Organ cellule 1 (invariants) sur-revendique `d[X;X] = 0`.** Reproduction : `d_ruzsa({0:0.5, 1:0.5}, {0:0.5, 1:0.5}, 4) = 0.500000` bit (cellule 5 du carnet, cas 2). Le 0.5 vient de `H(X'-X) = 1.5` bits (distribution `{0: 0.5, 1: 0.25, 3: 0.25}`) moins `H(X) = H(Y) = 1` bit. Le contrat correct est : `d[X;Y] = 0` si et seulement si Y est une translatee de X (`Y = X + a` pour un `a` du groupe), pas un cas général pour `X = Y`. L'invariant tient pour X uniforme sur G (cas 1 du carnet : Z/8Z uniforme → `d[X;X] = 0.000000`). + +2. **L'invariant de translation COMMUNE tient :** `d[X+a; Y+a] = d[X;Y]` pour tout `a` (cellule 5 du carnet, cas 3). Test sur `X = {0:0.5, 1:0.5}` (non uniforme), translations 0, 1, 2 : les trois valeurs de `d_ruzsa(X;X+a)` sont **identiques à 1e-15** (mêmes 0.5). L'invariant cellule 1 est donc **vrai** sous sa forme littérale (`d[X+a; Y+a] = d[X;Y]`) ; c'est sa **conséquence** `d[X;X] = 0` qui est sur-revendiquée. + +3. **Application à `factor_geometry.py` :** `synthesize_activations(bases, n_tokens=4000, signal_var=1.0, noise_var=0.1, rng)` produit `X ∈ ℝ^{4000 × 24}`. Quantification par signe (signe ±1 → groupe `Z/2Z` additif). Distribution marginale de la coordonnée 0 : `{0: 0.5045, 1: 0.4955}`, `H(X) = 0.9999` bits, `d_ruzsa(X;X) = 0.000058` bits — la structure orthogonale des facteurs + le bruit gaussien rendent la marginale **quasi-uniforme** sur Z/2Z, donc `d_ruzsa` est essentiellement 0. C'est le cas **favorable** d'application de l'organ sur un objet ICT. + +4. **Témoin de limite :** sur le **même** objet d'activations, 3 schémas de quantification différents donnent des valeurs différentes de `d_ruzsa` (cellule 8 du carnet, witness). Signe (Z/2Z) → 0.000058 bit ; 3-quantiles (Z/3Z) → 0.000000 bit (par construction, marginales uniformes) ; 5-quantiles (Z/5Z) → 0.000000 bit (idem) ; hash LSB (Z/2Z, exercice 1) → 0.072061 bit (LSB biaisé de la mantisse IEEE 754 → marginale `{0: 0.665, 1: 0.335}`). **C'est précisément le "mapping affine" que l'organ cellule 5 dénonce** : la valeur de `d_ruzsa` dépend du schéma de quantification, pas seulement de l'objet sous-jacent. L'organ fonctionne sur son terrain (groupes abéliens, X uniforme), mais ne transporte pas tel quel sur les objets ICT — il faudrait soit garantir l'uniformité marginale par construction, soit contrôler la quantification comme une variable explicite de la mesure. + +**Verdict c.1114** : + +- **Op 3 reste en file d'attente** (statut inchangé depuis c.1308). Le présent carnet **ne promeut pas** l'op 3 : il documente un **test de limite** (aboutissant 2 du point 3 de #18405 : « Distance de Ruzsa : application sur un objet ICT à structure de groupe, **ou** test de limite documenté »), pas une seconde attestation indépendante. La règle d'admission reste : 2ᵉ attestation sur substrat indépendant. +- **Contrat de l'organ documenté** : `d[X+a; Y+a] = d[X;Y]` (vrai), `d[X;X] = 0` (vrai ssi X uniforme sur G, **sur-revendiqué** par la cellule 1). Le carnet ICT-36b documente l'overclaim et le mécanisme sous-jacent (entropie de la différence plus petite que l'entropie marginale pour X non uniforme). **Suivi proposé** (hors périmètre de cette tranche) : PR sur la série source `SymbolicAI/Lean/ANALYSE/` pour corriger l'invariant cellule 1 (ajouter la condition « X uniforme sur G »). La qualification de l'organ est **indépendante** de cette correction (po-2025 l'a identifiée 36 h avant, cf commentaire #18405 du 2026-10-05T20:25:53Z). +- **Le témoin de limite est mesuré** : sur le même objet ICT, 4 schémas de quantification donnent 4 valeurs de `d_ruzsa` (0, 0, 0.000058, 0.072). La dépendance au schéma est le **résultat** de cette tranche, pas un échec — c'est l'illustration ICT du « mapping affine » que l'organ cellule 5 met en garde. + +**Effet sur la table #12204** : néant sur la promotion de l'op 3. La tranche **remplit** le point 3 de #18405 (test de limite documenté) et **étend** la qualification de l'organ source (overclaim cellule 1 identifié et reproduit). Pour une promotion en TABLE, il faudrait une 2ᵉ attestation sur substrat hors-PFR (cf précédent c.1308). + +**Acceptance sortie ce cycle :** + +- [x] Contrat organ qualifié firsthand (4 cas, 0 réécriture, organ cellule 2 vendorisé verbatim avec SPDX). +- [x] Overclaim cellule 1 reproduit et documenté (`d[X;X] = 0.5` pour X non uniforme sur Z/4Z). +- [x] Application à `ict.factor_geometry.synthesize_activations` livrée (carnet ICT-36b, 7 code cells exécutées). +- [x] Témoin de limite livré (3 schémas, 4 valeurs de `d_ruzsa` sur le même objet). +- [x] 5 questions organ-first documentées en cellule 9 du carnet. +- [x] Statut op 3 inchangé : file d'attente. + +## Tranche réconciliation (2026-10-04, po-2027:CoursIA) — ops 2 et 6 : deux 2ᵉ attestations enregistrées (artefacts antérieurs au dernier toucher du ledger, non comptés) + +Motif : pattern #11900 inversé — ce n'est pas le body qui a vieilli, c'est le **ledger**. Deux artefacts livrés sur `main` entre deux tranches n'ont jamais été enregistrés dans la table. Vérification firsthand des deux ce 04/10. + +**Op 2 — GT-19, l'attestation locale qui existait déjà.** `GameTheory/GameTheory-19-Abstraction-a-Dette-Python.ipynb` : né de l'issue [#12229](https://github.com/jsboige/CoursIA/issues/12229) (CLOSED, même voyage de digestion du 2026-08-21, **jamais rattachée à cette EPIC** — 0 citation du body), livré par PR #12267 (2026-09-11), digéré par #18317 (2026-10-01), toutes les cellules code exécutées avec outputs. Contenu vérifié : cellule 3 (abstraction par fusion d'états, partition de 6 états, matrices moyennées) → cellule 7 (**solve exact de G̃, retransport, mesure DANS G** — le pipeline α→solve→ρ→σ_G de la loi) → cellule 12 (**courbe de dette sur la chaîne de raffinement P6 < P4 < P3 < P2**, chaîne vérifiée par `refines`), plus l'atlas des 15 paires (exercice 2) et la partition hors chaîne P3B vs P3 à taille égale (exercice 3, P3 = 1.9091) — la question « qu'ai-je le droit d'oublier » chiffrée. C'est la forme de témoin exigée par le critère §1, en force empirique-notebook. +**Réserve d'indépendance (précédent c.1308)** : GT-19 **cite Kroer-Sandholm** comme source théorique et naît du même batch de digestion — la non-indépendance par le stimulus initial invoquée pour op 3 / Infer-20 s'applique a priori au couple (théorème externe, instantiation locale qui le cite). La promotion TABLE appartient donc à A7, qui tranche : le critère « deux endroits indépendants » compte-t-il une instantiation pédagogique de la source elle-même ? **Statut : en constitution, pas de promotion auto-décidée.** + +**Op 6 — Search-03f, la 2ᵉ attestation livrée hier par cette même lane.** `Search/Part1-Foundations/Search-03f-Reparer-Localement-Sous-Garantie-Python.ipynb`, PR #19013 **MERGED 2026-10-04T02:14:57Z** — postérieure au dernier toucher de ce ledger (2026-09-30 01:22), d'où la ligne restée en FILE D'ATTENTE. toutes les cellules code exécutées (exécution complète vérifiée), [DELIVERED] posé sur l'EPIC le 03/10 17:24Z. Trois témoins exigés par la table, vérifiés dans le carnet : garantie transportée (coût LPA\* = coût A\* from scratch, 8/8 concordances sur séquence de 8 changements), localité payée juste (12 expansions pour le repair), et le troisième lu en conclusion. **Indépendance par construction : 0 mention de Sandholm dans le carnet** (mesuré) — substrat recherche de chemin, pas jeux. +**Statut : en constitution, promotion TABLE à statuer par la revue** (convention des ops 11-13). + +**Effet sur la table :** la file d'attente passe de 4 à 2 opérations (restent **3 et 5**) ; les ops 2 et 6 rejoignent les 4 en constitution → **6 en constitution**. Le bilan A6 ci-dessus reste historique. A7, quand il statuera, trouvera deux dossiers de plus sur son bureau — c'est précisément le geste attendu d'une réconciliation : rendre visible ce qui était déjà là. + +## Références + +- EPIC : [#12204](https://github.com/jsboige/CoursIA/issues/12204) · tranches : A3 ([ledger](../ledgers/12204-ict-chantier-1-a3.md), PR #12293) · audit-froid (ce fichier) +- Revue extérieure (protocole + 4 contestations) : commentaire #12204 du 2026-08-22 +- Steering : ai-01 2026-08-22T20:54Z ([DISPATCH→inbox] dashboard workspace-CoursIA) +- Précédent de format : [`3801-sota-axe2.md`](../ledgers/3801-sota-axe2.md)