Accessible sets and diffsequences

DefinitionMonochromatic sequences of positive integers#✓fully proved

Let \(r\) and \(k\) be natural numbers and let \(c\) color the positive integers with the colors \(0, 1, \dots, r - 1\). A sequence \(x_0, \dots, x_{k-1}\) of positive integers is monochromatic for \(c\) when \(c(x_i) = c(x_j)\) for all \(i, j < k\).

public def IsMonochromatic {r k : ℕ} (c : ℕ+ → Fin r)
    (x : Fin k → ℕ+) : Prop :=
  ∀ i j, c (x i) = c (x j)

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Definition (r-large).

Used by 12

Used byColorings avoiding long diffsequences under fractional-part bounds · A 2-coloring with no monochromatic 4-term even-Fibonacci diffsequence · Arithmetic progressions with Fibonacci gaps are not \(2\)-regular · The Fibonacci numbers have degree of accessibility at most \(3\) · A 2-coloring with no monochromatic 6-term progression with positive Fibonacci gap · \(r\)-accessibility for colorings of the positive integers · Characterization of \(r\)-accessible sets · \(r\)-large sets · Characterization of \(r\)-large sets · The Lucas numbers are not \(4\)-accessible · Accessibility with more colors implies accessibility with fewer · Two-colorings avoiding long \(D\)-progressions

DefinitionArithmetic progressions with gap in \(D\)#✓fully proved

Let \(D\) be a set of natural numbers and \(k\) a natural number. A sequence \(x_0, \dots, x_{k-1}\) of positive integers is a \(k\)-term arithmetic progression with gap in \(D\) if there are a positive integer \(a\) and an element \(d \in D\) such that \(x_i = a + i d\) for every \(i < k\).

public def IsDAP (D : Set ℕ) (k : ℕ) (x : Fin k → ℕ+) : Prop :=
  ∃ a : ℕ+, ∃ d ∈ D, ∀ i, (x i : ℕ) = a + (i : ℕ) * d

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Definition (r-large).

Used by 6

Used byArithmetic progressions with Fibonacci gaps are not \(2\)-regular · A 2-coloring with no monochromatic 6-term progression with positive Fibonacci gap · Characterization of arithmetic progressions with gap in \(D\) · \(r\)-large sets · Characterization of \(r\)-large sets · Two-colorings avoiding long \(D\)-progressions

TheoremCharacterization of arithmetic progressions with gap in \(D\)#✓fully proved

Let \(D\) be a set of natural numbers, \(k\) a natural number and \(x_0, \dots, x_{k-1}\) positive integers. Then \(x_0, \dots, x_{k-1}\) is a \(k\)-term arithmetic progression with gap in \(D\) if and only if there are a positive integer \(a\) and an element \(d \in D\) such that \(x_i = a + i d\) for every \(i < k\).

public theorem isDAP_iff (D : Set ℕ) (k : ℕ) (x : Fin k → ℕ+) :
    IsDAP D k x ↔ ∃ a : ℕ+, ∃ d ∈ D, ∀ i, (x i : ℕ) = a + (i : ℕ) * d

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Definition (r-large).

Uses 1

Statement usesArithmetic progressions with gap in \(D\)

Definition\(r\)-large sets#✓fully proved

Let \(r\) be a natural number. A set \(D\) of natural numbers is \(r\)-large when every element of \(D\) is positive, \(r \ge 1\), and for every coloring \(c\) of the positive integers with the colors \(0, 1, \dots, r - 1\) and every natural number \(k \ge 1\) there are positive integers \(x_0, \dots, x_{k-1}\) that are monochromatic for \(c\) and form a \(D\)-AP: there are a positive integer \(a\) and some \(d \in D\) with \(x_i = a + i d\) for all \(i < k\).

Quantifying over every length \(k \ge 1\) formalizes "arbitrarily long" monochromatic \(D\)-APs.

public def IsRLarge (r : ℕ) (D : Set ℕ) : Prop :=
  D ⊆ Set.Ioi 0 ∧ 1 ≤ r ∧
    ∀ (c : ℕ+ → Fin r) (k : ℕ), 1 ≤ k →
      ∃ x : Fin k → ℕ+, IsMonochromatic c x ∧ IsDAP D k x

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Definition (r-large).

Uses 2 · Used by 9

Statement usesArithmetic progressions with gap in \(D\) · Monochromatic sequences of positive integers

Used byArithmetic progressions with Fibonacci gaps are not \(2\)-regular · The positive Fibonacci set is not 2-large · Finite unions of lacunary sets are not 2-large · Large set · Characterization of large sets · Characterization of \(r\)-large sets · Sets growing by a factor of three are not 2-large · Finite removal preserves \(r\)-largeness · 2-large sets contain multiples of every positive integer

TheoremCharacterization of \(r\)-large sets#✓fully proved

Let \(r\) be a natural number and \(D\) a set of natural numbers. Then \(D\) is \(r\)-large if and only if every element of \(D\) is positive, \(r \ge 1\), and for every coloring \(c\) of the positive integers with the colors \(0, 1, \dots, r - 1\) and every natural number \(k \ge 1\) there are positive integers \(x_0, \dots, x_{k-1}\) that are monochromatic for \(c\) and form a \(D\)-AP: there are a positive integer \(a\) and some \(d \in D\) with \(x_i = a + i d\) for all \(i < k\).

public theorem isRLarge_iff (r : ℕ) (D : Set ℕ) :
    IsRLarge r D ↔ D ⊆ Set.Ioi 0 ∧ 1 ≤ r ∧
      ∀ (c : ℕ+ → Fin r) (k : ℕ), 1 ≤ k →
        ∃ x : Fin k → ℕ+, IsMonochromatic c x ∧ IsDAP D k x

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Definition (r-large).

Uses 3

Statement usesArithmetic progressions with gap in \(D\) · Monochromatic sequences of positive integers · \(r\)-large sets

DefinitionLarge set#✓fully proved

A set \(D\) of natural numbers is large when it is \(r\)-large for every natural number \(r \ge 1\).

public def IsLarge (D : Set ℕ) : Prop :=
  ∀ r : ℕ, 1 ≤ r → IsRLarge r D

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Definition (r-large).

Uses 1 · Used by 3

Statement uses\(r\)-large sets

Used byCharacterization of large sets · Largeness is partition regular · Positive values of a polynomial vanishing at zero form a large set

TheoremCharacterization of large sets#✓fully proved

A set \(D\) of natural numbers is large if and only if it is \(r\)-large for every natural number \(r \ge 1\).

public theorem isLarge_iff (D : Set ℕ) : IsLarge D ↔ ∀ r : ℕ, 1 ≤ r → IsRLarge r D

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Definition (r-large).

Uses 2

Statement usesLarge set · \(r\)-large sets

Definition\(D\)-diffsequences#✓fully proved

Let \(D\) be a set of natural numbers and \(k\) a natural number. A finite sequence \(x_0, \dots, x_{k-1}\) of integers is a \(D\)-diffsequence when for every \(i\) with \(i + 1 < k\) there is \(d \in D\) with \(x_{i+1} - x_i = d\).

public def IsDDiffSequence (D : Set ℕ) {k : ℕ} (x : Fin k → ℤ) : Prop :=
  ∀ (i : ℕ) (h : i + 1 < k),
    ∃ d ∈ D, x ⟨i + 1, h⟩ - x ⟨i, by omega⟩ = (d : ℤ)

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Definition (D-diffsequence).

Used by 11

Used byA coloring criterion for accessibility of a shifted set · Colorings avoiding long diffsequences under fractional-part bounds · A 2-coloring with no monochromatic 4-term even-Fibonacci diffsequence · The Fibonacci numbers have degree of accessibility at most \(3\) · Characterization of \(D\)-diffsequences · \(r\)-accessibility for colorings of the positive integers · Characterization of \(r\)-accessible sets · The Lucas numbers are not \(4\)-accessible · Accessibility with more colors implies accessibility with fewer · Topological recurrence, accessibility and chromatic intersectivity · Sets containing their own long diffsequences are 2-accessible

TheoremCharacterization of \(D\)-diffsequences#✓fully proved

Let \(D\) be a set of natural numbers and \(x_0, \dots, x_{k-1}\) integers. Then \(x_0, \dots, x_{k-1}\) is a \(D\)-diffsequence if and only if for every \(i\) with \(i + 1 < k\) there is \(d \in D\) such that \(x_{i+1} - x_i = d\).

public theorem isDDiffSequence_iff (D : Set ℕ) {k : ℕ} (x : Fin k → ℤ) :
    IsDDiffSequence D x ↔ ∀ (i : ℕ) (h : i + 1 < k),
      ∃ d ∈ D, x ⟨i + 1, h⟩ - x ⟨i, by omega⟩ = (d : ℤ)

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Definition (D-diffsequence).

Uses 1

Statement uses\(D\)-diffsequences

Definition\(r\)-accessibility for colorings of the positive integers#✓fully proved

Let \(r\) be a natural number. A set \(D\) of natural numbers is \(r\)-accessible when every element of \(D\) is positive, \(r \ge 1\), and for every coloring \(c\) of the positive integers with the colors \(0, 1, \dots, r - 1\) and every natural number \(k \ge 1\) there are positive integers \(x_0, \dots, x_{k-1}\) that are monochromatic for \(c\) and form a \(D\)-diffsequence: \(x_{i+1} - x_i \in D\), the difference taken in the integers, for every \(i\) with \(i + 1 < k\).

public def IsRAccessible (r : ℕ) (D : Set ℕ) : Prop :=
  D ⊆ Set.Ioi 0 ∧ 1 ≤ r ∧
    ∀ (c : ℕ+ → Fin r) (k : ℕ), 1 ≤ k →
      ∃ x : Fin k → ℕ+,
        IsMonochromatic c x ∧ IsDDiffSequence D (fun i => ((x i : ℕ) : ℤ))

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Definition (r-accessible).

Uses 2 · Used by 15

Statement uses\(D\)-diffsequences · Monochromatic sequences of positive integers

Used byGrowth bound for the degree of accessibility · Multiples of \(d\) in an accessible set · Integral quotients of an accessible set · A coloring criterion for accessibility of a shifted set · The even Fibonacci set is not 2-accessible · The even Fibonacci numbers have degree of accessibility \(1\) · The Fibonacci numbers have degree of accessibility at most \(3\) · Accessible sets · Accessibility means \(r\)-accessibility for every \(r \ge 1\) · Characterization of \(r\)-accessible sets · The Lucas numbers are not \(4\)-accessible · Accessibility with more colors implies accessibility with fewer · Halved even Fibonacci numbers and \(4\)-accessibility of the Fibonacci numbers · Fast eventual growth rules out 2-accessibility · Sets containing their own long diffsequences are 2-accessible

