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

Cet article réexamine un théorème classique sur les automates des représentations $\phi$ en utilisant le prouveur Walnut pour en obtenir une preuve computationnelle directe, permettant ainsi de démontrer de manière uniforme et automatique des résultats existants et d'en établir de nouveaux.

L'essentiel

Voici une explication de l'article de Jeffrey Shallit, racontée comme une histoire d'exploration mathématique, sans jargon technique.

🌟 L'Exploration du Pays des Nombres d'Or

Imaginez que les nombres sont comme des maisons. Habituellement, nous construisons nos maisons avec des briques standard : le système décimal (0 à 9). C'est comme utiliser des briques de taille fixe pour tout construire.

Mais il existe un architecte visionnaire nommé George Bergman qui, en 1957, a eu une idée folle : et si on construisait nos maisons avec des briques faites d'Or ? Plus précisément, avec le nombre d'or, noté φ (phi), ce nombre mystérieux qui apparaît dans les coquillages, les tournesols et l'art.

Dans ce monde, un nombre comme 2 ne s'écrit pas "2", mais comme une suite infinie ou finie de 0 et de 1, un peu comme un code secret binaire, mais avec une règle bizarre : on ne peut jamais mettre deux "1" côte à côte (pas de "11"). C'est la règle d'or de ce pays.

🤖 Le Problème : Un Labyrinthe Invisible

Le problème, c'est que ce système est très difficile à maîtriser. Comment savoir si un code binaire donné correspond bien au nombre 42 ? Comment passer d'un système à l'autre ?

Pendant des décennies, des mathématiciens brillants comme Frougny et Sakarovitch ont dit : "Il existe une machine magique (un automate) capable de faire ce travail." Mais ils n'ont pas donné le plan de la machine ! C'était comme dire : "Il y a un robot qui résout ce labyrinthe", sans montrer le robot. Lire leurs travaux était comme essayer de comprendre un labyrinthe en regardant une carte dessinée dans une langue étrangère.

🛠️ La Solution : Le "Walnut", le Robot-Enquêteur

C'est là qu'intervient Jeffrey Shallit, l'auteur de cet article. Il a un outil formidable appelé Walnut.

Imaginez Walnut comme un détective robot ultra-puissant. Il ne devine pas les réponses ; il les prouve en vérifiant chaque possibilité, une par une, à une vitesse fulgurante.

