Formalizing the Real Numbers in Homotopy Type Theory with Cubical Agda

1. Declaração do Problema

A matemática construtiva visa fornecer interpretações computacionais para provas matemáticas, mas a construção dos números reais ($\mathbb{R}$) historicamente exigiu compromissos significativos:

• Construção Clássica de Cauchy: Requer o Axioma da Escolha Enumerável para selecionar representantes de classes de equivalência de sequências de Cauchy a fim de provar a completude de Cauchy. Isso é não-construtivo.
• Construção de Setoides de Bishop: Evita a escolha ao trabalhar com sequências de Cauchy equipadas com uma relação de equivalência explícita (setoides). No entanto, isso introduz uma sobrecarga de contabilidade persistente, exigindo provas de congruência explícitas para cada operação e teorema, o que complica as estruturas algébricas.
• Cortes de Dedekind: Na teoria dos tipos preditiva, os cortes de Dedekind exigem o rastreamento de níveis de universo (os reais vivem um nível acima de seus cortes), tornando os desenvolvimentos trabalhosos.

O Livro HoTT (Teoria dos Tipos de Homotopia) propõe uma solução: definir os números reais como um Tipo Indutivo-Indutivo Superior (HIIT). Esta construção evita a escolha, elimina a sobrecarga de setoides ao identificar reais $\epsilon$-próximos via construtores de caminhos e evita o rastreamento de níveis de universo. No entanto, formalizações anteriores (por exemplo, por Gilbert em Rocq) estavam incompletas porque os assistentes de prova careciam de suporte nativo para HIITs, forçando o autor a postular os construtores de caminhos e suas regras de computação em vez de derivá-los.

2. Metodologia

A tese apresenta uma formalização completa e verificada por máquina dos reais do livro HoTT usando Cubical Agda, um assistente de prova baseado na Teoria dos Tipos Cúbica.

• Suporte Nativo: O Cubical Agda suporta nativamente Tipos Indutivos Superiores (HITs) e definições Indutivas-Indutivas. Isso permite que o autor defina os reais e a relação de proximidade simultaneamente sem postulados, garantindo que os construtores de caminhos tenham regras de computação nativas.
• Escopo da Formalização: O trabalho formaliza mais de 13.000 linhas de código, cobrindo:
  1. A definição HIIT de $\mathbb{R}$ e a relação de proximidade ($\sim_\epsilon$).
  2. Princípios de indução e recursão.
  3. Propriedades da relação de proximidade (reflexividade, simetria, desigualdade triangular, arredondamento).
  4. Princípios de extensão para aplicações de Lipschitz e não expansivas.
  5. A construção de operações algébricas (adição, negação, min/max, multiplicação, recíproco).
  6. Teoria da ordem (desigualdades estritas/não estritas, apartamento).
  7. A prova de que $\mathbb{R}$ forma um corpo ordenado arquimediano.
• Ferramentas: O autor utilizou o Claude Code (agente de IA da Anthropic) para auxiliar na navegação pela grande biblioteca padrão do Cubical Agda e na conversão de esboços de prova informais em termos formais de Agda, acelerando significativamente o desenvolvimento de provas complexas, como a construção do recíproco.

3. Contribuições Principais

A. A Primeira Formalização Completa dos Reais HoTT

Esta é a primeira formalização dos reais do livro HoTT que não depende de postulados. Tentativas anteriores tiveram que assumir a existência de construtores de caminhos; este trabalho os deriva diretamente da teoria dos tipos do Cubical Agda, garantindo que todas as regras de computação se mantenham definicionalmente.

B. Resolução de Lacunas de Formalização

O processo de formalização revelou questões sutis na apresentação informal do livro HoTT que exigiram refinamento matemático:

