The continuous functional calculus in Lean

Resumen Técnico: El Cálculo Funcional Continuo en Lean

Planteamiento del Problema
El cálculo funcional continuo es una herramienta fundamental en la teoría de las $C^*$-álgebras, que permite la identificación de subálgebras $C^*$ conmutativas con álgebras de funciones continuas sobre espacios de Hausdorff compactos. Aunque está matemáticamente bien comprendido, su formalización en asistentes de pruebas como Lean presenta desafíos significativos. La dificultad principal radica en equilibrar la fidelidad matemática con la usabilidad. Una definición matemáticamente "natural" suele depender de tipos dependientes (por ejemplo, funciones definidas solo en el espectro de un elemento) y estructuras empaquetadas (por ejemplo, aplicaciones continuas como un tipo específico). Si bien estos son rigurosos, crean fricción en las pruebas formales: la reescritura de igualdades se vuelve difícil porque los tipos dependen de elementos específicos, y la composición de funciones requiere gestionar complejas coerciones de subtipos y pruebas de continuidad. Los autores identificaron que un diseño que prioriza la simplicidad matemática estricta suele fallar en las "pruebas de fuego" de la usabilidad práctica requeridas para una biblioteca como Mathlib.

Metodología y Decisiones de Diseño
Los autores desarrollaron una formalización del cálculo funcional continuo en Lean 4, integrada en la biblioteca Mathlib. Su metodología implicó un proceso de diseño iterativo, pasando de una definición matemáticamente "pura" a una interfaz "utilitaria". Las decisiones clave de diseño incluyen:

1. Desempaquetado y "Valores Basura" (Junk Values):
   En lugar de definir el cálculo funcional como un mapa desde el tipo de funciones continuas en el espectro $C(\sigma(a), \mathbb{C})$ hacia el álgebra, los autores definieron una función cfc que acepta cualquier función $f: \mathbb{C} \to \mathbb{C}$ y cualquier elemento $a$. Si $a$ no es normal o $f$ no es continua en el espectro, la función devuelve un "valor basura" (típicamente 0).

   • Racional: Esto permite a los usuarios escribir expresiones como $f(a)$ sin tener primero que probar que $a$ es normal o que $f$ es continua en el espectro. Esto imita el enfoque de "escribir primero, pensar después" de la matemática informal, retrasando la carga de la prueba hasta que se necesita una propiedad no trivial. Esto también permite una reescritura (rw) fluida porque los tipos de los argumentos ya no dependen de las propiedades específicas de $a$.

2. Abstracción Basada en Clases:
   Para manejar diferentes anillos escalares ($\mathbb{C}$, $\mathbb{R}$, y $\mathbb{R}_{\ge 0}$) y diferentes tipos de elementos (normales, autoadjuntos, no negativos), los autores implementaron el cálculo como una clase de tipo ContinuousFunctionalCalculus.

   • Generalización de Predicados: La clase está parametrizada por un predicado $p$ sobre los elementos del álgebra (por ejemplo, IsStarNormal, IsSelfAdjoint, 0 ≤ a). Esto permite que una única interfaz cubra varios casos sin duplicación de código.
   • Prop-Valued vs. Data: Las versiones tempranas incluían el $*$-homomorfismo como datos. Sin embargo, para evitar problemas con la igualdad definicional (donde dos construcciones distintas del mismo mapa podrían no ser definicionalmente iguales), el diseño final hace que la clase sea un Prop. Este afirma la existencia de un $*$-homomorfismo único con propiedades específicas, en lugar de almacenar el mapa en sí.

3. Manejo de Álgebras No Unitarias:
   La formalización se extiende a $C^*$-álgebras no unitarias. En lugar de depender de construcciones extrínsecas como la unitarización mínima para cada definición, los autores introdujeron una definición intrínseca del cuasiespectro. El cálculo funcional no unitario se define sobre funciones que se anulan en 0 (o que mapean 0 a 0), evitando la necesidad de cambiar constantemente entre contextos unitarios y no unitarios.

