Proving Properties of $φ$-Representations with the Walnut Theorem-Prover

Este artigo apresenta uma nova abordagem computacional para provar o teorema de Frougny e Sakarovitch sobre representações $\phi$, permitindo obter demonstrações simples e uniformes de resultados existentes e novos, incluindo a recuperação automática de trabalhos recentes de Dekking e Van Loon, utilizando o provador de teoremas Walnut.

O essencial

Imagine que você tem uma régua mágica para medir números. A maioria de nós usa a régua decimal (base 10), onde os números são feitos de 0 a 9. Mas e se a sua régua fosse feita de um número especial chamado Phi ($\phi$), que é a "Proporção Áurea" (aquele número mágico que aparece em conchas, girassóis e na arte, aproximadamente 1,618)?

Este artigo, escrito por Jeffrey Shallit, é como um manual de instruções para usar uma máquina de raciocínio automática (chamada "Walnut") para descobrir segredos sobre como os números se comportam nessa régua especial.

Aqui está a explicação do que o autor fez, usando analogias do dia a dia:

1. O Problema: A "Tradução" de Números

Imagine que você quer escrever o número 2.

• Na nossa régua normal (decimal), é fácil: 2.
• Na régua Phi, é mais estranho. O número 2 pode ser escrito como 10.01 (onde o ponto é a vírgula).
• Mas o problema é que existem muitas maneiras de escrever o mesmo número na régua Phi. É como ter várias receitas diferentes para fazer o mesmo bolo. O autor foca na "receita oficial" (chamada de representação canônica), que segue regras estritas para não ter repetições estranhas.

2. A Ferramenta: O "Walnut" (O Detetive Automático)

O autor não fez os cálculos à mão (o que seria como tentar contar cada grão de areia de uma praia). Em vez disso, ele usou um software chamado Walnut.

• A Analogia: Pense no Walnut como um robô detetive superinteligente. Você não precisa dizer a ele como resolver o problema passo a passo. Você apenas lhe dá as regras do jogo (em linguagem lógica) e pergunta: "Existe alguma maneira de quebrar essa regra?" ou "Quantas vezes isso acontece?".
• O robô então constrói um mapa de labirinto (um autômato) que mostra todas as soluções possíveis. Se o labirinto tem um caminho, a resposta é "Sim". Se não tem, é "Não".

3. O Grande Truque: O "Dobrador" de Números

O artigo revisita uma descoberta antiga de dois matemáticos (Frougny e Sakarovitch). Eles descobriram que, para entender os números na régua Phi, é melhor "dobrá-los" de uma maneira específica.

• A Analogia: Imagine que você tem uma fita métrica longa. Em vez de olhar para ela reta, você a dobra ao meio. Agora, o início da fita e o fim da fita estão lado a lado.
• O autor mostra como usar o robô Walnut para construir esse "dobrador" automaticamente. Isso transforma um problema matemático difícil em algo que o computador pode verificar em segundos.

4. O Que Eles Descobriram (As Recompensas)

Com esse novo "mapa de labirinto" em mãos, o autor conseguiu provar coisas que antes exigiam anos de trabalho manual e induções matemáticas complexas. Ele fez isso de forma "automática":

• Padrões Ocultos: Ele mostrou que os números de Fibonacci (aqueles onde cada número é a soma dos dois anteriores: 1, 1, 2, 3, 5, 8...) têm um padrão muito bonito e previsível quando escritos na régua Phi. O robô desenhou o mapa e mostrou que o padrão se repete a cada 4 números, como um ciclo de estações do ano.
• Contando "Bolos": Ele conseguiu contar quantas maneiras diferentes existem de escrever um número na régua Phi sem quebrar certas regras (chamadas expansões Knott). Antes, isso era um pesadelo de cálculo; com o robô, foi como contar quantas peças de Lego cabem em uma caixa.
• Palíndromos Numéricos: Ele descobriu quais números, quando escritos na régua Phi, são palíndromos (leem-se igual de trás para frente, como "101"). O robô listou todos eles.
• Novas Descobertas: O autor não só reprovou o que já sabíamos, mas encontrou novas sequências de números que ninguém tinha notado antes, como se estivesse explorando um novo continente usando um GPS.