• Relação de Proximidade Alternativa: A definição indutiva de proximidade ($\sim$) fornece condições suficientes, mas não necessárias, para extrair testemunhas. A formalização constrói rigorosamente uma relação auxiliar ($\approx$) que computa sobre construtores e prova $\sim \iff \approx$, permitindo análise de caso sobre hipóteses de proximidade.
• Princípio de Recursão Aprimorado: A notação do texto informal para o princípio de recursão assumia tacitamente o acesso à aproximação do domínio ($x_\epsilon$) dentro da hipótese indutiva. A formalização exigiu reformular explicitamente o princípio de recursão para carregar tanto a aproximação quanto a atribuição do codomínio, um detalhe perdido em transcrições iniciais ingênuas.
• Continuidade Multivariável: O livro HoTT implica que a continuidade separada é suficiente para estender identidades para múltiplas variáveis. A formalização provou isso explicitamente (Lema 2.3.4), mostrando que a continuidade separada é suficiente para estender identidades binárias e ternárias de $\mathbb{Q}$ para $\mathbb{R}$.

C. Construção de Multiplicação e Recíproco

Multiplicação e recíproco não são globalmente Lipschitz, portanto não podem ser definidos via princípios de extensão simples. A tese adota a estratégia local-para-global de Gilbert:

1. Definir operações em domínios restritos onde existem limites de Lipschitz (por exemplo, fixando um limite em um fator).
2. Provar que essas definições locais concordam nas sobreposições.
3. Usar o Teorema de Kraus (aplicações de truncamentos proposicionais para conjuntos) para eliminar a dependência do limite específico, resultando em uma definição global.
   Esta abordagem foi implementada usando o módulo SetElim da biblioteca padrão do Cubical Agda.

D. Eficiência Computacional

Diferentemente da construção de quociente clássica no Lean (onde $2+2=4$ em reais não é verdade definicionalmente), a construção HoTT no Cubical Agda permite que a aritmética em entradas racionais compute definicionalmente. Por exemplo, rational(2) + rational(2) = rational(4) reduz-se a refl (reflexividade) diretamente no verificador de tipos.

4. Resultados

• Corpo Ordenado Arquimediano: A formalização prova com sucesso que o tipo construído $\mathbb{R}$ satisfaz todos os axiomas de um corpo ordenado arquimediano, incluindo a existência de inversos para elementos apartados de zero.
• Disponibilidade do Código: Toda a base de código (aproximadamente 13.500 linhas) é de código aberto e verifica tipos sem lacunas ou postulados usando a mais recente biblioteca padrão do Cubical Agda.
• Desenvolvimento Assistido por IA: A tese demonstra a eficácia do uso de agentes de codificação baseados em LLM para matemática formal, especificamente para navegar em grandes bibliotecas e traduzir estratégias de prova de alto nível em termos de tipos dependentes de baixo nível.

5. Significado

• Fundamental para Análise Construtiva: Este trabalho fornece uma base robusta e verificada por máquina para a análise construtiva dentro do programa Fundamentos Univalentes. Remove o fardo de "contabilidade" dos setoides e o fardo de "escolha" dos quocientes clássicos.
• Evolução do Assistente de Prova: Valida o Cubical Agda como um ambiente superior para matemática baseada em HIIT em comparação com sistemas como Rocq (Coq) que carecem de suporte nativo a HITs.
• Trabalho Futuro: A formalização prepara o terreno para estender a análise construtiva a estruturas mais complexas (por exemplo, integração de Riemann, equações diferenciais) e generalizar conceitos como localizadores (estruturas que permitem computação em reais) para espaços métricos mais amplos.
• Insight Metodológico: A tese destaca que a formalização não é meramente um exercício de verificação, mas uma atividade matemática que pode revelar pressupostos implícitos e refinar teoremas de maneiras que a leitura informal sozinha não consegue.

Em resumo, a tese de Jackson Brough preenche a lacuna entre a elegância teórica dos números reais do livro HoTT e a matemática prática e executável, fornecendo uma base verificada, computacionalmente eficiente e livre de postulados para a análise real na teoria dos tipos.