• Vous lui donnez une règle (une phrase logique).
• Il construit instantanément le plan de la machine (l'automate) qui vérifie cette règle.
• Si la règle est vraie, il vous dit "Vrai" et vous donne le dessin de la machine.

Shallit a utilisé ce robot pour reconstruire la machine manquante de Frougny et Sakarovitch. Au lieu de faire des calculs manuels complexes et longs (comme grimper à une montagne à pied), il a demandé au robot de le faire pour lui.

🎭 Ce que le Robot a Découvert

Une fois le robot en main, Shallit a pu explorer le pays des nombres d'Or comme personne ne l'avait fait avant. Voici ce qu'il a trouvé, expliqué simplement :

1. Le Dictionnaire des Nombres : Il a créé un dictionnaire parfait qui traduit n'importe quel nombre entier en son code "Or".
2. Les Chiffres Qui Dansent : Il a étudié la somme des chiffres. Par exemple, dans le système normal, la somme des chiffres de 199 est 1+9+9=19. Dans le système Or, c'est différent. Le robot a prouvé des conjectures (des suppositions) qui traînaient depuis 2012, en montrant que la somme des chiffres dans le système Or est toujours plus grande ou égale à celle du système classique.
3. Les Miroirs (Palindromes) : Il a cherché les nombres qui se lisent pareil dans les deux sens (comme "radar"). Il a découvert exactement quels nombres ont un code "Or" qui est un palindrome. C'est comme trouver les visages qui se regardent dans un miroir parfait.
4. Les "Knott" et les "Naturels" : D'autres chercheurs avaient inventé des règles spéciales pour écrire les nombres (comme interdire certaines finitions de mots). Shallit a utilisé son robot pour compter instantanément combien de façons différentes on peut écrire un nombre selon ces règles, sans avoir à faire des heures de calculs à la main.

🧩 L'Analogie Finale : Le Traducteur Universel

Pour résumer, imaginez que les mathématiciens précédents avaient écrit un livre de grammaire pour une langue étrangère, mais qu'ils avaient oublié de donner le dictionnaire.

Jeffrey Shallit, avec son robot Walnut, a :

1. Imprimé le dictionnaire (l'automate) pour que tout le monde puisse l'utiliser.
2. Traduit des phrases compliquées (les théorèmes) en langage simple.
3. Découvert de nouveaux mots (de nouveaux résultats mathématiques) que personne n'avait vus auparavant.

Le plus beau dans tout cela ? Il n'a pas eu à faire des calculs manuels épuisants. Il a simplement écrit les règles du jeu en langage logique, et le robot a fait le travail de "prouver" que tout fonctionne parfaitement. C'est une victoire de l'intelligence artificielle (au sens large) sur la complexité mathématique, rendant accessible ce qui semblait être un labyrinthe inaccessible.

En conclusion, cet article nous dit : Parfois, pour voir la beauté d'un système complexe, il ne faut pas essayer de le comprendre seul, mais construire un robot capable de le cartographier pour nous.

Résumé technique

Voici un résumé technique détaillé de l'article "Proving Properties of φ-Representations with the Walnut Theorem-Prover" de Jeffrey Shallit, rédigé en français.

1. Problème et Contexte

L'article s'intéresse aux représentations en base $\phi$ (où $\phi = (1+\sqrt{5})/2$ est le nombre d'or), un sujet initié par George Bergman en 1957. Contrairement aux bases entières classiques, une représentation en base $\phi$ d'un nombre réel positif $z$ s'écrit sous la forme $z = \sum a_i \phi^i$ avec $a_i \in \{0, 1\}$.

Le problème central abordé est la caractérisation et l'analyse des propriétés de ces représentations, en particulier la représentation canonique (qui évite le motif "11" et les terminaisons infinies en $010101\dots$).
Un résultat fondamental, établi par Frougny et Sakarovitch, stipule qu'il existe un automate fini qui accepte les triplets $(n, x, y)$ tels que $n$ (représenté dans le système de Zeckendorf) soit égal à la valeur de la chaîne $x.y^R$ en base $\phi$. Cependant, l'article original de Frougny et Sakarovitch est difficile à lire et ne présente pas explicitement cet automate.

L'objectif de l'auteur est de :

1. Reconstruire explicitement et simplement l'automate de Frougny-Sakarovitch.
2. Utiliser cet automate pour fournir des preuves induction-free (sans induction) de résultats existants.
3. Découvrir de nouveaux résultats sur les représentations en base $\phi$ (sommes de chiffres, longueurs, palindromes, etc.).
4. Répondre à des conjectures ouvertes (notamment celle de Dale Gerdemann).

2. Méthodologie

La méthodologie repose entièrement sur l'utilisation de l'outil logiciel Walnut, un théorème-proveur (démonstrateur de théorèmes) développé par Hamoon Mousavi, capable de décider de la vérité de formules du premier ordre sur les suites automatiques.

Les étapes clés de la méthode sont :

• Construction d'automates modulaires : L'auteur décompose le problème complexe en petits automates gérant des tâches spécifiques :
  • Normalisation des représentations de Zeckendorf (pour les entiers positifs) et de NegaFibonacci (pour les entiers négatifs).
  • Décalages (shifters) et extraction de bits.
  • Conversion entre les systèmes de numération.
• Synthèse de l'automate principal : En combinant ces pièces via des opérations logiques (conjonction, quantification existentielle/universelle) dans Walnut, l'auteur construit l'automate de Frougny-Sakarovitch. Cet automate accepte les triplets $(n, x, y)$ si $n = [x.y]_\phi$.
• Preuve par décision : Au lieu d'utiliser des preuves mathématiques traditionnelles par récurrence, l'auteur exprime les propriétés à prouver comme des formules logiques. Walnut calcule alors l'automate correspondant ou retourne TRUE/FALSE.
• Représentations linéaires : Pour les fonctions arithmétiques (comme la somme des chiffres), l'auteur utilise la technique des représentations linéaires (triplets $(v, \gamma, w)$) générées par Walnut pour obtenir des formules de récurrence et des comportements asymptotiques.

3. Contributions Clés et Résultats

L'article produit un large éventail de résultats, classés par section :

A. Reconstruction et Caractérisation (Sections 2-5)

• Automate explicite : Construction d'un automate de 116 états (et une version canonique de 39 états) vérifiant la relation $n = [x.y]_\phi$.
• Représentations de Fibonacci et Lucas : Preuve automatique des formes canoniques des représentations en base $\phi$ des nombres de Fibonacci ($F_n$) et de Lucas ($L_n$), confirmant des résultats antérieurs de manière constructive.
• Caractérisation des parties gauche et droite :
  • Théorème 2.4 : Une chaîne binaire de longueur paire, finissant par 1 et sans "11", apparaît toujours comme partie droite d'une représentation canonique.
  • Théorème 2.5 : Caractérisation des parties gauches possibles (pas de "11" et pas de suffixe de la forme $1(00)^i1$).
• Somme des chiffres (Section 3) :
  • Résolution de la conjecture de Gerdemann (2012) : Preuve que la somme des chiffres de $n$ en représentation de Zeckendorf est toujours inférieure ou égale à la somme des chiffres de $n$ en base $\phi$ canonique. La preuve utilise un algorithme de Bellman-Ford sur un graphe pondéré dérivé de l'automate.
  • Calcul de la somme des chiffres de la partie gauche ($s_L$) et droite ($s_R$) via des représentations linéaires.

B. Propriétés Structurelles (Sections 4-6)

• Longueur des représentations : Analyse de la longueur de la partie entière, montrant que les écarts entre termes successifs sont liés aux nombres de Lucas.
• Bits individuels : Caractérisation des coefficients $d_0(n)$ et $d_1(n)$ via des suites de Sturmian.
• Connexion avec les représentations de Lucas : Preuve que le bit $d_{-1}(n)$ vaut 1 si et seulement si $n$ admet exactement deux représentations distinctes comme somme de nombres de Lucas.
• Palindromes et Anti-palindromes :
  • Identification des entiers ayant une représentation canonique palindrome (suite A362780).
  • Identification des entiers ayant une représentation (éventuellement non canonique) palindrome.
  • Caractérisation des nombres "antipalindromes" (où la partie droite est le complément bitwise de la partie gauche).

C. Généralisations et Expansions Spéciales (Sections 7-10)

• Expansions de Knott : L'auteur redécouvre et simplifie les résultats de Dekking et Van Loon sur le nombre d'expansions de Knott (représentations ne se terminant pas par 011). Il fournit une représentation linéaire permettant un calcul en $O(\log n)$ et dérive des formules fermées pour les nombres de Fibonacci et Lucas.
• Expansions Naturelles et DVL : Analyse d'autres types d'expansions définies par Dekking et Van Loon, en montrant comment les conditions de longueur ou de motifs spécifiques peuvent être imposées via l'intersection d'automates.
• Entiers Algébriques (Section 11) : Extension de la méthode aux entiers algébriques de $\mathbb{Q}(\sqrt{5})$ de la forme $m\phi + n$, en utilisant des représentations NegaFibonacci pour gérer les coefficients négatifs.

4. Signification et Impact

• Automatisation de la preuve : L'article démontre la puissance de l'approche "automatique" pour les problèmes de théorie des nombres liés aux bases non entières. Il remplace des preuves complexes par induction (souvent longues et sujettes à erreurs) par des calculs algorithmiques rigoureux et vérifiables.
• Nouveaux résultats : Plusieurs résultats sont présentés comme nouveaux (séquences A362716, A362780, A362781, etc.), notamment sur les sommes de chiffres partielles et les propriétés des bits individuels.
• Unification : La méthode permet de traiter de manière uniforme une grande variété de problèmes (palindromes, sommes, longueurs, types d'expansions) en modifiant simplement les conditions logiques dans Walnut.
• Accessibilité : En fournissant le code Walnut et en détaillant la construction des automates, l'auteur rend ces techniques accessibles à d'autres chercheurs, encourageant l'exploration de propriétés similaires pour d'autres nombres de Pisot quadratiques.

En résumé, cet article établit un nouveau paradigme pour l'étude des représentations en base $\phi$, transformant des problèmes de combinatoire des mots et de théorie des nombres en problèmes de décision sur les automates finis, résolus efficacement par des outils informatiques modernes.