pith. sign in

arxiv: 2305.02672 · v6 · pith:YTABGUIPnew · submitted 2023-05-04 · 🧮 math.NT · cs.DM· cs.FL

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

Jeffrey Shallit This is my paper

Pith reviewed 2026-05-24 08:35 UTC · model grok-4.3

classification 🧮 math.NT cs.DMcs.FL
keywords φ-representationsWalnut theorem-provergolden ratioautomatanumeration systemsFrougny-Sakarovitch theoremautomatic sequencesinduction-free proofs
0
0 comments X

The pith

Walnut theorem-prover derives the Frougny-Sakarovitch automata theorem for φ-representations computationally and yields induction-free proofs of their properties.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper revisits the classic result that automata recognize valid φ-representations of integers, where φ is the golden ratio, and obtains the same theorem by direct computation inside the Walnut prover. This encoding turns statements about the representations into first-order logic sentences that Walnut decides automatically. The approach supplies uniform proofs for many known facts about these representations and produces additional new facts, all without manual induction. A reader cares because the method replaces case-by-case reasoning with a single mechanical procedure that scales across related claims.

Core claim

Encoding questions about φ-representations as first-order statements in the language decided by Walnut recovers the Frougny-Sakarovitch theorem on the corresponding automata in a computationally direct way; the same encoding then supplies simple, induction-free proofs of existing results on these representations, automatically recovers many results from Dekking and Van Loon, and generates new results on φ-representations.

What carries the argument

Walnut theorem-prover deciding first-order statements about φ-representations and their automata.

If this is right

  • Existing results on φ-representations receive simple induction-free proofs in a uniform manner.
  • Results from recent papers of Dekking and Van Loon are recovered automatically.
  • New results on φ-representations are obtained through the same encoding technique.
  • The Frougny-Sakarovitch automata theorem itself is obtained by direct computation rather than traditional proof.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same encoding strategy could be tested on representations in other quadratic integer bases.
  • Walnut might discover further automatic identities among φ-representations that have not yet been conjectured by hand.
  • The technique suggests a route for automating proofs in related numeration systems whose validity conditions are expressible in the same logic.

Load-bearing premise

Properties of φ-representations can be faithfully encoded as first-order logical statements that the Walnut decision procedure handles without modeling error.

What would settle it

Walnut proving a known false statement about φ-representations or failing to prove a known true one.

Figures

Figures reproduced from arXiv: 2305.02672 by Jeffrey Shallit.

