The continuous functional calculus in Lean

Resumo Técnico: O Cálculo Funcional Contínuo em Lean

Enunciado do Problema
O cálculo funcional contínuo é uma ferramenta fundamental na teoria das $C^*$-álgebras, permitindo a identificação de $C^*$-subálgebras comutativas com álgebras de funções contínuas em espaços de Hausdorff compactos. Embora matematicamente bem compreendido, sua formalização em assistentes de prova como o Lean apresenta desafios significativos. A dificuldade principal reside em equilibrar a fidelidade matemática com a usabilidade. Uma definição matematicamente "natural" frequentemente recorre a tipos dependentes (ex: funções definidas apenas no espectro de um elemento) e estruturas agrupadas (bundled structures, ex: aplicações contínuas como um tipo específico). Embora estes sejam rigorosos, eles criam fricção em provas formais: reescrever igualdades torna-se difícil porque os tipos dependem de elementos específicos, e compor funções exige gerenciar coerções de subtipos complexos e provas de continuidade. Os autores identificaram que um design que prioriza a simplicidade matemática estrita frequentemente falha nos "testes de litígio" de usabilidade prática exigidos por uma biblioteca como a Mathlib.

Metodologia e Decisões de Design
Os autores desenvolveram uma formalização do cálculo funcional contínuo em Lean 4, integrada à biblioteca Mathlib. Sua metodologia envolveu um processo de design iterativo, movendo-se de uma definição matematicamente "pura" para uma interface "utilitária". As principais decisões de design incluem:

1. Desagrupamento e "Valores Lixo" (Junk Values):
   Em vez de definir o cálculo funcional como um mapa do tipo de funções contínuas no espectro $C(\sigma(a), \mathbb{C})$ para a álgebra, os autores definiram uma função cfc que aceita qualquer função $f: \mathbb{C} \to \mathbb{C}$ e qualquer elemento $a$. Se $a$ não for normal ou $f$ não for contínua no espectro, a função retorna um "valor lixo" (tipicamente 0).

   • Racional: Isso permite que os usuários escrevam expressões como $f(a)$ sem primeiro provar que $a$ é normal ou que $f$ é contínua. Isso mimetiza a abordagem "escreva primeiro, pense depois" da matemática informal, adiando o ônus da prova até que uma propriedade não trivial seja necessária. Isso também permite a reescrita (rewriting) fluida (rw), pois os tipos dos argumentos não dependem mais das propriedades específicas de $a$.

2. Abstração Baseada em Classes:
   Para lidar com diferentes anéis escalares ($\mathbb{C}$, $\mathbb{R}$ e $\mathbb{R}_{\ge 0}$) e diferentes tipos de elementos (normais, autoadjuntos, não-negativos), os autores implementaram o cálculo como uma classe de tipo ContinuousFunctionalCalculus.

   • Generalização de Predicados: A classe é parametrizada por um predicado $p$ nos elementos da álgebra (ex: IsStarNormal, IsSelfAdjoint, 0 ≤ a). Isso permite que uma única interface cubra vários casos sem duplicação de código.
   • Prop-Valued vs. Data: Versões anteriores incluíam o $*$-homomorfismo como dado. No entanto, para evitar problemas de igualdade definicional (onde duas construções diferentes do mesmo mapa podem não ser definicionalmente iguais), o design final torna a classe um Prop. Ela afirma a existência de um $*$-homomorfismo único com propriedades específicas, em vez de armazenar o mapa em si.

3. Lidando com Álgebras Não-Unitárias:
   A formalização estende-se a $C^*$-álgebras não-unitárias. Em vez de depender de construções extrínsecas como a unitização mínima para cada definição, os autores introduziram uma definição intrínseca do quasespectro. O cálculo funcional não-unitário é definido sobre funções que se anulam em 0 (ou mapeiam 0 para 0), evitando a necessidade de alternar constantemente entre contextos unitários e não-unitários.

