Stability Framework for the Singularity of the Euler Equations on $\mathbb{R}^3$

Resumen Técnico: Marco de Estabilidad para la Singularidad de las Ecuaciones de Euler en $\mathbb{R}^3$

Planteamiento del Problema
El artículo aborda el problema abierto central en la dinámica de fluidos sobre si los datos iniciales suaves para las ecuaciones de Euler incompresibles en 3D pueden conducir a la formación de una singularidad en tiempo finito (explosión o blowup). Si bien se ha establecido la explosión en tiempo finito para las ecuaciones de Euler con fronteras o bajo condiciones iniciales no suaves, la existencia de una singularidad derivada de datos iniciales suaves en el dominio no acotado $\mathbb{R}^3$ sigue sin probarse. Una estrategia común para resolver esto es construir un perfil singular aproximado y demostrar su estabilidad no lineal. Los autores señalan que, si bien se descubrió un perfil de auto-similitud aproximado de alta precisión en un estudio numérico complementario utilizando Redes Neuronales Informadas por la Física (PINNs), no se había establecido una prueba rigurosa de estabilidad para este perfil en $\mathbb{R}^3$. El desafío específico radica en la falta de una propiedad de flujo de salida ("outgoing") global (que típicamente ayuda a la estabilidad) y en la presencia de puntos fijos no triviales en el flujo meridional que pueden causar la concentración de las perturbaciones.

Metodología
El artículo establece un marco riguroso para probar la estabilidad no lineal del perfil de auto-similitud aproximado descubierto en el estudio complementario. La metodología procede a través de las siguientes etapas:

1. Representación del Perfil Aproximado: El perfil descubierto numéricamente mediante PINN se convierte en una representación de splines polinomiales por partes. Esta forma analítica permite la diferenciación exacta y la evaluación rigurosa de residuos y normas utilizando aritmética de intervalos (vía la biblioteca Arb), asegurando que los errores numéricos estén acotados (por ejemplo, $O(10^{-5})$ en $L^2$).
2. Redimensionamiento Dinámico y Linealización: Los autores emplean una formulación de redimensionamiento dinámico donde la solución se visualiza en un marco móvil que se expande o contrae para mantener la singularidad en una escala fija. El perfil aproximado se convierte en un estado estacionario en este marco redimensionado. El análisis de estabilidad implica la linealización de las ecuaciones de Euler redimensionadas alrededor de este estado estacionario.
3. Variables de Escala Consistente: Para manejar los diferentes comportamientos de escala de la velocidad y la vorticidad, el análisis se formula utilizando variables de perturbación de escala consistente: la perturbación de la vorticidad $\delta\omega$ y el gradiente de la perturbación de la velocidad $\nabla \delta u$.
4. Modulación y Normalización: El marco introduce parámetros de modulación para fijar la traslación y la amplitud del perfil, eliminando efectivamente las direcciones neutras (modos de simetría) del análisis de estabilidad. Esto asegura que la cuestión de la estabilidad se refiera a perturbaciones genuinas transversales a estas simetrías.
5. Estimaciones de Energía Ponderada: El núcleo de la prueba reside en la construcción de un funcional de energía completo $E_k^2 = E_0^2 + \mu_k H_k^2$, que combina:
   • Energía ponderada de bajo orden ($E_0$): Utiliza funciones de peso singulares $\Phi_\omega, \Phi_r, \Phi_z$ adaptadas al perfil para establecer el amortiguamiento lineal.
   • Energía ponderada de alto orden ($H_k$): Utiliza pesos de orden superior para controlar las derivadas y los valores puntuales necesarios para cerrar las estimaciones no lineales.