5. Por que isso é importante?

Antes, provar essas coisas era como tentar escalar uma montanha usando apenas as mãos e os pés (indução matemática). Era difícil, lento e propenso a erros.
Com o método do autor, é como se você tivesse um elevador que leva você direto ao topo.

• Simplicidade: Ele mostra que problemas que pareciam complicados são, na verdade, apenas questões de lógica que um computador pode resolver se você souber fazer a pergunta certa.
• Universalidade: A técnica pode ser usada para outros tipos de "réguas" matemáticas, não apenas para a Phi.

Resumo Final

Jeffrey Shallit pegou uma ideia matemática antiga e complexa sobre como escrever números usando a Proporção Áurea e a submeteu a um "detetive de computador" (Walnut). O resultado foi que o computador desenhou mapas (autômatos) que provaram teoremas antigos em segundos e descobriram novos segredos matemáticos, tudo sem precisar de longas e chatas provas manuais. É como trocar uma escada de corda por um elevador de vidro: você vê a mesma paisagem, mas chega lá muito mais rápido e com uma visão mais clara.

Resumo técnico

Aqui está um resumo técnico detalhado do artigo "Proving Properties of φ-Representations with the Walnut Theorem-Prover", de Jeffrey Shallit, apresentado em português.

1. Problema e Contexto

O artigo aborda a representação de números reais não negativos na base $\phi$ (a razão áurea, $\phi = \frac{1+\sqrt{5}}{2}$), conhecida como expansão $\phi$ ou representação de Bergman. Neste sistema, um número $z$ é expresso como uma soma de potências de $\phi$ com coeficientes binários ($0$ou$1$):
$$z = \sum a_i \phi^i$$
A representação canônica é única se impusermos a restrição de que não há dois "1"s consecutivos (sem o bloco "11") e certas condições sobre expansões infinitas.

O problema central investigado é a complexidade de provar propriedades sobre essas representações e sobre variantes específicas (como expansões de Knott, expansões "naturais" e expansões DVL). Trabalhos anteriores, notadamente de Frougny e Sakarovitch (2012), estabeleceram que existe um autômato finito que computa a representação $\phi$ de inteiros não negativos, mas a construção explícita e a aplicação desse autômato para provar teoremas eram consideradas desafiadoras e pouco diretas. O objetivo do artigo é demonstrar como automatizar a descoberta e prova de teoremas sobre essas representações, recuperando resultados existentes e gerando novos de forma sistemática.

2. Metodologia

A metodologia do artigo baseia-se inteiramente no uso do Walnut, um provador de teoremas de software livre desenvolvido por Hamoon Mousavi. O Walnut utiliza procedimentos de decisão para extensões da Aritmética de Presburger e lógica de primeira ordem para analisar sequências automáticas.

Os passos metodológicos principais são:

1. Construção de Autômatos Auxiliares: O autor define componentes básicos em Walnut para manipular representações numéricas:
   • Normalizadores: Autômatos que convertem strings binárias arbitrárias para suas representações canônicas em sistemas Zeckendorf (inteiros positivos) e negaFibonacci (inteiros negativos).
   • Deslocadores (Shifters): Autômatos para deslocar bits à esquerda ou à direita.
   • Conversores: Autômatos para converter entre representações negaFibonacci e Zeckendorf.
2. Reconstrução do Autômato de Frougny-Sakarovitch: Utilizando as equações algébricas que relacionam potências de $\phi$ com números de Fibonacci ($\phi^k = F_k\phi + F_{k-1}$), o autor codifica em lógica de primeira ordem as condições para que uma string $x.y$ seja a representação $\phi$ de um inteiro $n$. O Walnut gera automaticamente o autômato finito que aceita exatamente os triplets $(n, x, y)$ onde $n = [x.y]_\phi$.
3. Interseção e Restrição: Para estudar variantes (como expansões canônicas, expansões de Knott, etc.), o autor intersecciona o autômato principal com outros autômatos que impõem restrições específicas (ex: ausência de "11", condições de comprimento, padrões de palíndromos).
4. Análise de Propriedades: Uma vez construído o autômato, o Walnut é usado para:
   • Provar teoremas verificando a validade de fórmulas lógicas sobre os estados do autômato.
   • Calcular representações lineares (linear representations) para funções de contagem (ex: número de expansões possíveis, soma de dígitos).
   • Determinar sequências automáticas e seus autômatos mínimos.

