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

Dit artikel herlevert een klassiek stelling over automaten voor $\phi$-representaties met behulp van de Walnut-theoremaprover, waardoor eerdere resultaten op een uniforme en automatische manier kunnen worden bewezen en nieuwe inzichten worden verkregen.

De kern

De Wiskundige "Magische Spiegels" van Jeffrey Shallit

Stel je voor dat getallen niet alleen in ons vertrouwde decimale systeem (met cijfers 0 tot 9) bestaan, maar ook in een mysterieus land genaamd Fibonacciland. In dit land is de basis niet 10, maar het getal $\phi$ (de gulden snede, ongeveer 1,618). Dit getal is beroemd in de natuur: je vindt het in de spiralen van een zonnebloem, de schelp van een slak en de verhouding tussen de bladeren van een plant.

In dit artikel doet wiskundige Jeffrey Shallit iets heel bijzonders. Hij pakt een oude, ingewikkelde theorie uit de wiskunde op en laat zien hoe je deze kunt oplossen met een moderne, digitale "robot-rechter" genaamd Walnut.

Hier is wat hij doet, vertaald naar alledaags taal:

1. Het Probleem: Getallen in een vreemde taal

Normaal gesproken schrijven we getallen als een rijtje cijfers, bijvoorbeeld 123. In Fibanacciland (of $\phi$-land) kunnen we getallen ook schrijven, maar dan met een heel eigen regels.

• De Regels: Je mag niet twee keer achter elkaar een '1' gebruiken (geen "11").
• Het Doel: Ieder natuurlijk getal heeft een unieke, "nette" manier om geschreven te worden in dit systeem. Maar soms zijn er ook "rommelige" manieren (waar je wel "11" gebruikt).

Vroeger hadden wiskundigen al ontdekt dat er een soort "machine" (een automaat) bestaat die kan controleren of een rijtje cijfers een geldig getal in Fibanacciland is. Maar deze machine was zo complex en ondoorzichtig dat niemand hem echt kon begrijpen of gebruiken. Het was als een oude, roestige sleutel die niemand meer kon draaien.

2. De Oplossing: De Robot-Rechter (Walnut)

Shallit gebruikt een gratis softwareprogramma genaamd Walnut. Je kunt Walnut zien als een super-slimme robot-rechter die alleen logische vragen beantwoordt.

• Je zegt tegen de robot: "Als ik dit getal in Fibanacciland schrijf, klopt het dan met dit andere getal?"
• De robot denkt na en zegt: "Ja, dat klopt!" of "Nee, dat klopt niet!"
• Maar het mooiste is: als je de vraag goed stelt, bouwt de robot zelf de sleutel (de automaat) die het antwoord voor altijd vastlegt.

Shallit heeft deze robot gebruikt om de oude, ingewikkelde machine van Frougny en Sakarovitch te herbouwen. In plaats van urenlang handmatig te rekenen, heeft hij de robot de regels laten uitspugen. Het resultaat is een nieuwe, veel simpelere machine die precies doet wat de oude moest doen, maar nu begrijpelijk is.

3. Wat levert dit op? (De Magie)

Met deze nieuwe, schone machine kan Shallit dingen doen die voorheen bijna onmogelijk waren:

• Het tellen van manieren: Stel je wilt weten op hoeveel verschillende manieren je het getal 10 kunt schrijven in Fibanacciland zonder dat je "11" gebruikt. De robot telt dit er zo uit.
• Palindromen: Hij kijkt naar getallen die als een spiegelbeeld zijn (zoals "101" of "121"). De robot vindt precies welke getallen in Fibanacciland een spiegelbeeld zijn.
• Nieuwe ontdekkingen: Hij ontdekt patronen die niemand eerder zag. Bijvoorbeeld: "Elk keer als je een bepaald type getal hebt, is het aantal '1's in zijn schrijfwijze altijd kleiner dan of gelijk aan..."
• De "Knott" expansie: Hij lost een raadsel op van twee andere wiskundigen (Dekking en Van Loon) die een ingewikkelde methode hadden bedacht. De robot lost dit op in een handomdraai, zonder dat er één keer een saai bewijs met "inductie" (het stap-voor-stap bewijzen) nodig is.

4. De Metafoor: De Vertaler