6. Certificación Asistida por Computadora: La prueba reduce el problema de estabilidad de dimensión infinita a un problema de optimización de dimensión finita. Los autores derivan estimaciones analíticas explícitas para el amortiguamiento lineal, las interacciones no lineales y los residuos de la EDP. Estas estimaciones dependen de una gran colección de constantes explícitas (por ejemplo, límites de matrices, constantes de interpolación, normas de operadores elípticos). El marco requiere que estas constantes sean certificadas rigurosamente mediante aritmética de intervalos y límites de matrices certificados.
7. Formalización: El artículo menciona un esfuerzo paralelo (LeanPDE) para formalizar las derivaciones simbólicas y los pasos de la prueba en el demostrador de teoremas Lean, conectándolos con los cálculos numéricos certificados.

Contribuciones Clave

• Marco de Estabilidad: La contribución principal es la construcción de un marco detallado y modular para probar la estabilidad no lineal de un candidato a perfil de explosión de auto-similitud para las ecuaciones de Euler 3D en $\mathbb{R}^3$.
• Reducción a Verificación Finita: Los autores demuestran que la prueba de estabilidad puede reducirse a la certificación rigurosa de un conjunto finito de constantes y estimaciones explícitas. Esto desplaza la carga de la prueba del análisis cualitativo a la verificación cuantitativa.
• Manejo de Flujos No Salientes: El marco adapta con éxito las técnicas de estabilidad a un entorno sin una propiedad de salida global, utilizando una condición local más débil para alejar el flujo de los puntos fijos y empleando delicadas estimaciones de amortiguamiento de alto orden.
• Certificación Basada en Splines: El uso de splines polinomiales por partes para representar el perfil numérico permite la evaluación exacta de los residuos de la EDP y sus derivadas, un paso necesario para la certificación rigurosa de la aritmética de intervalos.
• Teorema de Estabilidad de Dos Radios: El artículo proporciona un teorema de estabilidad generalizado (Teorema 2) que permite límites separados para las energías de bajo y alto orden, ofreciendo flexibilidad en el proceso de certificación.

Resultados
El artículo no pretende haber completado la certificación numérica final de todas las constantes requeridas para cerrar la prueba. En su lugar, establece la arquitectura para tal prueba.

• Completitud Teórica: Los autores demuestran que, si las constantes explícitas (márgenes de amortiguamiento, límites no lineales, normas de residuos) pueden certificarse para satisfacer desigualdades específicas (por ejemplo, $\Lambda_{stab} > 0$), entonces el perfil de auto-similitud es no linealmente estable.
• Estabilidad Condicional: Condicionado a la certificación rigurosa de estas constantes, el marco garantiza que el perfil de auto-similitud es estable. Además, mediante el mecanismo de redimensionamiento dinámico, esta estabilidad implica la existencia de una solución admisible en las variables físicas originales que desarrolla una singularidad en tiempo finito.
• Límites de Residuos: El artículo reporta que la representación por splines del perfil satisface las ecuaciones del perfil de estado estacionario con residuos acotados por $O(10^{-5})$ en $L^2$ y $O(10^{-3})$ en $L^\infty$, comparable con los resultados originales de la PINN.

Significancia
El artículo sostiene que los obstáculos principales restantes para probar la explosión en tiempo finito para las ecuaciones de Euler 3D con datos iniciales suaves son ahora computacionales y cuantitativos en lugar de conceptuales. Al proporcionar un marco riguroso que reduce el problema a una colección finita de estimaciones verificables, los autores argumentan que el camino hacia una prueba completa es claro. El trabajo representa un paso crítico en el paradigma de la "prueba asistida por computadora" para las EDP, cerrando la brecha entre el descubrimiento numérico (PINNs) y la prueba matemática rigurosa. La significancia radica en demostrar que la estabilidad de un perfil singular complejo, descubierto numéricamente, puede someterse a un análisis sistemático y verificable, resolviendo potencialmente uno de los problemas del Premio Millennium, si las constantes restantes se certifican con éxito. El artículo enfatiza que la estructura modular del argumento permite refinamientos dirigidos (por ejemplo, agudizar estimaciones específicas o ajustar pesos) sin alterar el mecanismo de estabilidad subyacente.