TheoremCharacterization of \(r\)-accessible sets#✓fully proved

Let \(r\) be a natural number and \(D\) a set of natural numbers. Then \(D\) is \(r\)-accessible if and only if every element of \(D\) is positive, \(r \ge 1\), and for every coloring \(c\) of the positive integers with the colors \(0, 1, \dots, r - 1\) and every natural number \(k \ge 1\) there are positive integers \(x_0, \dots, x_{k-1}\) that are monochromatic for \(c\) and form a \(D\)-diffsequence: \(x_{i+1} - x_i \in D\), the difference taken in the integers, for every \(i\) with \(i + 1 < k\).

public theorem isRAccessible_iff (r : ℕ) (D : Set ℕ) :
    IsRAccessible r D ↔ D ⊆ Set.Ioi 0 ∧ 1 ≤ r ∧
      ∀ (c : ℕ+ → Fin r) (k : ℕ), 1 ≤ k →
        ∃ x : Fin k → ℕ+,
          IsMonochromatic c x ∧ IsDDiffSequence D (fun i => ((x i : ℕ) : ℤ))

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Definition (r-accessible).

Uses 3

Statement uses\(D\)-diffsequences · Monochromatic sequences of positive integers · \(r\)-accessibility for colorings of the positive integers

TheoremAccessibility with more colors implies accessibility with fewer#✓fully proved

Let \(D\) be a set of natural numbers and let \(r, s\) be natural numbers with \(1 \le r \le s\). If \(D\) is \(s\)-accessible, then \(D\) is \(r\)-accessible.

public theorem IsRAccessible.mono (D : Set ℕ) {r s : ℕ} (h : IsRAccessible s D)
    (hr : 1 ≤ r) (hrs : r ≤ s) : IsRAccessible r D

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Definition (r-accessible).

Uses 3

Statement uses\(r\)-accessibility for colorings of the positive integers

Proof uses\(D\)-diffsequences · Monochromatic sequences of positive integers

DefinitionAccessible sets#✓fully proved

A set \(D\) of natural numbers is accessible if it is \(r\)-accessible for every natural number \(r \ge 1\).

public def IsAccessible (D : Set ℕ) : Prop :=
  ∀ r : ℕ, 1 ≤ r → IsRAccessible r D

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Definition (r-accessible).

Uses 1 · Used by 3

Statement uses\(r\)-accessibility for colorings of the positive integers

Used byOne part of an accessible union is accessible · Accessibility means \(r\)-accessibility for every \(r \ge 1\) · Topological recurrence, accessibility and chromatic intersectivity

TheoremAccessibility means \(r\)-accessibility for every \(r \ge 1\)#✓fully proved

A set \(D\) of natural numbers is accessible if and only if it is \(r\)-accessible for every natural number \(r \ge 1\).

public theorem isAccessible_iff (D : Set ℕ) :
    IsAccessible D ↔ ∀ r : ℕ, 1 ≤ r → IsRAccessible r D

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Definition (r-accessible).

Uses 2

Statement usesAccessible sets · \(r\)-accessibility for colorings of the positive integers

DefinitionLacunary sequence#✓fully proved

A sequence \((m_n)_{n \ge 0}\) of natural numbers is lacunary when \(m_n > 0\) for every \(n\) and there is a real number \(\lambda > 1\) such that \(m_{n+1} \ge \lambda m_n\) for every \(n \ge 0\).

public def IsLacunary (m : ℕ → ℕ) : Prop :=
  (∀ n, 0 < m n) ∧ ∃ q : ℝ, 1 < q ∧
    ∀ n, (m (n + 1) : ℝ) ≥ q * (m n : ℝ)

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Context (lacunary sequence).

Used by 3

Used byCharacterization of lacunary sequences · Lacunary set · Characterization of lacunary sets

TheoremCharacterization of lacunary sequences#✓fully proved

A sequence \((m_n)_{n \ge 0}\) of natural numbers is lacunary if and only if \(m_n > 0\) for every \(n\) and there is a real number \(q > 1\) such that \(m_{n+1} \ge q \, m_n\) for every \(n \ge 0\).

public theorem isLacunary_iff (m : ℕ → ℕ) :
    IsLacunary m ↔ (∀ n, 0 < m n) ∧ ∃ q : ℝ, 1 < q ∧
      ∀ n, (m (n + 1) : ℝ) ≥ q * (m n : ℝ)

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Context (lacunary sequence).

Uses 1

Statement usesLacunary sequence

DefinitionLacunary set#✓fully proved

A set \(D\) of natural numbers is lacunary when \(D = \{m_n : n \ge 0\}\) for some lacunary sequence \((m_n)_{n \ge 0}\) of natural numbers.

public def IsLacunarySet (D : Set ℕ) : Prop :=
  ∃ m : ℕ → ℕ, IsLacunary m ∧ D = Set.range m

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Context (lacunary set).

Uses 1 · Used by 3

Statement usesLacunary sequence

Used byFinite unions of lacunary sets are not 2-large · Characterization of lacunary sets · Dilates of a finite union of lacunary sets stay away from the integers

TheoremCharacterization of lacunary sets#✓fully proved

A set \(D\) of natural numbers is lacunary if and only if there is a lacunary sequence \((m_n)_{n \ge 0}\) of natural numbers with \(D = \{m_n : n \ge 0\}\).

public theorem isLacunarySet_iff (D : Set ℕ) :
    IsLacunarySet D ↔ ∃ m : ℕ → ℕ, IsLacunary m ∧ D = Set.range m

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Context (lacunary set).

Uses 2

Statement usesLacunary sequence · Lacunary set

DefinitionMinimal system#✓fully proved

Let \(X\) be a compact metric space and \(T\) a homeomorphism of \(X\). The system \((X, T)\) is minimal when there is no closed set \(K \subseteq X\) that is nonempty, different from \(X\) and invariant, meaning \(T(K) = K\).

public def IsMinimalSystem {X : Type*} [MetricSpace X] [CompactSpace X]
    (T : X ≃ₜ X) : Prop :=
  ¬ ∃ K : Set X, IsClosed K ∧ K.Nonempty ∧ K ≠ Set.univ ∧ T '' K = K

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Definition (topological dynamical system, minimal).

Used by 5

Used byFurstenberg–Weiss correspondence for translation-invariant families · Sets of \(\ell\)-topological recurrence · Characterization of \(\ell\)-topological recurrence · Characterization of minimal systems · Topological recurrence, accessibility and chromatic intersectivity

TheoremCharacterization of minimal systems#✓fully proved

Let \(X\) be a compact metric space and \(T \colon X \to X\) a homeomorphism. Then \(T\) is minimal if and only if there is no closed set \(K \subseteq X\) with \(K \ne \emptyset\), \(K \ne X\) and \(T(K) = K\).

public theorem isMinimalSystem_iff {X : Type*} [MetricSpace X] [CompactSpace X]
    (T : X ≃ₜ X) :
    IsMinimalSystem T ↔
      ¬ ∃ K : Set X, IsClosed K ∧ K.Nonempty ∧ K ≠ Set.univ ∧ T '' K = K

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Definition (topological dynamical system, minimal).

Uses 1

Statement usesMinimal system

DefinitionIterated preimage#✓fully proved

For a homeomorphism \(T\) of a topological space \(X\), an integer \(s\) and a subset \(U \subseteq X\), the iterated preimage \(T^{-s} U\) is defined as the preimage \((T^s)^{-1}(U)\) of \(U\) under the \(s\)-th power \(T^s\) of \(T\) in the group of homeomorphisms of \(X\).

public def iteratePreimage {X : Type*} [TopologicalSpace X] (T : X ≃ₜ X)
    (s : ℤ) (U : Set X) : Set X :=
  (T ^ s) ⁻¹' U

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Definition (ℓ-topological recurrence).

Used by 5

Used byFurstenberg–Weiss correspondence for translation-invariant families · Sets of \(\ell\)-topological recurrence · Characterization of \(\ell\)-topological recurrence · Iterated preimage as a preimage under a power · Topological recurrence, accessibility and chromatic intersectivity

TheoremIterated preimage as a preimage under a power#✓fully proved

For a homeomorphism \(T\) of a topological space \(X\), an integer \(s\) and a subset \(U \subseteq X\), the iterated preimage \(T^{-s} U\) is the preimage \((T^s)^{-1}(U)\) of \(U\) under the \(s\)-th power \(T^s\) of \(T\) in the group of homeomorphisms of \(X\).

public theorem iteratePreimage_eq {X : Type*} [TopologicalSpace X] (T : X ≃ₜ X)
    (s : ℤ) (U : Set X) : iteratePreimage T s U = (T ^ s) ⁻¹' U

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Definition (ℓ-topological recurrence).

Uses 1

Statement usesIterated preimage

DefinitionSets of \(\ell\)-topological recurrence#✓fully proved

Let \(\ell\) be a natural number. A set \(D\) of natural numbers is a set of \(\ell\)-topological recurrence when every element of \(D\) is positive and, for every compact metric space \(X\), every minimal homeomorphism \(T \colon X \to X\) and every nonempty open set \(U \subseteq X\), there is \(d \in D\) such that \(\bigcap_{j=0}^{\ell} T^{-jd}(U)\) is nonempty, where \(T^{-jd}(U)\) is the preimage of \(U\) under the \(jd\)-th iterate of \(T\).

public def IsLTopologicalRecurrence (ℓ : ℕ) (D : Set ℕ) : Prop :=
  D ⊆ Set.Ioi 0 ∧
    ∀ (X : Type) [MetricSpace X] [CompactSpace X] (T : X ≃ₜ X),
      IsMinimalSystem T → ∀ U : Set X, IsOpen U → U.Nonempty →
        ∃ d ∈ D, (⋂ j : Fin (ℓ + 1),
          iteratePreimage T (((j : ℕ) : ℤ) * (d : ℤ)) U).Nonempty

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Definition (ℓ-topological recurrence).

Uses 2 · Used by 6

Statement usesMinimal system · Iterated preimage

Used byCharacterization of \(\ell\)-topological recurrence · Sets of multiple topological recurrence · Characterization of multiple topological recurrence · Sets of topological recurrence · Topological recurrence is \(1\)-topological recurrence · One part of a union inherits \(k\)-topological recurrence

TheoremCharacterization of \(\ell\)-topological recurrence#✓fully proved