Je kunt dit artikel zien als het vertalen van een oude, cryptische handleiding voor een complexe machine naar een duidelijke, moderne instructievideo.

• De oude machine: Een doolhof van gangen waar je verdwaalde.
• Walnut: Een GPS die je de kortste weg laat zien en zelfs de kaart tekent terwijl je loopt.
• Het resultaat: Wiskundigen kunnen nu niet alleen zien dat de machine werkt, maar ook waarom, en ze kunnen de machine gebruiken om nieuwe schatten te vinden in het land van de getallen.

Conclusie

Jeffrey Shallit toont aan dat je met de juiste digitale hulpmiddelen (zoals Walnut) oude, moeilijke wiskundige problemen kunt oplossen alsof je een puzzel oplost. Hij maakt de wiskunde van de "gulden snede" toegankelijker, sneller en leuker. Het is een feestje voor de verjaardag van Christiane Frougny (75 jaar), een van de oorspronkelijke ontdekkers van deze gebieden, en een eerbetoon aan de kracht van computers om de schoonheid van getallen bloot te leggen.

Kortom: Oude mysteries, opgelost met een moderne robot.

Technische samenvatting

Hier is een gedetailleerde technische samenvatting van het artikel "Proving Properties of φ-Representations with the Walnut Theorem-Prover" van Jeffrey Shallit, geschreven in het Nederlands.

Titel: Bewijzen van eigenschappen van φ-representaties met de Walnut Theorem-Prover

Auteur: Jeffrey Shallit
Publicatie: Communications in Mathematics 33 (2025), no. 2

---

1. Probleemstelling en Achtergrond

Het artikel richt zich op de representatie van getallen in het grondtal $\phi = \frac{1+\sqrt{5}}{2}$ (de gulden snede). Een niet-negatief reëel getal $z$ kan worden geschreven als $z = \sum a_i \phi^i$ met $a_i \in \{0, 1\}$.

• Canonieke representatie: Om uniekheid te garanderen, wordt de restrictie opgelegd dat er geen opeenvolgende enen voorkomen ($a_i a_{i+1} \neq 11$) en dat oneindige expansies niet eindigen in $010101\dots$.
• Historische context: In 1957 toonde Bergman aan dat natuurlijke getallen een eindige canonieke $\phi$-expansie hebben. Frougny en Sakarovitch bewezen later dat deze representaties berekend kunnen worden door een eindige automaat die parallel werkt met de Zeckendorf-voorstelling (Fibonacci-systeem) van het getal.
• Het probleem: Het oorspronkelijke artikel van Frougny en Sakarovitch is abstract en moeilijk te lezen; de automaat werd niet expliciet geconstrueerd. Daarnaast zijn er recente resultaten (o.a. van Dekking en Van Loon) over verschillende soorten expansies (zoals "Knott-expansies" en "DVL-expansies") die complexe inductieve bewijzen vereisen.

Het doel van dit artikel is om deze theorieën en resultaten op een meer computationele, uniforme en automatische manier te herleiden en uit te breiden.

2. Methodologie: De Walnut Theorem-Prover

De kern van de methode is het gebruik van Walnut, een gratis softwaretool ontwikkeld door Hamoon Mousavi. Walnut kan stellingen over automatische rijen bewijzen of weerleggen door gebruik te maken van een beslisprocedure voor een uitbreiding van de Presburger-aritmetiek.

De aanpak:

1. Formulering in Logica: De eigenschappen van $\phi$-representaties worden vertaald naar formules in de eerste-orde logica.
2. Constructie van Automaten: Als een logische stelling vrije variabelen bevat, berekent Walnut automatisch een eindige automaat die precies de waarden accepteert waarvoor de stelling waar is.
3. Lineaire Representaties: Voor functies die het aantal oplossingen tellen (zoals het aantal verschillende expansies voor een getal $n$), berekent Walnut een lineaire representatie (een triple $(v, \gamma, w)$). Dit stelt efficiënte berekening toe, zelfs voor grote $n$.
4. Combinatie van Componenten: De auteur bouwt complexe automaten door kleinere, bekende componenten te combineren, zoals:
   • Normalisatoren voor Zeckendorf- en negaFibonacci-systemen.
   • Verschuivingen (shifters) en extractie van laatste bits.
   • Conversies tussen verschillende representaties.

