Dead ends in square-free digit walks

Sintesi Tecnica: Vicoli Ciechi nelle Camminate di Numeri Liberi da Quadrati

Enunciato del Problema
Il saggio investiga l'esistenza e la densità dei "vicoli ciechi" (dead ends) nelle camminate di cifre libere da quadrati. Una camminata libera da quadrati in base $b$ inizia con un intero $N_0$ libero da quadrati e tenta di costruire una sequenza infinita $N_0, N_1, N_2, \dots$ dove ogni termine successivo è formato dall'aggiunta di una cifra $d \in \{0, \dots, b-1\}$ tale che $N_{k+1} = bN_k + d$ rimanga libero da quadrati.

Un intero positivo $N$ è definito come un vicolo cieco se:

1. $N$ è libero da quadrati.
2. Per ogni cifra $d$ nella base, l'estensione $bN + d$ non è libera da quadrati.

La questione centrale, posta da Miller et al. [5], è se esistano camminate infinite libere da quadrati. Sebbene un modello stocastico (il "Blind Unlimited Model") suggerisca che le camminate infinite esistano con probabilità vicina a 1 (implicando che i vicoli ciechi siano rari, con una densità asintotica di $\approx 5,218 \times 10^{-5}$ in base 10), questo saggio analizza rigorosamente la reale densità aritmetica dei vicoli ciechi per determinare se la previsione stocastica sia corretta.

Metodologia
Gli autori impiegano una combinazione di teoria dei numeri moltiplicativa elementare e principi di inclusione-esclusione, evitando le assunzioni probabilistiche del modello stocastico.

1. Funzioni Indicatrici: Il problema viene riformulato utilizzando la funzione di Möbius $\mu(n)$. Poiché $\mu(n)^2$ è la funzione indicatrice degli interi liberi da quadrati, l'indicatore di un vicolo cieco $N$ è espresso come:
   $$\mathbb{1}_{N \text{ è vicolo cieco}} = \mu(N)^2 \prod_{d \in D} (1 - \mu(bN + d)^2)$$
   dove $D$ è l'insieme delle cifre.

2. Inclusione-Esclusione: Il termine del prodotto viene espanso in una somma su tutti i sottoinsiemi $S$ dell'insieme delle cifre. Ciò trasforma la funzione di conteggio $D_b(X)$ (il numero di vicoli ciechi $\le X$) in una somma alternata di funzioni di conteggio $Q_S(X)$, dove $Q_S(X)$ conta gli interi $n \le X$ tali che $n$ e tutte le estensioni $bn+d$ (per $d \in S$) siano libere da quadrati.

3. Analisi del Setaccio (Sieve Analysis): Per un sottoinsieme $S$ fissato, la condizione che $n$ e $bn+d$ siano liberi da quadrati viene analizzata cifra per cifra (primo per primo). Gli autori definiscono classi di residui "cattive" modulo $p^2$ che devono essere evitate. Utilizzando il Teorema Cinese del Resto, determinano la densità degli interi che evitano tali classi.

   • Per i primi grandi $p$ (dove $p \nmid b$), la condizione $p^2 \mid (bn+d)$ costringe $n$ in un'unica classe di residui modulo $p^2$. Fondamentalmente, un singolo quadrato di un numero primo può ostacolare al massimo un'estensione di cifra alla volta.
   • La densità è espressa come un prodotto infinito (prodotto di Eulero) di fattori locali $(1 - \nu_{p,b}(S)/p^2)$, dove $\nu_{p,b}(S)$ conta il numero di classi di residui proibite modulo $p^2$.

4. Controllo del Termine di Errore: La dimostrazione controlla attentamente i termini di errore derivanti dal troncamento del setaccio a un parametro $z$ e dal contributo dei primi grandi, stabilendo un termine di errore di $O(X/\sqrt{\log X})$.

Risultati Chiave

• Teorema 1.1 (Base 10): La densità asintotica dei vicoli ciechi in base 10 esiste ed è data da:
  $$c_{\text{dead}} = \sum_{S \subseteq \{0,\dots,9\}} (-1)^{|S|} \prod_{p \text{ primo}} \left( 1 - \frac{\nu_p(S)}{p^2} \right)$$
  dove $\nu_p(S)$ è il conteggio delle classi di residui $n \pmod{p^2}$ tali che $p^2 \mid n$ o $p^2 \mid (10n+d)$ per qualche $d \in S$.
  Il valore calcolato è $c_{\text{dead}} \approx 1,317 \times 10^{-9}$.

• Teorema 1.2 (Base Generale $b$): Il risultato si generalizza a qualsiasi base $b \ge 2$. La densità $c_{\text{dead}}(b)$ è data da una simile espressione in forma chiusa che coinvolge una somma alternata di prodotti di Eulero. Il saggio fornisce approssimazioni calcolate per basi prime $b \in \{2, 3, 5, 7\}$.

• Discrepanza con i Modelli Stocastici: La vera densità ($\approx 1,3 \times 10^{-9}$) è circa 40.000 volte più piccola della previsione stocastica ($\approx 5,2 \times 10^{-5}$). Il saggio attribuisce ciò alle dipendenze aritmetiche: il modello stocastico ingenuo assume l'indipendenza tra le estensioni delle cifre, ma nella realtà, il requisito che tutte e dieci le estensioni falliscano simultaneamente richiede l'ostruzione simultanea da parte di molti quadrati di numeri primi distinti, una condizione molto più stringente rispetto al modello di probabilità indipendente.

Significato e Rivendicazioni

• Risoluzione della Congettura: Il saggio dimostra che, sebbene l'euristica stocastica preveda che le camminate infinite siano quasi certe, la reale struttura aritmetica rende i vicoli ciechi significativamente più rari di quanto previsto. Tuttavia, l'esistenza di una camminata infinita rimane un problema aperto; il saggio quantifica la rarità degli "ostacoli" (vicoli ciechi), ma non prova l'esistenza di un percorso infinito.
• Formalizzazione: Una rivendicazione primaria del saggio è che il teorema principale (Teorema 1.2) è stato completamente formalizzato in Lean/Mathlib e la dimostrazione è stata prodotta automaticamente da uno strumento di IA chiamato AxiomProver. Al sistema sono stati forniti solo l'enunciato in linguaggio naturale del problema e esso ha derivato autonomamente la formula in forma chiusa e la relativa dimostrazione.
• Contesto Storico (Aggiornamento): Gli autori notano che, dopo la pubblicazione iniziale su arXiv, hanno appreso da Kannan Soundararajan che il risultato principale era già stato ottenuto da Mirsky nel 1947 [6]. Il saggio riconosce che il lavoro del 2024 di Miller et al. [5] non ha citato questo precedente lavoro. Di conseguenza, sebbene la formalizzazione in Lean rappresenti una valida dimostrazione automatizzata, gli autori dichiarano che il manoscritto non sarà sottoposto a pubblicazione su riviste come contributo di ricerca primario, servendo invece come caso di studio per la dimostrazione automatica dei teoremi.

Conclusione
Il saggio fornisce una rigorosa derivazione aritmetica della densità dei vicoli ciechi nelle camminate di cifre libere da quadrati, rivelando una massiccia deviazione dalle previsioni stocastiche dovuta alle dipendenze teorico-numeriche. Il suo contributo più originale, come formulato dagli autori, è la riuscita formalizzazione end-to-end di questo risultato utilizzando AxiomProver, dimostrando la capacità dei sistemi di IA attuali di gestire problemi non banali nella teoria analitica dei numeri.