Beatty Sequences for a Quadratic Irrational: Decidability and Applications

Titolo: Sequenze di Beatty per Irrazionali Quadratici: Decidibilità e Applicazioni

1. Il Problema

Il lavoro si concentra sulle sequenze di Beatty inomogenee, definite come $(\lfloor n\alpha + \beta \rfloor)_{n \ge 1}$, dove $\alpha$ e $\beta$ sono numeri reali. Sebbene le sequenze di Beatty omogenee ($\beta=0$) e i loro collegamenti con le parole di Sturmian siano stati ampiamente studiati, la questione della decidibilità della teoria logica del primo ordine per queste sequenze, quando combinate con l'addizione, rimaneva parzialmente aperta o richiedeva tecniche complesse per casi specifici.

L'obiettivo principale è determinare se, per $\alpha$ e $\beta$ appartenenti allo stesso campo quadratico, sia possibile costruire un automato finito che riconosca la relazione funzionale $y = \lfloor n\alpha + \beta \rfloor$ quando $n$ e $y$ sono rappresentati in un sistema di numerazione specifico (rappresentazione di Ostrowski). La risoluzione di questo problema permetterebbe di decidere automaticamente proprietà complesse di queste sequenze, come la loro capacità di formare basi additive o la risoluzione di congetture aperte.

2. Metodologia

Gli autori adottano un approccio basato sulla teoria degli automi e la logica del primo ordine, sfruttando le seguenti componenti chiave:

• Rappresentazione di Ostrowski: Utilizzano il sistema di numerazione di Ostrowski basato su un numero irrazionale quadratico $\gamma$. In questo sistema, ogni intero naturale è rappresentato univocamente come combinazione lineare dei denominatori delle convergenti della frazione continua di $\gamma$.
• Sincronizzazione: Definiscono una sequenza come "sincronizzata" se esiste un automa finito che accetta in parallelo le rappresentazioni di $n$ e $y$ se e solo se $y = \lfloor n\alpha + \beta \rfloor$.
• Strumenti Computazionali: Implementano le loro procedure decisionali utilizzando Walnut, un software open-source per la dimostrazione di teoremi su sequenze automatiche. Walnut permette di tradurre formule logiche del primo ordine in automi finiti e di verificarne la validità.
• Strumenti Matematici:
  • Utilizzano la teoria delle frazioni continue (in particolare quelle puramente periodiche per irrazionali quadratici).
  • Applicano il teorema di Kronecker multidimensionale per analizzare la complessità delle parole (subword complexity).
  • Sfruttano le proprietà di chiusura delle sequenze sincronizzate (somma, composizione, ecc.).

3. Contributi Chiave e Risultati Principali

A. Teorema di Sincronizzazione (Teorema 9)
Il risultato centrale è la dimostrazione che se $\alpha$ e $\beta$ appartengono allo stesso campo quadratico $\mathbb{Q}(\gamma)$ (dove $\gamma$ è un irrazionale quadratico con frazione continua puramente periodica), allora la sequenza $(\lfloor n\alpha + \beta \rfloor)_{n \ge 1}$ è $\gamma$-Ostrowski sincronizzata.

• Questo implica che esiste un automa finito che, dato $n$ in rappresentazione di Ostrowski, calcola o verifica $\lfloor n\alpha + \beta \rfloor$.
• Viene anche provato il converso (Teorema 28): se la sequenza è sincronizzata, allora $\alpha$ e $\beta$ devono necessariamente appartenere a $\mathbb{Q}(\gamma)$.

B. Decidibilità della Teoria Logica (Corollario 11)
Come conseguenza diretta della sincronizzazione e dei risultati precedenti di Hieronymi, Terry e Baranwal, gli autori dimostrano che la teoria del primo ordine dei numeri naturali con l'addizione e la funzione $n \mapsto \lfloor n\alpha + \beta \rfloor$ è decidibile.

• Questo significa che qualsiasi affermazione logica del primo ordine su queste sequenze può essere verificata automaticamente come vera o falsa.

C. Applicazioni alle Basi Additive (Sezione 7)
Gli autori risolvono il problema della base additiva. Dimostrano che è decidibile se l'insieme $\{\lfloor n\alpha + \beta \rfloor : n \ge 1\}$ forma una base additiva (o asintotica) di ordine $r$.

• Viene mostrato che per ogni irrazionale quadratico, esiste un intero $h$ tale che la sequenza forma una base asintotica di ordine $h$, e tale $h$ è calcolabile.

D. Risoluzione di Congetture Aperte
Il metodo proposto viene utilizzato per risolvere diverse congetture e problemi aperti:

1. Congetture di Don Reble: Verifica automatica di proprietà riguardanti progressioni aritmetiche monocromatiche nella parola di Fibonacci, risolvendo le congetture relative alle sequenze OEIS A189377, A189378 e A189379.
2. Domanda di Graham: Viene dimostrato che il problema di Graham (sulle famiglie di copertura eventuale di interi tramite sequenze di Beatty) è decidibile quando i parametri appartengono allo stesso campo quadratico.
3. Sequenza di Hildebrand et al.: Viene fornita una caratterizzazione esplicita e una dimostrazione automatica per una sequenza studiata da Hildebrand, Li, Li e Xie, relativa alla differenza tra una sequenza e il suo complementare.
4. Problema dello "Swappage" di Kimberling: Viene fornita una prova alternativa e automatizzata per le congetture di Kimberling sulle sequenze di Wythoff modificate (OEIS A141104, ecc.).
5. Sequenze legate a $\sqrt{2}$: Vengono costruiti automi per sette sequenze OEIS correlate a $\sqrt{2}$, risolvendo congetture di Michel Dekking e Benedict Irwin.

E. Parti Frazionarie (Sezione 14)
Vengono sviluppati metodi per gestire confronti tra parti frazionarie $\{ \alpha x + \beta \}$ all'interno della logica del primo ordine, trasformando disuguaglianze su parti frazionarie in disuguaglianze su funzioni floor, rendendo possibile l'analisi di problemi geometrici su cerchi unitari.

4. Significato e Impatto

• Semplificazione Metodologica: Il contributo più significativo è la semplicità del metodo proposto. Invece di tecniche di eliminazione dei quantificatori complesse o analisi algebriche pesanti, gli autori mostrano che la costruzione di automi sincronizzati rende la decisione "meccanica" e implementabile in pochi secondi con Walnut.
• Generalizzazione: Il lavoro generalizza risultati noti (come quelli per il rapporto aureo o la parola di Fibonacci) a qualsiasi irrazionale quadratico, coprendo un'ampia classe di numeri.
• Potere Computazionale: Dimostra l'efficacia degli strumenti di dimostrazione automatica (come Walnut) nella teoria dei numeri e nella combinatoria sulle parole, trasformando problemi aperti in verifiche algoritmiche.
• Nuove Connessioni: Stabilisce un legame profondo tra la sincronizzazione degli automi, la struttura delle frazioni continue e la decidibilità logica, fornendo un quadro unificato per lo studio delle sequenze di Beatty.

In sintesi, il paper stabilisce un nuovo standard per l'analisi delle sequenze di Beatty irrazionali quadratiche, trasformando questioni teoriche complesse in problemi di verifica automatica risolvibili, con applicazioni concrete nella risoluzione di decenni di congetture matematiche.