Skip to content

fix(lean,#17357): Lean-21b -- lectures re-ancrees, mineur n=0 corrige, double lecture fusionnee #20101

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
myia-ai-01 merged 1 commit into from
Oct 10, 2026
Merged

fix(lean,#17357): Lean-21b -- lectures re-ancrees, mineur n=0 corrige, double lecture fusionnee #20101

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
163 changes: 73 additions & 90 deletions MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21b-MIMO-Converse-Native.ipynb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -725,9 +725,9 @@
"tags": []
},
"source": [
"**Lecture du lakefile et des modules** (cellule code[0]) :\n",
"**Lecture du lakefile et des modules** (cellule code[0], ouverture de la section 1) :\n",
"\n",
"La cellule ci-dessus est un *commentaire* Lean qui simule le contenu du\n",
"La cellule code[0], en ouverture de la section 1, est un *commentaire* Lean qui simule le contenu du\n",
"`lakefile.lean`. La structure typique d'un lakefile Lean 4 est :\n",
"\n",
"```lean\n",
Expand Down Expand Up @@ -1226,48 +1226,6 @@
"#eval 2 * Float.exp (-(4:Float) ^ 2 / 2)"
]
},
{
"cell_type": "markdown",
"id": "c13",
"metadata": {
"papermill": {
"duration": 0.020719,
"end_time": "2026-09-28T15:22:07.358315+00:00",
"exception": false,
"start_time": "2026-09-28T15:22:07.337596+00:00",
"status": "completed"
},
"tags": []
},
"source": [
"À trois écarts-types la borne tombe sous 2,5 %, à quatre sous 0,1 % : le bruit ne peut « s'échapper » que très rarement — c'est ce qui rend le score de flip stable.\n",
"\n",
"**Trois observations physiques** :\n",
"\n",
"1. **Loi en `exp(-t²/2)` vs `exp(-t)`** : la borne de concentration gaussienne est en exponentielle de `t²`, pas de `t`. C'est la difference majeure avec la borne de Markov (`P(X ≥ t) ≤ E[X]/t`) ou la borne sous-exponentielle. Pour `t = 4`, `exp(-16/2) = exp(-8) ≈ 3.35×10⁻⁴` (avant le facteur 2 de la borne symetrique), soit `0.000671` une fois double — exactement la valeur rendue par la cellule.\n",
"2. **Facteur 2 dans `2·exp(-t²/2)`** : il vient du symetrique : on borne `P(|‖X‖ - E‖X‖| ≥ t)`, qui est la reunion de `P(‖X‖ - E‖X‖ ≥ t)` et `P(E‖X‖ - ‖X‖ ≥ t)`. La borne symetrique a donc un facteur 2 par rapport a la borne unilaterale.\n",
"3. **Application au score de flip** : dans le decodeur ML du papier Papailiopoulos, le score de flip est `s·‖hᵢ‖² + √s·⟪hᵢ, w⟫`. Le bruit `⟪hᵢ, w⟫` est un scalaire gaussien de variance `‖hᵢ‖²`, donc il s'ecarte de plus de 3 ecarts-types avec probabilite au plus ~0.0222 — c'est la borne de Chernoff ci-dessus, la queue gaussienne **exacte** valant 0.0027, huit fois moins (cf. section 3.1). Pour un decodeur avec `N = 64` antennes, la probabilite qu'**un** `hᵢ` parmi les 64 ait un flip est bornee par `64 × 0.0222 ≈ 1.4`, qui depasse encore 1 : l'union bound ne suffit pas -- il faut la borne de Hanson-Wright (section 3) pour avoir une borne exponentiellement petite en `n`.\n",
"\n",
"**Transition vers la section 3** : la borne de Lipschitz borne la **norme** `‖w‖`, qui apparait lineairement dans le score de flip. Pour la **forme quadratique** `wᵀAw` (qui apparait quand on ecrit l'erreur ML au carre), il faut une borne de Hanson-Wright, qui est le sujet de la section suivante.\n",
"\n",
"**L'intuition derrière la stabilité du score de flip** : le score de flip est\n",
"`s·‖hᵢ‖² + √s·⟪hᵢ,w⟫`. Le premier terme est *déterministe* (ne dépend pas du\n",
"bruit). Le second terme est *aléatoire* et est ce qui peut faire « basculer » un\n",
"flip. Or `⟪hᵢ,w⟫ ≤ ‖hᵢ‖·‖w‖` par Cauchy-Schwarz. Si `‖hᵢ‖` et `‖w‖` sont\n",
"*concentrés* autour de leurs moyennes (c'est ce que `NormTails` prouve), alors\n",
"`⟪hᵢ,w⟫` est lui-même concentré. Le score de flip ne peut *s'échapper* que\n",
"lorsque les deux normes s'écartent simultanément — un événement *doublement*\n",
"rare.\n",
"\n",
"**La loi des petits nombres appliquée au score de flip** : la probabilité qu'un\n",
"flip donné « batte » le point de départ est dominée par la queue de\n",
"`‖w‖·‖hᵢ‖`. Quand les deux queues sont indépendantes (cas gaussien), la\n",
"probabilité *combinée* est le produit — d'où une probabilité *extrêmement*\n",
"petite. C'est ce que `Bridge.lean` capture formellement.\n",
"\n",
"**Coût** : pas de cellule code — c'est une interprétation."
]
},
{
"cell_type": "markdown",
"id": "b169162a",
Expand Down Expand Up @@ -1302,9 +1260,34 @@
"\n",
"**La decroissance est super-exponentielle** : d'un ecart-type au suivant, le facteur n'est pas constant — 1.213 → 0.271 (÷4,5), puis 0.271 → 0.0222 (÷12), puis 0.0222 → 0.000671 (÷33). C'est la signature du `t²` a l'exposant : chaque ecart-type supplementaire coute de plus en plus cher.\n",
"\n",
"**Lecture physique en une ligne** : À trois écarts-types la borne tombe sous 2,5 %, à quatre sous 0,1 % : le bruit ne peut « s'échapper » que très rarement — c'est ce qui rend le score de flip stable.\n",
"\n",
"**Pourquoi `Float` plutot que `Real`** : `Real.exp` est non-computable par defaut (la fonction `exp` reelle n'a pas d'algorithme exact en arithmetique flottante). Pour `#eval`, on a besoin d'un type **computable**, donc `Float` (IEEE 754 double precision). L'affichage a six decimales garde trois chiffres significatifs jusqu'a la plus petite des quatre valeurs (`0.000671`).\n",
"\n",
"**Implication pour la suite** : la section 3 sur le converse Hanson-Wright prend la releve pour les formes quadratiques. La borne de Lipschitz est suffisante pour la **norme**, mais insuffisante pour `wᵀAw`. La frontiere entre les deux routes est tracee dans la documentation du module `Converse`."
"**Trois observations physiques** :\n",
"\n",
"1. **Loi en `exp(-t²/2)` vs `exp(-t)`** : la borne de concentration gaussienne est en exponentielle de `t²`, pas de `t`. C'est la difference majeure avec la borne de Markov (`P(X ≥ t) ≤ E[X]/t`) ou la borne sous-exponentielle. Pour `t = 4`, `exp(-16/2) = exp(-8) ≈ 3.35×10⁻⁴` (avant le facteur 2 de la borne symetrique), soit `0.000671` une fois double — exactement la valeur rendue par la cellule.\n",
"2. **Facteur 2 dans `2·exp(-t²/2)`** : il vient du symetrique : on borne `P(|‖X‖ - E‖X‖| ≥ t)`, qui est la reunion de `P(‖X‖ - E‖X‖ ≥ t)` et `P(E‖X‖ - ‖X‖ ≥ t)`. La borne symetrique a donc un facteur 2 par rapport a la borne unilaterale.\n",
"3. **Application au score de flip** : dans le decodeur ML du papier Papailiopoulos, le score de flip est `s·‖hᵢ‖² + √s·⟪hᵢ, w⟫`. Le bruit `⟪hᵢ, w⟫` est un scalaire gaussien de variance `‖hᵢ‖²`, donc il s'ecarte de plus de 3 ecarts-types avec probabilite au plus ~0.0222 — c'est la borne de Chernoff ci-dessus, la queue gaussienne **exacte** valant 0.0027, huit fois moins (cf. section 3.1). Pour un decodeur avec `N = 64` antennes, la probabilite qu'**un** `hᵢ` parmi les 64 ait un flip est bornee par `64 × 0.0222 ≈ 1.4`, qui depasse encore 1 : l'union bound ne suffit pas -- il faut la borne de Hanson-Wright (section 3) pour avoir une borne exponentiellement petite en `n`.\n",
"\n",
"**L'intuition derrière la stabilité du score de flip** : le score de flip est\n",
"`s·‖hᵢ‖² + √s·⟪hᵢ,w⟫`. Le premier terme est *déterministe* (ne dépend pas du\n",
"bruit). Le second terme est *aléatoire* et est ce qui peut faire « basculer » un\n",
"flip. Or `⟪hᵢ,w⟫ ≤ ‖hᵢ‖·‖w‖` par Cauchy-Schwarz. Si `‖hᵢ‖` et `‖w‖` sont\n",
"*concentrés* autour de leurs moyennes (c'est ce que `NormTails` prouve), alors\n",
"`⟪hᵢ,w⟫` est lui-même concentré. Le score de flip ne peut *s'échapper* que\n",
"lorsque les deux normes s'écartent simultanément — un événement *doublement*\n",
"rare.\n",
"\n",
"**La loi des petits nombres appliquée au score de flip** : la probabilité qu'un\n",
"flip donné « batte » le point de départ est dominée par la queue de\n",
"`‖w‖·‖hᵢ‖`. Quand les deux queues sont indépendantes (cas gaussien), la\n",
"probabilité *combinée* est le produit — d'où une probabilité *extrêmement*\n",
"petite. C'est ce que `Bridge.lean` capture formellement.\n",
"\n",
"**Transition vers la section 3** : la borne de Lipschitz borne la **norme** `‖w‖`, qui apparait lineairement dans le score de flip. Pour la **forme quadratique** `wᵀAw` (qui apparait quand on ecrit l'erreur ML au carre), il faut une borne de Hanson-Wright, qui est le sujet de la section suivante — la frontiere entre les deux routes est tracee dans la documentation du module `Converse`.\n",
"\n",
"**Coût** : pas de cellule code — c'est une interprétation."
]
},
{
Expand Down Expand Up @@ -1496,9 +1479,9 @@
"tags": []
},
"source": [
"**Lecture des théorèmes SLT empruntés** (cellules code[1]–[2]) :\n",
"**Lecture des théorèmes SLT empruntés** (cellules code[1]–[2], section 1.1) :\n",
"\n",
"Les 4 `#check` rendent les *signatures* des théorèmes SLT consommés par le lac (les signatures complètes, verbatim, sont commentées en §1.1 ci-dessus).\n",
"Les 4 `#check` — exécutés en section 1.1, en tête du carnet — rendent les *signatures* des théorèmes SLT consommés par le lac (les signatures complètes, verbatim, y sont commentées).\n",
"\n",
"**`gaussian_lipschitz_concentration`** (de `GaussianLipConcen`) : le théorème certifie qu'une fonction `L`-Lipschitz d'un vecteur gaussien standard a une queue sous-gaussienne — l'écart à la moyenne est borné par `2·exp(-t²/(2L²))`. La sortie attendue par `#check` est juste le *type* — sans corps de preuve affiché.\n",
"\n",
Expand Down Expand Up @@ -1872,7 +1855,7 @@
"source": [
"**Lecture de `norm_concentration` et ses axiomes** (cellule code[4]) :\n",
"\n",
"La cellule ci-dessus inclut un `#print axioms Mimo.norm_concentration` — un\n",
"La cellule code[4] (section 2, Briques B) inclut un `#print axioms Mimo.norm_concentration` — un\n",
"*audit formel* des axiomes utilisés par ce théorème.\n",
"\n",
"**Résultat attendu** :\n",
Expand All @@ -1898,7 +1881,7 @@
"`axiom my_special_axiom : True` et ensuite « prouver » n'importe quoi. `#print\n",
"axioms` ferme cette porte.\n",
"\n",
"**Le `#print axioms Mimo.column_norm_tail`** de la cellule code[5] : même\n",
"**Le `#print axioms Mimo.column_norm_tail`** de la cellule code[5] (section 2, Briques C) : même\n",
"audit pour l'instanciation MIMO. Le résultat attendu est identique\n",
"(`propext, Classical.choice, Quot.sound`) — ce qui confirme que la\n",
"spécialisation MIMO n'introduit pas d'axiome exotique.\n",
Expand Down Expand Up @@ -2167,6 +2150,47 @@
},
"tags": []
},
"source": [
"### Lecture des minorations de la densite gaussienne (ancre sur code[10])\n",
"\n",
"La sortie verbatim de code[10] enumere les declarations. Certaines d'entre elles portent la substance :\n",
"\n",
"```\n",
"open Mimo in\n",
"#check gaussianPDFReal_lower_abs\n",
"─────▶ Mimo.gaussianPDFReal_lower_abs {R x : ℝ} (hx : |x| ≤ R) :\n",
" Real.exp (-R ^ 2 / 2) / √(2 * Real.pi) ≤ ProbabilityTheory.gaussianPDFReal 0 1 x\n",
"#check one_sub_pow_le_exp_mul\n",
"─────▶ Mimo.one_sub_pow_le_exp_mul {n : ℕ} {p : ℝ} (hn : 0 < n) (hp0 : 0 ≤ p) (hp : p ≤ 1) :\n",
" (1 - p) ^ n ≤ Real.exp (-(↑n * p))\n",
"```\n",
"\n",
"Les quatre autres sont `gaussianPDFReal_lower_two`, `gaussian_interval_mass_lower_param`, `gaussian_interval_mass_lower` et `gaussian_interval_mass_lower_inv_sqrt` — les variantes qui integrent la minoration ponctuelle sur un intervalle.\n",
"\n",
"**Trois roles** :\n",
"\n",
"1. **Minorer la densite** (`gaussianPDFReal_lower_abs`) : sur la boule `|x| ≤ R`, la densite standard vaut au moins sa valeur au bord. Minoration **uniforme**, sans parametre `ε` : c'est ce qui la rend integrable a la main.\n",
"2. **Minorer une masse d'intervalle** (`gaussian_interval_mass_lower*`) : integrer la constante precedente sur un intervalle donne une minoration de la masse gaussienne qu'il porte. C'est la brique dont se sert `flip_bat_prob_lower` pour produire son facteur `exp(-2)/√(2π)`.\n",
"3. **Composer sur les `N` colonnes** (`one_sub_pow_le_exp_mul`) : `(1-p)ⁿ ≤ exp(-np)`. Attention au sens de lecture — la probabilite qu'**aucune** des `N` colonnes ne s'ecarte est ainsi majoree par `exp(-N·p)`, donc celle qu'**au moins une** s'ecarte est **minoree** par `1 - exp(-N·p)`. C'est bien une minoration : un converse doit garantir qu'un echappement se produit, pas qu'il est rare. L'hypothese `hn : 0 < n` evite le cas degenere `n = 0`, ou les deux membres valent `1` (egalite triviale, qui ne porte aucune information) : elle garantit que la minoration a un contenu.\n",
"\n",
"**Composition dans le lake** : ces briques se retrouvent dans la borne `ml_error_prob_ge_threshold` (cf. section 4, `ml_error_prob_ge_threshold`), dont le membre de gauche `1 - exp(-(2·log N - log log N))` a exactement la forme produite par `one_sub_pow_le_exp_mul` une fois `p` instancie par la minoration de masse.\n",
"\n",
"**Pourquoi `Real` plutot que `Float`** : les minorations de queues sont des inegalites **continues**, pas des evaluations ponctuelles. On les prouve une fois pour toutes et elles valent pour tout `x` reel. La precision flottante n'est pas requise pour la preuve -- seulement pour l'evaluation (cf. `Float.exp` en section 2.1)."
]
},
{
"cell_type": "markdown",
"id": "b500bc33",
"metadata": {
"papermill": {
"duration": 0.052452,
"end_time": "2026-09-28T15:22:08.992786+00:00",
"exception": false,
"start_time": "2026-09-28T15:22:08.940334+00:00",
"status": "completed"
},
"tags": []
},
"source": [
"## 4. `Bridge` — ce que le converse dit du décodeur ML\n",
"\n",
Expand Down Expand Up @@ -2223,47 +2247,6 @@
"**Le théorème final de `Bridge`** : `ml_error_prob_ge_threshold` *minore* la probabilité d'erreur ML par une quantité de forme `1 - exp(…)` (signatures verbatim ci-dessus). C'est exactement ce qu'un converse doit produire — une limite inférieure, dérivée des queues de `NormTails` et `Converse`, qu'aucun décodeur ne peut dépasser."
]
},
{
"cell_type": "markdown",
"id": "b500bc33",
"metadata": {
"papermill": {
"duration": 0.052452,
"end_time": "2026-09-28T15:22:08.992786+00:00",
"exception": false,
"start_time": "2026-09-28T15:22:08.940334+00:00",
"status": "completed"
},
"tags": []
},
"source": [
"### Lecture des minorations de la densite gaussienne (ancre sur code[10])\n",
"\n",
"La sortie verbatim de code[10] enumere les declarations. Certaines d'entre elles portent la substance :\n",
"\n",
"```\n",
"open Mimo in\n",
"#check gaussianPDFReal_lower_abs\n",
"─────▶ Mimo.gaussianPDFReal_lower_abs {R x : ℝ} (hx : |x| ≤ R) :\n",
" Real.exp (-R ^ 2 / 2) / √(2 * Real.pi) ≤ ProbabilityTheory.gaussianPDFReal 0 1 x\n",
"#check one_sub_pow_le_exp_mul\n",
"─────▶ Mimo.one_sub_pow_le_exp_mul {n : ℕ} {p : ℝ} (hn : 0 < n) (hp0 : 0 ≤ p) (hp : p ≤ 1) :\n",
" (1 - p) ^ n ≤ Real.exp (-(↑n * p))\n",
"```\n",
"\n",
"Les quatre autres sont `gaussianPDFReal_lower_two`, `gaussian_interval_mass_lower_param`, `gaussian_interval_mass_lower` et `gaussian_interval_mass_lower_inv_sqrt` — les variantes qui integrent la minoration ponctuelle sur un intervalle.\n",
"\n",
"**Trois roles** :\n",
"\n",
"1. **Minorer la densite** (`gaussianPDFReal_lower_abs`) : sur la boule `|x| ≤ R`, la densite standard vaut au moins sa valeur au bord. Minoration **uniforme**, sans parametre `ε` : c'est ce qui la rend integrable a la main.\n",
"2. **Minorer une masse d'intervalle** (`gaussian_interval_mass_lower*`) : integrer la constante precedente sur un intervalle donne une minoration de la masse gaussienne qu'il porte. C'est la brique dont se sert `flip_bat_prob_lower` pour produire son facteur `exp(-2)/√(2π)`.\n",
"3. **Composer sur les `N` colonnes** (`one_sub_pow_le_exp_mul`) : `(1-p)ⁿ ≤ exp(-np)`. Attention au sens de lecture — la probabilite qu'**aucune** des `N` colonnes ne s'ecarte est ainsi majoree par `exp(-N·p)`, donc celle qu'**au moins une** s'ecarte est **minoree** par `1 - exp(-N·p)`. C'est bien une minoration : un converse doit garantir qu'un echappement se produit, pas qu'il est rare. L'hypothese `hn : 0 < n` est necessaire — l'enonce est faux pour `n = 0`, ou le membre de gauche vaut 1.\n",
"\n",
"**Composition dans le lake** : ces briques se retrouvent dans la borne `ml_error_prob_ge_threshold` (cf. cell[27]), dont le membre de gauche `1 - exp(-(2·log N - log log N))` a exactement la forme produite par `one_sub_pow_le_exp_mul` une fois `p` instancie par la minoration de masse.\n",
"\n",
"**Pourquoi `Real` plutot que `Float`** : les minorations de queues sont des inegalites **continues**, pas des evaluations ponctuelles. On les prouve une fois pour toutes et elles valent pour tout `x` reel. La precision flottante n'est pas requise pour la preuve -- seulement pour l'evaluation (cf. `Float.exp` en cell[13])."
]
},
{
"cell_type": "code",
"execution_count": 12,
Expand Down
Loading