Golden ratio base

DefinitionValue of a base phi expansion#✓fully proved

For a finite set \(S\) of integers, the base phi value of \(S\) is the real number \(\sum_{i \in S} \varphi^i\), where \(\varphi = (1 + \sqrt 5)/2\) is the golden ratio. It is the number represented by the base phi expansion with digit \(1\) at each position in \(S\) and digit \(0\) at every other position.

noncomputable def basePhiValue (S : Finset ℤ) : ℝ :=
  ∑ i ∈ S, φ ^ i

Sources

• Michel Dekking and Ad van Loon, Counting Base Phi Representations, Fibonacci Quarterly 62 (2024), Section 1 (definition of a base phi representation).

Used by 20

Used byThe empty base phi expansion has value zero · The base phi expansion \(10.01\) has value two · The single digit \(1\) at position \(0\) has value one · The base phi expansion \(1.11\) has value two · Lowest Bergman digit of \(N\) from its Lucas interval · Bergman expansion of \(L_{2n} + k\) · Recursive structure of Bergman expansions, odd Lucas case · Lucas interval of \(N\) from the gap between its two lowest Bergman digits · Bergman expansions of the Fibonacci numbers · Base phi expansion · Base phi expansion of one · Base phi expansion of zero · Recursion for the number of Knott expansions · Knott expansions · Natural expansions are counted by Fibonacci representations · Recursion for the number of natural expansions · Natural base phi expansions · The expansion 10.01 is a natural expansion of 2 · Golden mean flips connect all expansions to the Bergman expansion · A Knott expansion of two

DefinitionBergman expansions#✓fully proved

Encode a finite base phi expansion with digits \(0\) and \(1\) by the finite set \(S \subseteq \mathbb{Z}\) of positions of its digits \(1\). The expansion is a Bergman expansion when no two digits \(1\) are adjacent, that is, \(i + 1 \notin S\) for every \(i \in S\).

def IsBergmanExpansion (S : Finset ℤ) : Prop :=
  ∀ i ∈ S, i + 1 ∉ S

Sources

• Michel Dekking and Ad van Loon, Counting Base Phi Representations, Fibonacci Quarterly 62 (2024), Section 1 (Bergman representation).

Used by 14

Used byEvery even-length Zeckendorf word ending in \(1\) is a negative part · Lowest Bergman digit of \(N\) from its Lucas interval · Bergman expansion of \(L_{2n} + k\) · Recursive structure of Bergman expansions, odd Lucas case · Lucas interval of \(N\) from the gap between its two lowest Bergman digits · Bergman expansions of the Fibonacci numbers · Base phi expansion · Base phi expansion of one · Base phi expansion of zero · The expansion 10.01 is a Bergman expansion · Natural expansions are counted by Fibonacci representations · Natural base phi expansions · The expansion 10.01 is a natural expansion of 2 · Golden mean flips connect all expansions to the Bergman expansion

DefinitionGolden mean flips#✓fully proved

Encode a finite base phi expansion with digits \(0\) and \(1\) by the finite set of positions of its digits \(1\). An expansion \(T\) arises from an expansion \(S\) by a golden mean flip \(100 \to 011\) when there is a position \(i \in S\) with \(i - 1 \notin S\) and \(i - 2 \notin S\) such that \(T = (S \setminus \{i\}) \cup \{i - 1, i - 2\}\): the digit \(1\) at position \(i\) is replaced by digits \(1\) at positions \(i - 1\) and \(i - 2\), which were \(0\).

def IsGoldenMeanFlip (S T : Finset ℤ) : Prop :=
  ∃ i ∈ S, i - 1 ∉ S ∧ i - 2 ∉ S ∧ T = insert (i - 1) (insert (i - 2) (S.erase i))

Sources

• Michel Dekking and Ad van Loon, Counting Base Phi Representations, Fibonacci Quarterly 62 (2024), Sections 1 and 2 (the map T_i).

Used by 2

Used byA golden mean flip from 10.01 to 1.11 · Golden mean flips connect all expansions to the Bergman expansion

DefinitionKnott's truncation rule#✓fully proved

Let \(\varphi\) be the golden ratio. Encode a finite base \(\varphi\) expansion with digits \(0\) and \(1\) by the finite set \(S \subseteq \mathbb{Z}\) of the positions of its digits \(1\), and write \(a_i\) for its digit at position \(i\). The expansion satisfies Knott's condition when it does not end in the digits \(0, 1, 1\): if \(S\) is nonempty with least element \(R\), then \(a_{R+2} a_{R+1} a_R \ne 011\), that is, it is not the case that both \(R + 1 \in S\) and \(R + 2 \notin S\). The empty expansion satisfies the condition.

def SatisfiesKnottCondition (S : Finset ℤ) : Prop :=
  ∀ m ∈ S, (∀ j ∈ S, m ≤ j) → ¬ (m + 1 ∈ S ∧ m + 2 ∉ S)

Sources

• Michel Dekking and Ad van Loon, Counting Base Phi Representations, Fibonacci Quarterly 62 (2024), Section 1, Equation (1.1).

Used by 4

Used byKnott expansions · The expansion 0.11 violates Knott's truncation rule · The expansion 10.01 is a natural expansion of 2 · A Knott expansion of two

DefinitionKnott expansions#✓fully proved

Let \(\varphi\) be the golden ratio and \(N\) a natural number. Encode a finite base phi expansion with digits \(0\) and \(1\) by the finite set \(S \subseteq \mathbb{Z}\) of the positions of its digits \(1\). The Knott expansions of \(N\) are the expansions of value \(N\) that satisfy Knott's truncation rule: the set of all such \(S\) with \(\sum_{i \in S} \varphi^i = N\) that satisfy Knott's condition.

def knottExpansions (N : ℕ) : Set (Finset ℤ) :=
  {S | basePhiValue S = N ∧ SatisfiesKnottCondition S}

Sources

• Michel Dekking and Ad van Loon, Counting Base Phi Representations, Fibonacci Quarterly 62 (2024), Section 1.

Uses 2 · Used by 4

Statement usesKnott's truncation rule · Value of a base phi expansion

Used byNumber of Knott expansions · Natural base phi expansions · The expansion 10.01 is a natural expansion of 2 · A Knott expansion of two

DefinitionNumber of Knott expansions#✓fully proved

For a natural number \(N\), \(\mathrm{Tot}_\kappa(N)\) is the number of Knott expansions of \(N\) (OEIS A289749).

noncomputable def knottExpansionCount (N : ℕ) : ℕ :=
  (knottExpansions N).ncard

Sources

• Michel Dekking and Ad van Loon, Counting Base Phi Representations, Fibonacci Quarterly 62 (2024), Section 1.

Uses 1 · Used by 3

Statement usesKnott expansions

Used byRecursion for the number of Knott expansions · Knott expansions of Fibonacci numbers · Knott expansions of Lucas numbers

DefinitionNatural base phi expansions#✓fully proved

Let \(\varphi\) be the golden ratio and \(N\) a natural number. Encode a finite base phi expansion with digits \(0\) and \(1\) by the finite set \(S \subseteq \mathbb{Z}\) of the positions of its digits \(1\). The natural expansions of \(N\) are the Knott expansions \(S\) of \(N\) for which there is a Bergman expansion \(T\) with \(\sum_{i \in T} \varphi^i = N\) whose lowest digit \(1\) is at the same position as the lowest digit \(1\) of \(S\), that is, \(\min T = \min S\), where \(S\) and \(T\) both empty also counts as equal.

def naturalExpansions (N : ℕ) : Set (Finset ℤ) :=
  {S | S ∈ knottExpansions N ∧
    ∃ T : Finset ℤ, IsBergmanExpansion T ∧ basePhiValue T = N ∧ T.min = S.min}

Sources

• Michel Dekking and Ad van Loon, Counting Base Phi Representations, Fibonacci Quarterly 62 (2024), Section 4.

Uses 3 · Used by 2

Statement usesBergman expansions · Value of a base phi expansion · Knott expansions

Used byNumber of natural expansions · The expansion 10.01 is a natural expansion of 2

DefinitionNumber of natural expansions#✓fully proved

For a natural number \(N\), \(\mathrm{Tot}_\nu(N)\) is the number of natural base phi expansions of \(N\).

noncomputable def naturalExpansionCount (N : ℕ) : ℕ :=
  (naturalExpansions N).ncard

Sources

• Michel Dekking and Ad van Loon, Counting Base Phi Representations, Fibonacci Quarterly 62 (2024), Section 4.

Uses 1 · Used by 3

Statement usesNatural base phi expansions

Used byNatural expansions are counted by Fibonacci representations · Recursion for the number of natural expansions · Natural expansions of Fibonacci numbers

DefinitionNumber of Fibonacci representations#✓fully proved

For a natural number \(m\), \(\mathrm{Tot}_{\mathrm{FIB}}(m)\) is the number of finite sets \(T\) of indices \(i \ge 2\) with \(\sum_{i \in T} F_i = m\), where \(F_i\) are the Fibonacci numbers (\(F_0 = 0\), \(F_1 = 1\)); that is, the number of ways to write \(m\) as a sum of Fibonacci numbers with distinct indices at least \(2\) (OEIS A000119). Indices above \(m + 1\) never occur because \(F_{m+2} > m\).

def fibonacciRepresentationCount (m : ℕ) : ℕ :=
  ((Finset.Icc 2 (m + 1)).powerset.filter fun T => ∑ i ∈ T, Nat.fib i = m).card

Sources

• Michel Dekking and Ad van Loon, Counting Base Phi Representations, Fibonacci Quarterly 62 (2024), Section 1 (base Fibonacci representations).

Used by 2

Used bySmall values of the Fibonacci representation count · Natural expansions are counted by Fibonacci representations

TheoremThe empty base phi expansion has value zero#✓fully proved

The base phi value of the empty set of positions is \(0\).

theorem basePhiValue_empty : basePhiValue ∅ = 0

Sources

• Michel Dekking and Ad van Loon, Counting Base Phi Representations, Fibonacci Quarterly 62 (2024), Section 1.

Uses 1

Statement usesValue of a base phi expansion

TheoremThe single digit \(1\) at position \(0\) has value one#✓fully proved

The base phi value of the set \(\{0\}\) is \(1\), that is, \(\varphi^0 = 1\), where \(\varphi\) is the golden ratio.

theorem basePhiValue_singleton_zero : basePhiValue {0} = 1

Sources

• Michel Dekking and Ad van Loon, Counting Base Phi Representations, Fibonacci Quarterly 62 (2024), Section 1.

Uses 1

Statement usesValue of a base phi expansion

TheoremThe base phi expansion \(10.01\) has value two#✓fully proved

The base phi value of the set \(\{1, -2\}\) is \(2\), that is, \(\varphi + \varphi^{-2} = 2\), where \(\varphi\) is the golden ratio.

theorem basePhiValue_one_neg_two : basePhiValue {1, -2} = 2

Sources

• Michel Dekking and Ad van Loon, Counting Base Phi Representations, Fibonacci Quarterly 62 (2024), proof of Proposition 3.1.

Uses 1 · Used by 1

Statement usesValue of a base phi expansion

Used byThe expansion 10.01 is a natural expansion of 2

TheoremThe base phi expansion \(1.11\) has value two#✓fully proved

The base phi value of the set \(\{0, -1, -2\}\) is \(2\), that is, \(1 + \varphi^{-1} + \varphi^{-2} = 2\), where \(\varphi\) is the golden ratio.

theorem basePhiValue_zero_neg_one_neg_two : basePhiValue {0, -1, -2} = 2

Sources

• Michel Dekking and Ad van Loon, Counting Base Phi Representations, Fibonacci Quarterly 62 (2024), Section 2.

Uses 1 · Used by 1

Statement usesValue of a base phi expansion

Used byA Knott expansion of two

TheoremThe expansion 10.01 is a Bergman expansion#✓fully proved

The base phi expansion \(10.01\), with digits \(1\) at positions \(1\) and \(-2\) and digits \(0\) elsewhere, has no two adjacent digits \(1\), so it is a Bergman expansion.

theorem isBergmanExpansion_one_neg_two : IsBergmanExpansion {1, -2}

Sources

• Michel Dekking and Ad van Loon, Counting Base Phi Representations, Fibonacci Quarterly 62 (2024), Section 1.

Uses 1 · Used by 1

Statement usesBergman expansions

Used byThe expansion 10.01 is a natural expansion of 2

TheoremA golden mean flip from 10.01 to 1.11#✓fully proved

Applying the golden mean flip \(100 \to 011\) at the leading digit of \(10.01\) (the digit \(1\) at position \(1\), followed by digits \(0\) at positions \(0\) and \(-1\)) gives \(1.11\), the expansion with digits \(1\) at positions \(0\), \(-1\) and \(-2\).

theorem isGoldenMeanFlip_one_neg_two : IsGoldenMeanFlip {1, -2} {0, -1, -2}

Sources

• Michel Dekking and Ad van Loon, Counting Base Phi Representations, Fibonacci Quarterly 62 (2024), Section 2.

Uses 1

Statement usesGolden mean flips

TheoremA Knott expansion of two#✓fully proved

Let \(\varphi\) be the golden ratio. The base \(\varphi\) expansion \(1.11\), whose digits \(1\) sit at the positions \(0\), \(-1\) and \(-2\), is a Knott expansion of \(2\): its value is \(1 + \varphi^{-1} + \varphi^{-2} = 2\) and it satisfies Knott's truncation rule.

theorem zero_neg_one_neg_two_mem_knottExpansions : ({0, -1, -2} : Finset ℤ) ∈ knottExpansions 2

Sources

• Michel Dekking and Ad van Loon, Counting Base Phi Representations, Fibonacci Quarterly 62 (2024), Section 1.

Uses 4

Statement usesKnott expansions

Proof usesKnott's truncation rule · Value of a base phi expansion · The base phi expansion \(1.11\) has value two

TheoremThe expansion 0.11 violates Knott's truncation rule#✓fully proved

The finite base phi expansion \(0.11\), with digits \(1\) at positions \(-1\) and \(-2\) and no others, ends in the digits \(011\), so it does not satisfy Knott's truncation rule.

It represents \(1\), since \(\varphi^{-1} + \varphi^{-2} = 1\) for the golden ratio \(\varphi\), but is not a Knott expansion of \(1\).

theorem not_satisfiesKnottCondition_neg_one_neg_two :
    ¬ SatisfiesKnottCondition {-1, -2}

Sources

• Michel Dekking and Ad van Loon, Counting Base Phi Representations, Fibonacci Quarterly 62 (2024), Section 1, Equation (1.1).

Uses 1

Statement usesKnott's truncation rule

TheoremThe expansion 10.01 is a natural expansion of 2#✓fully proved

The finite base phi expansion \(10.01\), with digits \(1\) exactly at positions \(1\) and \(-2\), is a natural base phi expansion of \(2\).

It is the Bergman expansion of \(2\).

theorem one_neg_two_mem_naturalExpansions : ({1, -2} : Finset ℤ) ∈ naturalExpansions 2

Sources

• Michel Dekking and Ad van Loon, Counting Base Phi Representations, Fibonacci Quarterly 62 (2024), Section 4.

Uses 7

Statement usesNatural base phi expansions

Proof usesBergman expansions · Knott's truncation rule · Value of a base phi expansion · The base phi expansion \(10.01\) has value two · The expansion 10.01 is a Bergman expansion · Knott expansions

TheoremSmall values of the Fibonacci representation count#✓fully proved

Let \(F_i\) be the Fibonacci numbers (\(F_0 = 0\), \(F_1 = 1\)), and let \(\mathrm{Tot}_{\mathrm{FIB}}(m)\) be the number of ways to write \(m\) as a sum of Fibonacci numbers \(F_i\) with distinct indices \(i \ge 2\). Then \(\mathrm{Tot}_{\mathrm{FIB}}(0), \dots, \mathrm{Tot}_{\mathrm{FIB}}(8)\) are \(1, 1, 1, 2, 1, 2, 2, 1, 3\).