Let \(\ell\) be a natural number and \(D\) a set of natural numbers. Then \(D\) is a set of \(\ell\)-topological recurrence if and only if every element of \(D\) is positive and, for every compact metric space \(X\), every minimal homeomorphism \(T \colon X \to X\) and every nonempty open set \(U \subseteq X\), there is \(d \in D\) such that \(\bigcap_{j=0}^{\ell} T^{-jd}(U)\) is nonempty, where \(T^{-jd}(U)\) is the preimage of \(U\) under the \(jd\)-th iterate of \(T\).

public theorem isLTopologicalRecurrence_iff (ℓ : ℕ) (D : Set ℕ) :
    IsLTopologicalRecurrence ℓ D ↔ D ⊆ Set.Ioi 0 ∧
      ∀ (X : Type) [MetricSpace X] [CompactSpace X] (T : X ≃ₜ X),
        IsMinimalSystem T → ∀ U : Set X, IsOpen U → U.Nonempty →
          ∃ d ∈ D, (⋂ j : Fin (ℓ + 1),
            iteratePreimage T (((j : ℕ) : ℤ) * (d : ℤ)) U).Nonempty

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Definition (ℓ-topological recurrence).

Uses 3

Statement usesSets of \(\ell\)-topological recurrence · Minimal system · Iterated preimage

DefinitionSets of topological recurrence#✓fully proved

A set \(D\) of natural numbers is a set of topological recurrence when it is a set of \(\ell\)-topological recurrence for \(\ell = 1\).

public def IsTopologicalRecurrence (D : Set ℕ) : Prop :=
  IsLTopologicalRecurrence 1 D

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Definition (ℓ-topological recurrence).

Uses 1 · Used by 2

Statement usesSets of \(\ell\)-topological recurrence

Used byTopological recurrence is \(1\)-topological recurrence · Topological recurrence, accessibility and chromatic intersectivity

TheoremTopological recurrence is \(1\)-topological recurrence#✓fully proved

A set \(D\) of natural numbers is a set of topological recurrence if and only if it is a set of \(\ell\)-topological recurrence for \(\ell = 1\).

public theorem isTopologicalRecurrence_iff (D : Set ℕ) :
    IsTopologicalRecurrence D ↔ IsLTopologicalRecurrence 1 D

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Definition (ℓ-topological recurrence).

Uses 2

Statement usesSets of \(\ell\)-topological recurrence · Sets of topological recurrence

DefinitionSets of multiple topological recurrence#✓fully proved

A set \(D\) of natural numbers is a set of multiple topological recurrence when it is a set of \(\ell\)-topological recurrence for every natural number \(\ell \ge 1\).

public def IsMultipleTopologicalRecurrence (D : Set ℕ) : Prop :=
  ∀ ℓ : ℕ, 1 ≤ ℓ → IsLTopologicalRecurrence ℓ D

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Definition (ℓ-topological recurrence).

Uses 1 · Used by 1

Statement usesSets of \(\ell\)-topological recurrence

Used byCharacterization of multiple topological recurrence

TheoremCharacterization of multiple topological recurrence#✓fully proved

A set \(D\) of natural numbers is a set of multiple topological recurrence if and only if \(D\) is a set of \(\ell\)-topological recurrence for every natural number \(\ell \ge 1\).

public theorem isMultipleTopologicalRecurrence_iff (D : Set ℕ) :
    IsMultipleTopologicalRecurrence D ↔
      ∀ ℓ : ℕ, 1 ≤ ℓ → IsLTopologicalRecurrence ℓ D

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Definition (ℓ-topological recurrence).

Uses 2

Statement usesSets of \(\ell\)-topological recurrence · Sets of multiple topological recurrence

DefinitionChromatically intersective sets#✓fully proved

A set \(D\) of natural numbers is chromatically intersective if every element of \(D\) is positive and, for every natural number \(r \ge 1\) and every coloring of the positive integers with \(r\) colors, there are positive integers \(a\) and \(b\) of the same color whose difference \(a - b\), computed in the integers, lies in \(D\).

public def IsChromaticallyIntersective (D : Set ℕ) : Prop :=
  D ⊆ Set.Ioi 0 ∧ ∀ (r : ℕ), 1 ≤ r → ∀ c : ℕ+ → Fin r,
    ∃ a b : ℕ+, c a = c b ∧
      ∃ d ∈ D, ((a : ℕ) : ℤ) - ((b : ℕ) : ℤ) = (d : ℤ)

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Theorem 13(iv).

Used by 2

Used byCharacterization of chromatically intersective sets · Topological recurrence, accessibility and chromatic intersectivity

TheoremCharacterization of chromatically intersective sets#✓fully proved

A set \(D\) of natural numbers is chromatically intersective if and only if every element of \(D\) is positive and, for every natural number \(r \ge 1\) and every coloring of the positive integers with \(r\) colors, there are positive integers \(a\) and \(b\) of the same color whose difference \(a - b\), computed in the integers, lies in \(D\).

public theorem isChromaticallyIntersective_iff (D : Set ℕ) :
    IsChromaticallyIntersective D ↔
      D ⊆ Set.Ioi 0 ∧ ∀ (r : ℕ), 1 ≤ r → ∀ c : ℕ+ → Fin r,
        ∃ a b : ℕ+, c a = c b ∧
          ∃ d ∈ D, ((a : ℕ) : ℤ) - ((b : ℕ) : ℤ) = (d : ℤ)

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Theorem 13(iv).

Uses 1

Statement usesChromatically intersective sets

DefinitionPositive Fibonacci set#✓fully proved

The positive Fibonacci set is \(\{F_n : n \ge 2\}\), where the Fibonacci numbers are \(F_0 = 0\), \(F_1 = 1\) and \(F_{n+2} = F_{n+1} + F_n\). Equivalently, it is the set \(\{1, 2, 3, 5, 8, \dots\}\) of positive Fibonacci numbers, each counted once.

public def positiveFibonacciSet : Set ℕ :=
  {d | ∃ n : ℕ, 2 ≤ n ∧ d = Nat.fib n}

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Proposition 1.

Used by 6

Used byArithmetic progressions with Fibonacci gaps are not \(2\)-regular · The positive Fibonacci set is not 2-large · The Fibonacci numbers have degree of accessibility at most \(3\) · A 2-coloring with no monochromatic 6-term progression with positive Fibonacci gap · Membership in the positive Fibonacci set · Halved even Fibonacci numbers and \(4\)-accessibility of the Fibonacci numbers

TheoremMembership in the positive Fibonacci set#✓fully proved

Write \(F_n\) for the \(n\)-th Fibonacci number, with \(F_0 = 0\) and \(F_1 = 1\). A natural number \(d\) belongs to the positive Fibonacci set if and only if \(d = F_n\) for some natural number \(n \ge 2\).

public theorem mem_positiveFibonacciSet_iff (d : ℕ) :
    d ∈ positiveFibonacciSet ↔ ∃ n : ℕ, 2 ≤ n ∧ d = Nat.fib n

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Proposition 1.

Uses 1

Statement usesPositive Fibonacci set

DefinitionEven Fibonacci set#✓fully proved

Let \(F_m\) denote the \(m\)-th Fibonacci number, with \(F_0 = 0\) and \(F_1 = 1\). The even Fibonacci set is \(\{F_{3n+3} : n \ge 0\}\); its first terms are \(2, 8, 34, \dots\).

public def evenFibonacciSet : Set ℕ :=
  {d | ∃ n : ℕ, d = Nat.fib (3 * n + 3)}

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Proposition 2.

Used by 4

Used byThe even Fibonacci set is not 2-accessible · The even Fibonacci numbers have degree of accessibility \(1\) · A 2-coloring with no monochromatic 4-term even-Fibonacci diffsequence · Membership in the even Fibonacci set

TheoremMembership in the even Fibonacci set#✓fully proved

Write \(F_m\) for the \(m\)-th Fibonacci number, with \(F_0 = 0\) and \(F_1 = 1\). A natural number \(d\) belongs to the even Fibonacci set if and only if \(d = F_{3n+3}\) for some natural number \(n\).

public theorem mem_evenFibonacciSet_iff (d : ℕ) :
    d ∈ evenFibonacciSet ↔ ∃ n : ℕ, d = Nat.fib (3 * n + 3)

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Proposition 2.

Uses 1

Statement usesEven Fibonacci set

TheoremGrowth bound for the degree of accessibility#●ready to prove

Let \(r \ge 2\), let \(d_0 < d_1 < d_2 < \cdots\) be a strictly increasing sequence of natural numbers with \(d_0 > 0\), and let \(D = \{d_n : n \ge 0\}\). If there are a real number \(\delta > 0\) and an integer \(N \ge 1\) such that \(d_{n+1} \ge \left(2 + \frac{1}{r-1} + \delta\right) d_n\) for every \(n \ge N - 1\), then \(D\) is not \(r\)-accessible.

In the paper's terms, the degree of accessibility of \(D\) is at most \(r - 1\); the enumeration here starts at index \(0\), so \(d_n\) is the paper's \(d_{n+1}\).

public theorem_wanted accessibility_degree_growth_bound (r : ℕ) (D : Set ℕ)
    (d : ℕ → ℕ) (hr : 2 ≤ r) (hmono : StrictMono d)
    (hD : D = Set.range d) (hd0 : 0 < d 0) (δ : ℝ) (hδ : 0 < δ)
    (N : ℕ) (hN : 0 < N)
    (hgrowth : ∀ n : ℕ, N ≤ n + 1 →
      (d (n + 1) : ℝ) ≥
        (2 + (((r - 1 : ℕ) : ℝ)⁻¹) + δ) * (d n : ℝ)) :
    ¬ IsRAccessible r D

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Theorem 1.

Uses 1

Statement uses\(r\)-accessibility for colorings of the positive integers

TheoremFast eventual growth rules out 2-accessibility#●ready to prove

Let \(d_0 < d_1 < d_2 < \cdots\) be a strictly increasing sequence of natural numbers with \(d_0 > 0\), and let \(D = \{d_n : n \in \mathbb{N}\}\). Suppose there are a real number \(\delta > 0\) and a natural number \(N \ge 1\) such that \(d_{n+1} \ge (3 + \delta) d_n\) for every \(n \in \mathbb{N}\) with \(n + 1 \ge N\). Then \(D\) is not \(2\)-accessible.

public theorem_wanted not_two_accessible_of_growth (D : Set ℕ) (d : ℕ → ℕ)
    (hmono : StrictMono d) (hD : D = Set.range d) (hd0 : 0 < d 0)
    (δ : ℝ) (hδ : 0 < δ) (N : ℕ) (hN : 0 < N)
    (hgrowth : ∀ n : ℕ, N ≤ n + 1 →
      (d (n + 1) : ℝ) ≥ (3 + δ) * (d n : ℝ)) :
    ¬ IsRAccessible 2 D

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Corollary 1.

