Complex Bounded Operators in Isabelle/HOL

Com base no artigo fornecido, aqui está um resumo técnico detalhado da formalização de operadores limitados complexos no Isabelle/HOL.

Declaração do Problema

A motivação primária para este trabalho surge da formalização de linguagens de programação quântica e lógicas de Hoare quânticas. A literatura existente neste domínio frequentemente restringe, de forma implícita ou explícita, os resultados a sistemas de dimensão finita (ex: qubits) ou falha em distinguir rigorosamente entre espaços de Hilbert de dimensão finita e infinita. Ao lidar com variáveis infinitas (como inteiros quânticos), a matemática exige espaços de Hilbert de dimensão infinita, onde a intuição e os teoremas válidos para sistemas de dimensão finita (que dependem de matrizes) frequentemente falham ou requerem ajustes sutis em relação aos tipos de operadores (limitados vs. não limitados), topologias (norma do operador, forte, fraca, norma de traço, etc.) e convergência de somas infinitas.

Os autores observaram que muitos artigos na área definem conceitos como unitários, traços e produtos tensoriais sem especificar as restrições topológicas necessárias para dimensões infinitas, levando a potenciais erros matemáticos que são difíceis de verificar sem um conhecimento profundo de análise funcional. Além disso, as formalizações existentes no Isabelle/HOL (ex: por Li et al.) foram forçadas a restringir-se a variáveis finitas devido à falta de um background formalizado em análise complexa de dimensão infinita.

Metodologia

Os autores desenvolveram uma biblioteca abrangente dentro do provador de teoremas Isabelle/HOL, especificamente a sessão Complex_Bounded_Operators. A metodologia envolve:

1. Alinhamento Estrutural: A biblioteca espelha a estrutura das formalizações existentes do Isabelle/HOL para espaços vetoriais reais (encontradas em HOL-Analysis), criando teorias paralelas para espaços complexos (ex: Complex_Vector_Spaces, Complex_Inner_Product, Complex_Bounded_Linear_Function). Isso facilita a comparação e a futura portabilidade de resultados de vetores reais para o domínio complexo.
2. Abstração Baseada em Tipos: Em vez de depender apenas de predicados para funções lineares limitadas, os autores definem um tipo dedicado cblinfun (ou ⇒CL) para operadores limitados. Isso permite que operadores limitados sejam instanciados como um espaço vetorial normado e um espaço de Banach por direito próprio, simplificando a declaração de teoremas e permitindo o uso do sistema de classes de tipos do Isabelle para operadores.
3. Lidando com Dimensões Infinitas: A formalização aborda explicitamente espaços de dimensão infinita, definindo conceitos como subespaços fechados, complementos ortogonais e várias topologias de operadores (ex: topologia do operador forte). Ela distingue rigorosamente entre operadores limitados e não limitados e lida com a convergência de somas infinitas.
4. Geração de Código: Para o caso de dimensão finita, a biblioteca estabelece uma correspondência entre operadores lineares complexos limitados e matrizes formalizadas na entrada JNF (Forma Normal de Jordan) do AFP. Isso permite a geração de código, possibilitando que computações concretas sobre operadores e vetores de dimensão finita sejam executadas e verificadas.

Principais Contribuições

1. Espaços Vetoriais Complexos e Espaços com Produto Interno