3. Contribuições e Resultados Principais

O artigo apresenta uma série de resultados, divididos entre a reprodutibilidade de trabalhos anteriores e a descoberta de novos teoremas:

• Construção Explícita do Autômato: O autor fornece o código Walnut e a estrutura do autômato de Frougny-Sakarovitch (com 116 estados na versão geral e 39 na versão canônica), tornando acessível uma ferramenta que antes era apenas teórica e difícil de implementar.
• Caracterização de Representações de Números de Fibonacci e Lucas: O autor prova e visualiza as representações $\phi$ canônicas para $F_n$ e $L_n$, confirmando e generalizando resultados de Frougny-Sakarovitch e Dekking-Van Loon.
• Soma de Dígitos e Conjectura de Gerdemann:
  • É provada a conjectura de Dale Gerdemann (2012): a soma dos dígitos na representação Zeckendorf de $n$ é sempre menor ou igual à soma dos dígitos na representação $\phi$ canônica de $n$. A prova é feita computacionalmente, analisando os pesos das arestas no grafo de transição do autômato.
  • São geradas representações lineares para a soma de dígitos das partes esquerda e direita da expansão.
• Novas Sequências e Propriedades de Bits:
  • Caracterização dos bits individuais $d_i(n)$ da expansão $\phi$.
  • Conexão surpreendente entre o bit $d_{-1}(n)$ e o número de representações de Lucas distintas de $n$.
  • Análise de "corridas verticais" (vertical runs) de 1s, provando que seus comprimentos seguem padrões regulares relacionados aos números de Lucas, contradizendo afirmações anteriores de que não haveria regularidade.
• Palíndromos e Antipalíndromos:
  • Construção de autômatos que aceitam inteiros $n$ cujas representações $\phi$ são palíndromos (canônicos e não canônicos) ou antipalíndromos.
  • Geração de novas sequências no OEIS (On-Line Encyclopedia of Integer Sequences) baseadas nessas propriedades.
• Expansões de Knott e "Naturais":
  • Recuperação automática e simplificada dos resultados de Dekking e Van Loon sobre o número de expansões de Knott (expansões que não terminam em "011").
  • Derivação de fórmulas fechadas e comportamentos assintóticos para o número médio de expansões de Knott em intervalos de Fibonacci.
• Expansões DVL e Inteiros Algébricos:
  • Generalização para expansões DVL (uma variante "canônica" definida por Dekking-Van Loon) e para inteiros algébricos na forma $m\phi + n$, construindo autômatos que lidam com coeficientes negativos via representação negaFibonacci.

4. Significância

A significância deste trabalho reside em três pilares principais:

1. Mudança de Paradigma na Prova Matemática: O artigo demonstra que problemas complexos de teoria dos números e combinatória, que tradicionalmente exigiam induções longas e argumentos ad-hoc, podem ser resolvidos de forma "automática", uniforme e sem erros através de procedimentos de decisão em lógica de primeira ordem.
2. Acessibilidade e Reprodutibilidade: Ao fornecer o código Walnut e os autômatos explícitos, o autor torna as ferramentas de Frougny-Sakarovitch acessíveis a outros pesquisadores, permitindo a exploração sistemática de novas propriedades das representações $\phi$.
3. Descoberta de Novos Resultados: A abordagem computacional permitiu não apenas reprová-los, mas descobrir novas sequências, conjecturas e teoremas (como a relação entre bits específicos e representações de Lucas, e a regularidade das corridas verticais) que não eram óbvios através de métodos analíticos tradicionais.

Em resumo, o artigo estabelece um novo padrão para a investigação de representações numéricas em bases irracionais, mostrando que a automação via provadores de teoremas é uma ferramenta poderosa e indispensável para a pesquisa moderna em teoria dos números e sistemas formais.