Figure 1
Figure 1. Figure 1: The automaton fibnorm. 2.2 NegaFibonacci normalizer We also need the analogous “normalizer” for negaFibonacci expansions; it takes x and y as inputs, with x an arbitrary binary string and y a canonical negaFibonacci expansion of some integer n, and accepts if and only if n = [x]−F . Such an automaton has 5 states (or 4 if one omits the dead state). We call it negfibnorm. Correctness is left to the reader … view at source ↗
Figure 2
Figure 2. Figure 2: The automaton negfibnorm. 6 [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Canonical φ-representation of Fn. Inspection of the automaton shows that, ignoring leading zeros, there are essentially four different acceptance paths: • [1, 1, 0][0, 0, 1][0, 0, 0]([0, 0, 0][0, 1, 0][0, 0, 1][0, 0, 0])∗ . • [1, 1, 1][0, 0, 0][0, 0, 0][0, 0, 1]([0, 1, 0][0, 0, 0][0, 0, 0][0, 0, 1])∗ ; • [1, 1, 0]([0, 0, 1][0, 0, 0][0, 0, 0][0, 1, 0])∗ ; • [1, 1, 1][0, 0, 0]([0, 0, 0][0, 0, 1][0, 1, 0][0, … view at source ↗
Figure 4
Figure 4. Figure 4: Automaton accepting the folded representations of all [PITH_FULL_IMAGE:figures/full_fig_p010_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Automaton for weight-0 paths. To get the accepted set of n, we project to the first coordinate and determinize the resulting automaton. Thus we have proved the following result [PITH_FULL_IMAGE:figures/full_fig_p013_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Automaton for weight-0 paths. 13 [PITH_FULL_IMAGE:figures/full_fig_p013_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Fibonacci automaton for d(n). 4 Length of base-φ representations Similarly, one can study the length ℓ(n) of the left part of (n)φ (or, alternatively, one more than the exponent of the highest power of φ appearing in (n)φ). This is sequence A362692 in the OEIS. Here the idea is to create a simple automaton, onepos, that accepts binary strings x and t if and only if t contains a single 1 and it occurs at or… view at source ↗
Figure 8
Figure 8. Figure 8: Fibonacci DFAO for first difference of ℓ(n). Inspection of this automaton and observing that the Fibonacci representation of the Lucas numbers are of the form 1010∗, gives the following result: Theorem 4.1. We have ℓ(n)−ℓ(n−1) = 1 if and only if n = 1 or n = L2i or n = L2i−1+1 for i ≥ 1. This is implied by a result of Sanchis and Sanchis [32, Thm. 2.1]. 16 [PITH_FULL_IMAGE:figures/full_fig_p016_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: 0 [0,0] 1 [0,1] 2 [1,1] 3 [0,0] 4 [1,0] 5 [1,0] 6 [0,0] 7 [0,0] 8 [0,0] 9 [0,0] 10 [1,0] [0,0] 11 [1,0] 12 [0,0] [0,0] [1,0] [0,0] [PITH_FULL_IMAGE:figures/full_fig_p020_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: Fibonacci automaton for those n with palindromic φ-representations. 21 [PITH_FULL_IMAGE:figures/full_fig_p021_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: Fibonacci automaton for those n having some palindromic (possibly non￾canonical) φ-representations. The resulting sequence of n accepted by this automaton is 2, 6, 14, 36, 38, 94, 96, 100, 246, 248, 252, 260, . . . and forms sequence A330672 in the OEIS. We remark that the only new examples are those where the only 11 occurs as the 1 at the end of x (and hence at the beginning of x R), as can be verified … view at source ↗
Figure 12
Figure 12. Figure 12: Fibonacci automaton accepting Shevelev’s [PITH_FULL_IMAGE:figures/full_fig_p023_12.png] view at source ↗
Figure 13
Figure 13. Figure 13: Automaton checking the DVL condition. We can then use this automaton to “automatically” obtain many of the results in [14]; for example, their Proposition 3.3: Proposition 10.1. The canonical φ-representation of an integer n differs from the DVL expansion of n if and only if there exists m ≥ 1 such that n = ⌊(φ + 2)m⌋. Proof. We use the Walnut code reg equal {0,1} {0,1} "([0,0]|[1,1])*": def differ "?msd_… view at source ↗
read the original abstract

We revisit a classic theorem of Frougny and Sakarovitch concerning automata for $\varphi$-representations, and show how to obtain it in a different and more computationally direct way. Using it, we can find simple, induction-free proofs of existing results in the literature about these representations, in a uniform and straightforward manner. In particular, we can easily and "automatically'' recover many of the results of recent papers of Dekking and Van Loon. We also obtain a number of new results on $\varphi$-representations.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper revisits the Frougny-Sakarovitch theorem on automata for φ-representations and shows how the Walnut theorem-prover yields this result in a computationally direct manner. It then uses the approach to obtain simple, induction-free proofs of existing results (including those of Dekking and Van Loon) together with several new results on φ-representations, all expressed as first-order statements decided by Walnut.

Significance. If the encodings are faithful, the work supplies a uniform, automated route to proofs about φ-representations that avoids manual induction. The explicit use of machine-checked proofs via Walnut is a clear strength, offering reproducibility and a template for similar problems in automatic sequences and numeration systems.

minor comments (2)
  1. Abstract: the claim that results of Dekking and Van Loon are recovered would be strengthened by naming the specific theorems or propositions that are re-proved.
  2. The paper would benefit from a short appendix or subsection listing the exact Walnut predicates and automata constructions used for the central Frougny-Sakarovitch encoding.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary, assessment of significance, and recommendation to accept the paper. There are no major comments requiring a response.

Circularity Check

0 steps flagged

No circularity: external prover on independent encodings

full rationale

The paper encodes properties of φ-representations as first-order statements in the language decided by the external Walnut prover and obtains proofs via its decision procedure. This modeling step is the sole prerequisite; the prover itself is not defined inside the paper, and the target results (Frougny–Sakarovitch automata theorem and consequences) are recovered by computation rather than by fitting parameters or by any self-referential definition. Citations to prior literature are to independent external sources. No equation or claim reduces to its own input by construction, and no load-bearing step collapses to a self-citation chain.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The proof method depends on the soundness of the Walnut prover and the accurate modeling of φ-representations as automatic sequences; no free parameters or new entities are introduced.

axioms (2)
  • domain assumption The decision procedure implemented in Walnut is correct for the first-order theory of automatic sequences.
    The paper relies on Walnut's ability to prove the properties automatically.
  • domain assumption φ-representations can be modeled using morphisms and automata in a way compatible with Walnut's input language.
    Central to translating the theorem into a form Walnut can handle.

pith-pipeline@v0.9.0 · 5609 in / 1397 out tokens · 30605 ms · 2026-05-24T08:35:26.215729+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

38 extracted references · 38 canonical work pages

  1. [1]

    Berend and C

    D. Berend and C. Frougny. Computability by finite automata and Pisot bases. Math. Systems Theory, 27:275–282, 1994

    work page 1994

  2. [2]

    G. Bergman. A number system with an irrational base. Math. Mag., 31:98–110, 1957

    work page 1957

  3. [3]

    J. Berstel. An exercise on Fibonacci representations. RAIRO Inform. Th´ eor. App., 35:491–498, 2001

    work page 2001

  4. [4]

    Berstel and C

    J. Berstel and C. Reutenauer. Noncommutative Rational Series With Applications , volume 137 of Encyclopedia of Mathematics and Its Applications . Cambridge Univer- sity Press, 2011

    work page 2011

  5. [5]

    Bertrand-Mathis

    A. Bertrand-Mathis. Comment ´ ecrire les nombres entiers dans une base qui n’est pas enti` ere.Acta Math. Hung. , 54:237–241, 1989

    work page 1989

  6. [6]

    J. L. Brown, Jr. Unique representation of integers as sums of distinct Lucas numbers. Fibonacci Quart., 7:243–252, 1969. 30 Proving Properties of φ-Representations with the Walnut Theorem-Prover

    work page 1969

  7. [7]

    M. W. Bunder. Zeckendorf representations using negative Fibonacci numbers. Fi- bonacci Quart., 30:111–115, 1992

    work page 1992

  8. [8]

    H. V. Chu, D. C. Luo, and S. J. Miller. On Zeckendorf related partitions using the Lucas sequence. Fibonacci Quart., 60:111–119, 2022

    work page 2022

  9. [9]

    F. M. Dekking. The structure of base phi expansions. Arxiv preprint arXiv:2305.08349 [math.NT], May 15 2023. Available at https://arxiv.org/abs/2305.08349

    work page arXiv 2023

  10. [10]

    F. M. Dekking. Base phi representations and golden mean beta-expansions. Fibonacci Quart., 58:38–48, 2020

    work page 2020

  11. [11]

    F. M. Dekking. The sum of digits function of the base phi expansion of the natural numbers. INTEGERS, 20:#A45, 2020

    work page 2020

  12. [12]

    F. M. Dekking. The sum of digits functions of the Zeckendorf and the base phi expansions. Theoret. Comput. Sci., 859:70–79, 2021

    work page 2021

  13. [13]

    Dekking and A

    M. Dekking and A. Van Loon. Counting base phi representations. Arxiv preprint arXiv:2304.11387 [math.NT], April 22 2023. Available at https://arxiv.org/abs/ 2304.11387

    work page arXiv 2023

  14. [14]

    Dekking and A

    M. Dekking and A. Van Loon. On the representation of the natural numbers by powers of the golden mean. Arxiv preprint arXiv:2111.07544 [math.NT], November 15 2021. Available at https://arxiv.org/abs/2111.07544

    work page arXiv 2021

  15. [15]

    Fleischer and J

    L. Fleischer and J. O. Shallit. Automata, palindromes, and reversed subwords. J. Automata, Languages, and Combinatorics , 26:221–253, 2021

    work page 2021

  16. [16]

    C. Frougny. Linear numeration systems, θ-developments and finite automata. In B. Monien and R. Cori, editors, STACS 89, volume 349 of Lecture Notes in Computer Science, pages 144–155. Springer-Verlag, 1989

    work page 1989

  17. [17]

    C. Frougny. Representation of numbers in non-classical numeration systems. In P. Ko- rnerup and D. W. Matula, editors, Proc. 10th IEEE Symp. Computer Arithmetic , pages 17–21. IEEE Press, 1991

    work page 1991

  18. [18]

    C. Frougny. Confluent linear numeration systems. Theoret. Comput. Sci. , 106:183– 219, 1992

    work page 1992

  19. [19]

    C. Frougny. How to write integers in non-integer base. In I. Simon, editor, 1st Latin American Symposium on Theoretical Informatics (LATIN ’92) , Lecture Notes in Computer Science, pages 154–164. Springer-Verlag, 1992

    work page 1992

  20. [20]

    C. Frougny. Representations of numbers and finite automata. Math. Systems Theory, 25:37–60, 1992. 31 Jeffrey Shallit

    work page 1992

  21. [21]

    C. Frougny. Syst` emes de num´ eration lin´ eaires etθ-repr´ esentations.Theoret. Comput. Sci., 94:223–236, 1992

    work page 1992

  22. [22]

    C. Frougny. On-line digit set conversion in real base. Theoret. Comput. Sci., 292:221– 235, 2003

    work page 2003

  23. [23]

    Frougny and J

    C. Frougny and J. Sakarovitch. Automatic conversion from Fibonacci representation to representation in base φ, and a generalization. Internat. J. Algebra Comput. , 9:351–384, 1999

    work page 1999

  24. [24]

    Hart and L

    E. Hart and L. Sanchis. On the occurrence of Fn in the Zeckendorf decomposition of nFn. Fibonacci Quart., 37:21–33, 1999

    work page 1999

  25. [25]

    Labb´ e and J

    S. Labb´ e and J. Lepˇ sov´ a. A Fibonacci analogue of the two’s complement numeration system. RAIRO Inform. Th´ eor. App., 57:Paper 12, 2023

    work page 2023

  26. [26]

    C. G. Lekkerkerker. Voorstelling van natuurlijke getallen door een som van getallen van Fibonacci. Simon Stevin, 29:190–195, 1952

    work page 1952

  27. [27]

    Lothaire

    M. Lothaire. Algebraic Combinatorics on Words, volume 90 of Encyclopedia of Math- ematics and Its Applications . Cambridge University Press, 2002

    work page 2002

  28. [28]

    H. Mousavi. Automatic theorem proving in Walnut. Arxiv preprint, arXiv:1603.06017 [cs.FL], May 25 2021. Available at http://arxiv.org/abs/1603.06017

    work page arXiv 2021

  29. [29]

    W. Parry. On the β-expansions of real numbers. Acta Math. Acad. Sci. Hung., 11:401– 416, 1960

    work page 1960

  30. [30]

    A. R´ enyi. Representations for real numbers and their ergodic properties. Acta Math. Acad. Sci. Hung., 8:477–493, 1957

    work page 1957

  31. [31]

    Rousseau

    C. Rousseau. The phi number system revisited. Math. Mag., 68:283–284, 1995

    work page 1995

  32. [32]

    G. R. Sanchis and L. A. Sanchis. On the frequency of occurrence of αi in the α- expansions of the positive integers. Fibonacci Quart., 39:123–137, 2001

    work page 2001

  33. [33]

    J. Shallit. Robbins and Ardila meet Berstel. Inform. Process. Lett., 167:106081, 2021

    work page 2021

  34. [34]

    J. Shallit. The Logical Approach To Automatic Sequences: Exploring Combinatorics on Words with Walnut, volume 482 of London Math. Soc. Lecture Note Series . Cam- bridge University Press, 2023

    work page 2023

  35. [35]

    Shallit, S

    J. Shallit, S. L. Shan, and K.-H. Yang. Automatic sequences in negative bases and proofs of some conjectures of Shevelev. RAIRO Inform. Th´ eor. App., 57:4, 2023

    work page 2023

  36. [36]

    N. J. A. Sloane et al. The on-line encyclopedia of integer sequences. Electronic resource, available at https://oeis.org, 2023. 32 Proving Properties of φ-Representations with the Walnut Theorem-Prover

    work page 2023

  37. [37]

    I. N. Stewart and D. O. Tall. Algebraic Number Theory. Chapman and Hall, 1979

    work page 1979

  38. [38]

    Zeckendorf

    E. Zeckendorf. Repr´ esentation des nombres naturels par une somme de nombres de Fibonacci ou de nombres de Lucas. Bull. Soc. Roy. Li` ege, 41:179–182, 1972. Received: December 1, 2023 Accepted for publication: April 25, 2024 Communicated by: Rigo Michel, Emilie Charlier and Julien Leroy 33

    work page 1972