Écrite 2026-07-08 par la flotte de consolidation finale
(task-20260707-59f4) pour la réunion Étienne. Registre :
mathématiquement précis, pas de sur-revendication. Ce document raconte
comment la mission a avancé, ce qui a été
prouvé, ce qui a résisté et pourquoi, et
les leçons de méthode. Pour l'état de preuve chiffré et
à jour, voir report.md et completion-100.md ; pour la
narration en registre Feynman, ../lore/CHRONICLES.md.
Étienne (2026-04-17) : caractériser les statistiques \(\varphi : \mathbb{R}^d \to \mathbb{R}^r\) pour lesquelles la famille exponentielle \(p_\theta(x) \propto e^{-\theta^\top\varphi(x)}\) est stable par convolution gaussienne — c.-à-d. \(p_\theta \ast \gamma_\sigma\) reste dans la même famille à reparamétrisation \(\theta \mapsto \tilde\theta\) près. Trois niveaux : Q1 (caractérisation générale), Q2 (cas quadratique, tractable), Q3 (équivalence avec une EDP de type Hamilton–Jacobi).
Le résultat central, découvert tôt et jamais démenti : la stabilité équivaut à la clôture algébrique de la statistique sous l'opérateur de Cole–Hopf \(\mathcal{L}f = \tfrac12\|\nabla f\|^2 - \tfrac12\Delta f\), uniformément en \(\theta\) (Proposition \((\dagger)\), sous minimalité). Pour une famille polynomiale, \((\dagger)\) force \(\deg\varphi_i \le 2\) : toute famille polynomiale stable est au plus quadratique.
La mission a couru en deux grandes vagues, séparées par une migration
d'infrastructure (les répertoires ~/ →
~/galaxies/).
Délibération d'ouverture
(delib-20260416, panel Hawking / Shannon / von Neumann /
Feynman / Wheeler). Le problème d'Étienne est découpé en six molécules.
Feynman pose d'emblée la lecture qui gouvernera toute la suite : la Q3
n'est pas un cycle vicieux, elle est sous-spécifiée (voir
§4.1).
Q2 — le cas quadratique, prouvé analytiquement et en
Lean. C'est le marchepied. Pour \(\varphi(x) = (\mathrm{vec}(xx^\top), x)\),
coordonnées \((M, b)\), la stabilité
est explicite : \[\tilde M = M(I + \sigma^2
M)^{-1}, \qquad \tilde b = (I + \sigma^2 M)^{-1} b,\] dérivée de
façon autonome (complétion de carré + convolution de gaussiennes +
identité de Woodbury), avec le flot de Riccati \(\dot M = -M^2\), \(\dot b = -Mb\). Le volet Lean s'est
construit lemme par lemme (shift_posDef,
woodbury_commutative, reparam_injective,
tildeM_posDef), puis le théorème mesure-niveau
q2_stability a été fermé par la route de la
fonction caractéristique
(Measure.ext_of_charFun + charFun_conv +
charFun_multivariateGaussian). Le dernier
sorry (branche vacue \(d=0\) de tildeM_lt_inv_s) a
été fermé par un correctif de signature [Nonempty (Fin d)].
Résultat : Q2 machine-vérifié à 0 sorry / 0
axiom.
Papier + double revue adversariale. Un article principal et un volet méthodes formelles sont rédigés, puis soumis à deux passes indépendantes — un reviewer (top-down contre rubrique) et un sceptique (reconstruction bottom-up depuis l'énoncé). Elles convergent sur les défauts locaux (une formule de Fisher fabriquée, « cubique » pour « quartique ») et divergent sur les défauts structurels (glissement de portée abstract vs corps). Voir §4.3.
Le mur amont (2am, 2026-04-18). Le
sorry que la flotte voulait fermer dépendait d'un opérateur
laplacian sur les espaces de Hilbert de dimension finie
qui n'existait pas encore dans Mathlib. L'auto-pilote
refuse de forcer une tactique de plus. Décision : le
mur est architectural, pas tactique. C'est le moment fondateur
de la discipline 0-axiom (§4.4).
Après la migration, la flotte reprend et attaque les questions restées ouvertes.
Q1a — la caractérisation générale, formalisée.
La Proposition \((\dagger)\) est
prouvée dans les deux sens (sens ⇐ par construction du flot via
Cauchy–Lipschitz, contournant la circularité ; sens ⇒). Le Théorème 5.1
force inconditionnellement \(\deg\varphi_i \le
2\). Le cœur algébrique (borne de degré + clôture Cole–Hopf) est
formalisé en Lean à 0 sorry / 0
axiom.
Q1b — intégrabilité. Le domaine naturel \(\Theta^\star = \{\theta : Z_\theta <
\infty\}\) — dans le cas quadratique, le cône SPD ouvert \(\{\sum_k \theta_k A_k \succ 0\}\) — est
prouvé forward-invariant sous le flot de convolution. Comme
toute famille polynomiale stable est de degré ≤ 2 (Q1a), Q1b est
clos pour toute famille polynomiale stable. Le cœur SPD \(M \succ 0 \Rightarrow \tilde M \succ 0\)
est vérifié en Lean (tildeM_posDef).
Q1-exotique — le non-polynomial, largement clos. Deux théorèmes structurels : Thm A (rigidité analytique — l'ellipticité/hypoellipticité de \(P(\Delta)\) force toute statistique stable à être réel-analytique ; pas de bump function, donc tout le \(C^\infty\) non analytique tombe) et Thm B (doublement du rayon spectral — le carré du champ \(\Gamma\) double le rayon spectral de Fourier, qu'une famille finie ne peut soutenir ; tout le réel-analytique à croissance ≤ polynomiale, donc borné — \(1/(1+\|x\|^2)\), \(\arctan\), \(\tanh\), \(\cos\), Bessel… — est polynomial ≤ 2). Volet analytique pur, sans Lean (choix de portée). Reste une niche (§3.2).
Q3 — l'équivalence Hamilton–Jacobi. Le gros du
travail de la vague 2. L'énoncé : la stabilité régulière
(ponctuelle H1 + minimalité H2 + régularité \(C^1\) du chemin H3 + sous-gaussianité H4)
équivaut à l'existence d'un chemin \(t \mapsto
\theta_t\) vérifiant l'EDP (6). Le théorème principal Lean
q3_regular_stability_iff_admissible_path est
câblé-clos (0 sorry), réduit à deux lemmes
directionnels. Sa fermeture a demandé la construction de quatre briques
amont (§2).
Clôtures de juillet 2026.
task-20260707-ddc7 ferme deux des trois sorry
de EFS.Heat ; task-20260707-04c4 reformule le
crux Widder en classe Tychonoff et prouve l'ingrédient spatial du
principe du maximum. Le compte de sorry réels passe de
6 à 4.
La fermeture de Q3 en Lean ne bute pas sur la logique de la preuve — le papier est complet — mais sur des primitives analytiques absentes de Mathlib v4.29.0. La flotte les a nommées, scopées, et attaquées une par une.
| Brique | Objet | État |
|---|---|---|
M1 — laplacian_comp_scalar |
Laplacien d'une composition scalaire non-linéaire : \(\Delta(f\circ h) = f''(h)|\nabla h|^2 +
f'(h)\,\Delta h\). Construite (~160 lignes) par restriction
aux droites de coordonnées + iteratedDeriv_comp_two
(Faà-di-Bruno 1-D) + Parseval sur la base orthonormée. |
prouvée, 0 sorry / 0 axiom.
Ferme Cole–Hopf
(coleHopf_density_heat_iff). |
M2 — EFS.Heat |
L'équation de la chaleur du noyau gaussien : \(\partial_t(p \ast K_t) = \tfrac12\Delta_x(p \ast
K_t)\). Module dédié (candidat
Mathlib.Analysis.PDE.Heat). |
squelette + sous-lemmes prouvés + 1
sorry. heatKernel_solves_heat et
integrable_heatKernel fermés (juillet, ddc7) ; reste
gaussian_conv_solves_heat (différentiation dominée). |
W — EFS.Q3.Widder |
L'unicité de l'équation de la chaleur (le crux du sens ⇐). Reformulée en classe sous-gaussienne / Tychonoff (juillet, 04c4) : uniquement ce dont la preuve a besoin. | crux sorry unique ; l'algèbre Step-5
(density_injective_of_minimal), la linéarité
(isHeatSolution_sub) et l'ingrédient spatial du principe du
maximum (laplacian_nonpos_of_isLocalMax) sont prouvés. |
| S1 — enrichissement de fidélité | Décision opérateur : ConvolutionReproducesAt porte
désormais l'identité de convolution (H1) ; AdmissiblePath
contraint le chemin à \(\mathrm{int}(\Theta^\star)\) + régime
densitaire (H2/H3/H4). |
exécutée. Lève le « contrat creux » ; les deux directions deviennent prouvables-tels-qu'énoncés. Trois gardes adversariaux nouveaux. |
Le facteur ½ / variance du noyau mérite une note :
le \(\gamma_{\sqrt{2t}}\) d'Étienne
(variance \(2t\)) satisfait \(\partial_t = \Delta\) (facteur 1), pas le
\(\tfrac12\Delta\) canonique. Pour
garder l'opérateur \(\tfrac12\) de
Cole–Hopf (cœur de Q1/Q3) vrai, M2 utilise le noyau
variance-\(t\)
(substitution \(t = \sigma^2\)). C'est
une décision de fidélité, surfacée plutôt que patchée silencieusement
(docs/circular-heat-factor.md).
Deux poches restent ouvertes. Aucune ne touche le cœur scientifique de la question d'Étienne — les trois questions ont chacune une réponse prouvée.
La direction inverse de Q3 (\(\Leftarrow\)) bottom-out sur
l'unicité de l'équation de la chaleur sous croissance
sous-gaussienne (Tychonoff 1935). La route passe par le principe du
maximum parabolique faible sur cylindres bornés \((0,T]\times B_R\) + une barrière
Tychonoff–Täcklind quand \(R \to
\infty\). La flotte a prouvé son ingrédient
spatial (laplacian_nonpos_of_isLocalMax : \(\Delta g \le 0\) en un max spatial
intérieur) et la linéarité
(isHeatSolution_sub). Ce qui reste absent de Mathlib
v4.29.0 : (i) le case-split extrême espace-temps avec le signe de la
dérivée temporelle au bord, et (ii) la localisation par barrière (où
l'exposant de croissance \(a\) et
l'horizon fini \(T_0 = 1/(2a)\)
entrent).
Pourquoi ça résiste : aucune théorie PDE
parabolique n'existe dans Mathlib v4.29.0 — ni principe du maximum
parabolique, ni représentation de Widder, ni unicité de Tychonoff. C'est
un chantier amont de niveau recherche (multi-mois), pas une itération de
worker. Il a été surfacé cosmon-ward comme missing
primitive (task-20260624-8c36), conformément à la
discipline « le réacteur apprend de ce qu'il brûle » — pas contourné par
un axiom.
La brique M2 (gaussian_conv_solves_heat, existence de la
chaleur) est, elle, faisable : plusieurs centaines de
lignes de différentiation dominée, sans gap conceptuel. Une revue de
faisabilité (von Neumann) a corrigé un cadrage antérieur : le théorème
est vrai et prouvable tel qu'énoncé, la domination passant par
l'intégrabilité \(L^1\), pas par la
borne de croissance.
Le résidu analytique de Q1-exotique : les statistiques \(\varphi\) réel-analytiques, bornées inférieurement, à croissance strictement surpolynomiale, oscillantes (pour échapper à Q1b et à la Prop. 5), non exp-polynomiales (pour échapper au Thm 2). C'est l'intersection de tous les filtres connus. Aucun candidat explicite n'existe ; la classe est conjecturalement vide.
Pourquoi ça résiste : ce n'est pas une preuve manquante d'une affirmation utile — c'est l'aveu honnête que les outils actuels (rigidité elliptique + analyse de Fourier) ne ferment pas par théorème un coin du paysage où, à ce jour, personne ne sait exhiber d'objet. Fermer cette niche demanderait soit un candidat explicite (qui la remplirait), soit un théorème d'inexistence plus fin que le doublement du rayon spectral.
La galaxie est purement mathématique : pas de code de build, pas de suite de tests. La seule monnaie est la preuve propre. Quatre disciplines ont émergé et payé.
La Q3 d'Étienne se lisait comme une équivalence circulaire : dériver
l'EDP suppose le chemin \(\theta_t\)
dont on veut prouver l'existence. Le premier réflexe du panel fut de
crier « cycle vicieux ». La vraie lecture : l'énoncé n'est pas
auto-référent, il est sous-spécifié. Nommer les
hypothèses cachées (H2 minimalité, H3 régularité \(C^1\), H4 unicité sous-gaussienne)
convertit le faux cycle en équivalence propre entre notions raffinées.
Séparer les deux directions en budgets d'hypothèses
indépendants est comment on distingue le cycle de la
sous-spécification. Le même motif a resurgi en Q1a. Les notes
circular-*.md sont la trace laissée visible de cette
discipline.
Corollaire dur (chronique « A Property Cannot Be Both Axiom and Theorem ») : pour toute propriété de régularité, décider explicitement si c'est un axiome ou un théorème. H3 décrite à la fois comme « nécessaire » et « conséquence » n'est ni l'une ni l'autre — c'est un trou qui se propage silencieusement.
Chaque sous-question a été traitée par un worker, auditée par un adversaire distinct, et chroniquée. La leçon (chronique « Reviewer and Sceptic Must Read Different Inputs ») : quand deux passes adversariales tournent en parallèle, leur donner des artefacts d'entrée différents — le reviewer lit le papier top-down contre la rubrique, le sceptique lit l'énoncé bottom-up et reconstruit. L'overlap sur les défauts locaux (arithmétique, nommage) est la redondance qu'on veut ; la divergence sur les défauts structurels (glissement de portée, lemmes non nommés, mauvaise attribution) est la couverture qu'on a payée.
23 entrées
(lean/EFS/EFS/Adversarial/{Q2,Q3}/*.lean), chacune une
formulation affaiblie d'un énoncé (SPD manquant, minimalité
manquante, facteur ½ silencieux, signe H-J faux, contrat de convolution
creux, positivité densitaire manquante…) que Lean doit
rejeter. Le corpus est le garde dual du
sorry : là où le sorry dit « voici ce qui
n'est pas encore prouvé », le corpus dit « voici ce que nos énoncés ne
doivent jamais silencieusement devenir ». Un
verify-corpus.sh mécanique échoue si une seule entrée
passe. Il a attrapé, en temps réel, les tentatives d'affaiblir un énoncé
pour fermer un sorry — exactement le motif de
fausse-clôture qu'il existe pour détecter. 23/23
rejettent à ce jour.
À 2h du matin (2026-04-18), la tentation était de forcer une tactique
et d'appeler ça un progrès. L'auto-pilote a refusé — parce que la
même grammaire d'hallucination qui produit une citation périmée
produirait un terme Lean périmé. Le mur amont (une primitive
Mathlib absente) n'est pas un échec : c'est un point de décision
architectural. La réponse n'est jamais axiom (qui
laisserait les lemmes type-checker tout en cachant l'obligation), mais :
construire une brique locale honnête (M1, M2, W), ou surfacer la
primitive manquante cosmon-ward, ou reformuler la portée. Le mandat de
la galaxie — rigueur > vitesse, JAMAIS axiomatiser
— a tenu de bout en bout : 0 axiom custom dans tout le
corpus, du premier lemme Q2 au dernier ingrédient du principe du
maximum. La frontière ouverte reste visible ; c'est le titre de crédit,
pas l'inverse.
Mathématiquement — la mission est complète. Q1 (caractérisation + classification polynomiale), Q2 (forme fermée + Riccati), Q3 (équivalence Hamilton–Jacobi sous stabilité régulière) ont chacune une réponse prouvée. Le seul résidu mathématique est une niche exotique conjecturalement vide, sans candidat connu.
Mécaniquement (Lean 4) — vérification à ~85 %.
Q1a et Q2 machine-vérifiés à 0 sorry / 0 axiom. Q3 :
théorème principal câblé-clos, Cole–Hopf prouvé (M1), structures
enrichies (S1), EFS.Heat tombé de 3 à 1 sorry,
direction inverse réduite à un crux unique. Reste 4
sorry, tous amont-PDE, 0 axiom, se ramenant à
deux obligations racines : l'existence de la chaleur
(M2, faisable) et le crux Widder (research-grade, absent de
Mathlib).
Ce que la mission a produit au-delà des réponses
: deux articles (principal + volet formel), une bibliothèque
Lean 4 réutilisable (dont la brique laplacian_comp_scalar,
candidate à contribution upstream), un corpus adversarial de 23 gardes,
neuf notes de preuve, treize cartes concept, et une trace narrative
(docs/lore/) des principes illuminés.
Le mouvement net depuis avril : d'un problème qui « semblait tourner en rond » à trois réponses prouvées + une frontière Lean nommée, scopée, et honnête — un seul crux research-grade la sépare de la vérification mécanique complète, et ce crux est un chantier amont de PDE parabolique, pas une décision en suspens.
Question scientifique © Étienne (2026-04-17). Produit par une flotte d'agents Noogram.