Dead ends in square-free digit walks

Resumo Técnico: Pontos de Parada em Caminhadas de Dígitos Livres de Quadrados

Enunciado do Problema
O artigo investiga a existência e a densidade de "pontos de parada" (dead ends) em caminhadas de dígitos livres de quadrados. Uma caminhada livre de quadrados na base $b$ começa com um número inteiro livre de quadrados $N_0$ e tenta construir uma sequência infinita $N_0, N_1, N_2, \dots$ onde cada termo subsequente é formado pela anexação de um dígito $d \in \{0, \dots, b-1\}$ tal que $N_{k+1} = bN_k + d$ permaneça livre de quadrados.

Um número inteiro positivo $N$ é definido como um ponto de parada se:

1. $N$ é livre de quadrados.
2. Para todo dígito $d$ na base, a extensão $bN + d$ não é livre de quadrados.

A questão central, proposta por Miller et al. [5], é se existem caminhadas infinitas livres de quadrados. Embora um modelo estocástico (o "Modelo Cego Ilimitado") sugira que caminhadas infinitas existem com probabilidade próxima a 1 (implicando que os pontos de parada são raros, com uma densidade assintótica de $\approx 5,218 \times 10^{-5}$ na base 10), este artigo analisa rigorosamente a densidade aritmética real dos pontos de parada para determinar se a previsão estocástica se sustenta.

Metodologia
Os autores empregam uma combinação de teoria multiplicativa elementar dos números e princípios de inclusão-exclusão, evitando as suposições probabilísticas do modelo estocástico.

1. Funções Indicadoras: O problema é reformulado usando a função de Möbius $\mu(n)$. Como $\mu(n)^2$ é a função indicadora para inteiros livres de quadrados, o indicador para um ponto de parada $N$ é expresso como:
   $$\mathbb{1}_{N \text{ é ponto de parada}} = \mu(N)^2 \prod_{d \in D} (1 - \mu(bN + d)^2)$$
   onde $D$ é o conjunto de dígitos.

2. Inclusão-Exclusão: O termo do produto é expandido em uma soma sobre todos os subconjuntos $S$ do conjunto de dígitos. Isso transforma a função de contagem $D_b(X)$ (o número de pontos de parada $\le X$) em uma soma alternada de funções de contagem $Q_S(X)$, onde $Q_S(X)$ conta inteiros $n \le X$ tais que $n$ e todas as extensões $bn+d$ (para $d \in S$) são livres de quadrados.

3. Análise de Crivo: Para um subconjunto fixo $S$, a condição de que $n$ e $bn+d$ sejam livres de quadrados é analisada primo a primo. Os autores definem classes de resíduos "ruins" módulo $p^2$ que devem ser evitadas. Usando o Teorema Chinês do Resto, eles determinam a densidade de inteiros que evitam essas classes.

   • Para primos grandes (onde $p \nmid b$), a condição $p^2 \mid (bn+d)$ força $n$ para uma única classe de resíduo módulo $p^2$. Crucialmente, um único quadrado de primo pode obstruir no máximo uma extensão de dígito por vez.
   • A densidade é expressa como um produto infinito (produto de Euler) de fatores locais $(1 - \nu_{p,b}(S)/p^2)$, onde $\nu_{p,b}(S)$ conta o número de classes de resíduos proibidas módulo $p^2$.

4. Controle do Termo de Erro: A prova controla cuidadosamente os termos de erro decorrentes da truncagem do crivo em um parâmetro $z$ e da contribuição de primos grandes, estabelecendo um termo de erro de $O(X/\sqrt{\log X})$.

Principais Resultados

• Teorema 1.1 (Base 10): A densidade assintótica dos pontos de parada na base 10 existe e é dada por:
  $$c_{\text{dead}} = \sum_{S \subseteq \{0,\dots,9\}} (-1)^{|S|} \prod_{p \text{ primo}} \left( 1 - \frac{\nu_p(S)}{p^2} \right)$$
  onde $\nu_p(S)$ é a contagem de classes de resíduos $n \pmod{p^2}$ tal que $p^2 \mid n$ ou $p^2 \mid (10n+d)$ para algum $d \in S$.
  O valor calculado é $c_{\text{dead}} \approx 1,317 \times 10^{-9}$.

• Teorema 1.2 (Base Geral $b$): O resultado se generaliza para qualquer base $b \ge 2$. A densidade $c_{\text{dead}}(b)$ é dada por uma expressão de forma fechada semelhante envolvendo uma soma alternada de produtos de Euler. O artigo fornece aproximações calculadas para bases primas $b \in \{2, 3, 5, 7\}$.

• Discrepância com Modelos Estocásticos: A densidade real ($\approx 1,3 \times 10^{-9}$) é aproximadamente 40.000 vezes menor do que a previsão estocástica ($\approx 5,2 \times 10^{-5}$). O artigo atribui isso às dependências aritméticas: o modelo estocástico ingênuo assume independência entre as extensões de dígitos, mas na realidade, o requisito de que todas as dez extensões falhem simultaneamente exige a obstrução simultânea por muitos quadrados de primos distintos, uma condição muito mais rigorosa do que o modelo de probabilidade independente sugere.

Significância e Alegações

• Resolução de Conjectura: O artigo demonstra que, embora a heurística estocástica preveja que caminhadas infinitas são quase certas, a estrutura aritmética real torna os pontos de parada significativamente mais raros do que o previsto. No entanto, a existência de uma caminhada infinita permanece um problema em aberto; o artigo quantifica a raridade das "obstruções" (pontos de parada), mas não prova a existência de um caminho infinito.
• Formalização: Uma principal alegação do artigo é que o teorema principal (Teorema 1.2) foi totalmente formalizado em Lean/Mathlib e a prova foi produzida automaticamente por uma ferramenta de IA chamada AxiomProver. O sistema recebeu apenas uma afirmação em linguagem natural do problema e derivou autonomamente a fórmula de forma fechada e a prova.
• Contexto Histórico (Atualização): Os autores observam que, após a postagem inicial no arXiv, souberam por Kannan Soundararajan que o resultado principal já havia sido obtido por Mirsky em 1947 [6]. O artigo reconhece que o trabalho de 2024 de Miller et al. [5] falhou em referenciar este trabalho anterior. Consequentemente, embora a formalização em Lean seja uma prova automatizada válida, os autores afirmam que o manuscrito não será submetido para publicação em periódicos como uma contribuição de pesquisa primária, servindo, em vez disso, como um estudo de caso para prova de teoremas automatizada.

Conclusão
O artigo fornece uma derivação aritmética rigorosa da densidade de pontos de parada em caminhadas de dígitos livres de quadrados, revelando uma enorme divergência das previsões estocásticas devido a dependências da teoria dos números. Sua contribuição mais inovadora, conforme formulada pelos autores, é a formalização end-to-end bem-sucedida deste resultado usando o AxiomProver, demonstrando a capacidade de sistemas de IA atuais lidarem com problemas não triviais na teoria analítica dos números.