Uses 1

Statement uses\(r\)-accessibility for colorings of the positive integers

Theorem2-large sets contain multiples of every positive integer#●ready to prove

Every \(2\)-large set \(D\) of positive integers contains a multiple of each positive integer \(m\).

public theorem_wanted two_large_contains_multiples (D : Set ℕ) (h : IsRLarge 2 D) :
    ∀ m : ℕ, 0 < m → ∃ d ∈ D, m ∣ d

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Theorem 2.

Uses 1

Statement uses\(r\)-large sets

TheoremFinite removal preserves \(r\)-largeness#●ready to prove

Let \(r\) be a natural number. If a set \(D \subseteq \mathbb{N}\) is \(r\)-large and \(F \subseteq \mathbb{N}\) is finite, then \(D \setminus F\) is \(r\)-large.

public theorem_wanted rLarge_sdiff_finite (r : ℕ) (D F : Set ℕ)
    (hD : IsRLarge r D) (hF : F.Finite) :
    IsRLarge r (D \ F)

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Theorem 3.

Uses 1

Statement uses\(r\)-large sets

TheoremLargeness is partition regular#●ready to prove

If \(D_1, D_2 \subseteq \mathbb{N}\) and their union \(D = D_1 \cup D_2\) is large, then \(D_1\) is large or \(D_2\) is large.

public theorem_wanted large_union_partition (D D₁ D₂ : Set ℕ)
    (hD : D = D₁ ∪ D₂) (hlarge : IsLarge D) :
    IsLarge D₁ ∨ IsLarge D₂

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Theorem 4.

Uses 1

Statement usesLarge set

TheoremSets growing by a factor of three are not 2-large#●ready to prove

Let \(d_0 < d_1 < d_2 < \cdots\) be a strictly increasing sequence of natural numbers with \(d_0 > 0\) and \(d_{n+1} \ge 3 d_n\) for every \(n \in \mathbb{N}\), and let \(D = \{d_n : n \in \mathbb{N}\}\). Then \(D\) is not \(2\)-large.

public theorem_wanted not_two_large_of_triple_growth (D : Set ℕ) (d : ℕ → ℕ)
    (hmono : StrictMono d) (hD : D = Set.range d) (hd0 : 0 < d 0)
    (hgrowth : ∀ n : ℕ, d (n + 1) ≥ 3 * d n) :
    ¬ IsRLarge 2 D

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Theorem 5.

Uses 1

Statement uses\(r\)-large sets

TheoremDilates of a finite union of lacunary sets stay away from the integers#●ready to prove

Let \(\ell \ge 1\) and let \(S_0, \dots, S_{\ell-1} \subseteq \mathbb{N}\) be lacunary sets with union \(S = \bigcup_i S_i\). Then there are real numbers \(\alpha\) and \(\varepsilon > 0\) such that the infimum over \(s \in S\) of the distance \(|\alpha s - \operatorname{round}(\alpha s)|\) from \(\alpha s\) to its nearest integer \(\operatorname{round}(\alpha s)\) equals \(\varepsilon\).

public theorem_wanted lacunary_union_avoids_integers (ℓ : ℕ) (hℓ : 0 < ℓ)
    (S : Fin ℓ → Set ℕ) (hS : ∀ i, IsLacunarySet (S i)) :
    ∃ α ε : ℝ, 0 < ε ∧
      sInf ((fun s : ℕ => |α * (s : ℝ) - round (α * (s : ℝ))|) '' (⋃ i, S i)) = ε

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Theorem 6.

Uses 1

Statement usesLacunary set

TheoremTwo-colorings avoiding long \(D\)-progressions#●ready to prove

Let \(D\) be a set of positive integers, let \(\alpha\) be a real number and let \(\varepsilon > 0\) be such that \(\lVert \alpha d \rVert \ge \varepsilon\) for every \(d \in D\), where \(\lVert t \rVert\) denotes the distance from \(t\) to the nearest integer. Then there is a \(2\)-coloring of the positive integers with no monochromatic \(D\)-arithmetic progression of length \(\lceil 1/(2\varepsilon) \rceil + 1\).

public theorem_wanted two_coloring_avoids_long_DAP (D : Set ℕ)
    (hD : D ⊆ Set.Ioi 0) (α ε : ℝ) (hε : 0 < ε)
    (hsep : ∀ d ∈ D, ε ≤ |α * (d : ℝ) - round (α * (d : ℝ))|) :
    ∃ c : ℕ+ → Fin 2,
      ¬ ∃ x : Fin (Nat.ceil ((2 * ε)⁻¹) + 1) → ℕ+,
        IsMonochromatic c x ∧ IsDAP D (Nat.ceil ((2 * ε)⁻¹) + 1) x

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Theorem 7.

Uses 2

Statement usesArithmetic progressions with gap in \(D\) · Monochromatic sequences of positive integers

TheoremFinite unions of lacunary sets are not 2-large#●ready to prove

For every \(n \ge 1\) and all lacunary sets \(D_1, \dots, D_n\), the union \(D_1 \cup \dots \cup D_n\) is not 2-large.

public theorem_wanted finite_union_lacunary_not_two_large (n : ℕ) (hn : 0 < n)
    (D : Fin n → Set ℕ) (hD : ∀ i, IsLacunarySet (D i)) :
    ¬ IsRLarge 2 (⋃ i, D i)

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Theorem 8.

Uses 2

Statement usesLacunary set · \(r\)-large sets

TheoremPositive values of a polynomial vanishing at zero form a large set#●ready to prove

Let \(p\) be a polynomial with integer coefficients, positive leading coefficient and \(p(0) = 0\). Then the set of positive integers \(d\) such that \(p(n) = d\) for some positive integer \(n\) is large.

public theorem_wanted polynomial_range_large (p : Polynomial ℤ)
    (hlead : 0 < p.leadingCoeff) (hzero : p.eval 0 = 0) :
    IsLarge {d : ℕ | 0 < d ∧ ∃ n : ℕ+, p.eval (n : ℤ) = (d : ℤ)}

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Theorem 9.

Uses 1

Statement usesLarge set

TheoremA coloring criterion for accessibility of a shifted set#●ready to prove

Let \(r \ge 2\) and \(c\) be natural numbers, let \(D\) be a set of positive integers, and write \(D + c = \{d + c : d \in D\}\). Suppose that for every coloring of \(D\) with \(r - 1\) colors and every \(k \ge 1\) there are \(x_0, \dots, x_{k-1} \in D\), all of the same color, that form a \((D + c)\)-diffsequence, that is, \(x_{i+1} - x_i \in D + c\) for every \(i < k - 1\). Then \(D + c\) is \(r\)-accessible.