4. Automatización vía autoParam:
   Para mitigar la verbosidad de pasar pruebas de continuidad y normalidad manualmente, los autores utilizaron la característica autoParam de Lean. Las hipótesis como "$f$ es continua en el espectro" están equipadas con tácticas por defecto. Si el usuario no proporciona una prueba, Lean intenta sintetizarla automáticamente utilizando lemas existentes (por ejemplo, aesop, fun_prop).

5. Unicidad como una Clase Separada:
   La propiedad de composición ($g(f(a)) = (g \circ f)(a)$) es central en la teoría. Los autores demostraron esto utilizando un argumento de unicidad en lugar del teorema de Stone–Weierstrass (que falla para $\mathbb{R}_{\ge 0}$). Encapsularon la unicidad de los $*$-homomorfismos en una clase separada ContinuousMap.UniqueHom, permitiendo que la propiedad de composición se derive genéricamente a través de diferentes anillos escalares.

Contribuciones Clave y Resultados

• Primera Formalización: Este trabajo constituye la primera formalización del cálculo funcional continuo en cualquier asistente de pruebas.
• Integración en Mathlib: La implementación se ha fusionado en Mathlib, proporcionando una interfaz unificada para los cálculos funcionales complejos, reales y de reales no negativos.
• Verificación de Usabilidad: El diseño fue validado mediante pruebas de fuego específicas, incluyendo:
  • Definir inversos ($f(a^{-1})$) usando funciones que no son continuas en todas partes (por ejemplo, $x \mapsto x^{-1}$).
  • Construir partes positivas/negativas y raíces cuadradas para elementos autoadjuntos y no negativos.
  • Aplicar el cálculo a matrices sobre $\mathbb{R}$ (que carecen de una estructura métrica global en Mathlib).
• Automatización: La interfaz soporta automatización de alto nivel, permitiendo a los usuarios probar propiedades como $f(-a) = (x \mapsto f(-x))(a)$ con una intervención manual mínima.
• Aplicaciones: La interfaz ya ha sido utilizada para formalizar resultados avanzados, incluyendo:
  • La existencia de unidades aproximadas en $C^*$-álgebras no unitarias.
  • La continuidad del cálculo funcional en ambas variables.
  • Propiedades de los mapas $a \mapsto |a|$, $a \mapsto a^p$, y $a \mapsto \log(a)$.
  • Resultados relativos a elementos unitarios y proyecciones.

Significado y Limitaciones
El artículo reclama su importancia principalmente en su filosofía de diseño: demostrar que para que una herramienta sea efectiva en una biblioteca formal de gran escala, debe priorizar la ergonomía del usuario final (usabilidad) sobre la pureza matemática estricta en la definición. Al aceptar "valores basura" y desempacar tipos, los autores crearon una interfaz que se comporta intuitivamente para los matemáticos, permitiendo manipulaciones complejas (como la composición y la reescritura) que serían prohibitivamente difíciles con un enfoque de tipos dependientes estrictos.

Los autores son modestos sobre el estado actual, reconociendo también algunas limitaciones:

• Lemas de Simp: Debido a la necesidad de argumentos explícitos para activar autoParam, muchos lemas no pueden usarse como reglas de simp sin intervención manual, lo que hace que algunas pruebas sean más verbosas de lo deseado.
• Complicaciones de $\mathbb{R}_{\ge 0}$: El uso de los reales no negativos como anillo escalar introduce obstáculos técnicos específicos (por ejemplo, resta truncada, falta de estructura de anillo) que requieren enunciados de teoremas separados.
• $C^*$-álgebras Reales: Aunque el marco está diseñado para soportar $C^*$-álgebras reales, el caso específico del cálculo funcional sobre $\mathbb{C}$ para álgebras reales (que requiere un dominio de funciones diferente) aún no está totalmente integrado y se planea para trabajos futuros.

En conclusión, el artículo documenta una traducción exitosa de una profunda teoría de álgebras de operadores a un sistema formal utilizable, destacando los compromisos entre la elegancia matemática y la utilidad práctica en el contexto de la demostración de teoremas interactiva.