3. Belangrijkste Bijdragen en Resultaten

A. Constructie van de Frougny-Sakarovitch Automaten

De auteur construeert expliciet de automaat die de relatie vaststelt tussen een getal $n$ (in Zeckendorf-notatie) en zijn $\phi$-expansie $x.y$.

• Er wordt een automaat met 116 toestanden gebouwd voor algemene expansies.
• Door de canonieke voorwaarde (geen '11') toe te voegen, wordt een vereenvoudigde automaat van slechts 39 toestanden verkregen.
• Hiermee worden bekende resultaten over Fibonacci- en Lucas-getallen in $\phi$-notatie automatisch bewezen.

B. Bewijzen zonder Inductie

Het artikel demonstreert dat vele complexe resultaten uit de literatuur (specifiek van Dekking en Van Loon) op een "automatische" manier kunnen worden bewezen zonder ingewikkelde handmatige inductie:

• Knott-expansies: Expansies die niet eindigen in '011'. De auteur levert een lineaire representatie voor het aantal Knott-expansies van $n$ en bewijst formules voor $F_k$ en $L_k$.
• DVL-expansies: Een variant waarbij '11' alleen als de laatste twee cijfers ($d_1d_0$) is toegestaan onder specifieke voorwaarden. De auteur bewijst automatisch eigenschappen over deze expansies, inclusief de lengte van verticale runs van enen.
• Gemiddeld aantal expansies: De auteur berekent het asymptotische gemiddelde aantal Knott-expansies voor getallen in het interval $[F_i, F_{i+1})$, wat leidt tot een constante $\rho \approx 1.533$.

C. Nieuwe Resultaten

Naast het herleiden van bestaande theorieën, worden diverse nieuwe stellingen en rijen geïntroduceerd:

• Som van cijfers: Bewijs dat de som van de cijfers in de Zeckendorf-notatie altijd kleiner is dan of gelijk is aan de som in de canonieke $\phi$-notatie (een conjectuur van Dale Gerdemann uit 2012).
• Lengte van expansies: Een karakterisering van het verschil in lengte tussen opeenvolgende getallen in hun $\phi$-notatie.
• Individuele bits: Karakteriseringen van specifieke bits (zoals $d_0(n)$ en $d_{-1}(n)$) in termen van Sturmiaanse rijen en Lucas-representaties.
• Palindromen en Antipalindromen: Automaten die natuurlijke getallen identificeren met palindromische of antipalindromische $\phi$-expansies (zowel canoniek als niet-canoniek).
• Algebraïsche gehele getallen: Een methode om $\phi$-expansies te berekenen voor getallen van de vorm $m\phi + n$ (waarbij $m, n$ gehele getallen zijn), inclusief negatieve waarden, via het negaFibonacci-systeem.

4. Significatie en Impact

• Automatisering van Bewijzen: Het artikel toont aan dat complexe problemen in de getaltheorie en automaattheorie kunnen worden opgelost door ze te vertalen naar logica en te laten "bewijzen" door een computer. Dit elimineert de noodzaak voor menselijke, vaak lastige inductieve redeneringen.
• Unificatie: Het biedt een uniforme framework om verschillende soorten $\phi$-expansies (Zeckendorf, negaFibonacci, Knott, DVL, etc.) te analyseren.
• Nieuwe Inzichten: Door de automatische generatie van automaten en lineaire representaties worden nieuwe rijen in de OEIS (On-Line Encyclopedia of Integer Sequences) geïdentificeerd en nieuwe conjectures bewezen.
• Toepasbaarheid: Hoewel het artikel zich focust op $\phi$, suggereert de auteur dat deze techniek breed toepasbaar is op $\beta$-expansies voor andere kwadratische Pisot-getallen.

Conclusie

Jeffrey Shallit presenteert in dit artikel een krachtige demonstratie van hoe de Walnut theorem-prover kan worden ingezet om de theorie rondom $\phi$-representaties te moderniseren. Door de brug te slaan tussen formele logica, automaattheorie en getaltheorie, levert het werk niet alleen eenvoudige, inductievrije bewijzen voor bekende stellingen op, maar opent het ook de deur tot een stroom van nieuwe, computationeel gegenereerde resultaten die voorheen moeilijk toegankelijk waren.