• Espaços Vetoriais: Define espaços vetoriais complexos, espaços normados, espaços de Banach e álgebras como classes de tipos. Introduz conceitos de funções antilineares e sesquilineares.
• Espaços Conjugados: Introduz um tipo de "espaço conjugado" ('a conjugate_space) para transformar funções antilineares em funções lineares, permitindo o reuso de teoremas de funções lineares.
• Espaços de Hilbert: Formaliza espaços de Hilbert complexos, incluindo a existência de bases ortonormais (ONB), complementos ortogonais e o teorema da representação de Riesz.
• Espaços Unidimensionais: Define uma classe de tipo one_dim para espaços unidimensionais, fornecendo um isomorfismo canônico entre quaisquer dois desses espaços e os números complexos. Isso formaliza notações matemáticas comuns (ex: identificar $\psi^* \phi$ com o produto interno).

2. Operadores Lineares Complexos Limitados (cblinfun)

• Definição de Tipo: Introduz o tipo cblinfun para operadores lineares limitados entre espaços normados complexos.
• Propriedades de Operadores: Desenvolve a teoria de adjuntos, unitários, isometrias, isometrias parciais e projetores.
• Ordem de Loewner: Define a ordem de Loewner ($A \le B$) para operadores positivos. Isso exigiu um contorno técnico para lidar com a classe de tipo order para operadores não quadráticos usando uma "identidade heterogênea" e isomorfismos unitários.
• Operadores de Posto-1: Formaliza operadores "butterfly" ($|\psi\rangle\langle\phi|$) e prova suas propriedades, incluindo seu papel na construção de projetores e na cobertura do espaço de operadores compactos.
• Teoremas de Extensão: Fornece o teorema de Banach-Steinhaus e o teorema da Transformação Linear Limitada (BLT) para estender operadores limitados de subespaços densos para todo o espaço.

3. Funções Quadrado-Somáveis ($\ell^2$) e Matrizes

• Espaço $\ell^2$: Formaliza o espaço de Hilbert de funções quadrado-somáveis ('a ell2), estabelecendo-o como o espaço de Hilbert canônico para qualquer tipo de base 'a.
• Kets e Truncamento: Define vetores da base canônica ("kets") e uma operação de truncamento para aproximar vetores infinitos por vetores finitos, facilitando argumentos de limite.
• Correspondência de Matrizes: Para espaços de dimensão finita, estabelece um isomorfismo rigoroso entre cblinfun e matrizes JNF. Isso inclui o mapeamento de operações (adição, composição, adjunto, aplicação) entre o domínio do operador e o domínio da matriz.

4. Geração de Código

• Configura a geração de código para vetores, operadores e subespaços de dimensão finita ao envolver o código JNF existente.
• Representa subespaços como listas de vetores geradores (vetores JNF) e implementa operações como span, interseção e projeção usando ortogonalização de Gram-Schmidt.
• Permite que usuários verifiquem fatos sobre operadores concretos de dimensão finita através de computação explícita (ex: comandos value).

Resultados e Escopo

A biblioteca contém aproximadamente 18.758 linhas de código, 186 definições e 1.645 lemas provados.

• Completude: Cobre a teoria central de espaços de Hilbert complexos e operadores limitados necessária para formalizações de lógica quântica, incluindo o teorema da representação de Riesz, propriedades espectrais de projetores e a estrutura do reticulado de subespaços fechados (reticulado ortomodular completo).
• Limitações: A formalização é restrita a espaços vetoriais complexos. Embora muitos teoremas também se apliquem a espaços reais, os autores não criaram um framework genérico para cobrir ambos simultaneamente devido às limitações de classe de tipo do Isabelle/HOL em relação ao campo escalar. Consequentemente, algumas definições e provas tiveram que ser duplicadas ou adaptadas das bibliotecas de vetores reais existentes.
• Finito vs. Infinito: A biblioteca suporta tanto dimensões finitas quanto infinitas. No entanto, a geração de código é explicitamente limitada ao caso de dimensão finita, onde os operadores são isomórficos a matrizes.

Significância

O artigo afirma que esta formalização preenche uma lacuna crítica no ecossistema Isabelle/HOL, permitindo a verificação rigorosa de resultados em programação quântica e criptografia quântica que dependem de espaços de Hilbert de dimensão infinita.

• Verificação de Lógicas Quânticas: Serve como a fundação matemática para ferramentas como qrhl-tool e formalizações de referências quânticas, que anteriormente não podiam lidar com variáveis infinitas sem suposições matemáticas ad-hoc ou incompletas.
• Rigor Matemático: Ao lidar explicitamente com topologias, limitação e somas infinitas, a biblioteca evita os erros sutis encontrados na literatura informal, onde a intuição de dimensão finita é aplicada incorretamente a sistemas infinitos.
• Reutilização: A biblioteca foi desenhada para ser um recurso geral para análise funcional no Isabelle/HOL, não apenas para mecânica quântica. Os autores observam que, embora muitos resultados provavelmente existam em outras bibliotecas (como a mathlib do Lean), a integração específica com o sistema de tipos do Isabelle, geração de código e o tratamento explícito do caso complexo para operadores limitados fornece um recurso único e necessário para seus casos de uso específicos.

Os autores enfatizam que sua seleção de teoremas foi guiada pelas necessidades práticas de formalizar lógicas quânticas, garantindo que a biblioteca seja "bem arredondada" para esse domínio, permanecendo ao mesmo tempo uma contribuição significativa para a formalização da análise funcional em geral.