theorem fibonacciRepresentationCount_small :
    (List.range 9).map fibonacciRepresentationCount = [1, 1, 1, 2, 1, 2, 2, 1, 3]

Sources

• Michel Dekking and Ad van Loon, Counting Base Phi Representations, Fibonacci Quarterly 62 (2024), Section 1 (the listed values of Tot_FIB).

Uses 1

Statement usesNumber of Fibonacci representations

TheoremGolden mean flips connect all expansions to the Bergman expansion#●ready to prove

Let \(N\) be a natural number, let \(S\) be a Bergman expansion of \(N\) and let \(T\) be any finite base phi expansion of \(N\) with digits \(0\) and \(1\). Then \(T\) is obtained from \(S\) by finitely many (possibly zero) golden mean flips \(100 \to 011\).

public theorem_wanted reflTransGen_isGoldenMeanFlip_of_isBergmanExpansion (N : ℕ)
    {S T : Finset ℤ} (hS : IsBergmanExpansion S) (hSN : basePhiValue S = N)
    (hTN : basePhiValue T = N) :
    Relation.ReflTransGen IsGoldenMeanFlip S T

Sources

• Michel Dekking and Ad van Loon, Counting Base Phi Representations, Fibonacci Quarterly 62 (2024), Article 62-2/dekking11102023, Theorem 2.1.

Uses 3

Statement usesBergman expansions · Golden mean flips · Value of a base phi expansion

TheoremRecursion for the number of Knott expansions#●ready to prove

Let \(\varphi\) be the golden ratio, let \(N \ge 2\) and \(n\) be natural numbers, and let \(p_0, \dots, p_n\) be integers with \(p_{k+1} \ge p_k + 2\) for all \(k < n\) and \(\sum_{k=0}^{n} \varphi^{p_k} = N\). Thus \(N\) has the base phi expansion \(10^{s_n} \cdots 10^{s_1} 1\) with digits \(1\) at positions \(p_0 < \dots < p_n\), where \(s_k = p_k - p_{k-1} - 1\) for \(1 \le k \le n\). Let \(r_0, r_1, \dots\) be integers with \(r_0 = 1\); if \(n \ge 1\), let \(r_1 = s_1/2 + 1\) when \(s_1\) is even and \(r_1 = (s_1 + 1)/2 + 1\) when \(s_1\) is odd; and for \(2 \le k \le n\), let \(r_k = (s_k/2 + 1)\, r_{k-1}\) when \(s_k\) is even and \(r_k = ((s_k + 1)/2 + 1)\, r_{k-1} - r_{k-2}\) when \(s_k\) is odd. Then the number of Knott expansions of \(N\) is \(r_n\).

public theorem_wanted knottExpansionCount_eq_of_recursion (N : ℕ) (hN : 2 ≤ N) (n : ℕ)
    (p : ℕ → ℤ) (hgap : ∀ k < n, p k + 2 ≤ p (k + 1))
    (hval : basePhiValue ((Finset.range (n + 1)).image p) = N)
    (s : ℕ → ℤ) (hs : ∀ k, 1 ≤ k → k ≤ n → s k = p k - p (k - 1) - 1)
    (r : ℕ → ℤ) (hr0 : r 0 = 1)
    (hr1 : 1 ≤ n → (Even (s 1) → 2 * r 1 = s 1 + 2) ∧ (Odd (s 1) → 2 * r 1 = s 1 + 3))
    (hr : ∀ k, 2 ≤ k → k ≤ n →
      (Even (s k) → 2 * r k = (s k + 2) * r (k - 1)) ∧
      (Odd (s k) → 2 * r k = (s k + 3) * r (k - 1) - 2 * r (k - 2))) :
    (knottExpansionCount N : ℤ) = r n

Sources

• Michel Dekking and Ad van Loon, Counting Base Phi Representations, Fibonacci Quarterly 62 (2024), Article 62-2/dekking11102023, Theorem 2.3.

Uses 2

Statement usesValue of a base phi expansion · Number of Knott expansions

TheoremBergman expansions of the Fibonacci numbers#●ready to prove

Let \(n \ge 1\) and write \(F_m\) for the \(m\)-th Fibonacci number, with \(F_1 = F_2 = 1\). Let \(S\) be a finite set of integers with no two consecutive elements (a Bergman expansion). If the base phi value of \(S\) is \(F_{2n}\), then \(S = \{t + 4j : 0 \le j < n\}\) for some integer \(t\). If the base phi value of \(S\) is \(F_{2n+1}\), then \(S = \{t\} \cup \{t + 3 + 4j : 0 \le j < n\}\) for some integer \(t\).

Read from the highest to the lowest position, these are the digit words \((1000)^{n-1}1\) and \((1000)^{n-1}1001\); the position of the radix point is not determined.

public theorem_wanted bergmanWord_fib (n : ℕ) (hn : 1 ≤ n) :
    (∀ S : Finset ℤ, IsBergmanExpansion S → basePhiValue S = Nat.fib (2 * n) →
      ∃ t : ℤ, S = (Finset.range n).image fun j : ℕ => 4 * (j : ℤ) + t) ∧
    (∀ S : Finset ℤ, IsBergmanExpansion S → basePhiValue S = Nat.fib (2 * n + 1) →
      ∃ t : ℤ, S = insert t ((Finset.range n).image fun j : ℕ => 4 * (j : ℤ) + 3 + t))

Sources

• Michel Dekking and Ad van Loon, Counting Base Phi Representations, Fibonacci Quarterly 62 (2024), Article 62-2/dekking11102023, Proposition 3.1.

Uses 2

Statement usesBergman expansions · Value of a base phi expansion

TheoremKnott expansions of Fibonacci numbers#●ready to prove

Let \(F_n\) be the Fibonacci numbers (\(F_0 = 0\), \(F_1 = 1\)). For every \(n \ge 1\), the number of Knott expansions of \(F_n\) is \(F_n\).

public theorem_wanted knottExpansionCount_fib (n : ℕ) (hn : 1 ≤ n) :
    knottExpansionCount (Nat.fib n) = Nat.fib n

Sources

• Michel Dekking and Ad van Loon, Counting Base Phi Representations, Fibonacci Quarterly 62 (2024), Article 62-2/dekking11102023, Theorem 3.2.

Uses 1

Statement usesNumber of Knott expansions

TheoremKnott expansions of Lucas numbers#●ready to prove

For every \(n \ge 1\), each of the Lucas numbers \(L_{2n}\) and \(L_{2n+1}\) (with \(L_0 = 2\), \(L_1 = 1\)) has exactly \(2n + 1\) Knott expansions.

public theorem_wanted knottExpansionCount_lucasNumber (n : ℕ) (hn : 1 ≤ n) :
    knottExpansionCount (lucasNumber (2 * n)) = 2 * n + 1 ∧
      knottExpansionCount (lucasNumber (2 * n + 1)) = 2 * n + 1

Sources

• Michel Dekking and Ad van Loon, Counting Base Phi Representations, Fibonacci Quarterly 62 (2024), Article 62-2/dekking11102023, Theorem 3.3.

Uses 2

Statement usesNumber of Knott expansions · Lucas numbers

TheoremRecursion for the number of natural expansions#●ready to prove

Let \(N\) and \(n\) be natural numbers and let \(p_0, \dots, p_n\) be integers with \(p_k + 2 \le p_{k+1}\) for \(k < n\) such that the base phi expansion with digits \(1\) at positions \(p_0, \dots, p_n\) represents \(N\). Put \(s_k = p_k - p_{k-1} - 1\) for \(1 \le k \le n\). Let \(r_0, r_1, \dots\) be integers with \(r_0 = 1\) such that, if \(n \ge 1\), \(2 r_1 = s_1 + 2\) when \(s_1\) is even and \(2 r_1 = s_1 + 1\) when \(s_1\) is odd, and for \(2 \le k \le n\), \(2 r_k = (s_k + 2) r_{k-1}\) when \(s_k\) is even and \(2 r_k = (s_k + 3) r_{k-1} - 2 r_{k-2}\) when \(s_k\) is odd. Then the number \(\mathrm{Tot}_\nu(N)\) of natural base phi expansions of \(N\) equals \(r_n\).

Compared with the recursion for the number of Knott expansions, only the value of \(r_1\) for odd \(s_1\) differs, and \(N \ge 2\) is not assumed.

public theorem_wanted naturalExpansionCount_eq_of_recursion (N : ℕ) (n : ℕ)
    (p : ℕ → ℤ) (hgap : ∀ k < n, p k + 2 ≤ p (k + 1))
    (hval : basePhiValue ((Finset.range (n + 1)).image p) = N)
    (s : ℕ → ℤ) (hs : ∀ k, 1 ≤ k → k ≤ n → s k = p k - p (k - 1) - 1)
    (r : ℕ → ℤ) (hr0 : r 0 = 1)
    (hr1 : 1 ≤ n → (Even (s 1) → 2 * r 1 = s 1 + 2) ∧ (Odd (s 1) → 2 * r 1 = s 1 + 1))
    (hr : ∀ k, 2 ≤ k → k ≤ n →
      (Even (s k) → 2 * r k = (s k + 2) * r (k - 1)) ∧
      (Odd (s k) → 2 * r k = (s k + 3) * r (k - 1) - 2 * r (k - 2))) :
    (naturalExpansionCount N : ℤ) = r n

Sources

• Michel Dekking and Ad van Loon, Counting Base Phi Representations, Fibonacci Quarterly 62 (2024), Article 62-2/dekking11102023, Theorem 4.1.

Uses 2

Statement usesValue of a base phi expansion · Number of natural expansions

TheoremFibonacci numbers in the Lucas intervals#●ready to prove

Let \(F_k\) be the Fibonacci numbers (\(F_0 = 0\), \(F_1 = 1\)) and \(L_k\) the Lucas numbers (\(L_0 = 2\), \(L_1 = 1\)). Call \(\Lambda_{2n} = [L_{2n}, L_{2n+1}]\) the even Lucas interval and \(\Lambda_{2n+1} = [L_{2n+1} + 1, L_{2n+2} - 1]\) the odd Lucas interval. For every \(n \ge 1\), \(F_{2n+2} \in \Lambda_{2n}\) and \(F_{2n+3} \in \Lambda_{2n+1}\).

public theorem_wanted fib_mem_lucasIntervals (n : ℕ) (hn : 1 ≤ n) :
    Nat.fib (2 * n + 2) ∈ Set.Icc (lucasNumber (2 * n)) (lucasNumber (2 * n + 1)) ∧
      Nat.fib (2 * n + 3) ∈
        Set.Icc (lucasNumber (2 * n + 1) + 1) (lucasNumber (2 * n + 2) - 1)

Sources

• Michel Dekking and Ad van Loon, Counting Base Phi Representations, Fibonacci Quarterly 62 (2024), Article 62-2/dekking11102023, Lemma 4.2.

Uses 1

Statement usesLucas numbers

TheoremNatural expansions of Fibonacci numbers#●ready to prove

Write \(\mathrm{Tot}_\nu(N)\) for the number of natural base phi expansions of a natural number \(N\) and \(F_k\) for the \(k\)-th Fibonacci number. Then for every \(n \ge 0\), \(\mathrm{Tot}_\nu(F_{2n+2}) = F_{2n+1}\) and \(\mathrm{Tot}_\nu(F_{2n+3}) = F_{2n+3}\).

public theorem_wanted naturalExpansionCount_fib (n : ℕ) :
    naturalExpansionCount (Nat.fib (2 * n + 2)) = Nat.fib (2 * n + 1) ∧
      naturalExpansionCount (Nat.fib (2 * n + 3)) = Nat.fib (2 * n + 3)

Sources

• Michel Dekking and Ad van Loon, Counting Base Phi Representations, Fibonacci Quarterly 62 (2024), Article 62-2/dekking11102023, Theorem 4.3.

Uses 1

Statement usesNumber of natural expansions

TheoremNatural expansions are counted by Fibonacci representations#●ready to prove

Write \(F_k\) for the \(k\)-th Fibonacci number. Let \(N > 3\) be a natural number, let \(S\) be a Bergman expansion of \(N\) and let \(R\) be the lowest position of a digit \(1\) in \(S\). Then the number \(\mathrm{Tot}_\nu(N)\) of natural base phi expansions of \(N\) equals the number \(\mathrm{Tot}_{\mathrm{FIB}}(F_{2-R} N)\) of representations of \(F_{2-R} N\) as a sum of Fibonacci numbers with distinct indices at least \(2\).

public theorem_wanted naturalExpansionCount_eq_fibonacciRepresentationCount (N : ℕ)
    (hN : 3 < N) {S : Finset ℤ} (hS : IsBergmanExpansion S) (hSN : basePhiValue S = N)
    {R : ℤ} (hR : IsLeast (S : Set ℤ) R) :
    naturalExpansionCount N = fibonacciRepresentationCount (Nat.fib (2 - R).toNat * N)

Sources

• Michel Dekking and Ad van Loon, Counting Base Phi Representations, Fibonacci Quarterly 62 (2024), Article 62-2/dekking11102023, Theorem 4.4.

Uses 4

Statement usesBergman expansions · Value of a base phi expansion · Number of Fibonacci representations · Number of natural expansions

TheoremLucas interval of \(N\) from the gap between its two lowest Bergman digits#●ready to prove

Let \(N \ge 2\) be a natural number, let \(S\) be a finite set of integers with no two consecutive elements (a Bergman expansion) whose base phi value is \(N\), and let \(a\) be an integer and \(s\) a natural number such that the elements of \(S\) that are at most \(a + s + 1\) are exactly \(a\) and \(a + s + 1\) (so the expansion ends in the digits \(10^s1\)). Write \(L_m\) for the \(m\)-th Lucas number. Then \(L_{2n} \le N \le L_{2n+1}\) for some natural number \(n\) if and only if \(s\) is odd, and \(L_{2n+1} + 1 \le N \le L_{2n+2} - 1\) for some natural number \(n\) if and only if \(s\) is even.

public theorem_wanted bergman_tail_parity_iff_lucasInterval (N : ℕ) (hN : 2 ≤ N)
    {S : Finset ℤ} (hS : IsBergmanExpansion S) (hSN : basePhiValue S = N) (a : ℤ) (s : ℕ)
    (htail : S.filter (· ≤ a + s + 1) = {a, a + s + 1}) :
    ((∃ n : ℕ, N ∈ Set.Icc (lucasNumber (2 * n)) (lucasNumber (2 * n + 1))) ↔ Odd s) ∧
      ((∃ n : ℕ, N ∈ Set.Icc (lucasNumber (2 * n + 1) + 1) (lucasNumber (2 * n + 2) - 1)) ↔
        Even s)

Sources

• Michel Dekking and Ad van Loon, Counting Base Phi Representations, Fibonacci Quarterly 62 (2024), Article 62-2/dekking11102023, Proposition 5.1(a).

Uses 3

Statement usesBergman expansions · Value of a base phi expansion · Lucas numbers

TheoremLowest Bergman digit of \(N\) from its Lucas interval#●ready to prove

Let \(N\) and \(n\) be natural numbers, let \(S\) be a finite set of integers with no two consecutive elements (a Bergman expansion) whose base phi value is \(N\), and let \(R\) be the least element of \(S\). Write \(L_m\) for the \(m\)-th Lucas number. If \(L_{2n} \le N \le L_{2n+1}\), then \(-R = 2n\). If \(L_{2n+1} + 1 \le N \le L_{2n+2} - 1\), then \(-R = 2n + 2\).

public theorem_wanted bergman_lowest_position_lucasInterval (N n : ℕ) {S : Finset ℤ}
    (hS : IsBergmanExpansion S) (hSN : basePhiValue S = N) {R : ℤ}
    (hR : IsLeast (S : Set ℤ) R) :
    (N ∈ Set.Icc (lucasNumber (2 * n)) (lucasNumber (2 * n + 1)) → -R = 2 * n) ∧
      (N ∈ Set.Icc (lucasNumber (2 * n + 1) + 1) (lucasNumber (2 * n + 2) - 1) →
        -R = 2 * n + 2)