public theorem_wanted accessible_of_colored_subset_diffsequences (c r : ℕ)
    (hr : 2 ≤ r) (D : Set ℕ) (hD : D ⊆ Set.Ioi 0)
    (hcolor : ∀ χ : ({n : ℕ+ // (n : ℕ) ∈ D} → Fin (r - 1)),
      ∀ k : ℕ, 1 ≤ k →
        ∃ x : Fin k → {n : ℕ+ // (n : ℕ) ∈ D},
          (∀ i j, χ (x i) = χ (x j)) ∧
          IsDDiffSequence {e : ℕ | ∃ d ∈ D, e = d + c}
            (fun i => (((x i : {n : ℕ+ // (n : ℕ) ∈ D}) : ℕ+) : ℕ))) :
    IsRAccessible r {e : ℕ | ∃ d ∈ D, e = d + c}

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Theorem 10.

Uses 2

Statement uses\(D\)-diffsequences · \(r\)-accessibility for colorings of the positive integers

TheoremSets containing their own long diffsequences are 2-accessible#●ready to prove

Let \(D\) be a set of positive integers. If for every \(k \ge 1\) there are positive integers \(x_1, \dots, x_k\), all in \(D\), that form a \(D\)-diffsequence, then \(D\) is \(2\)-accessible.

public theorem_wanted two_accessible_of_internal_diffsequences (D : Set ℕ)
    (hD : D ⊆ Set.Ioi 0)
    (hseq : ∀ k : ℕ, 1 ≤ k → ∃ x : Fin k → ℕ+,
      (∀ i, (x i : ℕ) ∈ D) ∧
        IsDDiffSequence D (fun i => ((x i : ℕ) : ℤ))) :
    IsRAccessible 2 D

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Corollary 2.

Uses 2

Statement uses\(D\)-diffsequences · \(r\)-accessibility for colorings of the positive integers

TheoremIntegral quotients of an accessible set#●ready to prove

Let \(d \ge 1\) and \(r\) be natural numbers and let \(A\) be a set of natural numbers. If \(A\) is \(rd\)-accessible, then the set \(\{n \ge 1 : nd \in A\}\), that is, the positive integers of the form \(a/d\) with \(a \in A\), is \(r\)-accessible.

public theorem_wanted accessible_integral_quotients (A : Set ℕ) (d r : ℕ)
    (hd : 0 < d) (hA : IsRAccessible (r * d) A) :
    IsRAccessible r {n : ℕ | 0 < n ∧ ∃ a ∈ A, a = n * d}

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Theorem 11(i).

Uses 1

Statement uses\(r\)-accessibility for colorings of the positive integers

TheoremMultiples of \(d\) in an accessible set#●ready to prove

Let \(d \ge 1\) and \(r\) be natural numbers and let \(A\) be a set of natural numbers. If \(A\) is \(rd\)-accessible, then the set \(\{a \in A : d \mid a\}\) of members of \(A\) divisible by \(d\) is \(r\)-accessible.

public theorem_wanted accessible_divisible_subset (A : Set ℕ) (d r : ℕ)
    (hd : 0 < d) (hA : IsRAccessible (r * d) A) :
    IsRAccessible r {a : ℕ | a ∈ A ∧ a % d = 0}

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Theorem 11(ii).

Uses 1

Statement uses\(r\)-accessibility for colorings of the positive integers

TheoremColorings avoiding long diffsequences under fractional-part bounds#●ready to prove

Let \(r \ge 1\), let \(d_0 < d_1 < \cdots\) be a strictly increasing sequence of natural numbers with \(d_0 > 0\), and let \(D = \{d_n : n \ge 0\}\). Suppose there are real numbers \(\alpha\) and \(\varepsilon > 0\) such that for every \(n\) the fractional part of \(\alpha d_n\) lies in the closed interval \([\varepsilon, (r-1)/r]\). Then there is a coloring of the positive integers with \(r\) colors that has no monochromatic \(D\)-diffsequence of positive integers of length \(\lceil 1/(r\varepsilon) \rceil + 1\).

public theorem_wanted coloring_avoids_diffsequence_of_fractional_bounds
    (r : ℕ) (hr : 1 ≤ r) (D : Set ℕ) (d : ℕ → ℕ)
    (hmono : StrictMono d) (hD : D = Set.range d) (hd0 : 0 < d 0)
    (α ε : ℝ) (hε : 0 < ε)
    (hfrac : ∀ n : ℕ, Int.fract (α * (d n : ℝ)) ∈
      Set.Icc ε (((r - 1 : ℕ) : ℝ) / (r : ℝ))) :
    ∃ c : ℕ+ → Fin r,
      ¬ ∃ x : Fin (Nat.ceil (((r : ℝ) * ε)⁻¹) + 1) → ℕ+,
        IsMonochromatic c x ∧
          IsDDiffSequence D (fun i => ((x i : ℕ) : ℤ))

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Theorem 12.

Uses 2

Statement uses\(D\)-diffsequences · Monochromatic sequences of positive integers

TheoremA 2-coloring with no monochromatic 6-term progression with positive Fibonacci gap#●ready to prove

There is a coloring of the positive integers with two colors such that no 6-term arithmetic progression \(a, a + d, \dots, a + 5d\) of positive integers whose gap \(d\) is a positive Fibonacci number is monochromatic.

public theorem_wanted fibonacci_two_coloring_avoids_six_term_AP :
    ∃ c : ℕ+ → Fin 2,
      ¬ ∃ x : Fin 6 → ℕ+,
        IsMonochromatic c x ∧ IsDAP positiveFibonacciSet 6 x

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Proposition 1 (coloring claim).

Uses 3

Statement usesArithmetic progressions with gap in \(D\) · Monochromatic sequences of positive integers · Positive Fibonacci set

TheoremThe positive Fibonacci set is not 2-large#●ready to prove

Let \(F_n\) denote the \(n\)-th Fibonacci number, with \(F_0 = 0\) and \(F_1 = 1\). The positive Fibonacci set \(\{F_n : n \ge 2\} = \{1, 2, 3, 5, 8, \dots\}\) is not \(2\)-large.

public theorem_wanted fibonacci_not_two_large :
    ¬ IsRLarge 2 positiveFibonacciSet

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Proposition 1 (consequence).

Uses 2

Statement uses\(r\)-large sets · Positive Fibonacci set

TheoremA 2-coloring with no monochromatic 4-term even-Fibonacci diffsequence#●ready to prove

Let \(F_m\) denote the \(m\)-th Fibonacci number, with \(F_0 = 0\) and \(F_1 = 1\), and let \(E = \{F_{3n+3} : n \ge 0\} = \{2, 8, 34, \dots\}\) be the even Fibonacci set. There is a coloring of the positive integers with \(2\) colors under which no four positive integers \(x_0, x_1, x_2, x_3\) of the same color satisfy \(x_{i+1} - x_i \in E\) for \(i = 0, 1, 2\).

public theorem_wanted even_fibonacci_two_coloring_avoids_four_term_diffsequence :
    ∃ c : ℕ+ → Fin 2,
      ¬ ∃ x : Fin 4 → ℕ+,
        IsMonochromatic c x ∧
          IsDDiffSequence evenFibonacciSet (fun i => ((x i : ℕ) : ℤ))

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Proposition 2 (coloring claim).

Uses 3

Statement uses\(D\)-diffsequences · Monochromatic sequences of positive integers · Even Fibonacci set

TheoremThe even Fibonacci set is not 2-accessible#●ready to prove

Let \(F_m\) denote the \(m\)-th Fibonacci number, with \(F_0 = 0\) and \(F_1 = 1\). The even Fibonacci set \(\{F_{3n+3} : n \ge 0\} = \{2, 8, 34, \dots\}\) is not \(2\)-accessible.

public theorem_wanted even_fibonacci_not_two_accessible :
    ¬ IsRAccessible 2 evenFibonacciSet

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Proposition 2 (consequence).

Uses 2

Statement uses\(r\)-accessibility for colorings of the positive integers · Even Fibonacci set

TheoremFurstenberg–Weiss correspondence for translation-invariant families#●ready to prove

Let \(\mathcal{A}\) be a collection of finite sets of integers that is closed under translation, that is, \(A + t \in \mathcal{A}\) for all \(A \in \mathcal{A}\) and \(t \in \mathbb{Z}\), and let \(r \ge 1\). For a homeomorphism \(T\) and an integer \(a\), write \(T^{-a}(U)\) for the preimage of \(U\) under the \(a\)-th power of \(T\). Then the following three conditions are equivalent: (a) for every coloring of \(\mathbb{Z}\) with \(r\) colors there are a color \(i\) and a set \(A \in \mathcal{A}\) all of whose elements have color \(i\); (b) for every nonempty compact metric space \(X\), every homeomorphism \(T\) of \(X\) and every cover of \(X\) by \(r\) open sets \(U_1, \dots, U_r\), there are \(i\) and \(A \in \mathcal{A}\) such that \(\bigcap_{a \in A} T^{-a}(U_i)\) is nonempty; (c) the same holds for every nonempty compact metric space \(X\), every minimal homeomorphism \(T\) of \(X\) and every cover of \(X\) by \(r\) clopen sets \(U_1, \dots, U_r\).

MetaMathlibExt.furstenberg_weiss_correspondence · 23 lines

public theorem_wanted furstenberg_weiss_correspondence
    (𝒜 : Set (Finset ℤ))
    (htrans : ∀ A ∈ 𝒜, ∀ t : ℤ, A.image (fun a => a + t) ∈ 𝒜)
    (r : ℕ) (hr : 1 ≤ r) :
    ((∀ c : ℤ → Fin r, ∃ i : Fin r, ∃ A ∈ 𝒜, ∀ a ∈ A, c a = i) ↔
      (∀ (X : Type) [MetricSpace X] [CompactSpace X] [Nonempty X]
        (T : X ≃ₜ X)
        (U : Fin r → Set X),
        (∀ i, IsOpen (U i)) → (∀ x, ∃ i, x ∈ U i) →
          ∃ i : Fin r, ∃ A ∈ 𝒜,
            (⋂ a : A, iteratePreimage T (a : ℤ) (U i)).Nonempty)) ∧
    ((∀ (X : Type) [MetricSpace X] [CompactSpace X] [Nonempty X]
        (T : X ≃ₜ X)
        (U : Fin r → Set X),
        (∀ i, IsOpen (U i)) → (∀ x, ∃ i, x ∈ U i) →
          ∃ i : Fin r, ∃ A ∈ 𝒜,
            (⋂ a : A, iteratePreimage T (a : ℤ) (U i)).Nonempty) ↔
      (∀ (X : Type) [MetricSpace X] [CompactSpace X] [Nonempty X]
        (T : X ≃ₜ X),
        IsMinimalSystem T → ∀ U : Fin r → Set X,
        (∀ i, IsClopen (U i)) → (∀ x, ∃ i, x ∈ U i) →
          ∃ i : Fin r, ∃ A ∈ 𝒜,
            (⋂ a : A, iteratePreimage T (a : ℤ) (U i)).Nonempty))

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Lemma 1.

Uses 2

Statement usesMinimal system · Iterated preimage

TheoremTopological recurrence, accessibility and chromatic intersectivity#●ready to prove

Let \(D\) be a set of positive integers. Say that \(D\) has diffsequence recurrence if for every compact metric space \(X\), every minimal homeomorphism \(T\) of \(X\), every nonempty open set \(U \subseteq X\) and every \(k \ge 1\) there are integers \(s_1, \dots, s_k\) forming a \(D\)-diffsequence such that \(U \cap T^{-s_1}U \cap \dots \cap T^{-s_k}U\) is nonempty, where \(T^{-s}U\) is the preimage of \(U\) under the integer power \(T^s\). Then the following are equivalent: \(D\) is a set of topological recurrence; \(D\) has diffsequence recurrence; \(D\) is accessible; \(D\) is chromatically intersective.

MetaMathlibExt.recurrence_accessibility_equivalences · 15 lines

public theorem_wanted recurrence_accessibility_equivalences (D : Set ℕ)
    (hD : D ⊆ Set.Ioi 0) :
    (IsTopologicalRecurrence D ↔
      ∀ (X : Type) [MetricSpace X] [CompactSpace X] (T : X ≃ₜ X),
        IsMinimalSystem T → ∀ U : Set X, IsOpen U → U.Nonempty →
          ∀ k : ℕ, 1 ≤ k → ∃ s : Fin k → ℤ,
            IsDDiffSequence D s ∧
              (U ∩ ⋂ i : Fin k, iteratePreimage T (s i) U).Nonempty) ∧
    ((∀ (X : Type) [MetricSpace X] [CompactSpace X] (T : X ≃ₜ X),
        IsMinimalSystem T → ∀ U : Set X, IsOpen U → U.Nonempty →
          ∀ k : ℕ, 1 ≤ k → ∃ s : Fin k → ℤ,
            IsDDiffSequence D s ∧
              (U ∩ ⋂ i : Fin k, iteratePreimage T (s i) U).Nonempty) ↔
      IsAccessible D) ∧
    (IsAccessible D ↔ IsChromaticallyIntersective D)

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Theorem 13.

Uses 6

Statement usesAccessible sets · Chromatically intersective sets · \(D\)-diffsequences · Minimal system · Sets of topological recurrence · Iterated preimage

TheoremOne part of a union inherits \(k\)-topological recurrence#●ready to prove

Let \(k\) be a natural number and let \(D_1, D_2 \subseteq \mathbb{N}\). If \(D_1 \cup D_2\) is a set of \(k\)-topological recurrence, then \(D_1\) or \(D_2\) is a set of \(k\)-topological recurrence.

public theorem_wanted topological_recurrence_union_partition (k : ℕ)
    (D D₁ D₂ : Set ℕ) (hD : D = D₁ ∪ D₂)
    (hrec : IsLTopologicalRecurrence k D) :
    IsLTopologicalRecurrence k D₁ ∨ IsLTopologicalRecurrence k D₂

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Theorem 14.

Uses 1

Statement usesSets of \(\ell\)-topological recurrence

TheoremOne part of an accessible union is accessible#●ready to prove

Let \(D\), \(D_1\) and \(D_2\) be sets of natural numbers with \(D = D_1 \cup D_2\). If \(D\) is accessible, then \(D_1\) is accessible or \(D_2\) is accessible.

public theorem_wanted accessible_union_partition (D D₁ D₂ : Set ℕ)
    (hD : D = D₁ ∪ D₂) (hacc : IsAccessible D) :
    IsAccessible D₁ ∨ IsAccessible D₂

Sources

• Oscar Quester, On Some Properties of Accessible Sets, INTEGERS 25 (2025), Article A64, Corollary 3.

Uses 1

Statement usesAccessible sets

DefinitionMonochromatic finite sequences#✓fully proved

Given a colouring \(c : \mathbb{N} \to \{0, \dots, r - 1\}\) of the natural numbers with \(r\) colours, a finite sequence \(x_0, \dots, x_{k-1}\) of natural numbers is monochromatic when all its terms have the same colour: \(c(x_i) = c(x_j)\) for all \(i, j < k\).

def IsMonochromatic {r k : ℕ} (c : ℕ → Fin r) (x : Fin k → ℕ) : Prop :=
  ∀ i j, c (x i) = c (x j)

Sources

• OPG-1797 (Open Problem Garden, node 1797, http://www.openproblemgarden.org/op/2_accessibility_of_primes): formalizes "monochromatic sequence" from the definition of r-accessible.

Used by 1

Used by\(r\)-accessible sets of natural numbers

DefinitionFinite \(S\)-diffsequences#✓fully proved

For a set \(S\) of natural numbers, a finite sequence \(x_0, \dots, x_{k-1}\) of natural numbers is an \(S\)-diffsequence when each term is the previous one plus an element of \(S\): for every \(i\) with \(i + 1 < k\) there is \(d \in S\) with \(x_{i+1} = x_i + d\).

def IsSDiffSequence (S : Set ℕ) {k : ℕ} (x : Fin k → ℕ) : Prop :=
  ∀ (i : ℕ) (h : i + 1 < k), ∃ d ∈ S, x ⟨i + 1, h⟩ = x ⟨i, by omega⟩ + d

Sources

• OPG-1797 (Open Problem Garden, node 1797, http://www.openproblemgarden.org/op/2_accessibility_of_primes): formalizes "S-diffsequence", i.e. x_{i+1} - x_i ∈ S, stated additively as x (i+1) = x i + d with d ∈ S.

Used by 1

Used by\(r\)-accessible sets of natural numbers

Definition\(r\)-accessible sets of natural numbers#✓fully proved

A set \(S \subseteq \mathbb{N}\) is \(r\)-accessible when for every colouring \(c : \mathbb{N} \to \{0, \dots, r - 1\}\) with \(r\) colours and every length \(k \ne 1\) there is a sequence \(x_0, \dots, x_{k-1}\) of natural numbers that is monochromatic for \(c\) and is an \(S\)-diffsequence: for each \(i\) with \(i + 1 < k\) there is \(d \in S\) with \(x_{i+1} = x_i + d\).

def IsRAccessible (r : ℕ) (S : Set ℕ) : Prop :=
  ∀ (c : ℕ → Fin r) (k : ℕ), k ≠ 1 → ∃ x : Fin k → ℕ,
    IsMonochromatic c x ∧ IsSDiffSequence S x

Sources

• OPG-1797 (Open Problem Garden, node 1797, http://www.openproblemgarden.org/op/2_accessibility_of_primes): S is r-accessible if for every r-coloring of ℕ and every k ∈ ℕ \ {1} there is a monochromatic S-diffsequence of length k.

Uses 2 · Used by 1

Statement usesMonochromatic finite sequences · Finite \(S\)-diffsequences

Used by2-accessibility of the primes

Definition2-accessibility of the primes#✓fully proved

The statement that the set of prime numbers is \(2\)-accessible: for every colouring \(c : \mathbb{N} \to \{0, 1\}\) of the natural numbers with two colours and every length \(k \ne 1\) there is a sequence \(x_0, \dots, x_{k-1}\) of natural numbers, all of the same colour, such that each difference \(x_{i+1} - x_i\) is a prime number. Open Problem Garden question OPG-1797 asks whether this holds.

def conjecture : Prop :=
  IsRAccessible 2 { n | Nat.Prime n }

Sources

• OPG-1797 (Open Problem Garden, node 1797, http://www.openproblemgarden.org/op/2_accessibility_of_primes): "Is the set of prime numbers 2-accessible?"

Uses 1 · Used by 1

Statement uses\(r\)-accessible sets of natural numbers

Used byThe primes are 2-accessible

TheoremThe primes are 2-accessible#●ready to prove

The set of prime numbers is \(2\)-accessible: for every colouring \(c : \mathbb{N} \to \{0, 1\}\) of the natural numbers with two colours and every length \(k \ne 1\) there is a sequence \(x_0, \dots, x_{k-1}\) of natural numbers, all of the same colour, such that each difference \(x_{i+1} - x_i\) is a prime number.

Quester proves this as a special case of Theorem 1 of the paper, using the Frantzikinakis–Host–Kra recurrence theorem along shifted primes.

public theorem_wanted conjecture_holds : conjecture

Sources

• Oscar Quester, The Primes are 2-Accessible, arXiv preprint (2026), arXiv:2606.00410, https://arxiv.org/abs/2606.00410; Nikos Frantzikinakis, Bernard Host, Bryna Kra, The polynomial multidimensional Szemeredi theorem along shifted primes, Israel J. Math. 194 (2013), 331-348, arXiv:1009.1484, https://arxiv.org/abs/1009.1484.

Uses 1

Statement uses2-accessibility of the primes

DefinitionHalves of even Fibonacci numbers#✓fully proved

Let \(F_m\) be the \(m\)-th Fibonacci number, with \(F_0 = 0\) and \(F_1 = 1\). The set of halves of the positive even Fibonacci numbers is \(G = \{F_{3n}/2 : n \ge 1\} = \{1, 4, 17, 72, \dots\}\); its elements are written \(g_n = F_{3n}/2\) for \(n \ge 1\).

def halfEvenFibonacciSet : Set ℕ :=
  Set.range fun n => Nat.fib (3 * (n + 1)) / 2

Sources

• William J. Wesley, Improved Ramsey-Type Theorems for Fibonacci Numbers and Other Sequences, INTEGERS 25 (2025), Article A29, Section 2 (notation G, g_n).

Used by 2

Used by\(4\) is half of an even Fibonacci number · Halved even Fibonacci numbers and \(4\)-accessibility of the Fibonacci numbers

Theorem\(4\) is half of an even Fibonacci number#✓fully proved

Let \(F_m\) be the \(m\)-th Fibonacci number, with \(F_0 = 0\) and \(F_1 = 1\). The number \(4\) belongs to the set \(G = \{F_{3n}/2 : n \ge 1\} = \{1, 4, 17, 72, \dots\}\) of halves of the positive even Fibonacci numbers; indeed \(4 = F_6/2\).

theorem four_mem_halfEvenFibonacciSet : 4 ∈ halfEvenFibonacciSet

Sources

• William J. Wesley, Improved Ramsey-Type Theorems for Fibonacci Numbers and Other Sequences, INTEGERS 25 (2025), Article A29, Section 2 (notation G, g_n).

Uses 1

Statement usesHalves of even Fibonacci numbers

DefinitionThe Thue–Morse morphism \(\mu\)#✓fully proved

The morphism \(\mu\) on binary words sends the letter \(0\) to the word \(10\) and the letter \(1\) to the word \(01\).

def thueMorseMorphism : Bool → List Bool
  | false => [true, false]
  | true => [false, true]

Sources

• William J. Wesley, Improved Ramsey-Type Theorems for Fibonacci Numbers and Other Sequences, INTEGERS 25 (2025), Article A29, Definition 1.

Used by 1

Used byWesley's word \(S\)

DefinitionThe morphism \(\nu\)#✓fully proved

The morphism \(\nu\) is given on the letters \(0\) and \(1\) by \(\nu(0) = 1\) and \(\nu(1) = 00\).

def fibonacciNuMorphism : Bool → List Bool
  | false => [true]
  | true => [false, false]

Sources

• William J. Wesley, Improved Ramsey-Type Theorems for Fibonacci Numbers and Other Sequences, INTEGERS 25 (2025), Article A29, Definition 1.

Used by 1

Used byWesley's word \(T\)

DefinitionWesley's word \(S\)#✓fully proved

Let \(\mu\) be the morphism of binary words with \(0 \mapsto 10\) and \(1 \mapsto 01\), and let \(f_0 = 0\), \(f_1 = 01\), \(f_2 = 010\), \(\dots\) be the finite Fibonacci words. The word \(S\) is the infinite binary word, indexed from \(0\), whose letter at index \(n\) is the letter at index \(n\) of \(\mu(f_{n+2})\).

Since each \(f_k\) is a prefix of \(f_{k+1}\), \(S = \mu(F_\infty) = 1001101001\dots\), where \(F_\infty = 010010100\dots\) is the infinite Fibonacci word.

def wesleyWordS (n : ℕ) : Bool :=
  ((fibWord (n + 2)).flatMap thueMorseMorphism).getD n false

Sources

• William J. Wesley, Improved Ramsey-Type Theorems for Fibonacci Numbers and Other Sequences, INTEGERS 25 (2025), Article A29, Definition 1.

Uses 2 · Used by 2

Statement usesFinite Fibonacci words · The Thue–Morse morphism \(\mu\)

Used byBeatty-sequence descriptions of the words \(F_\infty\), \(S\) and \(T\) · The first ten letters of Wesley's words \(S\) and \(T\)

DefinitionWesley's word \(T\)#✓fully proved

Let \(\nu\) be the morphism of binary words with \(0 \mapsto 1\) and \(1 \mapsto 00\), and let \(f_0 = 0\), \(f_1 = 01\), \(f_2 = 010\), \(\dots\) be the finite Fibonacci words. The word \(T\) is the infinite binary word, indexed from \(0\), whose letter at index \(n\) is the letter at index \(n\) of \(\nu(f_{n+2})\).

Since each \(f_k\) is a prefix of \(f_{k+1}\), \(T = \nu(F_\infty) = 1001100100\dots\), where \(F_\infty = 010010100\dots\) is the infinite Fibonacci word.

def wesleyWordT (n : ℕ) : Bool :=
  ((fibWord (n + 2)).flatMap fibonacciNuMorphism).getD n false

Sources

• William J. Wesley, Improved Ramsey-Type Theorems for Fibonacci Numbers and Other Sequences, INTEGERS 25 (2025), Article A29, Definition 1.

Uses 2 · Used by 2

Statement usesFinite Fibonacci words · The morphism \(\nu\)

Used byBeatty-sequence descriptions of the words \(F_\infty\), \(S\) and \(T\) · The first ten letters of Wesley's words \(S\) and \(T\)

TheoremThe first ten letters of Wesley's words \(S\) and \(T\)#✓fully proved

Indexing letters from \(0\), the letters of \(S\) at indices \(0, 1, \dots, 9\) are \(1, 0, 0, 1, 1, 0, 1, 0, 0, 1\) and the letters of \(T\) at indices \(0, 1, \dots, 9\) are \(1, 0, 0, 1, 1, 0, 0, 1, 0, 0\); that is, \(S\) begins with \(1001101001\) and \(T\) begins with \(1001100100\).

theorem wesleyWords_first_ten :
    (List.range 10).map wesleyWordS =
        [true, false, false, true, true, false, true, false, false, true] ∧
      (List.range 10).map wesleyWordT =
        [true, false, false, true, true, false, false, true, false, false]

Sources

• William J. Wesley, Improved Ramsey-Type Theorems for Fibonacci Numbers and Other Sequences, INTEGERS 25 (2025), Article A29, Definition 1.

Uses 2

Statement usesWesley's word \(S\) · Wesley's word \(T\)

DefinitionWesley's constants \(c_{n,\varepsilon}\)#✓fully proved

For a natural number \(n\) and an integer \(\varepsilon\), the real number \(c_{n,\varepsilon}\) is defined by the residue of \(n\) modulo \(4\): if \(n \equiv 0 \pmod 4\), then \(c_{n,\varepsilon} = (4 + (2\sqrt5 - 5)\varepsilon)/10\); if \(n \equiv 1 \pmod 4\), then \(c_{n,\varepsilon} = (11 - 4\sqrt5)/5\) when \(\varepsilon = -4\) and \(c_{n,\varepsilon} = (4 + (4\sqrt5 - 5)\varepsilon)/20\) otherwise; if \(n \equiv 2 \pmod 4\), then \(c_{n,\varepsilon} = (6 + (2\sqrt5 - 5)\varepsilon)/10\); if \(n \equiv 3 \pmod 4\), then \(c_{n,\varepsilon} = (9 - 4\sqrt5)/5\) when \(\varepsilon = -4\) and \(c_{n,\varepsilon} = (8 + (2\sqrt5 - 5)\varepsilon)/10\) otherwise.

Lemma 5 uses these constants only for \(\varepsilon \in \{-4, 0, 4\}\).

noncomputable def wesleyFractionalConstant (n : ℕ) (ε : ℤ) : ℝ :=
  if n % 4 = 0 then (4 + (2 * √5 - 5) * ε) / 10
  else if n % 4 = 1 then (if ε = -4 then (11 - 4 * √5) / 5 else (4 + (4 * √5 - 5) * ε) / 20)
  else if n % 4 = 2 then (6 + (2 * √5 - 5) * ε) / 10
  else (if ε = -4 then (9 - 4 * √5) / 5 else (8 + (2 * √5 - 5) * ε) / 10)

Sources

• William J. Wesley, Improved Ramsey-Type Theorems for Fibonacci Numbers and Other Sequences, INTEGERS 25 (2025), Article A29, Lemma 5 (definition of c_{n,ε}).

Used by 2

Used byFractional parts of shifted Fibonacci numbers divided by \(\sqrt{5}\) · Wesley's constant \(c_{n,0}\) for \(n \equiv 0 \pmod 4\)

TheoremWesley's constant \(c_{n,0}\) for \(n \equiv 0 \pmod 4\)#✓fully proved

For every natural number \(n\) with \(n \equiv 0 \pmod 4\), Wesley's constant satisfies \(c_{n,0} = 2/5\).

theorem wesleyFractionalConstant_zero_of_mod_four_eq_zero {n : ℕ} (hn : n % 4 = 0) :
    wesleyFractionalConstant n 0 = 2 / 5

Sources

• William J. Wesley, Improved Ramsey-Type Theorems for Fibonacci Numbers and Other Sequences, INTEGERS 25 (2025), Article A29, Lemma 5 (definition of c_{n,ε}).

Uses 1

Statement usesWesley's constants \(c_{n,\varepsilon}\)

TheoremThe Fibonacci numbers have degree of accessibility at most \(3\)#●ready to prove

The positive Fibonacci set \(\{1, 2, 3, 5, 8, \dots\}\) is not \(r\)-accessible for any natural number \(r \ge 4\). Moreover, some coloring of the positive integers with four colors admits no monochromatic \(4\)-term diffsequence with differences in the positive Fibonacci set: there are no positive integers \(x_0, x_1, x_2, x_3\) of one color such that \(x_{i+1} - x_i\) is a positive Fibonacci number for \(i = 0, 1, 2\).

public theorem_wanted fibonacciSet_degreeOfAccessibility_le_three :
    (∀ r, 4 ≤ r → ¬ IsRAccessible r positiveFibonacciSet) ∧
    ∃ c : ℕ+ → Fin 4, ¬ ∃ x : Fin 4 → ℕ+,
      IsMonochromatic c x ∧ IsDDiffSequence positiveFibonacciSet (fun i => ((x i : ℕ) : ℤ))

Sources

• William J. Wesley, Improved Ramsey-Type Theorems for Fibonacci Numbers and Other Sequences, INTEGERS 25 (2025), Article A29, Theorem 1.

Uses 4

Statement uses\(D\)-diffsequences · Monochromatic sequences of positive integers · \(r\)-accessibility for colorings of the positive integers · Positive Fibonacci set

TheoremArithmetic progressions with Fibonacci gaps are not \(2\)-regular#●ready to prove

There is a coloring of the positive integers with two colors that admits no monochromatic \(5\)-term arithmetic progression with gap in the positive Fibonacci set \(\{1, 2, 3, 5, 8, \dots\}\), that is, no positive integers \(x_0, \dots, x_4\) of one color with \(x_i = a + i d\) for all \(i < 5\), for a positive integer \(a\) and a positive Fibonacci number \(d\). Moreover, the positive Fibonacci set is \(1\)-large, and it is not \(r\)-large for any natural number \(r \ge 2\).

public theorem_wanted fibonacci_gap_progressions_not_two_regular :
    (∃ c : ℕ+ → Fin 2, ¬ ∃ x : Fin 5 → ℕ+,
      IsMonochromatic c x ∧ IsDAP positiveFibonacciSet 5 x) ∧
    IsRLarge 1 positiveFibonacciSet ∧ ∀ r, 2 ≤ r → ¬ IsRLarge r positiveFibonacciSet

Sources

• William J. Wesley, Improved Ramsey-Type Theorems for Fibonacci Numbers and Other Sequences, INTEGERS 25 (2025), Article A29, Theorem 2.

Uses 4

Statement usesArithmetic progressions with gap in \(D\) · Monochromatic sequences of positive integers · \(r\)-large sets · Positive Fibonacci set

TheoremFibonacci numbers divided by the golden ratio#●ready to prove

Let \(F_n\) be the \(n\)-th Fibonacci number, with \(F_0 = 0\) and \(F_1 = 1\), and let \(\varphi = (1 + \sqrt{5})/2\) be the golden ratio. For every natural number \(n \ge 2\),

\[\frac{F_n}{\varphi} - F_{n-1} = (-1)^{n+1} \varphi^{-n}.\]

public theorem_wanted fib_div_goldenRatio_sub_fib (n : ℕ) (hn : 2 ≤ n) :
    (Nat.fib n : ℝ) / Real.goldenRatio - Nat.fib (n - 1) =
      (-1) ^ (n + 1) * Real.goldenRatio ^ (-(n : ℤ))

Sources

• William J. Wesley, Improved Ramsey-Type Theorems for Fibonacci Numbers and Other Sequences, INTEGERS 25 (2025), Article A29, Corollary 1.

TheoremBeatty-sequence descriptions of the words \(F_\infty\), \(S\) and \(T\)#●ready to prove

Let \(\varphi = (1 + \sqrt{5})/2\) be the golden ratio and \(F_\infty = 010010100\cdots\) the infinite Fibonacci word. Let \(S = \mu(F_\infty)\) be its image under the morphism \(\mu\) with \(\mu(0) = 10\) and \(\mu(1) = 01\), and \(T = \nu(F_\infty)\) its image under the morphism \(\nu\) with \(\nu(0) = 1\) and \(\nu(1) = 00\). For a word \(W\) and an integer \(n \ge 1\), write \(W(n)\) for the \(n\)-th letter of \(W\), counting from \(1\). Then: (i) for every integer \(n \ge 1\), \(F_\infty(n) = 0\) if and only if \(n = \lfloor m\varphi \rfloor\) for some integer \(m\); (ii) for every integer \(n\), positive or not, if \(n \ne \lfloor m\varphi \rfloor\) for every integer \(m\), then \(n + 1 = \lfloor m'\varphi \rfloor\) and \(n - 1 = \lfloor m''\varphi \rfloor\) for some integers \(m'\) and \(m''\); (iii) for every integer \(n \ge 1\), \(S(n) = 0\) if and only if either \(n\) is even and \(n/2 = \lfloor m\varphi \rfloor\) for some integer \(m\), or \(n\) is odd and \((n+1)/2 \ne \lfloor m\varphi \rfloor\) for every integer \(m\); (iv) for every integer \(n \ge 1\), \(T(n) = 1\) if and only if \(n = 2\lfloor m\varphi \rfloor - m\) for some integer \(m\).

public theorem_wanted fibonacciWord_beatty_properties :
    (∀ n : ℕ, 1 ≤ n → (fibInf (n - 1) = false ↔ ∃ m : ℤ, (n : ℤ) = ⌊m * Real.goldenRatio⌋)) ∧
    (∀ n : ℤ, (∀ m : ℤ, n ≠ ⌊m * Real.goldenRatio⌋) →
      (∃ m' : ℤ, n + 1 = ⌊m' * Real.goldenRatio⌋) ∧ ∃ m'' : ℤ, n - 1 = ⌊m'' * Real.goldenRatio⌋) ∧
    (∀ n : ℕ, 1 ≤ n → (wesleyWordS (n - 1) = false ↔
      (Even n ∧ ∃ m : ℤ, ((n / 2 : ℕ) : ℤ) = ⌊m * Real.goldenRatio⌋) ∨
        (Odd n ∧ ∀ m : ℤ, (((n + 1) / 2 : ℕ) : ℤ) ≠ ⌊m * Real.goldenRatio⌋))) ∧
    ∀ n : ℕ, 1 ≤ n → (wesleyWordT (n - 1) = true ↔
      ∃ m : ℤ, (n : ℤ) = 2 * ⌊m * Real.goldenRatio⌋ - m)

Sources

• William J. Wesley, Improved Ramsey-Type Theorems for Fibonacci Numbers and Other Sequences, INTEGERS 25 (2025), Article A29, Lemma 2.

Uses 3

Statement usesInfinite Fibonacci word · Wesley's word \(S\) · Wesley's word \(T\)

TheoremHalved even Fibonacci numbers and \(4\)-accessibility of the Fibonacci numbers#●ready to prove

Write \(f_n\) for the \(n\)-th Fibonacci number (\(f_0 = 0\), \(f_1 = 1\)). Let \(F = \{1, 2, 3, 5, 8, \dots\}\) be the set of positive Fibonacci numbers and \(G = \{f_{3n}/2 : n \ge 1\} = \{1, 4, 17, 72, \dots\}\) the set of halves of the even Fibonacci numbers. If \(G\) is not \(2\)-accessible, then \(F\) is not \(4\)-accessible.

public theorem_wanted not_accessible_four_of_halfEvenFibonacci
    (h : ¬ IsRAccessible 2 halfEvenFibonacciSet) :
    ¬ IsRAccessible 4 positiveFibonacciSet

Sources

• William J. Wesley, Improved Ramsey-Type Theorems for Fibonacci Numbers and Other Sequences, INTEGERS 25 (2025), Article A29, Lemma 3.

Uses 3

Statement uses\(r\)-accessibility for colorings of the positive integers · Halves of even Fibonacci numbers · Positive Fibonacci set

TheoremDifferences of fractional parts of multiples of the golden ratio#●ready to prove

Let \(F_m\) be the \(m\)-th Fibonacci number, with \(F_0 = 0\) and \(F_1 = 1\), let \(\varphi = (1 + \sqrt{5})/2\) be the golden ratio, and write \(\{y\} = y - \lfloor y \rfloor\) for the fractional part. Let \(i \ge 1\) be a natural number, put \(g_i = F_{3i}/2\) (an integer, since \(F_{3i}\) is even), and let \(x_1, x_2, m_1, m_2\) be integers. Then: (i) if \(g_i\) is even, \(2(x_2 - x_1) = g_i\), \(x_1 = \lfloor m_1\varphi \rfloor\) and \(x_2 = \lfloor m_2\varphi \rfloor\), then \(\{m_2\varphi\} - \{m_1\varphi\} \le (\varphi^{-3i+1} - \varphi)/4 < -0.38\); (ii) if \(g_i\) is odd, \(2(x_2 - x_1) = g_i + 1\), \(x_1 = \lfloor m_1\varphi \rfloor\) and \(x_2 + 1 = \lfloor m_2\varphi \rfloor\), then \(\{m_2\varphi\} - \{m_1\varphi\} < (3\varphi - 6)/4 < -0.28\); (iii) if \(g_i\) is odd, \(i > 1\), \(2(x_2 - x_1) = g_i - 1\), \(x_1 + 1 = \lfloor m_1\varphi \rfloor\) and \(x_2 = \lfloor m_2\varphi \rfloor\), then \(\{m_2\varphi\} - \{m_1\varphi\} < (-5\varphi + 6)/4 < -0.52\).

The paper states (i) with a strict inequality, but equality occurs: \(i = 2\), \(m_1 = 1\), \(m_2 = 2\), \(x_1 = 1\), \(x_2 = 3\) give \(\{2\varphi\} - \{\varphi\} = (\varphi^{-5} - \varphi)/4\).

public theorem_wanted fract_goldenRatio_differences (i : ℕ) (hi : 1 ≤ i) (x₁ x₂ m₁ m₂ : ℤ) :
    (Even (Nat.fib (3 * i) / 2) → 2 * (x₂ - x₁) = (Nat.fib (3 * i) / 2 : ℕ) →
      x₁ = ⌊m₁ * Real.goldenRatio⌋ → x₂ = ⌊m₂ * Real.goldenRatio⌋ →
      Int.fract (m₂ * Real.goldenRatio) - Int.fract (m₁ * Real.goldenRatio) ≤
        (Real.goldenRatio ^ (-(3 * i : ℤ) + 1) - Real.goldenRatio) / 4 ∧
      (Real.goldenRatio ^ (-(3 * i : ℤ) + 1) - Real.goldenRatio) / 4 < -0.38) ∧
    (Odd (Nat.fib (3 * i) / 2) → 2 * (x₂ - x₁) = (Nat.fib (3 * i) / 2 : ℕ) + 1 →
      x₁ = ⌊m₁ * Real.goldenRatio⌋ → x₂ + 1 = ⌊m₂ * Real.goldenRatio⌋ →
      Int.fract (m₂ * Real.goldenRatio) - Int.fract (m₁ * Real.goldenRatio) <
        (3 * Real.goldenRatio - 6) / 4 ∧ (3 * Real.goldenRatio - 6) / 4 < -0.28) ∧
    (Odd (Nat.fib (3 * i) / 2) → 1 < i → 2 * (x₂ - x₁) = (Nat.fib (3 * i) / 2 : ℕ) - 1 →
      x₁ + 1 = ⌊m₁ * Real.goldenRatio⌋ → x₂ = ⌊m₂ * Real.goldenRatio⌋ →
      Int.fract (m₂ * Real.goldenRatio) - Int.fract (m₁ * Real.goldenRatio) <
        (-5 * Real.goldenRatio + 6) / 4 ∧ (-5 * Real.goldenRatio + 6) / 4 < -0.52)

Sources

• William J. Wesley, Improved Ramsey-Type Theorems for Fibonacci Numbers and Other Sequences, INTEGERS 25 (2025), Article A29, Lemma 4.

TheoremFractional parts of shifted Fibonacci numbers divided by \(\sqrt{5}\)#●ready to prove

Let \(F_n\) be the \(n\)-th Fibonacci number, with \(F_0 = 0\) and \(F_1 = 1\), let \(\varphi = (1 + \sqrt{5})/2\) be the golden ratio, so that \(2\varphi - 1 = \sqrt{5}\), and write \(\{y\} = y - \lfloor y \rfloor\) for the fractional part. Let \(n \ge 13\) be a natural number and \(\varepsilon \in \{-4, 0, 4\}\), let \(c_{n,\varepsilon}\) be Wesley's constant, which depends on \(n \bmod 4\) and \(\varepsilon\), and put \(y = (F_n + \varepsilon)/(2\varphi - 1)\). Then (i) \(\{y\} = -2(-\varphi)^{-n}/5 + c_{n,\varepsilon}\), and (ii) \(\lfloor y \rfloor\) is even if and only if \(\varepsilon = 0\) and \(n \equiv 0, 1, 2, 3, 5, 10 \pmod{12}\), or \(\varepsilon = 4\) and \(n \equiv 0, 2, 3, 9, 10 \pmod{12}\), or \(\varepsilon = -4\) and \(n \equiv 0, 1, 2, 5, 7, 10, 11 \pmod{12}\).

The paper prints \(+2(-\varphi)^{-n}/5\) in (i). The sign \(-\) is the one its proof derives (Equation (1)); the printed sign fails for every \(n \ge 13\), since this term is nonzero.

public theorem_wanted fract_fib_add_div_sqrt_five (n : ℕ) (hn : 13 ≤ n) (ε : ℤ)
    (hε : ε = -4 ∨ ε = 0 ∨ ε = 4) :
    Int.fract (((Nat.fib n : ℝ) + ε) / (2 * Real.goldenRatio - 1)) =
        -(2 * (-Real.goldenRatio) ^ (-(n : ℤ)) / 5) + wesleyFractionalConstant n ε ∧
    (Even ⌊((Nat.fib n : ℝ) + ε) / (2 * Real.goldenRatio - 1)⌋ ↔
      (ε = 0 ∧ n % 12 ∈ ({0, 1, 2, 3, 5, 10} : Finset ℕ)) ∨
      (ε = 4 ∧ n % 12 ∈ ({0, 2, 3, 9, 10} : Finset ℕ)) ∨
      (ε = -4 ∧ n % 12 ∈ ({0, 1, 2, 5, 7, 10, 11} : Finset ℕ)))

Sources

• William J. Wesley, Improved Ramsey-Type Theorems for Fibonacci Numbers and Other Sequences, INTEGERS 25 (2025), Article A29, Lemma 5.

Uses 1

Statement usesWesley's constants \(c_{n,\varepsilon}\)

TheoremThe Lucas numbers are not \(4\)-accessible#●ready to prove

Let \(L = \{2, 1, 3, 4, 7, \dots\}\) be the set of Lucas numbers \(L_0 = 2\), \(L_1 = 1\), \(L_{n+2} = L_{n+1} + L_n\). There is a coloring of the positive integers with the colors \(0, 1, 2, 3\) for which no sequence \(x_0, x_1, x_2\) of positive integers is both monochromatic and an \(L\)-diffsequence; and \(L\) is not \(r\)-accessible for any \(r \ge 4\).

public theorem_wanted lucasSet_not_four_accessible :
    (∃ c : ℕ+ → Fin 4, ¬ ∃ x : Fin 3 → ℕ+,
      IsMonochromatic c x ∧ IsDDiffSequence (Set.range lucasNumber) (fun i => ((x i : ℕ) : ℤ))) ∧
    ∀ r, 4 ≤ r → ¬ IsRAccessible r (Set.range lucasNumber)

Sources

• William J. Wesley, Improved Ramsey-Type Theorems for Fibonacci Numbers and Other Sequences, INTEGERS 25 (2025), Article A29, Lemma 6.

Uses 4

Statement uses\(D\)-diffsequences · Monochromatic sequences of positive integers · \(r\)-accessibility for colorings of the positive integers · Lucas numbers

TheoremThe even Fibonacci numbers have degree of accessibility \(1\)#●ready to prove

The even Fibonacci set \(\{2, 8, 34, \dots\}\) is \(1\)-accessible, and it is not \(r\)-accessible for any natural number \(r \ge 2\).

public theorem_wanted evenFibonacciSet_degreeOfAccessibility_eq_one :
    IsRAccessible 1 evenFibonacciSet ∧ ∀ r, 2 ≤ r → ¬ IsRAccessible r evenFibonacciSet

Sources

• William J. Wesley, Improved Ramsey-Type Theorems for Fibonacci Numbers and Other Sequences, INTEGERS 25 (2025), Article A29, Corollary 2.

Uses 2

Statement uses\(r\)-accessibility for colorings of the positive integers · Even Fibonacci set

47 fully proved33 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.