4. Automação via autoParam:
   Para mitigar a verbosidade de passar provas de continuidade e normalidade manualmente, os autores utilizaram o recurso autoParam do Lean. Hipóteses como "f é contínua no espectro" são equipadas com táticas padrão. Se o usuário não fornecer uma prova, o Lean tenta sintetizá-la automaticamente usando lemas existentes (ex: aesop, fun_prop).

5. Unicidade como uma Classe Separada:
   A propriedade de composição ($g(f(a)) = (g \circ f)(a)$) é central para a teoria. Os autores provaram isso usando um argumento de unicidade em vez do teorema de Stone–Weierstrass (que falha para $\mathbb{R}_{\ge 0}$). Eles encapsularam a unicidade de $*$-homomorfismos em uma classe separada ContinuousMap.UniqueHom, permitindo que a propriedade de composição seja derivada genericamente através de diferentes anéis escalares.

Principais Contribuições e Resultados

• Primeira Formalização: Este trabalho constitui a primeira formalização do cálculo funcional contínuo em qualquer assistente de prova.
• Integração com Mathlib: A implementação foi fundida à Mathlib, fornecendo uma interface unificada para cálculos funcionais complexos, reais e de reais não-negativos.
• Verificação de Usabilidade: O design foi validado contra testes de litígio específicos, incluindo:
  • Definir inversos ($f(a^{-1})$) usando funções que não são contínuas em todo lugar (ex: $x \mapsto x^{-1}$).
  • Construir partes positivas/negativas e raízes quadradas para elementos autoadjuntos e não-negativos.
  • Aplicar o cálculo a matrizes sobre $\mathbb{R}$ (que carecem de uma estrutura métrica global na Mathlib).
• Automação: A interface suporta automação de alto nível, permitindo que usuários provem propriedades como $f(-a) = (x \mapsto f(-x))(a)$ com intervenção manual mínima.
• Aplicações: A interface já foi utilizada para formalizar resultados avançados, incluindo:
  • A existência de unidades aproximadas em $C^*$-álgebras não-unitárias.
  • A continuidade do cálculo funcional em ambas as variáveis.
  • Propriedades de mapas $a \mapsto |a|$, $a \mapsto a^p$ e $a \mapsto \log(a)$.
  • Resultados relativos a elementos unitários e projeções.

Significância e Limitações
O artigo reivindica significância principalmente em seu filosofia de design: demonstrar que, para uma ferramenta ser eficaz em uma grande biblioteca formal, ela deve priorizar a ergonomia do usuário final (usabilidade) sobre a pureza matemática estrita na definição. Ao aceitar "valores lixo" e desagrupar tipos, os autores criaram uma interface que se comporta intuitivamente para matemáticos, permitindo manipulações complexas (como composição e reescrita) que seriam proibitivamente difíceis com uma abordagem de tipo dependente estrita.

Os autores são modestos quanto ao estado atual, reconhecendo algumas limitações:

• Lemas de simp: Devido à necessidade de argumentos explícitos para acionar o autoParam, muitos lemas não podem ser usados como regras de simp sem intervenção manual, tornando algumas provas mais verbosas do que o desejado.
• Complicações de $\mathbb{R}_{\ge 0}$: O uso dos reais não-negativos como um anel escalar introduz obstáculos técnicos específicos (ex: subtração truncada, falta de estrutura de anel) que requerem declarações de teoremas separadas.
• $C^*$-álgebras Reais: Embora o framework seja projetado para suportar $C^*$-álgebras reais, o caso específico do cálculo funcional sobre $\mathbb{C}$ para álgebras reais (que requer um domínio de funções diferente) ainda não está totalmente integrado e está planejado para trabalhos futuros.

Em conclusão, o artigo documenta uma tradução bem-sucedida de uma profunda teoria de álgebra de operadores para um sistema formal utilizável, destacando os compromissos entre elegância matemática e utilidade prática no contexto da prova de teoremas interativa.