Sources

• Michel Dekking and Ad van Loon, Counting Base Phi Representations, Fibonacci Quarterly 62 (2024), Article 62-2/dekking11102023, Proposition 5.1(b).

Uses 3

Statement usesBergman expansions · Value of a base phi expansion · Lucas numbers

TheoremBergman expansion of \(L_{2n} + k\)#●ready to prove

Let \(n \ge 1\) and let \(k\) be a natural number with \(k \le L_{2n-1}\), where \(L_m\) is the \(m\)-th Lucas number. Let \(S\) and \(T\) be finite sets of integers, each with no two consecutive elements (Bergman expansions), whose base phi values are \(k\) and \(L_{2n} + k\) respectively. Then \(2n \notin S\), \(-2n \notin S\), and \(T = S \cup \{2n, -2n\}\).

public theorem_wanted bergman_lucas_even_add (n k : ℕ) (hn : 1 ≤ n)
    (hk : k ≤ lucasNumber (2 * n - 1)) {S T : Finset ℤ}
    (hS : IsBergmanExpansion S) (hSk : basePhiValue S = k)
    (hT : IsBergmanExpansion T) (hTN : basePhiValue T = (lucasNumber (2 * n) + k : ℕ)) :
    (2 * n : ℤ) ∉ S ∧ -(2 * n : ℤ) ∉ S ∧ T = insert (2 * n : ℤ) (insert (-(2 * n : ℤ)) S)

Sources

• Michel Dekking and Ad van Loon, Counting Base Phi Representations, Fibonacci Quarterly 62 (2024), Article 62-2/dekking11102023, Theorem 5.2 I, quoting F. M. Dekking, How to add two numbers in base phi.

Uses 3

Statement usesBergman expansions · Value of a base phi expansion · Lucas numbers

TheoremRecursive structure of Bergman expansions, odd Lucas case#●ready to prove

