Circularité — Invariance de \(\Theta^\star\) sous le flot (Q1b)

Note annexée à q1b-integrability.md §2.7. Pendant Q1b de la note circular-q1a-stability-vs-closure.md.

Symptôme

La preuve de stabilité \((\Leftarrow)\) de q1a §4.1 construit le flot \(t\mapsto\theta_t\) en résolvant l'EDO polynomiale \(\dot\theta_{t,k} = A_k(\theta_t)\) (Cauchy–Lipschitz), puis écrit explicitement :

« Sa permanence dans \(\Theta\) sur tout l'intervalle \(t\in[0,\sigma^2/2]\) d'intérêt est une question d'intégrabilité renvoyée à Q1b. »

Donc q1a délègue à q1b la preuve que la trajectoire reste dans \(\Theta^\star\). Si, pour établir cette permanence, q1b s'appuyait à son tour sur l'existence du flot construit en q1a, on aurait la boucle :

\[ \text{stabilité} \xrightarrow{\text{q1a }\Leftarrow} \text{flot }\theta_t \xrightarrow{\text{permanence ?}} \text{intégrabilité (q1b)} \xrightarrow{?} \text{stabilité}. \]

Diagnostic

La boucle est réelle uniquement si la seule voie vers \(\tilde\theta\) est le flot ODE. Elle se brise dès qu'on dispose d'une construction indépendante de \(\tilde\theta\) qui ne présuppose ni le flot ni la stabilité.

Contournement effectif — le cas quadratique

Dans le cas quadratique (et donc, par q1a Thm 5.1, dans tout le cas polynomial stable), une telle construction existe : la forme fermée Fourier (Q2.⋆) de q2 §3–4,

\[ \tilde M = M(I+\sigma^2 M)^{-1}, \qquad \tilde b = (I+\sigma^2 M)^{-1} b, \]

est obtenue directement en calculant \(\widehat{p_\theta\ast\gamma_\sigma}\) par transformée de Fourier + Woodbury. Aucun flot, aucune hypothèse de stabilité n'y entre. L'invariance \(\tilde M \succ 0\) (donc \(\tilde\theta\in\Theta^\star\), q1b Thm 2.4) est alors un fait géométrique pur sur le cône SPD — formellement vérifié en Lean 4 (tildeM_posDef, lean/EFS/EFS/Q2.lean), indépendant de toute la machinerie q1a.

La boucle est donc brisée : q1b prouve la permanence par la voie Fourier, pas par le flot q1a. Le flot q1a et la forme fermée q2 coïncident (la Riccati \(\dot M=-M^2\) a pour solution \(M(I+2tM)^{-1}\), q2 §6), mais la preuve d'invariance n'a besoin que de la seconde, autonome.

Résidu

La boucle ressurgirait pour une hypothétique famille non-polynomiale exotique satisfaisant \((\dagger)\) : là, pas de forme fermée Fourier, et l'invariance de \(\Theta^\star\) devrait se prouver via le critère de coercivité / sous-tangentialité de Nagumo (q1b Critère 2.6) — qui, lui, raisonne sur le champ \(A_k(\theta)\) issu de q1a. Mais :

1. Cette classe est conjecturalement vide (q1-exotique).
2. Le critère 2.6 utilise \(\log Z\) comme fonction de Lyapunov indépendante de la stabilité (convexité, Prop. 1.1) — il ne suppose pas le résultat cherché ; il énonce une condition (Nagumo) nécessaire et suffisante à vérifier, pas un acquis.

Donc même dans le résidu, il n'y a pas de tautologie masquée : il y a une condition ouverte explicite, pas une preuve circulaire.

Statut

Circularité neutralisée :

• cas quadratique / polynomial : brisée par la forme fermée Fourier (autonome, Lean-vérifiée) ;
• cas exotique : sans objet (classe conjecturalement vide), et réduit à un critère Nagumo explicite, non circulaire.

Cohérent avec circular-q1a-stability-vs-closure.md : la direction \((\Leftarrow)\) y était déjà identifiée comme la voie non-circulaire ; q1b la complète en fournissant la permanence dans \(\Theta^\star\) par voie indépendante.