Let \(n \ge 2\), let \(k\) be a natural number, and write \(L_m\) for the \(m\)-th Lucas number. Call a finite set of integers with no two consecutive elements a Bergman expansion. Let \(S\) and \(T\) be Bergman expansions, let \(a\) and \(t\) be the least and the greatest element of \(S\), let \(S' = S \setminus \{a, t\}\), and for an integer \(c\) write \(S' + c = \{x + c : x \in S'\}\).

(i) If \(1 \le k \le L_{2n-2} - 1\), the base phi value of \(S\) is \(L_{2n-1} + k\) and that of \(T\) is \(L_{2n+1} + k\), then there is an integer \(b\) with \(T = \{b, b + 3, b + (t - a) + 4\} \cup (S' + (b - a + 2))\).

(ii) If \(1 \le k \le L_{2n-2} - 1\), the base phi value of \(S\) is \(L_{2n-1} + k\) and that of \(T\) is \(L_{2n+1} + L_{2n-1} + k\), then there is an integer \(b\) with \(T = \{b, b + (t - a) + 2, b + (t - a) + 4\} \cup (S' + (b - a + 2))\).

(iii) If \(k \le L_{2n-3}\), the base phi value of \(S\) is \(L_{2n-2} + k\) and that of \(T\) is \(L_{2n+1} + L_{2n-2} + k\), then there is an integer \(b\) with \(T = \{b, b + 3, b + (t - a) + 4, b + (t - a) + 7\} \cup (S' + (b - a + 4))\).

MetaMathlibExt.bergman_lucas_odd_add · 22 lines

public theorem_wanted bergman_lucas_odd_add (n : ℕ) (hn : 2 ≤ n) :
    (∀ k : ℕ, 1 ≤ k → k ≤ lucasNumber (2 * n - 2) - 1 →
      ∀ S T : Finset ℤ, ∀ a t : ℤ, IsBergmanExpansion S →
        basePhiValue S = (lucasNumber (2 * n - 1) + k : ℕ) →
        IsLeast (S : Set ℤ) a → IsGreatest (S : Set ℤ) t → IsBergmanExpansion T →
        basePhiValue T = (lucasNumber (2 * n + 1) + k : ℕ) →
        ∃ b : ℤ, T = {b, b + 3, b + (t - a) + 4} ∪
          ((S.erase a).erase t).image (· + (b - a + 2))) ∧
    (∀ k : ℕ, 1 ≤ k → k ≤ lucasNumber (2 * n - 2) - 1 →
      ∀ S T : Finset ℤ, ∀ a t : ℤ, IsBergmanExpansion S →
        basePhiValue S = (lucasNumber (2 * n - 1) + k : ℕ) →
        IsLeast (S : Set ℤ) a → IsGreatest (S : Set ℤ) t → IsBergmanExpansion T →
        basePhiValue T = (lucasNumber (2 * n + 1) + lucasNumber (2 * n - 1) + k : ℕ) →
        ∃ b : ℤ, T = {b, b + (t - a) + 2, b + (t - a) + 4} ∪
          ((S.erase a).erase t).image (· + (b - a + 2))) ∧
    (∀ k : ℕ, k ≤ lucasNumber (2 * n - 3) →
      ∀ S T : Finset ℤ, ∀ a t : ℤ, IsBergmanExpansion S →
        basePhiValue S = (lucasNumber (2 * n - 2) + k : ℕ) →
        IsLeast (S : Set ℤ) a → IsGreatest (S : Set ℤ) t → IsBergmanExpansion T →
        basePhiValue T = (lucasNumber (2 * n + 1) + lucasNumber (2 * n - 2) + k : ℕ) →
        ∃ b : ℤ, T = {b, b + 3, b + (t - a) + 4, b + (t - a) + 7} ∪
          ((S.erase a).erase t).image (· + (b - a + 4)))

Sources

• Michel Dekking and Ad van Loon, Counting Base Phi Representations, Fibonacci Quarterly 62 (2024), Article 62-2/dekking11102023, Theorem 5.2 II, quoting F. M. Dekking, How to add two numbers in base phi.

Uses 3

Statement usesBergman expansions · Value of a base phi expansion · Lucas numbers

DefinitionBase phi expansion#✓fully proved

Let \(\varphi\) be the golden ratio. A finite set \(S\) of integers, read as the positions of the digits \(1\) of a finite expansion with digits \(0\) and \(1\), is a base phi expansion of the natural number \(N\) when it is a Bergman expansion (no two digits \(1\) are adjacent: \(i \in S\) implies \(i + 1 \notin S\)) and its value \(\sum_{i \in S} \varphi^i\) equals \(N\).

def IsBasePhiExpansion (N : ℕ) (S : Finset ℤ) : Prop :=
  IsBergmanExpansion S ∧ basePhiValue S = N

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Section 1 (definition of β(N)).

Uses 2 · Used by 17

Statement usesBergman expansions · Value of a base phi expansion

Used byThe digit blocks \(10 \cdot 1\) and \(00 \cdot 1\) around the radix point · Border words and codes of Lucas numbers · The codes of the negative parts follow an orbit of addition modulo a Fibonacci number · The codes of the negative parts follow the golden rotation · Every even-length Zeckendorf word ending in \(1\) is a negative part · The blocks \(10^{2m} \cdot 1\) and \(10^{2m+1} \cdot 0\) never occur · For \(m \ge 2\), no base phi expansion has end block \(1\,0^{2m}\,1\) · Occurrence set of a digit block · Embedding of base phi expansions into Zeckendorf expansions · Propagation principle for base phi expansions · Recursive structure theorem for base phi expansions, part (A) · Recursive structure of the negative parts of base phi expansions · Recursive structure of base phi expansions on Lucas intervals · Trident splitting at an even Lucas number · Base phi expansion of one · Base phi expansion of zero · A base phi expansion of 1 ends in the digit 1

TheoremBase phi expansion of zero#✓fully proved

The empty set of positions, the expansion with no digit \(1\), is a base phi expansion of \(0\): it has no two adjacent digits \(1\), and its value, the empty sum, is equal to \(0\).

theorem isBasePhiExpansion_zero : IsBasePhiExpansion 0 ∅

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Section 1.

Uses 3

Statement usesBase phi expansion

Proof usesBergman expansions · Value of a base phi expansion

TheoremBase phi expansion of one#✓fully proved

The set \(\{0\}\), read as the positions of the digits \(1\), is a base phi expansion of \(1\): the expansion with a single digit \(1\) at position \(0\) has no two adjacent digits \(1\), and its value \(\varphi^0\) equals \(1\), where \(\varphi\) is the golden ratio.

theorem isBasePhiExpansion_one : IsBasePhiExpansion 1 {0}

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Table 1.

Uses 3 · Used by 1

Statement usesBase phi expansion

Proof usesBergman expansions · Value of a base phi expansion

Used byA base phi expansion of 1 ends in the digit 1

DefinitionDigit block of an expansion#✓fully proved

Let \(S\) be a finite set of integers, read as the positions of the digits \(1\) of an expansion with digits \(d_i\), so \(d_i = 1\) if \(i \in S\) and \(d_i = 0\) otherwise. For an integer \(k\) and a finite word \(w = w_0 w_1 \cdots w_{m-1}\) over the natural numbers, \(w\) occurs as a digit block of \(S\) at position \(k\) when the digits \(d_k d_{k-1} \cdots d_{k-m+1}\), read from the highest position down, are the letters of \(w\): for every \(i < m\), \(d_{k-i} = 1\) holds exactly when \(w_i = 1\). A letter \(1\) stands for the digit \(1\) and any other letter for the digit \(0\); the empty word occurs at every position.

def HasDigitBlock (S : Finset ℤ) : ℤ → List ℕ → Prop
  | _, [] => True
  | k, b :: w => (k ∈ S ↔ b = 1) ∧ HasDigitBlock S (k - 1) w

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Sections 6 and 7 (digit blocks d_{m-1} ⋯ d_0 and d_{-1} ⋯ d_{-m}).

Used by 8

Used byThe digit blocks \(10 \cdot 1\) and \(00 \cdot 1\) around the radix point · The blocks \(10^{2m} \cdot 1\) and \(10^{2m+1} \cdot 0\) never occur · For \(m \ge 2\), no base phi expansion has end block \(1\,0^{2m}\,1\) · Occurrence set of a digit block · Propagation principle for base phi expansions · Peeling off the leading letter of a digit block · The empty digit block occurs everywhere · A base phi expansion of 1 ends in the digit 1

TheoremThe empty digit block occurs everywhere#✓fully proved

For every finite set \(S\) of integers, read as the positions of the digits \(1\) of an expansion, and every integer \(k\), the empty word occurs as a digit block of \(S\) at position \(k\).

theorem hasDigitBlock_nil (S : Finset ℤ) (k : ℤ) : HasDigitBlock S k []

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Section 6.

Uses 1

Statement usesDigit block of an expansion

TheoremPeeling off the leading letter of a digit block#✓fully proved

Let \(S\) be a finite set of integers, read as the positions of the digits \(1\) of an expansion. For every integer \(k\), every natural number \(b\) and every finite word \(w\) over the natural numbers, the word \(bw\) (the letter \(b\) followed by \(w\)) occurs as a digit block of \(S\) at position \(k\) if and only if both \(k \in S\) holds exactly when \(b = 1\), and \(w\) occurs as a digit block of \(S\) at position \(k - 1\).

theorem hasDigitBlock_cons (S : Finset ℤ) (k : ℤ) (b : ℕ) (w : List ℕ) :
    HasDigitBlock S k (b :: w) ↔ (k ∈ S ↔ b = 1) ∧ HasDigitBlock S (k - 1) w

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Section 6.

Uses 1

Statement usesDigit block of an expansion

DefinitionOccurrence set of a digit block#✓fully proved

For an integer \(k\) and a word \(w = w_1 w_2 \cdots w_\ell\) of natural numbers, the occurrence set of \(w\) at position \(k\) is the set of natural numbers \(N\) that have a base phi expansion \(S\) (the set of positions of its digits \(1\)) whose digits \(d_k d_{k-1} \cdots d_{k-\ell+1}\) spell \(w\): for each \(j = 1, \dots, \ell\), the position \(k - j + 1\) lies in \(S\) if and only if \(w_j = 1\).

The paper's \(R_w\), the set of \(N\) whose expansion has the end block \(w\) at positions \(\ell - 1, \dots, 0\), is the case \(k = \ell - 1\), and \(R_{\cdot w}\), the set of \(N\) whose digits at positions \(-1, \dots, -\ell\) spell \(w\), is the case \(k = -1\).

def basePhiOccurrences (k : ℤ) (w : List ℕ) : Set ℕ :=
  {N | ∃ S, IsBasePhiExpansion N S ∧ HasDigitBlock S k w}

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Sections 6 and 7 (occurrence sequences R_w).

Uses 2 · Used by 7

Statement usesDigit block of an expansion · Base phi expansion

Used byEnd blocks \(u1 \cdot 0\) and \(u0 \cdot 0\) of consecutive numbers · End blocks ending in \(0\) are Lucas–Wythoff sequences · End blocks ending in \(1\) are Lucas–Wythoff sequences · Short end blocks · End blocks of length at most three ending in \(0\) · Short prefixes of the negative parts of base phi expansions · A base phi expansion of 1 ends in the digit 1

TheoremA base phi expansion of 1 ends in the digit 1#✓fully proved

The number \(1\) lies in the occurrence set of the one-letter digit block \(1\) placed at position \(0\) (the paper's \(R_1\)): some base phi expansion of \(1\) has the digit \(1\) at position \(0\).

theorem one_mem_basePhiOccurrences_one : 1 ∈ basePhiOccurrences 0 [1]

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Theorem 6.

Uses 4

Statement usesOccurrence set of a digit block

Proof usesDigit block of an expansion · Base phi expansion · Base phi expansion of one

DefinitionGeneralized Beatty sequence#✓fully proved

Let \(\varphi\) be the golden ratio. For integers \(p, q, r\), the generalized Beatty sequence \(V(p, q, r)\) is the integer sequence defined for every natural number \(n\), including \(n = 0\), by \(V(p, q, r)(n) = p\lfloor n\varphi \rfloor + qn + r\).

noncomputable def generalizedBeatty (p q r : ℤ) (n : ℕ) : ℤ :=
  p * ⌊(n : ℝ) * φ⌋ + q * n + r

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Section 5.

Used by 9

Used byThe value at one is a term of a generalized Beatty sequence · Embedding of base phi expansions into Zeckendorf expansions · Terms of a generalized Beatty sequence · Terms of a generalized Beatty sequence from index zero · Generalized Beatty sequences composed with the Wythoff sequences · First differences of a generalized Beatty sequence · Generalized Beatty sequence at one · Generalized Beatty sequence at zero · The initial term of a generalized Beatty set

TheoremGeneralized Beatty sequence at zero#✓fully proved

Let \(\varphi\) be the golden ratio. For all integers \(p, q, r\), the generalized Beatty sequence \(V(p, q, r)(n) = p\lfloor n\varphi \rfloor + qn + r\) takes the value \(V(p, q, r)(0) = r\) at \(n = 0\).

theorem generalizedBeatty_zero (p q r : ℤ) : generalizedBeatty p q r 0 = r

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Section 6 (V₀).

Uses 1 · Used by 1

Statement usesGeneralized Beatty sequence

Used byThe initial term of a generalized Beatty set

TheoremGeneralized Beatty sequence at one#✓fully proved

Let \(\varphi\) be the golden ratio. For all integers \(p, q, r\), the generalized Beatty sequence \(V(p, q, r)(n) = p\lfloor n\varphi \rfloor + qn + r\) takes the value \(V(p, q, r)(1) = p + q + r\) at \(n = 1\), since \(\lfloor \varphi \rfloor = 1\).

theorem generalizedBeatty_one (p q r : ℤ) : generalizedBeatty p q r 1 = p + q + r

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Section 5.

Uses 1 · Used by 1

Statement usesGeneralized Beatty sequence

Used byThe value at one is a term of a generalized Beatty sequence

DefinitionTerms of a generalized Beatty sequence#✓fully proved

For integers \(p\), \(q\) and \(r\), this is the set of integers \(p \lfloor n\varphi \rfloor + qn + r\) for natural numbers \(n \ge 1\), where \(\varphi\) is the golden ratio: the set of terms \(V(p, q, r)(n)\), \(n \ge 1\), of the generalized Beatty sequence \(V(p, q, r)\).

def beattySet (p q r : ℤ) : Set ℤ :=
  {x | ∃ n : ℕ, 1 ≤ n ∧ x = generalizedBeatty p q r n}

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Section 5.

Uses 1 · Used by 8

Statement usesGeneralized Beatty sequence

Used byThe value at one is a term of a generalized Beatty sequence · The digit blocks \(10 \cdot 1\) and \(00 \cdot 1\) around the radix point · End blocks ending in \(0\) are Lucas–Wythoff sequences · End blocks ending in \(1\) are Lucas–Wythoff sequences · Short end blocks · End blocks of length at most three ending in \(0\) · Short prefixes of the negative parts of base phi expansions · Complement of the lower Wythoff part of a generalized Beatty sequence

DefinitionTerms of a generalized Beatty sequence from index zero#✓fully proved

For integers \(p\), \(q\) and \(r\), this is the set of integers \(p \lfloor n\varphi \rfloor + qn + r\) for all natural numbers \(n \ge 0\), where \(\varphi\) is the golden ratio: the set of values \(V(p, q, r)(n)\), \(n \ge 0\), of the generalized Beatty sequence \(V(p, q, r)\), which the paper denotes \(V_0(p, q, r)\).

def beattySet₀ (p q r : ℤ) : Set ℤ :=
  Set.range (generalizedBeatty p q r)

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Section 6 (definition of V₀).

Uses 1 · Used by 6

Statement usesGeneralized Beatty sequence

Used byEnd blocks ending in \(0\) are Lucas–Wythoff sequences · End blocks ending in \(1\) are Lucas–Wythoff sequences · Short end blocks · End blocks of length at most three ending in \(0\) · Short prefixes of the negative parts of base phi expansions · The initial term of a generalized Beatty set

TheoremThe value at one is a term of a generalized Beatty sequence#✓fully proved

Let \(\varphi\) be the golden ratio. For all integers \(p, q, r\), the number \(p + q + r\) is a term \(p \lfloor n \varphi \rfloor + q n + r\), \(n \ge 1\), of the generalized Beatty sequence \(V(p, q, r)\); it is the term at \(n = 1\), since \(\lfloor \varphi \rfloor = 1\).

theorem add_add_mem_beattySet (p q r : ℤ) : p + q + r ∈ beattySet p q r

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Section 5.

Uses 3

Statement usesTerms of a generalized Beatty sequence

Proof usesGeneralized Beatty sequence · Generalized Beatty sequence at one

TheoremThe initial term of a generalized Beatty set#✓fully proved

For all integers \(p\), \(q\) and \(r\), the integer \(r\) belongs to the set \(V_0(p, q, r)\) of terms \(p \lfloor n\varphi \rfloor + qn + r\), \(n \ge 0\), of the generalized Beatty sequence, where \(\varphi\) is the golden ratio; indeed \(r\) is its term at \(n = 0\).

theorem mem_beattySet₀_self (p q r : ℤ) : r ∈ beattySet₀ p q r

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Section 6.

Uses 3

Statement usesTerms of a generalized Beatty sequence from index zero

Proof usesGeneralized Beatty sequence · Generalized Beatty sequence at zero

TheoremThe blocks \(10^{2m} \cdot 1\) and \(10^{2m+1} \cdot 0\) never occur#●ready to prove

For every \(m \ge 1\), no base phi expansion of a natural number has digits \(d_{2m} \cdots d_0 \cdot d_{-1} = 10^{2m} \cdot 1\), and none has digits \(d_{2m+1} \cdots d_0 \cdot d_{-1} = 10^{2m+1} \cdot 0\).

public theorem_wanted basePhi_no_block_one_zeros_dot (m : ℕ) (hm : 1 ≤ m) (N : ℕ)
    (S : Finset ℤ) (hS : IsBasePhiExpansion N S) :
    ¬ HasDigitBlock S (2 * m) (1 :: List.replicate (2 * m) 0 ++ [1]) ∧
      ¬ HasDigitBlock S (2 * m + 1) (1 :: List.replicate (2 * m + 1) 0 ++ [0])

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Lemma 1.

Uses 2

Statement usesDigit block of an expansion · Base phi expansion

TheoremPropagation principle for base phi expansions#●ready to prove

Let \(w = w_1 \cdots w_8\) be a word of length \(8\) over the natural numbers. Say that a base phi expansion \(S\) (the set of positions of its digits \(1\)) contains \(w\) centrally if for each \(j = 1, \dots, 8\) the position \(4 - j\) lies in \(S\) exactly when \(w_j = 1\), that is, if its digits \(d_3 d_2 d_1 d_0 \cdot d_{-1} d_{-2} d_{-3} d_{-4}\) spell \(w\). If no base phi expansion of any natural number \(N \le 17\) contains \(w\) centrally, then no base phi expansion of any natural number contains \(w\) centrally.

The hypothesis includes \(N = 0\), as in the paper's proof.

public theorem_wanted basePhi_propagation_principle (w : List ℕ) (hw : w.length = 8)
    (h : ∀ N ≤ 17, ∀ S, IsBasePhiExpansion N S → ¬ HasDigitBlock S 3 w) (N : ℕ)
    (S : Finset ℤ) (hS : IsBasePhiExpansion N S) : ¬ HasDigitBlock S 3 w

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Lemma 2 (a).

Uses 2

Statement usesDigit block of an expansion · Base phi expansion

TheoremGeneralized Beatty sequences composed with the Wythoff sequences#●ready to prove

Let \(\varphi\) be the golden ratio and, for integers \(a\), \(b\), \(c\) and natural numbers \(n\), let \(V(a, b, c)(n) = a \lfloor n\varphi \rfloor + bn + c\). Let \(A(n) = \lfloor n\varphi \rfloor\) and \(B(n) = \lfloor n\varphi \rfloor + n\) be the lower and upper Wythoff sequences. For all integers \(p\), \(q\), \(r\) and every natural number \(n \ge 1\), \(V(p, q, r)(A(n)) = V(p + q, p, r - p)(n)\) and \(V(p, q, r)(B(n)) = V(2p + q, p + q, r)(n)\).

public theorem_wanted generalizedBeatty_comp_wythoff (p q r : ℤ) (n : ℕ) (hn : 1 ≤ n) :
    generalizedBeatty p q r ⌊(n : ℝ) * φ⌋₊ = generalizedBeatty (p + q) p (r - p) n ∧
      generalizedBeatty p q r (⌊(n : ℝ) * φ⌋₊ + n) =
        generalizedBeatty (2 * p + q) (p + q) r n

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Lemma 3.

Uses 1

Statement usesGeneralized Beatty sequence

TheoremComplement of the lower Wythoff part of a generalized Beatty sequence#●ready to prove

Let \(\varphi\) be the golden ratio and, for integers \(a\), \(b\), \(c\), let \(V(a, b, c)\) be the set of integers \(a \lfloor n\varphi \rfloor + bn + c\) for natural numbers \(n \ge 1\). Let \(p\), \(q\), \(r\) be integers with \(p + q > 0\) and \(2p + q > 0\). If \(U\) and \(W\) are disjoint sets of integers with \(U \cup W = V(p, q, r)\) and \(U = V(p + q, p, r - p)\), then \(W = V(2p + q, p + q, r)\).

This is the converse of the composition lemma. The hypotheses \(p + q > 0\) and \(2p + q > 0\) say that the sequence \(n \mapsto p \lfloor n\varphi \rfloor + qn + r\) is increasing, as the paper's sequences are.

public theorem_wanted beattySet_complement_of_lowerWythoff (p q r : ℤ) (hpq : 0 < p + q)
    (h2pq : 0 < 2 * p + q) (U W : Set ℤ) (hdisj : Disjoint U W)
    (hunion : U ∪ W = beattySet p q r) (hU : U = beattySet (p + q) p (r - p)) :
    W = beattySet (2 * p + q) (p + q) r

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Lemma 4.

Uses 1

Statement usesTerms of a generalized Beatty sequence

TheoremFirst differences of a generalized Beatty sequence#●ready to prove

Let \(\varphi\) be the golden ratio, for integers \(p, q, r\) let \(V(p, q, r)\) be the sequence \(n \mapsto p\lfloor n\varphi \rfloor + qn + r\) on the natural numbers, and let \(x_0 x_1 x_2 \cdots\) be the infinite Fibonacci word. For all integers \(p, q, r\) and every \(n \ge 1\), the difference \(V(p, q, r)(n+1) - V(p, q, r)(n)\) equals \(p + q\) if \(x_{n-1} = 1\) and \(2p + q\) if \(x_{n-1} = 0\). Conversely, for all integers \(a, b\) and every sequence \(v\) of integers indexed by the natural numbers such that, for every \(n \ge 1\), \(v(n+1) - v(n)\) equals \(b\) if \(x_{n-1} = 1\) and \(a\) if \(x_{n-1} = 0\), there is an integer \(r'\) with \(v(n) = V(a - b, 2b - a, r')(n)\) for every \(n \ge 1\).

public theorem_wanted generalizedBeatty_diff_eq_fibInf (p q r : ℤ) :
    (∀ n : ℕ, 1 ≤ n → generalizedBeatty p q r (n + 1) - generalizedBeatty p q r n =
      if fibInf (n - 1) then p + q else 2 * p + q) ∧
    ∀ (a b : ℤ) (v : ℕ → ℤ),
      (∀ n : ℕ, 1 ≤ n → v (n + 1) - v n = if fibInf (n - 1) then b else a) →
        ∃ r' : ℤ, ∀ n : ℕ, 1 ≤ n → v n = generalizedBeatty (a - b) (2 * b - a) r' n

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Lemma 5.

Uses 2

Statement usesInfinite Fibonacci word · Generalized Beatty sequence

TheoremFor \(m \ge 2\), no base phi expansion has end block \(1\,0^{2m}\,1\)#●ready to prove

Let \(m \ge 2\), let \(N\) be a natural number and let \(S\) be a base phi expansion of \(N\), given as the set of positions of its digits \(1\). Then the digits \(d_{2m+1} d_{2m} \cdots d_1 d_0\) at positions \(2m+1, \dots, 0\) are not \(1\,0^{2m}\,1\): it is not the case that \(2m+1 \in S\), \(0 \in S\) and no \(i\) with \(1 \le i \le 2m\) lies in \(S\).

public theorem_wanted basePhi_no_end_block_one_zeros_one (m : ℕ) (hm : 2 ≤ m) (N : ℕ)
    (S : Finset ℤ) (hS : IsBasePhiExpansion N S) :
    ¬ HasDigitBlock S (2 * m + 1) (1 :: List.replicate (2 * m) 0 ++ [1])

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Lemma 6.

Uses 2

Statement usesDigit block of an expansion · Base phi expansion

TheoremEnd blocks \(u1 \cdot 0\) and \(u0 \cdot 0\) of consecutive numbers#●ready to prove

Let \(u\) be a nonempty word of length \(m - 1\), read as the digits \(d_{m-1} \cdots d_1\) (a letter \(1\) is a digit \(1\), any other letter a digit \(0\)), such that the word \(u1\) has no two adjacent letters \(1\). Then for every \(N \ge 1\), some base phi expansion of \(N\) has digits \(d_{m-1} \cdots d_1 d_0 \cdot d_{-1} = u1 \cdot 0\) if and only if some base phi expansion of \(N - 1\) has digits \(d_{m-1} \cdots d_1 d_0 \cdot d_{-1} = u0 \cdot 0\).

The hypothesis that \(u1\) has no \(11\) is the paper's implicit standing assumption on digit blocks: for \(u = 1\) the block \(11 \cdot 0\) never occurs, while \(10 \cdot 0\) occurs in the expansion \(10 \cdot 01\) of \(2\).

public theorem_wanted basePhi_end_block_one_iff_pred (u : List ℕ) (hu : u ≠ [])
    (hz : List.IsChain (fun a b => ¬ (a = 1 ∧ b = 1)) (u ++ [1])) (N : ℕ) (hN : 1 ≤ N) :
    N ∈ basePhiOccurrences u.length (u ++ [1, 0]) ↔
      N - 1 ∈ basePhiOccurrences u.length (u ++ [0, 0])

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Lemma 7.

Uses 1

Statement usesOccurrence set of a digit block

TheoremLucas numbers from Fibonacci numbers#●ready to prove

For every natural number \(n\), \(F_n + 3F_{n+1} = L_{n+2}\), where \(F_j\) is the \(j\)-th Fibonacci number (\(F_0 = 0\), \(F_1 = 1\)) and \(L_j\) is the \(j\)-th Lucas number (\(L_0 = 2\), \(L_1 = 1\)).

public theorem_wanted fib_add_three_mul_fib_succ_eq_lucasNumber (n : ℕ) :
    Nat.fib n + 3 * Nat.fib (n + 1) = lucasNumber (n + 2)

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Lemma 9.

Uses 1

Statement usesLucas numbers

TheoremBorder words and codes of Lucas numbers#●ready to prove

Let \(n \ge 1\), and write \(F_k\) for the Fibonacci numbers and \(L_k\) for the Lucas numbers. Let \(S_1, S_2, S_3, S_4\) be base phi expansions (sets of positions of the digits \(1\)) of \(L_{2n}\), \(L_{2n+1}\), \(L_{2n+1} + 1\) and \(L_{2n+2} - 1\) respectively, and let \(S_k^-\) be the set of negative positions in \(S_k\). Then \(S_1^- = \{-2n\}\), \(S_2^- = \{-2j : 1 \le j \le n\}\), \(S_3^- = \{-2n-2\} \cup \{1 - 2j : 1 \le j \le n\}\) and \(S_4^- = \{-2n-2\}\); that is, the negative parts \(\beta^-\) of these numbers are the words \(0^{2n-2}01\), \((01)^n\), \((10)^n 01\) and \(0^{2n}01\). Moreover \(\sum_{i \in S_1^-} F_{i+2n} = 0\), \(\sum_{i \in S_2^-} F_{i+2n} = F_{2n-1} - 1\), \(\sum_{i \in S_3^-} F_{i+2n+2} = F_{2n+2} - 1\) and \(\sum_{i \in S_4^-} F_{i+2n+2} = 0\).

In the paper's notation, with \(\gamma^-(N)\) the word \(\beta^-(N)\) with its final \(01\) removed, this says \(\gamma^-(L_{2n}) = 0^{2n-2}\), \(\gamma^-(L_{2n+1}) = (01)^{n-1}\), \(\gamma^-(L_{2n+1}+1) = (10)^n\) and \(\gamma^-(L_{2n+2}-1) = 0^{2n}\), and that the codes \(C(N)\) of the words \(\gamma^-(N)\), which equal \(\sum_{i \in \beta^-(N)} F_{i+2j}\) when \(\beta^-(N)\) has length \(2j\), are \(C(L_{2n}) = 0\), \(C(L_{2n+1}) = F_{2n-1} - 1\), \(C(L_{2n+1}+1) = F_{2n+2} - 1\) and \(C(L_{2n+2}-1) = 0\).

public theorem_wanted basePhi_lucas_border_codes (n : ℕ) (hn : 1 ≤ n) (S₁ S₂ S₃ S₄ : Finset ℤ)
    (h₁ : IsBasePhiExpansion (lucasNumber (2 * n)) S₁)
    (h₂ : IsBasePhiExpansion (lucasNumber (2 * n + 1)) S₂)
    (h₃ : IsBasePhiExpansion (lucasNumber (2 * n + 1) + 1) S₃)
    (h₄ : IsBasePhiExpansion (lucasNumber (2 * n + 2) - 1) S₄) :
    S₁.filter (· < 0) = {-(2 * n : ℤ)} ∧
    S₂.filter (· < 0) = (Finset.Icc 1 n).image (fun j : ℕ => -(2 * j : ℤ)) ∧
    S₃.filter (· < 0) =
      insert (-(2 * n + 2 : ℤ)) ((Finset.Icc 1 n).image (fun j : ℕ => 1 - (2 * j : ℤ))) ∧
    S₄.filter (· < 0) = {-(2 * n + 2 : ℤ)} ∧
    ∑ i ∈ S₁.filter (· < 0), Nat.fib (i + 2 * n).toNat = 0 ∧
    ∑ i ∈ S₂.filter (· < 0), Nat.fib (i + 2 * n).toNat = Nat.fib (2 * n - 1) - 1 ∧
    ∑ i ∈ S₃.filter (· < 0), Nat.fib (i + 2 * n + 2).toNat = Nat.fib (2 * n + 2) - 1 ∧
    ∑ i ∈ S₄.filter (· < 0), Nat.fib (i + 2 * n + 2).toNat = 0

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Lemma 10.

Uses 2

Statement usesBase phi expansion · Lucas numbers

TheoremThe digit blocks \(10 \cdot 1\) and \(00 \cdot 1\) around the radix point#●ready to prove

Let \(\varphi\) be the golden ratio, let \(N \ge 1\) and let \(S\) be a base phi expansion of \(N\), with digits \(d_i\) (\(d_i = 1\) if \(i \in S\), else \(d_i = 0\)). Then \(d_1 d_0 \cdot d_{-1} \ne 10 \cdot 1\), and \(d_1 d_0 \cdot d_{-1} = 00 \cdot 1\) if and only if \(N = 3 \lfloor n \varphi \rfloor + n + 1\) for some integer \(n \ge 1\).

public theorem_wanted basePhi_digits_dot_one (N : ℕ) (hN : 1 ≤ N) (S : Finset ℤ)
    (hS : IsBasePhiExpansion N S) :
    ¬ HasDigitBlock S 1 [1, 0, 1] ∧
      (HasDigitBlock S 1 [0, 0, 1] ↔ (N : ℤ) ∈ beattySet 3 1 1)

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Proposition 1.

Uses 3

Statement usesDigit block of an expansion · Base phi expansion · Terms of a generalized Beatty sequence

TheoremEnd blocks of length at most three ending in \(0\)#●ready to prove

Let \(\varphi\) be the golden ratio. For integers \(p, q, r\) let \(V(p, q, r) = \{p \lfloor n\varphi \rfloor + qn + r : n \ge 1\}\) and \(V_0(p, q, r) = \{p \lfloor n\varphi \rfloor + qn + r : n \ge 0\}\). For a word \(w\) of length \(\ell\) let \(R_w\) be the set of natural numbers having a base phi expansion whose digits \(d_{\ell-1} \cdots d_0\) at positions \(\ell - 1, \dots, 0\) spell \(w\). Then for every natural number \(N \ge 1\): \(N \in R_0\) if and only if \(N \in V(-1, 3, 0)\); \(N \in R_{00}\) if and only if \(N \in V_0(1, 2, 0) \cup V(3, 1, 1)\); \(N \in R_{10}\) if and only if \(N \in V(1, 2, -1)\); \(N \in R_{010}\) if and only if \(N \in V(1, 2, -1)\); \(N \in R_{000}\) if and only if \(N \in V_0(4, 3, 0) \cup V(3, 1, 1)\); and \(N \in R_{100}\) if and only if \(N \in V(3, 1, -1)\). Moreover \(V_0(1, 2, 0)\) and \(V_0(4, 3, 0)\) are each disjoint from \(V(3, 1, 1)\).

public theorem_wanted basePhi_short_end_blocks_zero (N : ℕ) (hN : 1 ≤ N) :
    (N ∈ basePhiOccurrences 0 [0] ↔ (N : ℤ) ∈ beattySet (-1) 3 0) ∧
    (N ∈ basePhiOccurrences 1 [0, 0] ↔ (N : ℤ) ∈ beattySet₀ 1 2 0 ∪ beattySet 3 1 1) ∧
    (N ∈ basePhiOccurrences 1 [1, 0] ↔ (N : ℤ) ∈ beattySet 1 2 (-1)) ∧
    (N ∈ basePhiOccurrences 2 [0, 1, 0] ↔ (N : ℤ) ∈ beattySet 1 2 (-1)) ∧
    (N ∈ basePhiOccurrences 2 [0, 0, 0] ↔ (N : ℤ) ∈ beattySet₀ 4 3 0 ∪ beattySet 3 1 1) ∧
    (N ∈ basePhiOccurrences 2 [1, 0, 0] ↔ (N : ℤ) ∈ beattySet 3 1 (-1)) ∧
    Disjoint (beattySet₀ 1 2 0) (beattySet 3 1 1) ∧ Disjoint (beattySet₀ 4 3 0) (beattySet 3 1 1)

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Proposition 2.

Uses 3

Statement usesOccurrence set of a digit block · Terms of a generalized Beatty sequence · Terms of a generalized Beatty sequence from index zero

TheoremShort prefixes of the negative parts of base phi expansions#●ready to prove

Let \(\varphi\) be the golden ratio. For integers \(p, q, r\) let \(V(p, q, r) = \{p \lfloor n\varphi \rfloor + qn + r : n \ge 1\}\) and \(V_0(p, q, r) = \{p \lfloor n\varphi \rfloor + qn + r : n \ge 0\}\). For a word \(w\) of length \(\ell\) let \(R_{\cdot w}\) be the set of natural numbers having a base phi expansion whose digits \(d_{-1} d_{-2} \cdots d_{-\ell}\) spell \(w\), where \(d_i = 1\) if position \(i\) carries a digit \(1\) and \(d_i = 0\) otherwise. Then for every natural number \(N \ge 2\): \(N \in R_{\cdot 0}\) if and only if \(N \in V(1, 2, -1) \cup V(1, 2, 0) \cup V(1, 2, 1)\); \(N \in R_{\cdot 1}\) if and only if \(N \in V(3, 1, 1)\); \(N \in R_{\cdot 10}\) if and only if \(N \in V(3, 1, 1)\); \(N \in R_{\cdot 00}\) if and only if \(N \in V(3, 1, 2) \cup V(3, 1, 3) \cup V(3, 1, 4)\); \(N \in R_{\cdot 01}\) if and only if \(N \in V_0(4, 3, 2) \cup V_0(4, 3, 3) \cup V_0(4, 3, 4)\); \(N \in R_{\cdot 010}\) if and only if \(N \in V_0(4, 3, 2) \cup V_0(4, 3, 3) \cup V_0(4, 3, 4)\); \(N \in R_{\cdot 000}\) if and only if \(N \in V(4, 3, -1) \cup V(4, 3, 0) \cup V(4, 3, 1)\); \(N \in R_{\cdot 001}\) if and only if \(N \in V(7, 4, 2) \cup V(7, 4, 3) \cup V(7, 4, 4)\); \(N \in R_{\cdot 100}\) if and only if \(N \in V(4, 3, -2)\); and \(N \in R_{\cdot 101}\) if and only if \(N \in V(7, 4, 1)\).

The bound \(N \ge 2\) makes the negative part nonempty: the expansion of \(1\) is \(1\) itself. The first equivalence follows the reading \(R_{\cdot 0} = V(1, 2, [-1, 0, 1])\) of the paper's Figure 3: as printed, \(V(2, 1, -1) \cup V(2, 1, 0) \cup V(2, 1, 1)\) misses \(6\), whose expansion is \(1010 \cdot 0001\), and contains \(12\), whose expansion is \(100000 \cdot 101001\).

MetaMathlibExt.basePhi_short_negative_prefixes · 17 lines

public theorem_wanted basePhi_short_negative_prefixes (N : ℕ) (hN : 2 ≤ N) :
    (N ∈ basePhiOccurrences (-1) [0] ↔
      (N : ℤ) ∈ beattySet 1 2 (-1) ∪ beattySet 1 2 0 ∪ beattySet 1 2 1) ∧
    (N ∈ basePhiOccurrences (-1) [1] ↔ (N : ℤ) ∈ beattySet 3 1 1) ∧
    (N ∈ basePhiOccurrences (-1) [1, 0] ↔ (N : ℤ) ∈ beattySet 3 1 1) ∧
    (N ∈ basePhiOccurrences (-1) [0, 0] ↔
      (N : ℤ) ∈ beattySet 3 1 2 ∪ beattySet 3 1 3 ∪ beattySet 3 1 4) ∧
    (N ∈ basePhiOccurrences (-1) [0, 1] ↔
      (N : ℤ) ∈ beattySet₀ 4 3 2 ∪ beattySet₀ 4 3 3 ∪ beattySet₀ 4 3 4) ∧
    (N ∈ basePhiOccurrences (-1) [0, 1, 0] ↔
      (N : ℤ) ∈ beattySet₀ 4 3 2 ∪ beattySet₀ 4 3 3 ∪ beattySet₀ 4 3 4) ∧
    (N ∈ basePhiOccurrences (-1) [0, 0, 0] ↔
      (N : ℤ) ∈ beattySet 4 3 (-1) ∪ beattySet 4 3 0 ∪ beattySet 4 3 1) ∧
    (N ∈ basePhiOccurrences (-1) [0, 0, 1] ↔
      (N : ℤ) ∈ beattySet 7 4 2 ∪ beattySet 7 4 3 ∪ beattySet 7 4 4) ∧
    (N ∈ basePhiOccurrences (-1) [1, 0, 0] ↔ (N : ℤ) ∈ beattySet 4 3 (-2)) ∧
    (N ∈ basePhiOccurrences (-1) [1, 0, 1] ↔ (N : ℤ) ∈ beattySet 7 4 1)

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Proposition 3.

Uses 3

Statement usesOccurrence set of a digit block · Terms of a generalized Beatty sequence · Terms of a generalized Beatty sequence from index zero

TheoremEmbedding of base phi expansions into Zeckendorf expansions#●ready to prove

Let \(\varphi\) be the golden ratio and let \(F_j\) be the Fibonacci numbers, \(F_0 = 0\), \(F_1 = F_2 = 1\). For a natural number \(M\) let \(Z(M)\) be the set of indices \(i \ge 0\) such that \(F_{i+2}\) occurs in the Zeckendorf representation of \(M\), so that \(M = \sum_{i \in Z(M)} F_{i+2}\). Let \(N\) be a natural number, let \(S\) be a base phi expansion of \(N\) (the set of positions of its digits \(1\)), and let \(s(N)\) be the number of integers \(n\) with \(1 \le n \le N\) and \(3 \lfloor n \varphi \rfloor + n + 1 < N\). Then \(\{i \in S : i \ge 0\} = Z(N + s(N))\).

Since \(3 \lfloor n \varphi \rfloor + n + 1 > N\) for \(n \ge N\), \(s(N)\) is the number of all \(n \ge 1\) with \(3 \lfloor n \varphi \rfloor + n + 1 < N\), that is, the number of \(M < N\) whose digit at position \(-1\) is \(1\), as in the paper's proof. Both formulas for \(s(N)\) printed in the paper are off by one: \(\max\{k : 3 \lfloor k \varphi \rfloor + k \le N\}\) gives \(s(4) = 1\), but \(Z(5) = \{3\}\) while \(4 = \varphi^2 + 1 + \varphi^{-2}\) has nonnegative positions \(\{0, 2\}\); and \(\max\{k : 3 \lfloor k \varphi \rfloor + k + 1 \le N\} - 1\) gives \(s(6) = 0\), but \(Z(6) = \{0, 3\}\) while \(6 = \varphi^3 + \varphi + \varphi^{-4}\) has nonnegative positions \(\{1, 3\}\).

public theorem_wanted basePhi_positive_part_eq_zeckendorf (N : ℕ) (S : Finset ℤ)
    (hS : IsBasePhiExpansion N S) :
    S.filter (0 ≤ ·) =
      ((Nat.zeckendorf
          (N + ((Finset.Icc 1 N).filter (fun n => generalizedBeatty 3 1 1 n < N)).card)).map
        (fun k : ℕ => (k : ℤ) - 2)).toFinset

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Theorem 1.

Uses 2

Statement usesBase phi expansion · Generalized Beatty sequence

TheoremRecursive structure theorem for base phi expansions, part (A)#●ready to prove

Let \(n \ge 2\) and let \(L_j\) be the Lucas numbers; \(k\) denotes a natural number, and base phi expansions are given as sets of positions of digits \(1\). (I) If \(1 \le k \le L_{2n-2} - 1\), \(T\) is a base phi expansion of \(L_{2n-1} + k\) and \(S\) is a base phi expansion of \(L_{2n+1} + k\), then \(2n-1 \in T\), \(2n-2 \notin T\), \(1-2n \notin T\), \(-2n \in T\) and \(S = (T \setminus \{2n-1, -2n\}) \cup \{2n+1, 1-2n, -2n-2\}\). (K) If \(1 \le k \le L_{2n-2} - 1\), \(T\) is a base phi expansion of \(L_{2n-1} + k\) and \(S\) is a base phi expansion of \(L_{2n+1} + L_{2n-1} + k\), then \(2n-1 \in T\), \(2n-2 \notin T\), \(1-2n \notin T\), \(-2n \in T\) and \(S = (T \setminus \{-2n\}) \cup \{2n+1, -2n-2\}\). (J) If \(0 \le k \le L_{2n-3}\), \(T\) is a base phi expansion of \(L_{2n-2} + k\) and \(S\) is a base phi expansion of \(L_{2n+1} + L_{2n-2} + k\), then \(2n-2 \in T\), \(2n-3 \notin T\), \(3-2n \notin T\), \(2-2n \in T\) and \(S = (T \setminus \{2-2n\}) \cup \{2n+1, 1-2n, -2n-2\}\).

In the paper's word notation, where \(\beta(M)\) is the expansion of \(M\) written as a word of digits (with \(\cdot\) between positions \(0\) and \(-1\)) and \((10)^{-1}\), \((01)^{-1}\) cancel a leading \(10\) and a trailing \(01\), these are \(\beta(L_{2n+1}+k) = 1000\,(10)^{-1}\,\beta(L_{2n-1}+k)\,(01)^{-1}\,1001\), \(\beta(L_{2n+1}+L_{2n-1}+k) = 1010\,(10)^{-1}\,\beta(L_{2n-1}+k)\,(01)^{-1}\,0001\) and \(\beta(L_{2n+1}+L_{2n-2}+k) = 10010\,(10)^{-1}\,\beta(L_{2n-2}+k)\,(01)^{-1}\,001001\). The source's ranges \(k \le L_{2n} - 1\) for (I) and (K) and \(k \le L_{2n-1}\) for (J) are too wide: for \(n = 2\) and \(k = 3\), \(\beta(L_3 + 3) = \beta(7) = 10000 \cdot 0001\) has no digit \(1\) at position \(3\).

MetaMathlibExt.basePhi_recursive_structure · 18 lines

public theorem_wanted basePhi_recursive_structure (n : ℕ) (T S : Finset ℤ) :
    (2 ≤ n → ∀ k, 1 ≤ k → k + 1 ≤ lucasNumber (2 * n - 2) →
      IsBasePhiExpansion (lucasNumber (2 * n - 1) + k) T →
      IsBasePhiExpansion (lucasNumber (2 * n + 1) + k) S →
        (2 * n - 1 : ℤ) ∈ T ∧ (2 * n - 2 : ℤ) ∉ T ∧ (1 - 2 * n : ℤ) ∉ T ∧ -(2 * n : ℤ) ∈ T ∧
          S = insert (2 * n + 1 : ℤ) (insert (1 - 2 * n : ℤ) (insert (-2 * n - 2 : ℤ)
            ((T.erase (2 * n - 1 : ℤ)).erase (-(2 * n : ℤ)))))) ∧
    (2 ≤ n → ∀ k, 1 ≤ k → k + 1 ≤ lucasNumber (2 * n - 2) →
      IsBasePhiExpansion (lucasNumber (2 * n - 1) + k) T →
      IsBasePhiExpansion (lucasNumber (2 * n + 1) + lucasNumber (2 * n - 1) + k) S →
        (2 * n - 1 : ℤ) ∈ T ∧ (2 * n - 2 : ℤ) ∉ T ∧ (1 - 2 * n : ℤ) ∉ T ∧ -(2 * n : ℤ) ∈ T ∧
        S = insert (2 * n + 1 : ℤ) (insert (-2 * n - 2 : ℤ) (T.erase (-(2 * n : ℤ))))) ∧
    (2 ≤ n → ∀ k, k ≤ lucasNumber (2 * n - 3) →
      IsBasePhiExpansion (lucasNumber (2 * n - 2) + k) T →
      IsBasePhiExpansion (lucasNumber (2 * n + 1) + lucasNumber (2 * n - 2) + k) S →
        (2 * n - 2 : ℤ) ∈ T ∧ (2 * n - 3 : ℤ) ∉ T ∧ (3 - 2 * n : ℤ) ∉ T ∧ (2 - 2 * n : ℤ) ∈ T ∧
          S = insert (2 * n + 1 : ℤ) (insert (1 - 2 * n : ℤ) (insert (-2 * n - 2 : ℤ)
            (T.erase (2 - 2 * n : ℤ)))))

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Theorem 2.

Uses 2

Statement usesBase phi expansion · Lucas numbers

TheoremRecursive structure of base phi expansions on Lucas intervals#●ready to prove

Let \(n \ge 1\), let \(L_k\) be the Lucas numbers, and for \(j \ge 0\) let \(\Lambda_{2j}\) be the set of natural numbers in \([L_{2j}, L_{2j+1}]\) and \(\Lambda_{2j+1}\) the set of natural numbers in \([L_{2j+1} + 1, L_{2j+2} - 1]\). Let \(T\) be a base phi expansion of a natural number \(M\) and \(S\) a base phi expansion of a natural number \(N\), both given as sets of positions of digits \(1\). Then: (A)(a) if \(M \in \Lambda_{2n-1}\) and \(N = M + L_{2n}\), then \(2n-1 \in T\), \(2n-2 \notin T\), \(1-2n \notin T\), \(-2n \in T\) and \(S = (T \setminus \{2n-1, -2n\}) \cup \{2n+1, 1-2n, -2n-2\}\); (A)(b) if \(M \in \Lambda_{2n-2}\) and \(N = M + L_{2n+1}\), then \(3-2n \notin T\), \(2-2n \in T\) and \(S = (T \setminus \{2-2n\}) \cup \{2n+1, 1-2n, -2n-2\}\); (A)(c) if \(M \in \Lambda_{2n-1}\) and \(N = M + L_{2n+1}\), then \(2n-1 \in T\), \(1-2n \notin T\), \(-2n \in T\) and \(S = (T \setminus \{-2n\}) \cup \{2n+1, -2n-2\}\); (B)(a) if \(M \in \Lambda_{2n}\) and \(N = M + L_{2n+1}\), then \(2n \in T\), \(2n-1 \notin T\), \(1-2n \notin T\), \(-2n \in T\) and \(S = (T \setminus \{2n, -2n\}) \cup \{2n+2, -2n-2\}\); (B)(b) if \(M \in \Lambda_{2n-1}\) and \(N = M + L_{2n+2}\), then \(S = T \cup \{2n+2, -2n-2\}\); (B)(c) if \(M \in \Lambda_{2n}\) and \(N = M + L_{2n+2}\), then \(S = T \cup \{2n+2, -2n-2\}\).

In the paper's word notation, where \(\beta(M)\) is the expansion of \(M\) written as a word of digits (with \(\cdot\) between positions \(0\) and \(-1\)) and \((10)^{-1}\), \((01)^{-1}\) cancel a leading \(10\) and a trailing \(01\), (A)(a) is \(\beta(M + L_{2n}) = 1000\,(10)^{-1}\,\beta(M)\,(01)^{-1}\,1001\) and (B)(b) is \(\beta(M + L_{2n+2}) = 100\,\beta(M)\,01\); the digit conditions on \(T\) make the cancellations \((10)^{-1}\) and \((01)^{-1}\) valid. In (B)(c) the source writes \(\beta(N - L_{2n+1})\) for \(N \in \Lambda_{2n} + L_{2n+2}\); the shift \(L_{2n+2}\) is used here, since as printed \(n = 1\) and \(N = 10\) give \(10\,\beta(6)\,01 = 101010 \cdot 000101\), which is not \(\beta(10) = 10100 \cdot 0101\).

MetaMathlibExt.basePhi_recursive_structure_lucas_intervals · 26 lines

public theorem_wanted basePhi_recursive_structure_lucas_intervals (n : ℕ) (hn : 1 ≤ n)
    (M : ℕ) (T S : Finset ℤ) (hT : IsBasePhiExpansion M T) :
    (M ∈ Finset.Icc (lucasNumber (2 * n - 1) + 1) (lucasNumber (2 * n) - 1) →
      IsBasePhiExpansion (M + lucasNumber (2 * n)) S →
        (2 * n - 1 : ℤ) ∈ T ∧ (2 * n - 2 : ℤ) ∉ T ∧ (1 - 2 * n : ℤ) ∉ T ∧ -(2 * n : ℤ) ∈ T ∧
          S = insert (2 * n + 1 : ℤ) (insert (1 - 2 * n : ℤ) (insert (-2 * n - 2 : ℤ)
            ((T.erase (2 * n - 1 : ℤ)).erase (-(2 * n : ℤ)))))) ∧
    (M ∈ Finset.Icc (lucasNumber (2 * n - 2)) (lucasNumber (2 * n - 1)) →
      IsBasePhiExpansion (M + lucasNumber (2 * n + 1)) S →
        (3 - 2 * n : ℤ) ∉ T ∧ (2 - 2 * n : ℤ) ∈ T ∧
          S = insert (2 * n + 1 : ℤ) (insert (1 - 2 * n : ℤ) (insert (-2 * n - 2 : ℤ)
            (T.erase (2 - 2 * n : ℤ))))) ∧
    (M ∈ Finset.Icc (lucasNumber (2 * n - 1) + 1) (lucasNumber (2 * n) - 1) →
      IsBasePhiExpansion (M + lucasNumber (2 * n + 1)) S →
        (2 * n - 1 : ℤ) ∈ T ∧ (1 - 2 * n : ℤ) ∉ T ∧ -(2 * n : ℤ) ∈ T ∧
          S = insert (2 * n + 1 : ℤ) (insert (-2 * n - 2 : ℤ) (T.erase (-(2 * n : ℤ))))) ∧
    (M ∈ Finset.Icc (lucasNumber (2 * n)) (lucasNumber (2 * n + 1)) →
      IsBasePhiExpansion (M + lucasNumber (2 * n + 1)) S →
        (2 * n : ℤ) ∈ T ∧ (2 * n - 1 : ℤ) ∉ T ∧ (1 - 2 * n : ℤ) ∉ T ∧ -(2 * n : ℤ) ∈ T ∧
          S = insert (2 * n + 2 : ℤ) (insert (-2 * n - 2 : ℤ) ((T.erase (2 * n : ℤ)).erase (-(2 * n : ℤ))))) ∧
    (M ∈ Finset.Icc (lucasNumber (2 * n - 1) + 1) (lucasNumber (2 * n) - 1) →
      IsBasePhiExpansion (M + lucasNumber (2 * n + 2)) S →
        S = insert (2 * n + 2 : ℤ) (insert (-2 * n - 2 : ℤ) T)) ∧
    (M ∈ Finset.Icc (lucasNumber (2 * n)) (lucasNumber (2 * n + 1)) →
      IsBasePhiExpansion (M + lucasNumber (2 * n + 2)) S →
        S = insert (2 * n + 2 : ℤ) (insert (-2 * n - 2 : ℤ) T))

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Theorem 3.

Uses 2

Statement usesBase phi expansion · Lucas numbers

TheoremShort end blocks#●ready to prove

Let \(\varphi\) be the golden ratio. For integers \(p, q, r\) let \(V(p, q, r)\) be the set of the integers \(p \lfloor n\varphi \rfloor + qn + r\) with \(n \ge 1\), and \(V_0(p, q, r)\) the same set with \(n \ge 0\). Then for every natural number \(N \ge 1\): some base phi expansion of \(N\) has digit \(1\) at position \(0\) if and only if \(N \in V_0(1, 2, 1)\); some base phi expansion of \(N\) has digits \(1, 0\) at positions \(1, 0\) if and only if \(N \in V(1, 2, -1)\); some base phi expansion of \(N\) has digits \(0, 0, 0\) at positions \(1, 0, -1\) if and only if \(N \in V_0(1, 2, 0)\); and some base phi expansion of \(N\) has digits \(0, 0, 1\) at positions \(1, 0, -1\) if and only if \(N \in V(3, 1, 1)\).

In the paper's notation: \(R_1 = V_0(1, 2, 1)\), \(R_{10} = V(1, 2, -1)\), \(R_{00 \cdot 0} = V_0(1, 2, 0)\) and \(R_{00 \cdot 1} = V(3, 1, 1)\), on the numbers \(N \ge 1\).

public theorem_wanted basePhi_short_end_blocks (N : ℕ) (hN : 1 ≤ N) :
    (N ∈ basePhiOccurrences 0 [1] ↔ (N : ℤ) ∈ beattySet₀ 1 2 1) ∧
    (N ∈ basePhiOccurrences 1 [1, 0] ↔ (N : ℤ) ∈ beattySet 1 2 (-1)) ∧
    (N ∈ basePhiOccurrences 1 [0, 0, 0] ↔ (N : ℤ) ∈ beattySet₀ 1 2 0) ∧
    (N ∈ basePhiOccurrences 1 [0, 0, 1] ↔ (N : ℤ) ∈ beattySet 3 1 1)

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Theorem 6.

Uses 3

Statement usesOccurrence set of a digit block · Terms of a generalized Beatty sequence · Terms of a generalized Beatty sequence from index zero

TheoremEnd blocks ending in \(0\) are Lucas–Wythoff sequences#●ready to prove

Let \(\varphi\) be the golden ratio and \(L_n\) the Lucas numbers. For integers \(p, q, r\) let \(V(p, q, r)\) be the set of the integers \(p \lfloor n\varphi \rfloor + qn + r\) with \(n \ge 1\), and \(V_0(p, q, r)\) the same set with \(n \ge 0\). For a word \(w = w_{m-1} \cdots w_0\) of length \(m\) over the natural numbers, let \(R_w\) be the set of natural numbers \(N\) with a base phi expansion whose digit at position \(i\) is \(1\) exactly when \(w_i = 1\), for \(i = m - 1, \dots, 0\). Then: (1) for every word \(w = w_{m-1} \cdots w_0\) of length \(m \ge 2\) with letters in \(\{0, 1\}\), no two consecutive letters \(1\), \(w_0 = 0\) and \(w \ne 0^m\), there is an integer \(\gamma \le 0\) such that every natural number \(N \ge 1\) lies in \(R_w\) if and only if it lies in \(V(L_{m-2}, L_{m-3}, \gamma)\) when \(w_{m-1} = 0\), respectively in \(V(L_{m-1}, L_{m-2}, \gamma)\) when \(w_{m-1} = 1\); (2) for every \(m \ge 1\) and every natural number \(N \ge 1\), \(N \in R_{0^{2m}}\) if and only if \(N \in V(L_{2m}, L_{2m-1}, 1) \cup V_0(L_{2m-1}, L_{2m-2}, 0)\), and \(N \in R_{0^{2m+1}}\) if and only if \(N \in V_0(L_{2m+1}, L_{2m}, 0) \cup V(L_{2m}, L_{2m-1}, 1)\); moreover \(V(L_{2m}, L_{2m-1}, 1)\) and \(V_0(L_{2m-1}, L_{2m-2}, 0)\) are disjoint, and \(V_0(L_{2m+1}, L_{2m}, 0)\) and \(V(L_{2m}, L_{2m-1}, 1)\) are disjoint.

MetaMathlibExt.basePhi_end_blocks_lucasWythoff · 20 lines

public theorem_wanted basePhi_end_blocks_lucasWythoff :
    (∀ w : List ℕ, 2 ≤ w.length → (∀ d ∈ w, d ≤ 1) →
      List.IsChain (fun a b => ¬ (a = 1 ∧ b = 1)) w → w.getLast? = some 0 →
      w ≠ List.replicate w.length 0 →
        ∃ γ : ℤ, γ ≤ 0 ∧ ∀ N : ℕ, 1 ≤ N →
          (N ∈ basePhiOccurrences (w.length - 1) w ↔
            (N : ℤ) ∈ (if w.head? = some 0 then
              beattySet (lucasNumber (w.length - 2)) (lucasNumber (w.length - 3)) γ
            else beattySet (lucasNumber (w.length - 1)) (lucasNumber (w.length - 2)) γ))) ∧
    ∀ m : ℕ, 1 ≤ m → ∀ N : ℕ, 1 ≤ N →
      (N ∈ basePhiOccurrences (2 * m - 1) (List.replicate (2 * m) 0) ↔
        (N : ℤ) ∈ beattySet (lucasNumber (2 * m)) (lucasNumber (2 * m - 1)) 1 ∪
          beattySet₀ (lucasNumber (2 * m - 1)) (lucasNumber (2 * m - 2)) 0) ∧
      (N ∈ basePhiOccurrences (2 * m) (List.replicate (2 * m + 1) 0) ↔
        (N : ℤ) ∈ beattySet₀ (lucasNumber (2 * m + 1)) (lucasNumber (2 * m)) 0 ∪
          beattySet (lucasNumber (2 * m)) (lucasNumber (2 * m - 1)) 1) ∧
      Disjoint (beattySet (lucasNumber (2 * m)) (lucasNumber (2 * m - 1)) 1)
        (beattySet₀ (lucasNumber (2 * m - 1)) (lucasNumber (2 * m - 2)) 0) ∧
      Disjoint (beattySet₀ (lucasNumber (2 * m + 1)) (lucasNumber (2 * m)) 0)
        (beattySet (lucasNumber (2 * m)) (lucasNumber (2 * m - 1)) 1)

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Theorem 7.

Uses 4

Statement usesOccurrence set of a digit block · Terms of a generalized Beatty sequence · Terms of a generalized Beatty sequence from index zero · Lucas numbers

TheoremEnd blocks ending in \(1\) are Lucas–Wythoff sequences#●ready to prove

Let \(\varphi\) be the golden ratio and \(L_n\) the Lucas numbers. For integers \(p, q, r\) let \(V(p, q, r)\) be the set of the integers \(p \lfloor n\varphi \rfloor + qn + r\) with \(n \ge 1\), and \(V_0(p, q, r)\) the same set with \(n \ge 0\). For a word \(w = w_{m-1} \cdots w_0\) of length \(m\) over the natural numbers, let \(R_w\) be the set of natural numbers \(N\) with a base phi expansion whose digit at position \(i\) is \(1\) exactly when \(w_i = 1\), for \(i = m - 1, \dots, 0\). Then: (1) for every word \(w = w_{m-1} \cdots w_0\) of length \(m \ge 3\) with letters in \(\{0, 1\}\), no two consecutive letters \(1\) and \(w_0 = 1\), which is not of the form \(0^k 1\) or \(1 0^k 1\) with \(k \ge 2\), and for which \(R_w\) is nonempty, there is an integer \(\gamma \le 0\) such that every natural number \(N \ge 1\) lies in \(R_w\) if and only if it lies in \(V(L_{m-2}, L_{m-3}, \gamma)\) when \(w_{m-1} = 0\), respectively in \(V(L_{m-1}, L_{m-2}, \gamma)\) when \(w_{m-1} = 1\); (2) for every \(m \ge 1\) and every natural number \(N \ge 1\): \(N \in R_{0^{2m} 1}\) if and only if \(N \in V_0(L_{2m+1}, L_{2m}, 1)\); \(N \in R_{0^{2m+1} 1}\) if and only if \(N \in V_0(L_{2m+1}, L_{2m}, 1)\); \(N \notin R_{1 0^{2m} 1}\); and \(N \in R_{1 0^{2m+1} 1}\) if and only if \(N \in V(L_{2m+2}, L_{2m+1}, 1 - L_{2m+1})\).

The hypothesis that \(R_w\) is nonempty is added to the printed statement: as printed, the statement fails for \(w = 01001\), which never occurs (its end block \(1001\) is excluded), while every \(V(p, q, \gamma)\) is nonempty; the source's proof derives its description of \(R_w\) only under the assumption \(R_w \ne \emptyset\).

MetaMathlibExt.basePhi_end_blocks_one_lucasWythoff · 20 lines

public theorem_wanted basePhi_end_blocks_one_lucasWythoff :
    (∀ w : List ℕ, 3 ≤ w.length → (∀ d ∈ w, d ≤ 1) →
      List.IsChain (fun a b => ¬ (a = 1 ∧ b = 1)) w → w.getLast? = some 1 →
      (∀ k : ℕ, 2 ≤ k → w ≠ List.replicate k 0 ++ [1]) →
      (∀ k : ℕ, 2 ≤ k → w ≠ 1 :: List.replicate k 0 ++ [1]) →
      (basePhiOccurrences (w.length - 1) w).Nonempty →
        ∃ γ : ℤ, γ ≤ 0 ∧ ∀ N : ℕ, 1 ≤ N →
          (N ∈ basePhiOccurrences (w.length - 1) w ↔
            (N : ℤ) ∈ (if w.head? = some 0 then
              beattySet (lucasNumber (w.length - 2)) (lucasNumber (w.length - 3)) γ
            else beattySet (lucasNumber (w.length - 1)) (lucasNumber (w.length - 2)) γ))) ∧
    ∀ m : ℕ, 1 ≤ m → ∀ N : ℕ, 1 ≤ N →
      (N ∈ basePhiOccurrences (2 * m) (List.replicate (2 * m) 0 ++ [1]) ↔
        (N : ℤ) ∈ beattySet₀ (lucasNumber (2 * m + 1)) (lucasNumber (2 * m)) 1) ∧
      (N ∈ basePhiOccurrences (2 * m + 1) (List.replicate (2 * m + 1) 0 ++ [1]) ↔
        (N : ℤ) ∈ beattySet₀ (lucasNumber (2 * m + 1)) (lucasNumber (2 * m)) 1) ∧
      N ∉ basePhiOccurrences (2 * m + 1) (1 :: List.replicate (2 * m) 0 ++ [1]) ∧
      (N ∈ basePhiOccurrences (2 * m + 2) (1 :: List.replicate (2 * m + 1) 0 ++ [1]) ↔
        (N : ℤ) ∈ beattySet (lucasNumber (2 * m + 2)) (lucasNumber (2 * m + 1))
          (1 - (lucasNumber (2 * m + 1) : ℤ)))

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Theorem 8.

Uses 4

Statement usesOccurrence set of a digit block · Terms of a generalized Beatty sequence · Terms of a generalized Beatty sequence from index zero · Lucas numbers

TheoremEvery even-length Zeckendorf word ending in \(1\) is a negative part#●ready to prove

Let \(n \ge 1\) and let \(T\) be a finite set of integers with \(T \subseteq [-2n, -1]\) and \(-2n \in T\) that contains no two consecutive integers. Then there are a natural number \(N\) and a base phi expansion \(S\) of \(N\) (the set of positions of its digits \(1\)) with \(\{i \in S : i < 0\} = T\). In words, every Zeckendorf word of even length \(2n \ge 2\) ending in \(1\) is the negative part \(\beta^-(N)\) of some \(N\).

public theorem_wanted basePhi_negative_parts_surject (n : ℕ) (hn : 1 ≤ n) (T : Finset ℤ)
    (hT : T ⊆ Finset.Icc (-(2 * n : ℤ)) (-1)) (hlast : -(2 * n : ℤ) ∈ T)
    (hB : IsBergmanExpansion T) :
    ∃ N S, IsBasePhiExpansion N S ∧ S.filter (· < 0) = T

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Theorem 9.

Uses 2

Statement usesBase phi expansion · Bergman expansions

TheoremRecursive structure of the negative parts of base phi expansions#●ready to prove

Let \(n \ge 1\), let \(L_k\) be the Lucas numbers, and for \(j \ge 0\) let \(\Lambda_{2j}\) be the set of natural numbers in \([L_{2j}, L_{2j+1}]\) and \(\Lambda_{2j+1}\) the set of natural numbers in \([L_{2j+1} + 1, L_{2j+2} - 1]\). Let \(T\) be a base phi expansion of a natural number \(M\) and \(S\) a base phi expansion of a natural number \(N\), both given as sets of positions of digits \(1\). Write \(S^- = \{i \in S : i < 0\}\) and, for an integer \(a\), \(T_a = \{i \in T : a \le i < 0\}\). Then: (A)(a) if \(M \in \Lambda_{2n-1}\) and \(N = M + L_{2n}\), then \(S^- = T_{2-2n} \cup \{1-2n, -2n-2\}\); (A)(b) if \(M \in \Lambda_{2n-2}\) and \(N = M + L_{2n+1}\), then \(S^- = T_{4-2n} \cup \{1-2n, -2n-2\}\); (A)(c) if \(M \in \Lambda_{2n-1}\) and \(N = M + L_{2n+1}\), then \(S^- = T_{2-2n} \cup \{-2n-2\}\); (B)(a) if \(M \in \Lambda_{2n}\) and \(N = M + L_{2n+1}\), then \(S^- = T_{2-2n} \cup \{-2n-2\}\); (B)(b) if \(M \in \Lambda_{2n-1}\) and \(N = M + L_{2n+2}\), then \(S^- = T_{2-2n} \cup \{-2n, -2n-2\}\); (B)(c) if \(M \in \Lambda_{2n}\) and \(N = M + L_{2n+2}\), then \(S^- = T_{2-2n} \cup \{-2n, -2n-2\}\).

These are the paper's identities for the words \(\gamma^-(N)\), the negative part of the expansion of \(N\) with its final digits \(01\) removed; for example (A)(a) is \(\gamma^-(M + L_{2n}) = \gamma^-(M)\,10\). In (B)(c) the source writes \(\gamma^-(N - L_{2n+1})\) for \(N \in \Lambda_{2n} + L_{2n+2}\); the shift \(L_{2n+2}\) is used here, since as printed \(n = 1\) and \(N = 10\) give \(\gamma^-(6)\,01 = 0001\) while \(\gamma^-(10) = 01\).

MetaMathlibExt.basePhi_recursive_structure_gamma · 24 lines

public theorem_wanted basePhi_recursive_structure_gamma (n : ℕ) (hn : 1 ≤ n)
    (M : ℕ) (T S : Finset ℤ) (hT : IsBasePhiExpansion M T) :
    (M ∈ Finset.Icc (lucasNumber (2 * n - 1) + 1) (lucasNumber (2 * n) - 1) →
      IsBasePhiExpansion (M + lucasNumber (2 * n)) S →
        S.filter (· < 0) = insert (1 - 2 * n : ℤ) (insert (-2 * n - 2 : ℤ)
          (T.filter (fun i => (2 - 2 * n : ℤ) ≤ i ∧ i < 0)))) ∧
    (M ∈ Finset.Icc (lucasNumber (2 * n - 2)) (lucasNumber (2 * n - 1)) →
      IsBasePhiExpansion (M + lucasNumber (2 * n + 1)) S →
        S.filter (· < 0) = insert (1 - 2 * n : ℤ) (insert (-2 * n - 2 : ℤ)
          (T.filter (fun i => (4 - 2 * n : ℤ) ≤ i ∧ i < 0)))) ∧
    (M ∈ Finset.Icc (lucasNumber (2 * n - 1) + 1) (lucasNumber (2 * n) - 1) →
      IsBasePhiExpansion (M + lucasNumber (2 * n + 1)) S →
        S.filter (· < 0) = insert (-2 * n - 2 : ℤ) (T.filter (fun i => (2 - 2 * n : ℤ) ≤ i ∧ i < 0))) ∧
    (M ∈ Finset.Icc (lucasNumber (2 * n)) (lucasNumber (2 * n + 1)) →
      IsBasePhiExpansion (M + lucasNumber (2 * n + 1)) S →
        S.filter (· < 0) = insert (-2 * n - 2 : ℤ) (T.filter (fun i => (2 - 2 * n : ℤ) ≤ i ∧ i < 0))) ∧
    (M ∈ Finset.Icc (lucasNumber (2 * n - 1) + 1) (lucasNumber (2 * n) - 1) →
      IsBasePhiExpansion (M + lucasNumber (2 * n + 2)) S →
        S.filter (· < 0) = insert (-(2 * n : ℤ)) (insert (-2 * n - 2 : ℤ)
          (T.filter (fun i => (2 - 2 * n : ℤ) ≤ i ∧ i < 0)))) ∧
    (M ∈ Finset.Icc (lucasNumber (2 * n)) (lucasNumber (2 * n + 1)) →
      IsBasePhiExpansion (M + lucasNumber (2 * n + 2)) S →
        S.filter (· < 0) = insert (-(2 * n : ℤ)) (insert (-2 * n - 2 : ℤ)
          (T.filter (fun i => (2 - 2 * n : ℤ) ≤ i ∧ i < 0))))

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Theorem 10.

Uses 2

Statement usesBase phi expansion · Lucas numbers

TheoremThe codes of the negative parts follow an orbit of addition modulo a Fibonacci number#●ready to prove

Let \(n \ge 1\), write \(F_k\) for the Fibonacci numbers and \(L_k\) for the Lucas numbers, and let \(c\) be a function from the natural numbers to the natural numbers such that \(c(N) = \sum_{i \in S,\, i < 0} F_{i+2n}\) (with \(F_k\) read as \(0\) for \(k < 0\)) whenever \(S\) is a base phi expansion of \(N\). List the values \(c(N)\) for \(N = L_{2n-1} + 1, \dots, L_{2n+1}\) (the interval \(\Xi_n\)) in increasing order of \(N\), and merge every run of equal consecutive values into a single entry. The resulting list is \((F_{2n} - 1 + j F_{2n-2}) \bmod F_{2n}\) for \(j = 0, 1, \dots, F_{2n} - 1\): the orbit of \(F_{2n} - 1\) under addition of \(F_{2n-2}\) in \(\mathbb{Z}/F_{2n}\mathbb{Z}\).

Here \(c(N)\) is the paper's code \(C(N)\) of the negative part \(\beta^-(N)\) (the digits of \(N\) at negative positions), and the merged runs are its tridents.

public theorem_wanted basePhi_negative_part_order_orbit (n : ℕ) (hn : 1 ≤ n) (c : ℕ → ℕ)
    (hc : ∀ N S, IsBasePhiExpansion N S →
      c N = ∑ i ∈ S.filter (· < 0), Nat.fib (i + 2 * n).toNat) :
    ((List.range' (lucasNumber (2 * n - 1) + 1) (lucasNumber (2 * n))).map c).destutter
        (· ≠ ·) =
      (List.range (Nat.fib (2 * n))).map
        (fun j => (Nat.fib (2 * n) - 1 + j * Nat.fib (2 * n - 2)) % Nat.fib (2 * n))

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Theorem 11.

Uses 2

Statement usesBase phi expansion · Lucas numbers

DefinitionLeft end of a Lucas interval#✓fully proved

Let \(L_0 = 2\), \(L_1 = 1\), \(L_{j+2} = L_{j+1} + L_j\) be the Lucas numbers, and let the Lucas intervals be \(\Lambda_{2n} = [L_{2n}, L_{2n+1}]\) and \(\Lambda_{2n+1} = [L_{2n+1} + 1, L_{2n+2} - 1]\). The left end of \(\Lambda_m\) is \(L_m\) when \(m\) is even and \(L_m + 1\) when \(m\) is odd.

def lucasIntervalLo (m : ℕ) : ℕ := if Even m then lucasNumber m else lucasNumber m + 1

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Section 3 (Lucas intervals).

Uses 1 · Used by 6

Statement usesLucas numbers

Used byLucas tilings · Lucas tilings of a list with a first interval · Dekking's Theorem 4: the coding of the canonical splittings of Lucas intervals · Endpoints of the Lucas interval \(\Lambda_5\) · Endpoints of the Lucas interval \(\Lambda_4\) · Endpoints of the Lucas interval \(\Lambda_3\)

DefinitionRight end of a Lucas interval#✓fully proved

Let \(L_0 = 2\), \(L_1 = 1\), \(L_{j+2} = L_{j+1} + L_j\) be the Lucas numbers, and let the Lucas intervals be \(\Lambda_{2n} = [L_{2n}, L_{2n+1}]\) and \(\Lambda_{2n+1} = [L_{2n+1} + 1, L_{2n+2} - 1]\). The right end of \(\Lambda_m\) is \(L_{m+1}\) when \(m\) is even and \(L_{m+1} - 1\) when \(m\) is odd.

def lucasIntervalHi (m : ℕ) : ℕ := if Even m then lucasNumber (m + 1) else lucasNumber (m + 1) - 1

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Section 3 (Lucas intervals).

Uses 1 · Used by 6

Statement usesLucas numbers

Used byLucas tilings · Lucas tilings of a list with a first interval · Dekking's Theorem 4: the coding of the canonical splittings of Lucas intervals · Endpoints of the Lucas interval \(\Lambda_5\) · Endpoints of the Lucas interval \(\Lambda_4\) · Endpoints of the Lucas interval \(\Lambda_3\)

TheoremEndpoints of the Lucas interval \(\Lambda_3\)#✓fully proved

The Lucas interval \(\Lambda_3\) has left end \(5\) and right end \(6\), that is, \(\Lambda_3 = [5, 6]\).

theorem lucasInterval_three : lucasIntervalLo 3 = 5 ∧ lucasIntervalHi 3 = 6

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Section 3.

Uses 2

Statement usesRight end of a Lucas interval · Left end of a Lucas interval

TheoremEndpoints of the Lucas interval \(\Lambda_4\)#✓fully proved

The Lucas interval \(\Lambda_4\) has left end \(7\) and right end \(11\), that is, \(\Lambda_4 = [7, 11]\).

theorem lucasInterval_four : lucasIntervalLo 4 = 7 ∧ lucasIntervalHi 4 = 11

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Section 3.

Uses 2

Statement usesRight end of a Lucas interval · Left end of a Lucas interval

TheoremEndpoints of the Lucas interval \(\Lambda_5\)#✓fully proved

The Lucas interval \(\Lambda_5\) has left end \(12\) and right end \(17\), that is, \(\Lambda_5 = [12, 17]\).

theorem lucasInterval_five : lucasIntervalLo 5 = 12 ∧ lucasIntervalHi 5 = 17

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Section 3.

Uses 2

Statement usesRight end of a Lucas interval · Left end of a Lucas interval

DefinitionLucas tilings#✓fully proved

Write \(\Lambda_k = [\ell_k, h_k]\) for the Lucas interval with left end \(\ell_k\) and right end \(h_k\). For natural numbers \(a\), \(b\) and a list \(P\) of pairs \((k, t)\) of natural numbers, \(P\) is a Lucas tiling of \([a, b]\) when the translated Lucas intervals \(\Lambda_k + t\), \((k, t) \in P\), taken in the order of \(P\), are adjacent and their union is \([a, b]\). Precisely, it is defined by recursion on \(P\): the empty list is a Lucas tiling of \([a, b]\) exactly when \(a = b + 1\), and the list consisting of \((k, t)\) followed by \(P\) is a Lucas tiling of \([a, b]\) exactly when \(\ell_k + t = a\) and \(P\) is a Lucas tiling of \([h_k + t + 1, b]\).

def IsLucasTiling : ℕ → ℕ → List (ℕ × ℕ) → Prop
  | a, b, [] => a = b + 1
  | a, b, p :: P => lucasIntervalLo p.1 + p.2 = a ∧ IsLucasTiling (lucasIntervalHi p.1 + p.2 + 1) b P

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Section 4 ("a union of adjacent translations" of Lucas intervals).

Uses 2 · Used by 4

Statement usesRight end of a Lucas interval · Left end of a Lucas interval

Used byLucas tilings of a list with a first interval · Lucas tilings by the empty list · Dekking's Theorem 4: the coding of the canonical splittings of Lucas intervals · Canonical splitting and coding of unions of two Lucas intervals

TheoremLucas tilings by the empty list#✓fully proved

For all natural numbers \(a\) and \(b\), the empty list is a Lucas tiling of \([a, b]\) if and only if \(a = b + 1\).

theorem isLucasTiling_nil (a b : ℕ) : IsLucasTiling a b [] ↔ a = b + 1

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Section 4.

Uses 1

Statement usesLucas tilings

TheoremLucas tilings of a list with a first interval#✓fully proved

Write \(\Lambda_k = [\ell_k, h_k]\) for the Lucas interval with left end \(\ell_k\) and right end \(h_k\). For all natural numbers \(a\), \(b\), \(k\), \(t\) and every list \(P\) of pairs of natural numbers, the list consisting of \((k, t)\) followed by \(P\) is a Lucas tiling of \([a, b]\) if and only if \(\ell_k + t = a\) and \(P\) is a Lucas tiling of \([h_k + t + 1, b]\).

theorem isLucasTiling_cons (a b : ℕ) (p : ℕ × ℕ) (P : List (ℕ × ℕ)) :
    IsLucasTiling a b (p :: P) ↔
      lucasIntervalLo p.1 + p.2 = a ∧ IsLucasTiling (lucasIntervalHi p.1 + p.2 + 1) b P

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Section 4.

Uses 3

Statement usesLucas tilings · Right end of a Lucas interval · Left end of a Lucas interval

DefinitionCanonical splitting of a Lucas interval#✓fully proved

Let \(L_j\) be the \(j\)-th Lucas number (\(L_0 = 2\), \(L_1 = 1\), \(L_{j+2} = L_{j+1} + L_j\)). For a natural number \(m\), the canonical splitting of the Lucas interval \(\Lambda_m\) is the list of pairs \((k, t)\) of natural numbers defined by recursion on \(m\): for \(m \le 5\) it is the one-pair list \([(m, 0)]\), and for \(m \ge 6\) it is the concatenation, in this order, of the canonical splitting of \(\Lambda_{m-2}\) with \(L_{m-1}\) added to the second coordinate of each pair, the canonical splitting of \(\Lambda_{m-3}\) with \(L_m\) added to the second coordinate of each pair, and the canonical splitting of \(\Lambda_{m-2}\) with \(L_m\) added to the second coordinate of each pair.

Here \(\Lambda_{2n} = [L_{2n}, L_{2n+1}]\) and \(\Lambda_{2n+1} = [L_{2n+1} + 1, L_{2n+2} - 1]\), and a pair \((k, t)\) stands for the translate \(\Lambda_k + t\). The recursion follows the second Recursive Structure Theorem \(\Lambda_m = (\Lambda_{m-2} + L_{m-1}) \cup (\Lambda_{m-3} + L_m) \cup (\Lambda_{m-2} + L_m)\) (the paper's splittings of \(\Lambda_6, \Lambda_7, \Lambda_8\), "continuing in this fashion"). That for \(m \ge 3\) the result splits \(\Lambda_m\) into adjacent translates of \(\Lambda_3\), \(\Lambda_4\) and \(\Lambda_5\) is the paper's Theorem 4. Only \(m \ge 3\) is used.

def canonicalLucasSplitting : ℕ → List (ℕ × ℕ)
  | m + 6 =>
      (canonicalLucasSplitting (m + 4)).map (fun p => (p.1, p.2 + lucasNumber (m + 5))) ++
        (canonicalLucasSplitting (m + 3)).map (fun p => (p.1, p.2 + lucasNumber (m + 6))) ++
        (canonicalLucasSplitting (m + 4)).map (fun p => (p.1, p.2 + lucasNumber (m + 6)))
  | m => [(m, 0)]

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Section 4 (canonical splitting).

Uses 1 · Used by 5

Statement usesLucas numbers

Used byRecursion for the canonical splitting · Canonical splitting of a short Lucas interval · Canonical splitting of the sixth Lucas interval · Dekking's Theorem 4: the coding of the canonical splittings of Lucas intervals · Canonical splitting and coding of unions of two Lucas intervals

TheoremCanonical splitting of a short Lucas interval#✓fully proved

For every natural number \(m < 6\), the canonical splitting of the Lucas interval \(\Lambda_m\) is the one-pair list \([(m, 0)]\), that is, \(\Lambda_m\) itself.

theorem canonicalLucasSplitting_of_lt_six (m : ℕ) (hm : m < 6) :
    canonicalLucasSplitting m = [(m, 0)]

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Section 4.

Uses 1

Statement usesCanonical splitting of a Lucas interval

TheoremRecursion for the canonical splitting#✓fully proved

For every natural number \(m\), the canonical splitting of the Lucas interval \(\Lambda_{m+6}\) is the concatenation, in this order, of the canonical splitting of \(\Lambda_{m+4}\) with \(L_{m+5}\) added to the second coordinate of each pair, the canonical splitting of \(\Lambda_{m+3}\) with \(L_{m+6}\) added to the second coordinate of each pair, and the canonical splitting of \(\Lambda_{m+4}\) with \(L_{m+6}\) added to the second coordinate of each pair, where \(L_j\) is the \(j\)-th Lucas number.

theorem canonicalLucasSplitting_add_six (m : ℕ) :
    canonicalLucasSplitting (m + 6) =
      (canonicalLucasSplitting (m + 4)).map (fun p => (p.1, p.2 + lucasNumber (m + 5))) ++
        (canonicalLucasSplitting (m + 3)).map (fun p => (p.1, p.2 + lucasNumber (m + 6))) ++
        (canonicalLucasSplitting (m + 4)).map (fun p => (p.1, p.2 + lucasNumber (m + 6)))

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Section 4.

Uses 2

Statement usesCanonical splitting of a Lucas interval · Lucas numbers

TheoremCanonical splitting of the sixth Lucas interval#✓fully proved

The canonical splitting of the Lucas interval \(\Lambda_6\) is the list \([(4, 11), (3, 18), (4, 18)]\).

The pairs stand for the translates \(\Lambda_4 + L_5\), \(\Lambda_3 + L_6\) and \(\Lambda_4 + L_6\), where \(L_5 = 11\) and \(L_6 = 18\) are Lucas numbers.

theorem canonicalLucasSplitting_six :
    canonicalLucasSplitting 6 = [(4, 11), (3, 18), (4, 18)]

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Section 4.

Uses 1

Statement usesCanonical splitting of a Lucas interval

TheoremDekking's Theorem 4: the coding of the canonical splittings of Lucas intervals#●ready to prove

Write \(\Lambda_m = [\ell_m, h_m]\) for the Lucas interval with left end \(\ell_m\) and right end \(h_m\). For every \(n \ge 3\), every pair \((k, t)\) in the canonical splitting of \(\Lambda_n\) has \(k \in \{3, 4, 5\}\), and the canonical splitting of \(\Lambda_n\) is a Lucas tiling of \([\ell_n, h_n]\). Let \(\kappa\) be the map on finite words of natural numbers that replaces each letter \(3\) by the word \(5\), each letter \(4\) by \(434\) and every other letter by \(545\), and let \(C(\Lambda_m)\) be the word formed by the first components \(k\) of the pairs \((k, t)\) of the canonical splitting of \(\Lambda_m\), in order. Then for every \(n \ge 0\), \(C(\Lambda_{2n+4}) = \kappa^n(4)\) and \(C(\Lambda_{2n+5}) = \kappa^n(5)\), where \(\kappa^n\) is the \(n\)-fold iterate of \(\kappa\) applied to the one-letter word.

public theorem_wanted lucasInterval_canonical_splitting_coding :
    (∀ n : ℕ, 3 ≤ n →
      (∀ p ∈ canonicalLucasSplitting n, p.1 = 3 ∨ p.1 = 4 ∨ p.1 = 5) ∧
        IsLucasTiling (lucasIntervalLo n) (lucasIntervalHi n) (canonicalLucasSplitting n)) ∧
    ∀ n : ℕ,
      (canonicalLucasSplitting (2 * n + 4)).map Prod.fst =
          (List.flatMap (fun x : ℕ => if x = 3 then [5] else if x = 4 then [4, 3, 4]
            else [5, 4, 5]))^[n] [4] ∧
        (canonicalLucasSplitting (2 * n + 5)).map Prod.fst =
          (List.flatMap (fun x : ℕ => if x = 3 then [5] else if x = 4 then [4, 3, 4]
            else [5, 4, 5]))^[n] [5]

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Theorem 4.

Uses 4

Statement usesLucas tilings · Canonical splitting of a Lucas interval · Right end of a Lucas interval · Left end of a Lucas interval

TheoremCanonical splitting and coding of unions of two Lucas intervals#●ready to prove

Let \(L_m\) denote the \(m\)-th Lucas number and \(\Lambda_m\) the Lucas interval, so \(\Lambda_{2k} = [L_{2k}, L_{2k+1}]\) and \(\Lambda_{2k+1} = [L_{2k+1} + 1, L_{2k+2} - 1]\). For \(n \ge 2\), let \(P_n\) be the canonical splitting of \(\Lambda_{2n-1}\) followed by the canonical splitting of \(\Lambda_{2n}\), a list of translations \(\Lambda_k + t\). Then every index \(k\) occurring in \(P_n\) is \(3\), \(4\) or \(5\), and the intervals of \(P_n\), taken in order, are adjacent with union \([L_{2n-1} + 1, L_{2n+1}]\). Moreover, for every \(n \ge 0\) the list of indices \(k\) of \(P_{n+2}\) (the coding \(C(\Xi_{n+2})\), where \(\Xi_n = \Lambda_{2n-1} \cup \Lambda_{2n}\)) equals \(\delta(h^n(b))\), where \(h\) is the morphism \(a \mapsto aab\), \(b \mapsto ab\) on words over \(\{a, b\}\) and \(\delta\) is the morphism \(a \mapsto 54\), \(b \mapsto 34\).

public theorem_wanted xi_canonical_splitting_coding :
    (∀ n : ℕ, 2 ≤ n →
      (∀ p ∈ canonicalLucasSplitting (2 * n - 1) ++ canonicalLucasSplitting (2 * n),
          p.1 = 3 ∨ p.1 = 4 ∨ p.1 = 5) ∧
        IsLucasTiling (lucasNumber (2 * n - 1) + 1) (lucasNumber (2 * n + 1))
          (canonicalLucasSplitting (2 * n - 1) ++ canonicalLucasSplitting (2 * n))) ∧
    ∀ n : ℕ,
      (canonicalLucasSplitting (2 * n + 3) ++ canonicalLucasSplitting (2 * n + 4)).map Prod.fst =
        ((List.flatMap (fun c : Char => if c = 'a' then ['a', 'a', 'b'] else ['a', 'b']))^[n]
          ['b']).flatMap (fun c : Char => if c = 'a' then [5, 4] else [3, 4])

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Theorem 5.

Uses 3

Statement usesLucas tilings · Canonical splitting of a Lucas interval · Lucas numbers

TheoremTrident splitting at an even Lucas number#●ready to prove

Let \(n \ge 1\) and let \(L_{2n}\) be the \(2n\)-th Lucas number. If \(S_1\), \(S_2\) and \(S_3\) are base phi expansions of \(L_{2n} - 1\), \(L_{2n}\) and \(L_{2n} + 1\) respectively, each given as the set of positions of its digits \(1\), then the negative positions \(i < 0\) of \(S_1\), of \(S_2\) and of \(S_3\) are the same.

In the paper's terms, the last number \(L_{2n} - 1\) of the Lucas interval \(\Lambda_{2n-1}\) and the first two numbers \(L_{2n}\), \(L_{2n} + 1\) of \(\Lambda_{2n}\) form a trident: three consecutive numbers \(N\), \(N + 1\), \(N + 2\) with \(\beta^-(N) = \beta^-(N+1) = \beta^-(N+2)\), where \(\beta^-\) is the negative part of the base phi expansion.

public theorem_wanted basePhi_trident_splitting (n : ℕ) (hn : 1 ≤ n) (S₁ S₂ S₃ : Finset ℤ)
    (h₁ : IsBasePhiExpansion (lucasNumber (2 * n) - 1) S₁)
    (h₂ : IsBasePhiExpansion (lucasNumber (2 * n)) S₂)
    (h₃ : IsBasePhiExpansion (lucasNumber (2 * n) + 1) S₃) :
    S₁.filter (· < 0) = S₂.filter (· < 0) ∧ S₂.filter (· < 0) = S₃.filter (· < 0)

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Lemma 8.

Uses 2

Statement usesBase phi expansion · Lucas numbers

TheoremThe codes of the negative parts follow the golden rotation#●ready to prove

Let \(n \ge 1\), write \(\varphi\) for the golden ratio, \(F_k\) for the Fibonacci numbers and \(L_k\) for the Lucas numbers, and let \(c\) be a function from the natural numbers to the natural numbers such that \(c(N) = \sum_{i \in S,\, i < 0} F_{i+2n}\) (with \(F_k\) read as \(0\) for \(k < 0\)) whenever \(S\) is a base phi expansion of \(N\). List the values \(c(N)\) for \(N = L_{2n-1} + 1, \dots, L_{2n+1}\) (the interval \(\Xi_n\)) in increasing order of \(N\), and merge every run of equal consecutive values into a single entry. The resulting list is a permutation of \(0, 1, \dots, F_{2n} - 1\), and the fractional parts \(\{(k+1)\varphi\}\) of its entries \(k\) strictly decrease along it: if \(k\) comes before \(k'\), then \(\{(k'+1)\varphi\} < \{(k+1)\varphi\}\).

This list is the paper's permutation \(\Pi^\beta_{2n}\) (the codes \(C(N)\) of the negative parts \(\beta^-(N)\), tridents merged, as in Theorem 11), and the statement says it is the order in which the first \(F_{2n}\) iterates of the rotation \(z \mapsto \exp(2\pi i(z - \varphi))\) occur on the circle, the entry \(k\) standing for the iterate number \(k + 1\). This is the reading fixed by the paper's worked case \(n = 3\), where \(\Pi^\beta_6 = 7\,2\,5\,0\,3\,6\,1\,4\).

public theorem_wanted basePhi_negative_part_order_rotation (n : ℕ) (hn : 1 ≤ n) (c : ℕ → ℕ)
    (hc : ∀ N S, IsBasePhiExpansion N S →
      c N = ∑ i ∈ S.filter (· < 0), Nat.fib (i + 2 * n).toNat) :
    (((List.range' (lucasNumber (2 * n - 1) + 1) (lucasNumber (2 * n))).map c).destutter
        (· ≠ ·)).Perm (List.range (Nat.fib (2 * n))) ∧
      (((List.range' (lucasNumber (2 * n - 1) + 1) (lucasNumber (2 * n))).map c).destutter
        (· ≠ ·)).Pairwise
          (fun i j => Int.fract (((j : ℝ) + 1) * φ) < Int.fract (((i : ℝ) + 1) * φ))

Sources

• F. Michel Dekking, The Structure of Base Phi Expansions, INTEGERS 24 (2024), Article A24, Theorem 12.

Uses 2

Statement usesBase phi expansion · Lucas numbers

46 fully proved38 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.