Göbel sequences

DefinitionThe (k, l)-Göbel sequence#✓fully proved

For natural numbers \(k\) and \(l\), the \((k, l)\)-Göbel sequence is the sequence of rational numbers \(g_{k,l}(n)\), \(n \ge 0\), given by \(g_{k,l}(0) = 0\), \(g_{k,l}(1) = l\) and, for \(n \ge 1\),

\[g_{k,l}(n + 1) = \frac{g_{k,l}(n) \bigl(n + g_{k,l}(n)^{k-1}\bigr)}{n + 1},\]

where \(k - 1\) is truncated subtraction, so the exponent is \(0\) when \(k = 0\).

The paper indexes from \(n = 1\) and takes \(k, l \ge 2\) (Lemma 5 also admits \(k, l \ge 1\)); the value at \(n = 0\) is a convention and plays no role.

public def gobelSequence (k l : ℕ) : ℕ → ℚ
  | 0 => 0
  | 1 => l
  | n + 2 => gobelSequence k l (n + 1) * ((n + 1 : ℚ) + gobelSequence k l (n + 1) ^ (k - 1))
      / (n + 2)

Sources

• Gima, Matsusaka, Miyazaki, and Yara, On Integrality and Asymptotic Behavior of the (k, l)-Göbel Sequences, Journal of Integer Sequences 27 (2024), Article 24.8.1, Definition 1.

Used by 24

Used byCounting prime first nonintegral indices of \(g_{k,2}\) for \(k \le 10^7\) · Failure of the residue sequence detects non-integrality · Asymptotic expansion of the \((k, l)\)-Göbel sequence · Series formula and bound for the Göbel error · The Göbel error term decays faster than every power of \(n\) · The first non-integral term of \(g_{2600725,2}\) is at index \(9011\) · Index-scaled Göbel terms with \(k = (p-1)/2\) are congruent to the residue walk · Göbel sequences at index \(p\) for primes \(p \equiv 3 \pmod 4\) · Odd starting values give a \(p\)-integral \(p\)-th term when \(p \equiv 1 \pmod 4\) · Unique boundary pair for Göbel sequences when \(p \equiv 1 \pmod 4\) · Integrality of the early terms of \((k, l)\)-Göbel sequences · Propagation of a congruence along the \((k, l)\)-Göbel sequence · A congruence class of non-integral Göbel sequences · A non-integral term of \(g_{k,2}\) by index \(29363\) for \(2 \le k \le 10^{14}\) · A non-integral term of \(g_{k,2}\) by index \(9011\) for \(2 \le k \le 10^7\) · Initial value of the \((k, l)\)-Göbel sequence · Key \(p\)-adic properties of the \((k, l)\)-Göbel sequences · Residues of the \((k, l)\)-Göbel sequence modulo \(p^r\) · Strict decrease of the normalized Göbel roots · The normalized Göbel roots converge to a limit greater than 1 · Integrality of Göbel sequences up to index 7 via finite \(p\)-adic checks · Recursion for the (k, l)-Göbel sequence · Göbel's original sequence · Somos-type sequences lie below Göbel sequences

TheoremInitial value of the \((k, l)\)-Göbel sequence#✓fully proved

For all natural numbers \(k\) and \(l\), the \((k, l)\)-Göbel sequence \(g_{k,l}\) satisfies \(g_{k,l}(1) = l\).

public theorem gobelSequence_one (k l : ℕ) : gobelSequence k l 1 = l

Sources

• Gima, Matsusaka, Miyazaki, and Yara, On Integrality and Asymptotic Behavior of the (k, l)-Göbel Sequences, Journal of Integer Sequences 27 (2024), Article 24.8.1, Definition 1.

Uses 1

Statement usesThe (k, l)-Göbel sequence

TheoremRecursion for the (k, l)-Göbel sequence#✓fully proved

For all natural numbers \(k\), \(l\) and \(n \ge 1\), the \((k, l)\)-Göbel sequence \(g_{k,l}\) satisfies, in \(\mathbb{Q}\),

\[(n + 1)\, g_{k,l}(n + 1) = g_{k,l}(n) \bigl(n + g_{k,l}(n)^{k-1}\bigr),\]

where \(k - 1\) is truncated subtraction, so the exponent is \(0\) when \(k = 0\).

public theorem gobelSequence_succ (k l n : ℕ) (hn : 1 ≤ n) :
    (n + 1 : ℚ) * gobelSequence k l (n + 1)
      = gobelSequence k l n * ((n : ℚ) + gobelSequence k l n ^ (k - 1))

Sources

• Gima, Matsusaka, Miyazaki, and Yara, On Integrality and Asymptotic Behavior of the (k, l)-Göbel Sequences, Journal of Integer Sequences 27 (2024), Article 24.8.1, Definition 1.

Uses 1

Statement usesThe (k, l)-Göbel sequence

TheoremGöbel's original sequence#✓fully proved

The \((2, 2)\)-Göbel sequence \(g_{2,2}\) satisfies \(g_{2,2}(2) = 3\), \(g_{2,2}(3) = 5\), \(g_{2,2}(4) = 10\) and \(g_{2,2}(5) = 28\).

public theorem gobelSequence_two_two_small :
    gobelSequence 2 2 2 = 3 ∧ gobelSequence 2 2 3 = 5 ∧ gobelSequence 2 2 4 = 10 ∧
      gobelSequence 2 2 5 = 28

Sources

• Gima, Matsusaka, Miyazaki, and Yara, On Integrality and Asymptotic Behavior of the (k, l)-Göbel Sequences, Journal of Integer Sequences 27 (2024), Article 24.8.1, Section 1.

Uses 1

Statement usesThe (k, l)-Göbel sequence

TheoremIntegrality of the early terms of \((k, l)\)-Göbel sequences#●ready to prove

Let \(g_{k,l}\) denote the \((k, l)\)-Göbel sequence. For all natural numbers \(k, l \ge 2\) and \(1 \le n \le 6\), the value \(g_{k,l}(n)\) is an integer. Moreover, for all natural numbers \(k, l \ge 2\), the value \(g_{k,l}(7)\) is not an integer if and only if \(k \equiv 2 \pmod 6\) and \(l \equiv 3 \pmod 7\).

Equivalently, if \(N_{k,l}\) is the first index at which \(g_{k,l}\) is not an integer, then \(\min_{k,l \ge 2} N_{k,l} = 7\), and \(N_{k,l} = 7\) if and only if \(k \equiv 2 \pmod 6\) and \(l \equiv 3 \pmod 7\).

public theorem_wanted gobelSequence_integral_le_six_and_seven_iff :
    (∀ k l : ℕ, 2 ≤ k → 2 ≤ l → ∀ n : ℕ, 1 ≤ n → n ≤ 6 →
        ∃ z : ℤ, gobelSequence k l n = z) ∧
      ∀ k l : ℕ, 2 ≤ k → 2 ≤ l →
        ((¬ ∃ z : ℤ, gobelSequence k l 7 = z) ↔ k % 6 = 2 ∧ l % 7 = 3)

Sources

• Gima, Matsusaka, Miyazaki, and Yara, On Integrality and Asymptotic Behavior of the (k, l)-Göbel Sequences, Journal of Integer Sequences 27 (2024), Article 24.8.1, Theorem 2 (jis-2024-24.8.1-thm-2).

Uses 1

Statement usesThe (k, l)-Göbel sequence

TheoremAsymptotic expansion of the \((k, l)\)-Göbel sequence#●ready to prove

Let \(k, l \ge 2\) be natural numbers and let \(g_{k,l}\) be the \((k, l)\)-Göbel sequence. There are a real number \(C > 1\) and real numbers \(a_1, a_2, \dots\) such that for every natural number \(R\), as \(n \to \infty\),

\[g_{k,l}(n) - C^{k^n} n^{1/(k-1)} \Bigl(1 + \sum_{r=1}^{R} \frac{a_r}{n^r}\Bigr) = O\Bigl(\frac{C^{k^n} n^{1/(k-1)}}{n^{R+1}}\Bigr).\]

In other words, \(g_{k,l}(n) \sim C^{k^n} n^{1/(k-1)} \bigl(1 + \sum_{r \ge 1} a_r / n^r\bigr)\) as an asymptotic expansion, generalizing Zagier's asymptotic for Göbel's sequence.

public theorem_wanted gobelSequence_asymptotic_expansion (k l : ℕ) (hk : 2 ≤ k) (hl : 2 ≤ l) :
    ∃ C : ℝ, 1 < C ∧ ∃ a : ℕ → ℝ, ∀ R : ℕ,
      (fun n : ℕ => (gobelSequence k l n : ℝ)
          - C ^ (k ^ n) * (n : ℝ) ^ ((1 : ℝ) / (k - 1))
            * (1 + ∑ r ∈ Finset.Icc 1 R, a r / (n : ℝ) ^ r))
        =O[atTop]
      (fun n : ℕ => C ^ (k ^ n) * (n : ℝ) ^ ((1 : ℝ) / (k - 1)) / (n : ℝ) ^ (R + 1))

Sources

• Gima, Matsusaka, Miyazaki, and Yara, On Integrality and Asymptotic Behavior of the (k, l)-Göbel Sequences, Journal of Integer Sequences 27 (2024), Article 24.8.1, Theorem 4 (jis-2024-24.8.1-thm-4).

Uses 1

Statement usesThe (k, l)-Göbel sequence

TheoremKey \(p\)-adic properties of the \((k, l)\)-Göbel sequences#●ready to prove

Let \(p\) be a prime, let \(N \ge 1\) be a natural number, let \(r = \nu_p(N!)\), where \(\nu_p\) is the \(p\)-adic valuation on \(\mathbb{Q}\) (with \(\nu_p(0) = 0\)), and write \(g_{k,l}\) for the \((k, l)\)-Göbel sequence. Write \(\mathbb{Z}_{(p)}\) for the set of rational numbers \(x\) with \(\nu_p(x) \ge 0\), and for an integer \(s\) write \(x \in p^s \mathbb{Z}_{(p)}\) when \(x = 0\) or \(\nu_p(x) \ge s\). Then: (1) for all natural numbers \(k, l \ge 1\), if \(p > N\) then \(g_{k,l}(N) \in \mathbb{Z}_{(p)}\); (2) for all natural numbers \(k, l \ge 1\) and \(1 \le n \le N\), if \(g_{k,l}(n) \notin \mathbb{Z}_{(p)}\) then \(g_{k,l}(n + 1) \notin \mathbb{Z}_{(p)}\); (3) if \(p \le N\), then for all natural numbers \(k_1, k_2 \ge r\) with \(k_1 \equiv k_2 \pmod{\varphi(p^r)}\), where \(\varphi\) is Euler's totient function, all \(l \ge 1\) and all \(1 \le n \le N\): \(g_{k_1,l}(n) \in \mathbb{Z}_{(p)}\) if and only if \(g_{k_2,l}(n) \in \mathbb{Z}_{(p)}\), and in that case \(g_{k_1,l}(n) - g_{k_2,l}(n) \in p^{r - \nu_p(n!)} \mathbb{Z}_{(p)}\); (4) if \(p \le N\), then for all natural numbers \(k, l_1, l_2 \ge 1\) with \(l_1 \equiv l_2 \pmod{p^r}\) and all \(1 \le n \le N\): \(g_{k,l_1}(n) \in \mathbb{Z}_{(p)}\) if and only if \(g_{k,l_2}(n) \in \mathbb{Z}_{(p)}\), and in that case \(g_{k,l_1}(n) - g_{k,l_2}(n) \in p^{r - \nu_p(n!)} \mathbb{Z}_{(p)}\).

MetaMathlibExt.gobelSequence_padic_key_properties · 23 lines

public theorem_wanted gobelSequence_padic_key_properties (p : ℕ) (hp : p.Prime)
    (N : ℕ) (hN : 1 ≤ N) :
    (∀ k l : ℕ, 1 ≤ k → 1 ≤ l → N < p → 0 ≤ padicValRat p (gobelSequence k l N)) ∧
    (∀ k l n : ℕ, 1 ≤ k → 1 ≤ l → 1 ≤ n → n ≤ N →
        padicValRat p (gobelSequence k l n) < 0 →
          padicValRat p (gobelSequence k l (n + 1)) < 0) ∧
    (∀ k₁ k₂ l n : ℕ, p ≤ N → 1 ≤ l → 1 ≤ n → n ≤ N →
        padicValNat p N.factorial ≤ k₁ → padicValNat p N.factorial ≤ k₂ →
        k₁ ≡ k₂ [MOD (p ^ padicValNat p N.factorial).totient] →
        ((0 ≤ padicValRat p (gobelSequence k₁ l n) ↔
            0 ≤ padicValRat p (gobelSequence k₂ l n)) ∧
          (0 ≤ padicValRat p (gobelSequence k₁ l n) →
            gobelSequence k₁ l n - gobelSequence k₂ l n = 0 ∨
              ((padicValNat p N.factorial : ℤ) - padicValNat p n.factorial
                ≤ padicValRat p (gobelSequence k₁ l n - gobelSequence k₂ l n))))) ∧
    (∀ k l₁ l₂ n : ℕ, p ≤ N → 1 ≤ k → 1 ≤ l₁ → 1 ≤ l₂ → 1 ≤ n → n ≤ N →
        l₁ ≡ l₂ [MOD p ^ padicValNat p N.factorial] →
        ((0 ≤ padicValRat p (gobelSequence k l₁ n) ↔
            0 ≤ padicValRat p (gobelSequence k l₂ n)) ∧
          (0 ≤ padicValRat p (gobelSequence k l₁ n) →
            gobelSequence k l₁ n - gobelSequence k l₂ n = 0 ∨
              ((padicValNat p N.factorial : ℤ) - padicValNat p n.factorial
                ≤ padicValRat p (gobelSequence k l₁ n - gobelSequence k l₂ n)))))

Sources

• Gima, Matsusaka, Miyazaki, and Yara, On Integrality and Asymptotic Behavior of the (k, l)-Göbel Sequences, Journal of Integer Sequences 27 (2024), Article 24.8.1, Lemma 5 (jis-2024-24.8.1-lem-5).

Uses 1

Statement usesThe (k, l)-Göbel sequence

TheoremIntegrality of Göbel sequences up to index 7 via finite \(p\)-adic checks#●ready to prove

Let \(g_{k,l}\) be the \((k, l)\)-Göbel sequence. For a prime \(p\), call a rational number \(x\) \(p\)-integral if \(x \in \mathbb{Z}_{(p)}\), that is, if \(x = 0\) or its \(p\)-adic valuation \(\nu_p(x)\) is nonnegative. The following two statements are equivalent.

(i) For all natural numbers \(k, l \ge 2\), the value \(g_{k,l}(n)\) is an integer for every \(1 \le n \le 6\), and \(g_{k,l}(7)\) is not an integer if and only if \(k \equiv 2 \pmod 6\) and \(l \equiv 3 \pmod 7\).

(ii) \(g_{k,l}(7)\) is \(2\)-integral for all \(2 \le k \le 11\) and \(1 \le l \le 16\); it is \(3\)-integral for all \(2 \le k \le 7\) and \(1 \le l \le 9\); it is \(5\)-integral for all \(1 \le k \le 4\) and \(1 \le l \le 5\); and for all \(1 \le k \le 6\) and \(1 \le l \le 7\), it is not \(7\)-integral if and only if \((k, l) = (2, 3)\).

Statement (i) is Theorem 2 of the source.

public theorem_wanted gobelSequence_seven_iff_padic_claims :
    ((∀ k l : ℕ, 2 ≤ k → 2 ≤ l → ∀ n : ℕ, 1 ≤ n → n ≤ 6 →
        ∃ z : ℤ, gobelSequence k l n = z) ∧
      ∀ k l : ℕ, 2 ≤ k → 2 ≤ l →
        ((¬ ∃ z : ℤ, gobelSequence k l 7 = z) ↔ k % 6 = 2 ∧ l % 7 = 3)) ↔
    ((∀ k ∈ Finset.Icc 2 11, ∀ l ∈ Finset.Icc 1 16,
        0 ≤ padicValRat 2 (gobelSequence k l 7)) ∧
      (∀ k ∈ Finset.Icc 2 7, ∀ l ∈ Finset.Icc 1 9,
        0 ≤ padicValRat 3 (gobelSequence k l 7)) ∧
      (∀ k ∈ Finset.Icc 1 4, ∀ l ∈ Finset.Icc 1 5,
        0 ≤ padicValRat 5 (gobelSequence k l 7)) ∧
      (∀ k ∈ Finset.Icc 1 6, ∀ l ∈ Finset.Icc 1 7,
        (padicValRat 7 (gobelSequence k l 7) < 0 ↔ k = 2 ∧ l = 3)))

Sources

• Gima, Matsusaka, Miyazaki, and Yara, On Integrality and Asymptotic Behavior of the (k, l)-Göbel Sequences, Journal of Integer Sequences 27 (2024), Article 24.8.1, Lemma 6 (jis-2024-24.8.1-lem-6).

Uses 1

Statement usesThe (k, l)-Göbel sequence

TheoremStrict decrease of the normalized Göbel roots#●ready to prove

Let \(k, l \ge 2\) be natural numbers, let \(g_{k,l}\) be the \((k, l)\)-Göbel sequence, and let \(C_{k,l}(n) = g_{k,l}(n)^{1/k^n}\), a real number. Then \(C_{k,l}(n) > C_{k,l}(n + 1) > 1\) for every natural number \(n \ge 1\).

public theorem_wanted gobelSequence_root_strictAnti (k l n : ℕ) (hk : 2 ≤ k) (hl : 2 ≤ l)
    (hn : 1 ≤ n) :
    (gobelSequence k l (n + 1) : ℝ) ^ ((1 : ℝ) / (k : ℝ) ^ (n + 1))
        < (gobelSequence k l n : ℝ) ^ ((1 : ℝ) / (k : ℝ) ^ n) ∧
      1 < (gobelSequence k l (n + 1) : ℝ) ^ ((1 : ℝ) / (k : ℝ) ^ (n + 1))

Sources

• Gima, Matsusaka, Miyazaki, and Yara, On Integrality and Asymptotic Behavior of the (k, l)-Göbel Sequences, Journal of Integer Sequences 27 (2024), Article 24.8.1, Lemma 7 (jis-2024-24.8.1-lem-7).

Uses 1

Statement usesThe (k, l)-Göbel sequence

TheoremRoot asymptotics of Somos-type sequences#●ready to prove

Let \(k \ge 2\) be a natural number, let \(\sigma_k = \exp\bigl(\sum_{m \ge 1} \log m / k^m\bigr)\) be the \(k\)-Somos constant, and let \(t : \mathbb{N} \to \mathbb{R}\) satisfy \(t(n + 1) = t(n)^k / (n + 1)\) for all \(n \ge 0\). If \(t(0) > \sigma_k\), then the sequence \(n \mapsto t(n)^{1/k^n}\) is nonincreasing and converges to some real number \(c > 1\).

The sequence is constant from \(n = 0\) to \(n = 1\), so the paper's "decreases monotonically" is read in the non-strict sense.

public theorem_wanted somosLike_root_antitone_tendsto (k : ℕ) (hk : 2 ≤ k) (t : ℕ → ℝ)
    (ht : ∀ n : ℕ, t (n + 1) = t n ^ k / (n + 1))
    (h0 : Real.exp (∑' m : ℕ, Real.log m / (k : ℝ) ^ m) < t 0) :
    ∃ c : ℝ, 1 < c ∧ Antitone (fun n : ℕ => t n ^ ((1 : ℝ) / (k : ℝ) ^ n)) ∧
      Tendsto (fun n : ℕ => t n ^ ((1 : ℝ) / (k : ℝ) ^ n)) atTop (𝓝 c)

Sources

• Gima, Matsusaka, Miyazaki, and Yara, On Integrality and Asymptotic Behavior of the (k, l)-Göbel Sequences, Journal of Integer Sequences 27 (2024), Article 24.8.1, Lemma 8 (jis-2024-24.8.1-lem-8).

TheoremSomos-type sequences lie below Göbel sequences#●ready to prove

Let \(k, l \ge 2\) be natural numbers, let \(g_{k,l}\) be the \((k, l)\)-Göbel sequence, and let \(t : \mathbb{N} \to \mathbb{R}\) satisfy \(t(n + 1) = t(n)^k / (n + 1)\) for all \(n \ge 0\). If \(t(0)^k \le l\), then \(t(n) \le g_{k,l}(n)\) for every \(n \ge 1\).

The paper also assumes \(t(0) > 1\); the statement holds without it (for even \(k\), \(t(n) \ge 0\) for \(n \ge 1\); for odd \(k\), \(x \mapsto x^k\) is monotone), so that hypothesis is dropped.

public theorem_wanted somosLike_le_gobelSequence (k l : ℕ) (hk : 2 ≤ k) (hl : 2 ≤ l)
    (t : ℕ → ℝ) (ht : ∀ n : ℕ, t (n + 1) = t n ^ k / (n + 1)) (h0 : t 0 ^ k ≤ l)
    (n : ℕ) (hn : 1 ≤ n) :
    t n ≤ gobelSequence k l n

Sources

• Gima, Matsusaka, Miyazaki, and Yara, On Integrality and Asymptotic Behavior of the (k, l)-Göbel Sequences, Journal of Integer Sequences 27 (2024), Article 24.8.1, Lemma 9 (jis-2024-24.8.1-lem-9).

Uses 1

Statement usesThe (k, l)-Göbel sequence

TheoremThe normalized Göbel roots converge to a limit greater than 1#●ready to prove

Let \(k, l \ge 2\) be natural numbers and let \(g_{k,l}\) be the \((k, l)\)-Göbel sequence. There is a real number \(C > 1\) such that the real numbers \(g_{k,l}(n)^{1/k^n}\) tend to \(C\) as \(n \to \infty\).

The paper defines \(C_{k,l}\) as this limit.

public theorem_wanted gobelSequence_root_tendsto_gt_one (k l : ℕ) (hk : 2 ≤ k) (hl : 2 ≤ l) :
    ∃ C : ℝ, 1 < C ∧
      Tendsto (fun n : ℕ => (gobelSequence k l n : ℝ) ^ ((1 : ℝ) / (k : ℝ) ^ n)) atTop (𝓝 C)

Sources

• Gima, Matsusaka, Miyazaki, and Yara, On Integrality and Asymptotic Behavior of the (k, l)-Göbel Sequences, Journal of Integer Sequences 27 (2024), Article 24.8.1, Proposition 10 (jis-2024-24.8.1-prop-10).

Uses 1

Statement usesThe (k, l)-Göbel sequence

TheoremThe Göbel error term decays faster than every power of \(n\)#●ready to prove

Let \(k, l \ge 2\) be natural numbers, let \(g_{k,l}\) be the \((k, l)\)-Göbel sequence, and let \(C\) be a real number such that the real numbers \(C_{k,l}(n) = g_{k,l}(n)^{1/k^n}\) tend to \(C\) as \(n \to \infty\). Then for every real number \(R > 0\), as \(n \to \infty\),

\[\exp\Bigl(\sum_{m=1}^{\infty} \frac{\log(m + n)}{k^m}\Bigr) - \Bigl(\frac{C_{k,l}(n)}{C}\Bigr)^{k^n} = O(n^{-R}).\]

public theorem_wanted gobelSequence_error_isBigO (k l : ℕ) (hk : 2 ≤ k) (hl : 2 ≤ l) (C : ℝ)
    (hC : Tendsto (fun n : ℕ => (gobelSequence k l n : ℝ) ^ ((1 : ℝ) / (k : ℝ) ^ n))
      atTop (𝓝 C))
    (R : ℝ) (hR : 0 < R) :
    (fun n : ℕ => Real.exp (∑' m : ℕ, Real.log ((m + 1 : ℝ) + n) / (k : ℝ) ^ (m + 1))
        - ((gobelSequence k l n : ℝ) ^ ((1 : ℝ) / (k : ℝ) ^ n) / C) ^ (k ^ n))
      =O[atTop] (fun n : ℕ => (n : ℝ) ^ (-R))

Sources

• Gima, Matsusaka, Miyazaki, and Yara, On Integrality and Asymptotic Behavior of the (k, l)-Göbel Sequences, Journal of Integer Sequences 27 (2024), Article 24.8.1, Theorem 11 (jis-2024-24.8.1-thm-11).

Uses 1

Statement usesThe (k, l)-Göbel sequence

TheoremSeries formula and bound for the Göbel error#●ready to prove

Let \(k, l \ge 2\) be natural numbers, let \(g_{k,l}\) be the \((k, l)\)-Göbel sequence, and let \(C\) be a real number such that the real numbers \(C_{k,l}(n) = g_{k,l}(n)^{1/k^n}\) tend to \(C\) as \(n \to \infty\). Then for every natural number \(n \ge 1\) the error

\[\varepsilon_{k,l}(n) = \sum_{m=1}^{\infty} \frac{\log(m + n)}{k^m} - k^n \bigl(\log C_{k,l}(n) - \log C\bigr)\]

satisfies

\[\varepsilon_{k,l}(n) = \sum_{m=1}^{\infty} \frac{1}{k^m} \log\Bigl(1 + \frac{m + n - 1}{g_{k,l}(m + n - 1)^{k-1}}\Bigr) \le \frac{2n}{C^{(k-1) k^n}}.\]

public theorem_wanted gobelSequence_error_eq_tsum_le (k l : ℕ) (hk : 2 ≤ k) (hl : 2 ≤ l) (C : ℝ)
    (hC : Tendsto (fun n : ℕ => (gobelSequence k l n : ℝ) ^ ((1 : ℝ) / (k : ℝ) ^ n))
      atTop (𝓝 C))
    (n : ℕ) (hn : 1 ≤ n) :
    (∑' m : ℕ, Real.log ((m + 1 : ℝ) + n) / (k : ℝ) ^ (m + 1))
        - (k : ℝ) ^ n * (Real.log ((gobelSequence k l n : ℝ) ^ ((1 : ℝ) / (k : ℝ) ^ n))
          - Real.log C)
      = ∑' m : ℕ, Real.log (1 + ((m + n : ℕ) : ℝ) / (gobelSequence k l (m + n) : ℝ) ^ (k - 1))
          / (k : ℝ) ^ (m + 1) ∧
    ∑' m : ℕ, Real.log (1 + ((m + n : ℕ) : ℝ) / (gobelSequence k l (m + n) : ℝ) ^ (k - 1))
          / (k : ℝ) ^ (m + 1)
      ≤ 2 * n / C ^ ((k - 1) * k ^ n)

Sources

• Gima, Matsusaka, Miyazaki, and Yara, On Integrality and Asymptotic Behavior of the (k, l)-Göbel Sequences, Journal of Integer Sequences 27 (2024), Article 24.8.1, Lemma 12 (jis-2024-24.8.1-lem-12).

Uses 1

Statement usesThe (k, l)-Göbel sequence

TheoremSondow–Hadjicostas asymptotic expansion#●ready to prove

Let \(k \ge 2\) be a natural number. For \(j \ge 1\) put \(S_j = \sum_{i \ge 1} i^j / k^i\) and \(b_j = (-1)^{j-1} S_j / j\), and for \(r \ge 0\) let

\[a_r = \sum_{m_1 + 2 m_2 + \dots + r m_r = r} \ \prod_{j=1}^{r} \frac{b_j^{m_j}}{m_j!},\]

where the sum runs over the tuples \((m_1, \dots, m_r)\) of natural numbers satisfying the constraint. For \(n \in \mathbb{N}\) let \(E(n) = \exp\bigl(\sum_{s \ge 1} \log(s + n) / k^s\bigr)\) and, for a natural number \(R\), let \(P_R(n) = 1 + \sum_{r=1}^{R} a_r / n^r\). Then for every natural number \(R\),

\[E(n) - n^{1/(k-1)} P_R(n) = O\bigl(n^{1/(k-1)} / n^{R+1}\bigr)\]

as \(n \to \infty\) through the natural numbers.

In the paper \(S_j\) appears as \(A_j(k) / (k - 1)^{j+1}\), with \(A_j\) the Eulerian polynomial.

public theorem_wanted somos_tsum_asymptotic_expansion (k : ℕ) (hk : 2 ≤ k) (a : ℕ → ℝ)
    (ha : ∀ r : ℕ, a r =
      ∑ m ∈ (Fintype.piFinset fun _ : Fin r => Finset.range (r + 1)).filter
          (fun m => ∑ j : Fin r, ((j : ℕ) + 1) * m j = r),
        ∏ j : Fin r, (1 / ((m j).factorial : ℝ)) *
          ((-1 : ℝ) ^ (j : ℕ) / ((j : ℕ) + 1) *
            ∑' i : ℕ, (i : ℝ) ^ ((j : ℕ) + 1) / (k : ℝ) ^ i) ^ (m j))
    (R : ℕ) :
    (fun n : ℕ => Real.exp (∑' m : ℕ, Real.log ((m + 1 : ℝ) + n) / (k : ℝ) ^ (m + 1))
        - (n : ℝ) ^ ((1 : ℝ) / (k - 1)) * (1 + ∑ r ∈ Finset.Icc 1 R, a r / (n : ℝ) ^ r))
      =O[atTop] (fun n : ℕ => (n : ℝ) ^ ((1 : ℝ) / (k - 1)) / (n : ℝ) ^ (R + 1))

Sources

• Gima, Matsusaka, Miyazaki, and Yara, On Integrality and Asymptotic Behavior of the (k, l)-Göbel Sequences, Journal of Integer Sequences 27 (2024), Article 24.8.1, Theorem 15, quoting Sondow and Hadjicostas (2007), Theorem 9 and Lemma 1 (jis-2024-24.8.1-thm-15).

DefinitionResidue of a rational number modulo an integer#✓fully proved

For a natural number \(m\) and a rational number \(x = a/b\) in lowest terms with \(b > 0\), the residue of \(x\) modulo \(m\) is the element \(a \cdot b^{-1}\) of \(\mathbb{Z}/m\mathbb{Z}\). When \(b\) is prime to \(m\), \(b^{-1}\) is the inverse of \(b\) modulo \(m\), so the residue is the class \(c\) with \(b c \equiv a \pmod m\); for other \(x\) the inverse, and hence the residue, is a conventional value with no arithmetic meaning.

For a prime \(p\) and a natural number \(r\), it is used to read congruences modulo \(p^r\) in the ring \(\mathbb{Z}_{(p)}\) of rational numbers whose denominator is prime to \(p\).

public def ratResidue (m : ℕ) (x : ℚ) : ZMod m :=
  (x.num : ZMod m) * (x.den : ZMod m)⁻¹

Sources

• Gima, Matsusaka, Miyazaki, and Yara, On Integrality and Asymptotic Behavior of the (k, l)-Göbel Sequences, Journal of Integer Sequences 27 (2024), Article 24.8.1, Section 4 (residues of g_{k,l}(n) modulo p^r in ℤ_(p)).

Used by 6

Used byResidues of the \((k, l)\)-Göbel sequence modulo \(p^r\) · Residue of an integer · The congruence \(p\sum_{j=0}^{p} B_j/(p-j+1) \equiv -1 \pmod p\) · The congruence \(\sum_{j=0}^{p-3} B_j \equiv -1 \pmod p\) · The congruence \(\sum_{j=0}^{p} E_j(0) \equiv 3/2 \pmod p\) · The congruence \(\sum_{j=0}^{p} pB_j \equiv -1 \pmod p\)

TheoremResidue of an integer#✓fully proved

For every natural number \(m\) and every integer \(z\), the residue modulo \(m\) of \(z\), viewed as a rational number, is the image of \(z\) in \(\mathbb{Z}/m\mathbb{Z}\).

public theorem ratResidue_intCast (m : ℕ) (z : ℤ) : ratResidue m z = (z : ZMod m)

Sources

• Gima, Matsusaka, Miyazaki, and Yara, On Integrality and Asymptotic Behavior of the (k, l)-Göbel Sequences, Journal of Integer Sequences 27 (2024), Article 24.8.1, Section 4.

Uses 1

Statement usesResidue of a rational number modulo an integer

TheoremResidues of the \((k, l)\)-Göbel sequence modulo \(p^r\)#●ready to prove

Let \(p\) be a prime, let \(k, l, r \ge 2\) be natural numbers, and let \(g_{k,l}\) be the \((k, l)\)-Göbel sequence. Let \(I\) be the set of natural numbers \(n\) with \(1 \le n < p\) such that \(g_{k,l}(n) = 0\) or \(\nu_p(g_{k,l}(n)) \ge r - 1\), where \(\nu_p\) is the \(p\)-adic valuation on \(\mathbb{Q}\); that is, \(g_{k,l}(n) \equiv 0 \pmod{p^{r-1}}\) in \(\mathbb{Z}_{(p)}\). Let \(G\) be the set of residues of the numbers \(g_{k,l}(n)\), \(n \in I\), in \(\mathbb{Z}/p^r\mathbb{Z}\), the residue of a rational number being its numerator times the inverse of its denominator. Then \(G = \{0\}\) or \(G\) has exactly as many elements as \(I\).

public theorem_wanted gobelSequence_residues_singleton_or_injective (p : ℕ) (hp : p.Prime)
    (k l r : ℕ) (hk : 2 ≤ k) (hl : 2 ≤ l) (hr : 2 ≤ r) :
    ((Finset.Ico 1 p).filter (fun n => gobelSequence k l n = 0 ∨
          ((r : ℤ) - 1 ≤ padicValRat p (gobelSequence k l n)))).image
        (fun n => ratResidue (p ^ r) (gobelSequence k l n)) = {0} ∨
      (((Finset.Ico 1 p).filter (fun n => gobelSequence k l n = 0 ∨
          ((r : ℤ) - 1 ≤ padicValRat p (gobelSequence k l n)))).image
        (fun n => ratResidue (p ^ r) (gobelSequence k l n))).card =
      ((Finset.Ico 1 p).filter (fun n => gobelSequence k l n = 0 ∨
          ((r : ℤ) - 1 ≤ padicValRat p (gobelSequence k l n)))).card

Sources

• Gima, Matsusaka, Miyazaki, and Yara, On Integrality and Asymptotic Behavior of the (k, l)-Göbel Sequences, Journal of Integer Sequences 27 (2024), Article 24.8.1, Theorem 18 (jis-2024-24.8.1-thm-18).

Uses 2

Statement usesThe (k, l)-Göbel sequence · Residue of a rational number modulo an integer

TheoremPropagation of a congruence along the \((k, l)\)-Göbel sequence#●ready to prove

Let \(p\) be a prime, let \(k, l, r \ge 2\) be natural numbers, let \(g_{k,l}\) be the \((k, l)\)-Göbel sequence, and let \(a, b\) be natural numbers with \(1 \le a < p\) and \(b < p\). For rational numbers \(x, y\) write \(x \equiv y \pmod{p^r}\) when \(x = y\) or \(\nu_p(x - y) \ge r\), where \(\nu_p\) is the \(p\)-adic valuation on \(\mathbb{Q}\). If \(g_{k,l}(a) \equiv b p^{r-1} \pmod{p^r}\), then \(n \, g_{k,l}(n) \equiv a b p^{r-1} \pmod{p^r}\) for every natural number \(n\) with \(a \le n < p\).

public theorem_wanted gobelSequence_mul_index_congr (p : ℕ) (hp : p.Prime) (k l r a b : ℕ)
    (hk : 2 ≤ k) (hl : 2 ≤ l) (hr : 2 ≤ r) (ha₁ : 1 ≤ a) (hap : a < p) (hbp : b < p)
    (hg : gobelSequence k l a - b * (p : ℚ) ^ (r - 1) = 0 ∨
      (r : ℤ) ≤ padicValRat p (gobelSequence k l a - b * (p : ℚ) ^ (r - 1)))
    (n : ℕ) (han : a ≤ n) (hnp : n < p) :
    n * gobelSequence k l n - a * b * (p : ℚ) ^ (r - 1) = 0 ∨
      (r : ℤ) ≤ padicValRat p (n * gobelSequence k l n - a * b * (p : ℚ) ^ (r - 1))

Sources

• Gima, Matsusaka, Miyazaki, and Yara, On Integrality and Asymptotic Behavior of the (k, l)-Göbel Sequences, Journal of Integer Sequences 27 (2024), Article 24.8.1, Lemma 20 (jis-2024-24.8.1-lem-20).

Uses 1

Statement usesThe (k, l)-Göbel sequence

DefinitionThe residue walk \(\tilde g_l\)#✓fully proved

For natural numbers \(p\) and \(l\), write \(\left(\frac{a}{p}\right)\) for the Jacobi symbol. The residue walk \(\tilde g_l \colon \mathbb{N} \to \mathbb{N}\) of \(p\) starting at \(l\) is defined by \(\tilde g_l(0) = 0\), \(\tilde g_l(1) = l\) and, for every \(n \ge 1\), \(\tilde g_l(n+1) = \tilde g_l(n) + \left(\frac{n}{p}\right)\left(\frac{\tilde g_l(n)}{p}\right)\) if \(0 < \tilde g_l(n) < p\), and \(\tilde g_l(n+1) = \tilde g_l(n)\) otherwise.

The sum in the first case is never negative, since \(\tilde g_l(n) \ge 1\) there. The paper only uses the indices \(1 \le n \le p\); the value at \(0\) and the values beyond \(p\) totalize the walk. For an odd prime \(p\) the Jacobi symbol is the Legendre symbol.

public def gobelResidueWalk (p l : ℕ) : ℕ → ℕ
  | 0 => 0
  | 1 => l
  | n + 2 =>
      let x := gobelResidueWalk p l (n + 1)
      if 0 < x ∧ x < p then
        Int.toNat ((x : ℤ) + jacobiSym (n + 1 : ℤ) p * jacobiSym (x : ℤ) p)
      else
        x

Sources

• Yuh Kobayashi and Shin-ichiro Seki, A Note on Non-Integrality of the (k, l)-Göbel Sequences, Journal of Integer Sequences 29 (2026), Article 26.3.8, Section 2 definition of tilde g_l.

Used by 11

Used byThe diagonal is zigzag-below every odd residue walk · The residue walk stays on the diagonal · Consecutive even residue walks form a zigzag chain when \(p \equiv 1 \pmod 4\) · Even residue walks lie zigzag-below the antidiagonal when \(p \equiv 3 \pmod 4\) · Initial value of the residue walk · Recurrence of the residue walk at interior values · The residue walk stays at \(p\) · The residue walk stays at \(0\) · Index-scaled Göbel terms with \(k = (p-1)/2\) are congruent to the residue walk · Left boundary of the even Göbel residue walks · Right boundary of the even Göbel residue walks

TheoremInitial value of the residue walk#✓fully proved

For all natural numbers \(p\) and \(l\), the residue walk \(\tilde g_l\) of \(p\) starting at \(l\) satisfies \(\tilde g_l(1) = l\).

public theorem gobelResidueWalk_one (p l : ℕ) : gobelResidueWalk p l 1 = l

Sources

• Yuh Kobayashi and Shin-ichiro Seki, A Note on Non-Integrality of the (k, l)-Göbel Sequences, Journal of Integer Sequences 29 (2026), Article 26.3.8, Section 2 definition of tilde g_l.

Uses 1

Statement usesThe residue walk \(\tilde g_l\)

TheoremRecurrence of the residue walk at interior values#✓fully proved

Let \(p\), \(l\) and \(n\) be natural numbers with \(n \ge 1\), write \(\tilde g_l\) for the residue walk of \(p\) starting at \(l\), and write \(\left(\frac{a}{p}\right)\) for the Jacobi symbol. If \(0 < \tilde g_l(n) < p\), then

\[\tilde g_l(n+1) = \max\bigl(0, \tilde g_l(n) + (\tfrac{n}{p})(\tfrac{\tilde g_l(n)}{p})\bigr).\]

The maximum with \(0\) records the conversion of the integer sum back to a natural number; the sum is never negative because \(\tilde g_l(n) \ge 1\).

public theorem gobelResidueWalk_succ_of_between (p l n : ℕ) (hn : 1 ≤ n)
    (hbetween : 0 < gobelResidueWalk p l n ∧ gobelResidueWalk p l n < p) :
    gobelResidueWalk p l (n + 1) =
      Int.toNat ((gobelResidueWalk p l n : ℤ) +
        jacobiSym (n : ℤ) p * jacobiSym (gobelResidueWalk p l n : ℤ) p)

Sources

• Yuh Kobayashi and Shin-ichiro Seki, A Note on Non-Integrality of the (k, l)-Göbel Sequences, Journal of Integer Sequences 29 (2026), Article 26.3.8, Section 2 definition of tilde g_l.

Uses 1

Statement usesThe residue walk \(\tilde g_l\)

TheoremThe residue walk stays at \(0\)#✓fully proved

Let \(p\), \(l\) and \(n\) be natural numbers with \(n \ge 1\), and write \(\tilde g_l\) for the residue walk of \(p\) starting at \(l\). If \(\tilde g_l(n) = 0\), then \(\tilde g_l(n+1) = 0\).

public theorem gobelResidueWalk_succ_of_eq_zero (p l n : ℕ) (hn : 1 ≤ n)
    (hzero : gobelResidueWalk p l n = 0) :
    gobelResidueWalk p l (n + 1) = 0

Sources

• Yuh Kobayashi and Shin-ichiro Seki, A Note on Non-Integrality of the (k, l)-Göbel Sequences, Journal of Integer Sequences 29 (2026), Article 26.3.8, Section 2 definition of tilde g_l.

Uses 1

Statement usesThe residue walk \(\tilde g_l\)

TheoremThe residue walk stays at \(p\)#✓fully proved

Let \(p\), \(l\) and \(n\) be natural numbers with \(n \ge 1\), and write \(\tilde g_l\) for the residue walk of \(p\) starting at \(l\). If \(\tilde g_l(n) = p\), then \(\tilde g_l(n+1) = p\).

public theorem gobelResidueWalk_succ_of_eq_prime (p l n : ℕ) (hn : 1 ≤ n)
    (hprime : gobelResidueWalk p l n = p) :
    gobelResidueWalk p l (n + 1) = p

Sources

• Yuh Kobayashi and Shin-ichiro Seki, A Note on Non-Integrality of the (k, l)-Göbel Sequences, Journal of Integer Sequences 29 (2026), Article 26.3.8, Section 2 definition of tilde g_l.

Uses 1

Statement usesThe residue walk \(\tilde g_l\)

DefinitionZigzag order on integer sequences#✓fully proved

For a natural number \(p\) and functions \(a, b : \mathbb{N} \to \mathbb{Z}\), \(a\) lies zigzag-below \(b\) up to \(p\), written \(a \preceq b\), when there is a natural number \(m \le p\) such that \(a(n) < b(n)\) for all \(1 \le n \le m\) and \(a(n) = b(n)\) for all \(m < n \le p\).

The paper's point sets are represented by their integer-valued coordinate functions; values outside \(1 \le n \le p\) play no role.

public def IsZigzagBelow (p : ℕ) (a b : ℕ → ℤ) : Prop :=
  ∃ m ≤ p,
    (∀ n, 1 ≤ n → n ≤ m → a n < b n) ∧
    (∀ n, m < n → n ≤ p → a n = b n)

Sources

• Yuh Kobayashi and Shin-ichiro Seki, A Note on Non-Integrality of the (k, l)- Göbel Sequences, Journal of Integer Sequences 29 (2026), Article 26.3.8, Section 2 definition of ⪯.

Used by 3

Used byThe diagonal is zigzag-below every odd residue walk · Consecutive even residue walks form a zigzag chain when \(p \equiv 1 \pmod 4\) · Even residue walks lie zigzag-below the antidiagonal when \(p \equiv 3 \pmod 4\)

DefinitionThe sign sequence \(a_{p,l}\)#✓fully proved

For natural numbers \(p\) and \(l\), a function \(a : \mathbb{N} \to \mathbb{Z}\) is an \(a_{p,l}\)-sequence when all of the following hold: \(a(n) \in \{1, -1\}\) for \(1 \le n \le p-1\); \(a(n) = 0\) for \(n = 0\) and for every \(n \ge p\); \(a(1) = 1\); \(a(n) = a(p-n)\) for \(1 \le n \le \lfloor (p-1)/2 \rfloor\); \(a(n) = -a(l+1-n)\) for \(1 \le n \le \lfloor l/2 \rfloor\); and \(a(n) = a(l+1+n)\) for \(1 \le n \le p-l-2\).

The values outside \(1 \le n \le p-1\) are fixed to \(0\) so that uniqueness of the paper's finite sequence becomes uniqueness of the function.

public def IsGobelASequence (p l : ℕ) (a : ℕ → ℤ) : Prop :=
  (∀ n, 1 ≤ n → n ≤ p - 1 → a n = 1 ∨ a n = -1) ∧
  (∀ n, n = 0 ∨ p ≤ n → a n = 0) ∧
  a 1 = 1 ∧
  (∀ n, 1 ≤ n → n ≤ (p - 1) / 2 → a n = a (p - n)) ∧
  (∀ n, 1 ≤ n → n ≤ l / 2 → a n = -a (l + 1 - n)) ∧
  (∀ n, 1 ≤ n → n ≤ p - l - 2 → a n = a (l + 1 + n))

Sources

• Yuh Kobayashi and Shin-ichiro Seki, A Note on Non-Integrality of the (k, l)-Göbel Sequences, Journal of Integer Sequences 29 (2026), Article 26.3.8, Proposition 17.

Used by 2

Used byExistence and uniqueness of the sequence \(a_{p,l}\) · The sequence \(a_{p,l}\) is not multiplicative at an even index

DefinitionThe periodic sign sequence \(b_{l,s}\)#✓fully proved

For natural numbers \(l\) and \(s\), a function \(b : \mathbb{Z} \to \mathbb{Z}\) is a \(b_{l,s}\)-sequence when all of the following hold: \(b(n) \in \{1, -1\}\) for every integer \(n\); \(b(n + l + 1) = b(n)\) for every integer \(n\); \(b(1) = 1\); \(b(n) = -b(l+1-n)\) for every integer \(n\) not divisible by \(l+1\); and \(b(s-n) = b(s+1+n)\) for every integer \(n\).

public def IsGobelBSequence (l s : ℕ) (b : ℤ → ℤ) : Prop :=
  (∀ n, b n = 1 ∨ b n = -1) ∧
  (∀ n, b (n + (l + 1 : ℤ)) = b n) ∧
  b 1 = 1 ∧
  (∀ n, Int.emod n (l + 1 : ℤ) ≠ 0 → b n = -b ((l + 1 : ℤ) - n)) ∧
  (∀ n, b ((s : ℤ) - n) = b ((s : ℤ) + 1 + n))

Sources

• Yuh Kobayashi and Shin-ichiro Seki, A Note on Non-Integrality of the (k, l)-Göbel Sequences, Journal of Integer Sequences 29 (2026), Article 26.3.8, Proposition 20.

Used by 3

Used byExistence and uniqueness of the sequence \(b_{l,s}\) · Complementary sequences \(b_{l,s}\) and \(b_{l,l-s}\) · Translation and reflection identities for \(b_{l,s}\)

DefinitionLeft boundary of the even Göbel residue walks#✓fully proved

Fix a natural number \(p\) and, for each natural number \(l\), let \(\tilde g_l\) denote the Göbel residue walk for \(p\) starting at \(l\). A natural number \(l_L\) is the left boundary for \(p\) when there is an even natural number \(l_0 < p\) with \(\tilde g_{l_0}(p) = 0\) and \(l_L = l_0 + 2\) such that every even natural number \(l < p\) with \(\tilde g_l(p) = 0\) satisfies \(l \le l_0\). In other words, the set of even \(l < p\) with \(\tilde g_l(p) = 0\) is nonempty and \(l_L\) is its maximum plus \(2\).

public def IsGobelLeftBoundary (p lL : ℕ) : Prop :=
  ∃ l0, Even l0 ∧ l0 < p ∧ gobelResidueWalk p l0 p = 0 ∧ lL = l0 + 2 ∧
    ∀ l, Even l → l < p → gobelResidueWalk p l p = 0 → l ≤ l0

Sources

• Yuh Kobayashi and Shin-ichiro Seki, A Note on Non-Integrality of the (k, l)-Göbel Sequences, Journal of Integer Sequences 29 (2026), Article 26.3.8, proof of Theorem 1.

Uses 1 · Used by 1

Statement usesThe residue walk \(\tilde g_l\)

Used byEquality of the left and right boundaries via Legendre symbols

DefinitionRight boundary of the even Göbel residue walks#✓fully proved

Fix a natural number \(p\) and, for each natural number \(l\), let \(\tilde g_l\) denote the Göbel residue walk for \(p\) starting at \(l\). A natural number \(l_R\) is the right boundary for \(p\) when \(l_R\) is even, \(l_R < p\), \(\tilde g_{l_R}(p) = p\), and every even natural number \(l < p\) with \(\tilde g_l(p) = p\) satisfies \(l_R \le l\). In other words, \(l_R\) is the least even \(l < p\) with \(\tilde g_l(p) = p\).

public def IsGobelRightBoundary (p lR : ℕ) : Prop :=
  Even lR ∧ lR < p ∧ gobelResidueWalk p lR p = p ∧
    ∀ l, Even l → l < p → gobelResidueWalk p l p = p → lR ≤ l

Sources

• Yuh Kobayashi and Shin-ichiro Seki, A Note on Non-Integrality of the (k, l)-Göbel Sequences, Journal of Integer Sequences 29 (2026), Article 26.3.8, proof of Theorem 1.

Uses 1 · Used by 1

Statement usesThe residue walk \(\tilde g_l\)

Used byEquality of the left and right boundaries via Legendre symbols

TheoremGöbel sequences at index \(p\) for primes \(p \equiv 3 \pmod 4\)#●ready to prove

Let \(g_{k,l}\) denote the \((k, l)\)-Göbel sequence and let \(p\) be a prime with \(p \equiv 3 \pmod 4\). Then for every natural number \(l < p\), the \(p\)-adic valuation of \(g_{(p-1)/2,\,l}(p)\) is nonnegative (the valuation of \(0\) is taken to be \(0\)); that is, \(g_{(p-1)/2,\,l}(p)\) lies in the localization \(\mathbb{Z}_{(p)}\).

public theorem_wanted gobelSequence_half_pred_mem_localization_of_three_mod_four
    (p : ℕ) (hp : p.Prime) (hmod : p % 4 = 3) :
    ∀ l, l < p → 0 ≤ padicValRat p (gobelSequence ((p - 1) / 2) l p)

Sources

• Yuh Kobayashi and Shin-ichiro Seki, A Note on Non-Integrality of the (k, l)-Göbel Sequences, Journal of Integer Sequences 29 (2026), Article 26.3.8, Theorem 1(a).

Uses 1

Statement usesThe (k, l)-Göbel sequence

TheoremOdd starting values give a \(p\)-integral \(p\)-th term when \(p \equiv 1 \pmod 4\)#●ready to prove

Let \(p\) be a prime with \(p \equiv 1 \pmod 4\), write \(k = (p-1)/2\), and let \(g_{k,l}\) denote the \((k,l)\)-Göbel sequence. Then for every odd natural number \(l < p\), the term \(g_{k,l}(p)\) lies in the localization \(\mathbb{Z}_{(p)}\), that is, its \(p\)-adic valuation is nonnegative.

public theorem_wanted gobelSequence_half_pred_mem_localization_of_one_mod_four_of_odd
    (p : ℕ) (hp : p.Prime) (hmod : p % 4 = 1) :
    ∀ l, Odd l → l < p → 0 ≤ padicValRat p (gobelSequence ((p - 1) / 2) l p)

Sources

• Yuh Kobayashi and Shin-ichiro Seki, A Note on Non-Integrality of the (k, l)- Göbel Sequences, Journal of Integer Sequences 29 (2026), Article 26.3.8, Theorem 1(b), odd case.

Uses 1

Statement usesThe (k, l)-Göbel sequence

TheoremUnique boundary pair for Göbel sequences when \(p \equiv 1 \pmod 4\)#●ready to prove

Let \(g_{k,l}\) denote the \((k, l)\)-Göbel sequence and let \(p \ge 13\) be a prime with \(p \equiv 1 \pmod 4\). Then there is exactly one pair \((l_L, l_R)\) of even natural numbers with \(2 \le l_L < l_R \le p-1\) such that, for every even natural number \(l < p\), the \(p\)-adic valuation of \(g_{(p-1)/2,\,l}(p)\) is nonnegative (the valuation of \(0\) is taken to be \(0\)) if and only if \(l < l_L\) or \(l_R \le l\).

Thus the even \(l < p\) split into the three intervals \(l < l_L\), \(l_L \le l < l_R\) and \(l_R \le l\), and \(g_{(p-1)/2,\,l}(p)\) lies in \(\mathbb{Z}_{(p)}\) exactly on the outer two.

public theorem_wanted gobelSequence_half_pred_unique_even_localization_decomposition
    (p : ℕ) (hp : p.Prime) (hmod : p % 4 = 1) (hp13 : 13 ≤ p) :
    ∃! bounds : ℕ × ℕ,
      Even bounds.1 ∧ Even bounds.2 ∧ 2 ≤ bounds.1 ∧ bounds.1 < bounds.2 ∧
      bounds.2 ≤ p - 1 ∧
      ∀ l, Even l → l < p →
        (0 ≤ padicValRat p (gobelSequence ((p - 1) / 2) l p) ↔
          l < bounds.1 ∨ bounds.2 ≤ l)

Sources

• Yuh Kobayashi and Shin-ichiro Seki, A Note on Non-Integrality of the (k, l)-Göbel Sequences, Journal of Integer Sequences 29 (2026), Article 26.3.8, Theorem 1(b), unique decomposition.

Uses 1

Statement usesThe (k, l)-Göbel sequence

TheoremA congruence class of non-integral Göbel sequences#●ready to prove

Let \(g_{k,l}\) denote the \((k, l)\)-Göbel sequence, let \(p \ge 13\) be a prime with \(p \equiv 1 \pmod 4\), and let \(k = \frac{p-1}{2} q\) for a positive odd natural number \(q\). Then there is an even natural number \(l\) with \(2 \le l \le p-3\) such that for every positive natural number \(l'\) with \(l' \equiv l \pmod p\), the \(p\)-adic valuation of \(g_{k,l'}(p)\) is negative, and some \(g_{k,l'}(n)\) with \(1 \le n \le p\) is not an integer.

Every such \(k\) is positive and even, as the paper requires.

public theorem_wanted gobelSequence_nonintegral_congruence_class_of_odd_multiple
    (k p : ℕ) (hp : p.Prime) (hp13 : 13 ≤ p)
    (hmod : p % 4 = 1)
    (hmultiple : ∃ q, 0 < q ∧ Odd q ∧ k = ((p - 1) / 2) * q) :
    ∃ l, Even l ∧ 2 ≤ l ∧ l ≤ p - 3 ∧
      ∀ l', 0 < l' → l' % p = l % p →
        padicValRat p (gobelSequence k l' p) < 0 ∧
        ∃ n, 1 ≤ n ∧ n ≤ p ∧ ¬∃ z : ℤ, gobelSequence k l' n = z

Sources

• Yuh Kobayashi and Shin-ichiro Seki, A Note on Non-Integrality of the (k, l)-Göbel Sequences, Journal of Integer Sequences 29 (2026), Article 26.3.8, Corollary 2.

Uses 1

Statement usesThe (k, l)-Göbel sequence

TheoremThe odd multiples of \((p-1)/2\) admit no finite subcover#●ready to prove

For a prime \(p\) write \(A_p = \{\tfrac{p-1}{2}(2m+1) : m \in \mathbb{N}\}\) for the set of odd multiples of \((p-1)/2\). For every finite set \(S\) of primes \(q\) with \(q \ge 13\) and \(q \equiv 1 \pmod 4\), there is a natural number \(k\) that lies in \(A_p\) for some prime \(p \ge 13\) with \(p \equiv 1 \pmod 4\) but lies in no \(A_q\) with \(q \in S\).

public theorem_wanted odd_multiple_prime_half_sets_not_finitely_coverable :
    ∀ S : Finset ℕ, (∀ p ∈ S, p.Prime ∧ 13 ≤ p ∧ p % 4 = 1) → ∃ k,
      (∃ p m, p.Prime ∧ 13 ≤ p ∧ p % 4 = 1 ∧
        k = ((p - 1) / 2) * (2 * m + 1)) ∧
      ∀ p ∈ S, ¬∃ m, k = ((p - 1) / 2) * (2 * m + 1)

Sources

• Yuh Kobayashi and Shin-ichiro Seki, A Note on Non-Integrality of the (k, l)- Göbel Sequences, Journal of Integer Sequences 29 (2026), Article 26.3.8, Lemma 3.

TheoremIndex-scaled Göbel terms with \(k = (p-1)/2\) are congruent to the residue walk#●ready to prove

Let \(p\) be an odd prime and \(l \le p - 1\) a natural number. Write \(k = (p-1)/2\), let \(g_{k,l}\) be the \((k,l)\)-Göbel sequence, and let \(\tilde g_l\) be the residue walk of \(p\) starting at \(l\). Then (a) for every \(1 \le n \le p\), the rational number \(n\,g_{k,l}(n) - \tilde g_l(n)\) is either \(0\) or has \(p\)-adic valuation at least \(1\), that is, \(n\,g_{k,l}(n) \equiv \tilde g_l(n) \pmod{p}\) in \(\mathbb{Z}_{(p)}\); and (b) \(g_{k,l}(p)\) lies in the localization \(\mathbb{Z}_{(p)}\), that is, has nonnegative \(p\)-adic valuation, if and only if \(\tilde g_l(p) = 0\) or \(\tilde g_l(p) = p\).

public theorem_wanted gobelSequence_half_pred_congruent_residue_walk
    (p l : ℕ) (hp : p.Prime) (hpodd : Odd p) (hl : l ≤ p - 1) :
    (∀ n, 1 ≤ n → n ≤ p →
      let d : ℚ := (n : ℚ) * gobelSequence ((p - 1) / 2) l n - gobelResidueWalk p l n
      d = 0 ∨ 1 ≤ padicValRat p d) ∧
    (0 ≤ padicValRat p (gobelSequence ((p - 1) / 2) l p) ↔
      gobelResidueWalk p l p = 0 ∨ gobelResidueWalk p l p = p)

Sources

• Yuh Kobayashi and Shin-ichiro Seki, A Note on Non-Integrality of the (k, l)-Göbel Sequences, Journal of Integer Sequences 29 (2026), Article 26.3.8, Lemma 6.

Uses 2

Statement usesThe residue walk \(\tilde g_l\) · The (k, l)-Göbel sequence

TheoremThe residue walk stays on the diagonal#●ready to prove

Let \(p\) be an odd prime, let \(l \le p - 1\) be a natural number, and let \(\tilde g_l\) be the residue walk of \(l\) for \(p\). If \(1 \le m \le p\) and \(\tilde g_l(m) = m\), then \(\tilde g_l(n) = n\) for every \(n\) with \(m \le n \le p\).

public theorem_wanted gobelResidueWalk_eq_index_of_eq_index
    (p l m : ℕ) (hp : p.Prime) (hpodd : Odd p) (hl : l ≤ p - 1)
    (hm1 : 1 ≤ m) (hmp : m ≤ p) (hmeq : gobelResidueWalk p l m = m) :
    ∀ n, m ≤ n → n ≤ p → gobelResidueWalk p l n = n

Sources

• Yuh Kobayashi and Shin-ichiro Seki, A Note on Non-Integrality of the (k, l)-Göbel Sequences, Journal of Integer Sequences 29 (2026), Article 26.3.8, Lemma 8.

Uses 1

Statement usesThe residue walk \(\tilde g_l\)

TheoremThe diagonal is zigzag-below every odd residue walk#●ready to prove

Let \(p\) be an odd prime, let \(l\) be an odd natural number with \(l < p\), and let \(\tilde g_l\) be the residue walk of \(l\) for \(p\). Then the diagonal \(n \mapsto n\) is zigzag-below \(\tilde g_l\) up to \(p\): there is \(m \le p\) such that \(n < \tilde g_l(n)\) for all \(1 \le n \le m\) and \(\tilde g_l(n) = n\) for all \(m < n \le p\).

public theorem_wanted diagonal_isZigzagBelow_gobelResidueWalk_of_odd
    (p l : ℕ) (hp : p.Prime) (hpodd : Odd p) (hlodd : Odd l) (hlp : l < p) :
    IsZigzagBelow p (fun n => (n : ℤ)) (fun n => gobelResidueWalk p l n)

Sources

• Yuh Kobayashi and Shin-ichiro Seki, A Note on Non-Integrality of the (k, l)-Göbel Sequences, Journal of Integer Sequences 29 (2026), Article 26.3.8, Proposition 9.

Uses 2

Statement usesZigzag order on integer sequences · The residue walk \(\tilde g_l\)

TheoremEven residue walks lie zigzag-below the antidiagonal when \(p \equiv 3 \pmod 4\)#●ready to prove

Let \(p\) be a prime with \(p \equiv 3 \pmod 4\), let \(l < p\) be an even natural number, and write \(\tilde g_l\) for the residue walk of \(p\) starting at \(l\). Then \(\tilde g_l\) is zigzag-below the function \(n \mapsto p - n\) up to \(p\): there is an \(m \le p\) such that \(\tilde g_l(n) < p - n\) for \(1 \le n \le m\) and \(\tilde g_l(n) = p - n\) for \(m < n \le p\).

public theorem_wanted gobelResidueWalk_isZigzagBelow_antidiagonal_of_three_mod_four
    (p l : ℕ) (hp : p.Prime) (hmod : p % 4 = 3)
    (hleven : Even l) (hlp : l < p) :
    IsZigzagBelow p (fun n => gobelResidueWalk p l n) (fun n => (p : ℤ) - n)

Sources

• Yuh Kobayashi and Shin-ichiro Seki, A Note on Non-Integrality of the (k, l)-Göbel Sequences, Journal of Integer Sequences 29 (2026), Article 26.3.8, Proposition 10.

Uses 2

Statement usesZigzag order on integer sequences · The residue walk \(\tilde g_l\)

TheoremConsecutive even residue walks form a zigzag chain when \(p \equiv 1 \pmod 4\)#●ready to prove

Let \(p\) be a prime with \(p \equiv 1 \pmod 4\), and for a natural number \(l\) write \(\tilde g_l\) for the residue walk of \(p\) starting at \(l\). Then for every even natural number \(l\) with \(l + 2 \le p - 1\), the walk \(\tilde g_l\) is zigzag-below \(\tilde g_{l+2}\) up to \(p\): there is an \(m \le p\) such that \(\tilde g_l(n) < \tilde g_{l+2}(n)\) for \(1 \le n \le m\) and \(\tilde g_l(n) = \tilde g_{l+2}(n)\) for \(m < n \le p\). Writing \(A \preceq B\) when \(A\) is zigzag-below \(B\) up to \(p\), these links form the chain \(\tilde g_0 \preceq \tilde g_2 \preceq \cdots \preceq \tilde g_{p-1}\).

public theorem_wanted gobelResidueWalk_even_chain_of_one_mod_four
    (p : ℕ) (hp : p.Prime) (hmod : p % 4 = 1) :
    ∀ l, Even l → l + 2 ≤ p - 1 →
      IsZigzagBelow p (fun n => gobelResidueWalk p l n)
        (fun n => gobelResidueWalk p (l + 2) n)

Sources

• Yuh Kobayashi and Shin-ichiro Seki, A Note on Non-Integrality of the (k, l)- Göbel Sequences, Journal of Integer Sequences 29 (2026), Article 26.3.8, Proposition 11.

Uses 2

Statement usesZigzag order on integer sequences · The residue walk \(\tilde g_l\)

TheoremEquality of the left and right boundaries via Legendre symbols#●ready to prove

Let \(p\) be a prime with \(p \equiv 1 \pmod 4\) and, for each \(l\), let \(\tilde g_l\) be the residue walk of \(l\) for \(p\). Suppose that \(l_0\) is the largest even \(l < p\) with \(\tilde g_l(p) = 0\), put \(l_L = l_0 + 2\), and suppose that \(l_R\) is the smallest even \(l < p\) with \(\tilde g_l(p) = p\). Then \(l_L = l_R\) if and only if there is an even natural number \(l \le p - 3\) such that \(\left(\frac{n}{p}\right) = -\left(\frac{l + 1 - n}{p}\right)\) for all \(1 \le n \le l/2\) and \(\left(\frac{n}{p}\right) = \left(\frac{l + 1 + n}{p}\right)\) for all \(1 \le n \le p - l - 2\), where \(\left(\frac{\cdot}{p}\right)\) is the Legendre symbol.

public theorem_wanted gobel_boundaries_eq_iff_jacobi_symmetries
    (p lL lR : ℕ) (hp : p.Prime) (hmod : p % 4 = 1)
    (hleft : IsGobelLeftBoundary p lL) (hright : IsGobelRightBoundary p lR) :
    lL = lR ↔
      ∃ l, Even l ∧ l ≤ p - 3 ∧
        (∀ n, 1 ≤ n → n ≤ l / 2 →
          jacobiSym (n : ℤ) p = -jacobiSym (l + 1 - n : ℤ) p) ∧
        (∀ n, 1 ≤ n → n ≤ p - l - 2 →
          jacobiSym (n : ℤ) p = jacobiSym (l + 1 + n : ℤ) p)

Sources

• Yuh Kobayashi and Shin-ichiro Seki, A Note on Non-Integrality of the (k, l)-Göbel Sequences, Journal of Integer Sequences 29 (2026), Article 26.3.8, Theorem 15.

Uses 2

Statement usesLeft boundary of the even Göbel residue walks · Right boundary of the even Göbel residue walks

TheoremArithmetic billiards in a tilted rectangle#●ready to prove

Let \(p\) be a prime with \(p \equiv 1 \pmod 4\) and let \(l\) be an even natural number with \(l + 3 \le p\). Put \(m = l + 1\) if \(2l + 5 \le p\) and \(m = p - (l + 1)\) otherwise, and let \(R \subseteq \mathbb{R}^2\) be the convex hull of the four points \((0, m)\), \((m, 0)\), \((p/2, p/2 - m)\) and \((p/2 - m, p/2)\). Let \(L\) be the set of integer points on the boundary of \(R\) other than \((0, m)\) and \((m, 0)\). Call a sequence \(P_0, P_1, \ldots\) of integer points a billiard path if \(P_0 = (0, m)\) and, for every \(i < p - 1\), the point \(P_{i+1}\) lies on the boundary of \(R\), differs from \(P_i\), and has the same second coordinate as \(P_i\) when \(i\) is even and the same first coordinate as \(P_i\) when \(i\) is odd. Then a billiard path exists, and every billiard path \(P\) maps \(\{1, \ldots, p - 2\}\) bijectively onto \(L\), satisfies \(P_{p-1} = (m, 0)\), and satisfies \(P_{p-1-i} = (y_i, x_i)\) for every \(i \le p - 1\), where \(P_i = (x_i, y_i)\).

MetaMathlibExt.arithmetic_billiards_rotated_rectangle · 15 lines

public theorem_wanted arithmetic_billiards_rotated_rectangle (p l : ℕ) (hp : p.Prime)
    (hp4 : p % 4 = 1) (hl : Even l) (hlp : l + 3 ≤ p) :
    let m : ℕ := if 2 * l + 5 ≤ p then l + 1 else p - (l + 1)
    let c : ℝ := if 2 * l + 5 ≤ p then (p : ℝ) / 2 - (l + 1) else (l + 1 : ℝ) - p / 2
    let R : Set (ℝ × ℝ) :=
      convexHull ℝ {((0 : ℝ), (m : ℝ)), ((m : ℝ), (0 : ℝ)), ((p : ℝ) / 2, c), (c, (p : ℝ) / 2)}
    let L : Set (ℤ × ℤ) :=
      {z | ((z.1 : ℝ), (z.2 : ℝ)) ∈ frontier R} \ {((0 : ℤ), (m : ℤ)), ((m : ℤ), (0 : ℤ))}
    let IsPath : (ℕ → ℤ × ℤ) → Prop := fun P =>
      P 0 = (0, (m : ℤ)) ∧ ∀ i < p - 1,
        (((P (i + 1)).1 : ℝ), ((P (i + 1)).2 : ℝ)) ∈ frontier R ∧ P (i + 1) ≠ P i ∧
          if Even i then (P (i + 1)).2 = (P i).2 else (P (i + 1)).1 = (P i).1
    (∃ P, IsPath P) ∧ ∀ P, IsPath P →
      Set.BijOn P (Set.Icc 1 (p - 2)) L ∧ P (p - 1) = ((m : ℤ), 0) ∧
        ∀ i ≤ p - 1, P (p - 1 - i) = (P i).swap

Sources

• Yuh Kobayashi and Shin-ichiro Seki, A Note on Non-Integrality of the (k, l)-Göbel Sequences, Journal of Integer Sequences 29 (2026), Article 26.3.8, Lemma 16 (lem:billiards).

TheoremExistence and uniqueness of the sequence \(a_{p,l}\)#●ready to prove

Let \(p\) be a prime with \(p \equiv 1 \pmod 4\) and let \(l\) be an even natural number with \(l \le p - 3\). Then exactly one function \(a : \mathbb{N} \to \mathbb{Z}\) satisfies the defining conditions of \(a_{p,l}\): \(a(n) = \pm 1\) for \(1 \le n \le p - 1\), \(a(n) = 0\) for \(n = 0\) and for \(n \ge p\), \(a(1) = 1\), \(a(n) = a(p - n)\) for \(1 \le n \le (p - 1)/2\), \(a(n) = -a(l + 1 - n)\) for \(1 \le n \le l/2\), and \(a(n) = a(l + 1 + n)\) for \(1 \le n \le p - l - 2\).

public theorem_wanted existsUnique_gobelASequence
    (p l : ℕ) (hp : p.Prime) (hmod : p % 4 = 1) (hleven : Even l) (hl : l ≤ p - 3) :
    ∃! a : ℕ → ℤ, IsGobelASequence p l a

Sources

• Yuh Kobayashi and Shin-ichiro Seki, A Note on Non-Integrality of the (k, l)-Göbel Sequences, Journal of Integer Sequences 29 (2026), Article 26.3.8, Proposition 17.

Uses 1

Statement usesThe sign sequence \(a_{p,l}\)

TheoremExistence and uniqueness of the sequence \(b_{l,s}\)#●ready to prove

Let \(l\) be an even natural number and \(s\) a natural number with \(s \le l\) such that \(2s + 1\) and \(l + 1\) are coprime. Then exactly one function \(b : \mathbb{Z} \to \mathbb{Z}\) satisfies the defining conditions of \(b_{l,s}\): \(b(n) = \pm 1\) for every integer \(n\), \(b(n + l + 1) = b(n)\) for every \(n\), \(b(1) = 1\), \(b(n) = -b(l + 1 - n)\) for every \(n\) not divisible by \(l + 1\), and \(b(s - n) = b(s + 1 + n)\) for every \(n\).

public theorem_wanted existsUnique_gobelBSequence
    (l s : ℕ) (hleven : Even l) (hs : s ≤ l) (hcoprime : Nat.Coprime (2 * s + 1) (l + 1)) :
    ∃! b : ℤ → ℤ, IsGobelBSequence l s b

Sources

• Yuh Kobayashi and Shin-ichiro Seki, A Note on Non-Integrality of the (k, l)-Göbel Sequences, Journal of Integer Sequences 29 (2026), Article 26.3.8, Proposition 20.

Uses 1

Statement usesThe periodic sign sequence \(b_{l,s}\)

TheoremComplementary sequences \(b_{l,s}\) and \(b_{l,l-s}\)#●ready to prove

Let \(l \ge 2\) be an even natural number and \(s \le l\) a natural number such that \(2s + 1\) and \(l + 1\) are coprime. Let \(b_1, b_2 : \mathbb{Z} \to \mathbb{Z}\) satisfy the defining conditions of \(b_{l,s}\) and of \(b_{l,l-s}\) respectively. Then for every integer \(n\), \(b_1(n) = b_2(n)\) if \(l + 1\) does not divide \(n\), and \(b_1(n) = -b_2(n)\) if \(l + 1\) divides \(n\).

public theorem_wanted gobelBSequence_complement
    (l s : ℕ) (hleven : Even l) (hs : s ≤ l) (hl2 : 2 ≤ l)
    (hcoprime : Nat.Coprime (2 * s + 1) (l + 1))
    (b₁ b₂ : ℤ → ℤ) (hb₁ : IsGobelBSequence l s b₁)
    (hb₂ : IsGobelBSequence l (l - s) b₂) :
    ∀ n, (Int.emod n (l + 1 : ℤ) ≠ 0 → b₁ n = b₂ n) ∧
      (Int.emod n (l + 1 : ℤ) = 0 → b₁ n = -b₂ n)

Sources

• Yuh Kobayashi and Shin-ichiro Seki, A Note on Non-Integrality of the (k, l)-Göbel Sequences, Journal of Integer Sequences 29 (2026), Article 26.3.8, Lemma 22.

Uses 1

Statement usesThe periodic sign sequence \(b_{l,s}\)

TheoremTranslation and reflection identities for \(b_{l,s}\)#●ready to prove

Let \(l \ge 2\) be an even natural number and \(s \le l\) a natural number such that \(2s + 1\) and \(l + 1\) are coprime, let \(b : \mathbb{Z} \to \mathbb{Z}\) satisfy the defining conditions of \(b_{l,s}\), and write \(t = l/2 - s\). Then the following hold. (a) For every integer \(n\) such that neither \(n\) nor \(n + 2s + 1\) is divisible by \(l + 1\), \(b(n) = -b(n + 2s + 1)\). (b) If \(s < l/2\), then for every integer \(n\) such that neither \(n\) nor \(n + 2t\) is divisible by \(l + 1\), \(b(n) = -b(n + 2t)\). (c) If \(s < l/2\), then for every integer \(n\) such that neither \(t - n\) nor \(t + n\) is divisible by \(l + 1\), \(b(t - n) = b(t + n)\).

MetaMathlibExt.gobelBSequence_translation_identities · 15 lines

public theorem_wanted gobelBSequence_translation_identities
    (l s : ℕ) (hleven : Even l) (hs : s ≤ l) (hl2 : 2 ≤ l)
    (hcoprime : Nat.Coprime (2 * s + 1) (l + 1))
    (b : ℤ → ℤ) (hb : IsGobelBSequence l s b) :
    (∀ n : ℤ, Int.emod n (l + 1 : ℤ) ≠ 0 →
      Int.emod (n + (2 * s + 1 : ℕ)) (l + 1 : ℤ) ≠ 0 →
      b n = -b (n + (2 * s + 1 : ℕ))) ∧
    (s < l / 2 →
      ∀ n : ℤ, Int.emod n (l + 1 : ℤ) ≠ 0 →
        Int.emod (n + (2 * (l / 2 - s) : ℕ)) (l + 1 : ℤ) ≠ 0 →
        b n = -b (n + (2 * (l / 2 - s) : ℕ))) ∧
    (s < l / 2 →
      ∀ n : ℤ, Int.emod (((l / 2 - s : ℕ) : ℤ) - n) (l + 1 : ℤ) ≠ 0 →
        Int.emod (((l / 2 - s : ℕ) : ℤ) + n) (l + 1 : ℤ) ≠ 0 →
        b (((l / 2 - s : ℕ) : ℤ) - n) = b (((l / 2 - s : ℕ) : ℤ) + n))

Sources

• Yuh Kobayashi and Shin-ichiro Seki, A Note on Non-Integrality of the (k, l)-Göbel Sequences, Journal of Integer Sequences 29 (2026), Article 26.3.8, Lemma 23.

Uses 1

Statement usesThe periodic sign sequence \(b_{l,s}\)

TheoremThe sequence \(a_{p,l}\) is not multiplicative at an even index#●ready to prove

Let \(p \ge 13\) be a prime with \(p \equiv 1 \pmod 4\), let \(l\) be an even natural number with \(2 \le l \le p - 3\), and let \(a : \mathbb{N} \to \mathbb{Z}\) satisfy the defining conditions of \(a_{p,l}\). Then there is a positive integer \(m\) with \(2m \le p - 3\) such that \(a(2m) \ne a(2)\,a(m)\).

public theorem_wanted gobelASequence_not_multiplicative_at_even_index
    (p l : ℕ) (hp : p.Prime) (hp13 : 13 ≤ p) (hmod : p % 4 = 1)
    (hleven : Even l) (hl2 : 2 ≤ l) (hlp : l ≤ p - 3)
    (a : ℕ → ℤ) (ha : IsGobelASequence p l a) :
    ∃ m, 0 < m ∧ 2 * m ≤ p - 3 ∧ a (2 * m) ≠ a 2 * a m

Sources

• Yuh Kobayashi and Shin-ichiro Seki, A Note on Non-Integrality of the (k, l)-Göbel Sequences, Journal of Integer Sequences 29 (2026), Article 26.3.8, Theorem 25.

Uses 1

Statement usesThe sign sequence \(a_{p,l}\)

TheoremThe first non-integral term of \(g_{2600725,2}\) is at index \(9011\)#●ready to prove

Let \(g_{k,l}\) denote the \((k,l)\)-Göbel sequence. The rational number \(g_{2600725,2}(9011)\) is not an integer, while \(g_{2600725,2}(n)\) is an integer for every natural number \(n\) with \(1 \le n < 9011\). Writing \(N_k\) for the first index at which \(g_{k,2}\) is not an integer, as in the paper, this says \(N_{2600725} = 9011\).

public theorem_wanted gobelSequence_first_nonintegral_2600725 :
    (¬∃ z : ℤ, gobelSequence 2600725 2 9011 = z) ∧
    ∀ n, 1 ≤ n → n < 9011 → ∃ z : ℤ, gobelSequence 2600725 2 n = z

Sources

• Yuh Kobayashi and Shin-ichiro Seki, A Note on Non-Integrality of the (k, l)-Göbel Sequences, Journal of Integer Sequences 29 (2026), Article 26.3.8, Theorem 26.

Uses 1

Statement usesThe (k, l)-Göbel sequence

TheoremA non-integral term of \(g_{k,2}\) by index \(9011\) for \(2 \le k \le 10^7\)#●ready to prove

Let \(g_{k,l}\) denote the \((k, l)\)-Göbel sequence. For every natural number \(k\) with \(2 \le k \le 10^7\), there is a natural number \(n\) with \(1 \le n \le 9011\) such that the rational number \(g_{k,2}(n)\) is not an integer.

Writing \(N_k\) for the first index at which \(g_{k,2}\) is not an integer, as in the paper, this says \(N_k \le 9011\) for \(2 \le k \le 10^7\); together with \(N_{2600725} = 9011\), this makes \(9011\) the largest of these thresholds. The paper also reports that each of these \(N_k\) was determined explicitly by computation; that claim is not part of this statement.

public theorem_wanted gobelSequence_nonintegral_index_le_9011
    (k : ℕ) (hk2 : 2 ≤ k) (hkmax : k ≤ 10 ^ 7) :
    ∃ n, 1 ≤ n ∧ n ≤ 9011 ∧ ¬∃ z : ℤ, gobelSequence k 2 n = z

Sources

• Yuh Kobayashi and Shin-ichiro Seki, A Note on Non-Integrality of the (k, l)-Göbel Sequences, Journal of Integer Sequences 29 (2026), Article 26.3.8, Theorem 26.

Uses 1

Statement usesThe (k, l)-Göbel sequence

TheoremCounting prime first nonintegral indices of \(g_{k,2}\) for \(k \le 10^7\)#●ready to prove

Exactly \(8649270\) natural numbers \(k\) with \(2 \le k \le 10^7\) have the following property: for the \((k, 2)\)-Göbel sequence \(g_{k,2}\) there is a prime \(q\) such that \(g_{k,2}(q)\) is not an integer and \(g_{k,2}(n)\) is an integer for every \(1 \le n < q\).

public theorem_wanted card_gobelSequence_prime_first_nonintegral_index :
    Nat.card {k : ℕ // 2 ≤ k ∧ k ≤ 10 ^ 7 ∧
      ∃ q, q.Prime ∧ (¬∃ z : ℤ, gobelSequence k 2 q = z) ∧
        ∀ n, 1 ≤ n → n < q → ∃ z : ℤ, gobelSequence k 2 n = z} = 8649270

Sources

• Yuh Kobayashi and Shin-ichiro Seki, A Note on Non-Integrality of the (k, l)- Göbel Sequences, Journal of Integer Sequences 29 (2026), Article 26.3.8, Theorem 26.

Uses 1

Statement usesThe (k, l)-Göbel sequence

TheoremA non-integral term of \(g_{k,2}\) by index \(29363\) for \(2 \le k \le 10^{14}\)#●ready to prove

Let \(g_{k,l}\) denote the \((k, l)\)-Göbel sequence. For every natural number \(k\) with \(2 \le k \le 10^{14}\), there is a natural number \(n\) with \(1 \le n \le 29363\) such that the rational number \(g_{k,2}(n)\) is not an integer.

Writing \(N_k\) for the first index at which \(g_{k,2}\) is not an integer, as in the paper, this says \(N_k \le 29363\).

public theorem_wanted gobelSequence_nonintegral_index_le_29363
    (k : ℕ) (hk2 : 2 ≤ k) (hkmax : k ≤ 10 ^ 14) :
    ∃ n, 1 ≤ n ∧ n ≤ 29363 ∧ ¬∃ z : ℤ, gobelSequence k 2 n = z

Sources

• Yuh Kobayashi and Shin-ichiro Seki, A Note on Non-Integrality of the (k, l)-Göbel Sequences, Journal of Integer Sequences 29 (2026), Article 26.3.8, Theorem 29.

Uses 1

Statement usesThe (k, l)-Göbel sequence

DefinitionResidue sequence of the \(k\)-Göbel sequence#✓fully proved

Fix natural numbers \(k\), \(p\), \(r\) and write \(\nu_p\) for the \(p\)-adic valuation. The residue sequence \(g_{k,p,r}(n)\), meant for \(n \ge 1\) with \(\nu_p(n!) \le r\), takes values in \(\mathbb{Z}/p^{r - \nu_p(n!)}\mathbb{Z} \cup \{F\}\), where \(F\) is a failure value; a residue class is represented by its least nonnegative representative. It is defined by \(g_{k,p,r}(0) = F\), \(g_{k,p,r}(1) = 2 \bmod p^r\) and, for \(n \ge 2\), as follows. If \(g_{k,p,r}(n-1) = F\) then \(g_{k,p,r}(n) = F\). Otherwise let \(g_{k,p,r}(n-1) = a\) and let \(N\) be the least nonnegative residue of \((n-1)a + a^k\) modulo \(p^{r - \nu_p((n-1)!)}\), with \(a^k\) computed by modular exponentiation. If \(N \not\equiv 0 \pmod{p^{\nu_p(n)}}\) then \(g_{k,p,r}(n) = F\); otherwise \(g_{k,p,r}(n) = (N/p^{\nu_p(n)}) \cdot c \bmod p^{r - \nu_p(n!)}\), where \(c\) is the inverse of the quotient \(n/p^{\nu_p(n)}\) modulo \(p^{r - \nu_p(n!)}\) (it exists when \(p\) is prime; when no inverse exists, \(c\) is the junk value that Mathlib's inverse in \(\mathbb{Z}/p^{r - \nu_p(n!)}\mathbb{Z}\) returns, which need not be \(0\)).

For a prime \(p\) with \(\nu_p(n!) \le r\) we have \(\nu_p(n) + (r - \nu_p(n!)) = r - \nu_p((n-1)!)\), so the reduction keeps exactly the information both the divisibility test and the next residue need, and the recursion agrees with the source's, which tests and divides \((n-1)a + a^k\) itself. Values with \(\nu_p(n!) > r\) and at \(n = 0\) are junk and never used.

MetaMathlibExt.gobelResidue · 15 lines

public def gobelResidue (k p r : ℕ) : ℕ → Option ℕ
  | 0 => none
  | 1 => some (2 % p ^ r)
  | n + 2 =>
    match gobelResidue k p r (n + 1) with
    | none => none
    | some a =>
      let N := (((n + 1 : ℕ) : ZMod (p ^ (r - padicValNat p (n + 1).factorial))) * a +
        (a : ZMod (p ^ (r - padicValNat p (n + 1).factorial))) ^ k).val
      if N % p ^ padicValNat p (n + 2) ≠ 0 then none
      else
        some ((N / p ^ padicValNat p (n + 2) *
          (((n + 2) / p ^ padicValNat p (n + 2) :
            ZMod (p ^ (r - padicValNat p (n + 2).factorial)))⁻¹).val) %
            p ^ (r - padicValNat p (n + 2).factorial))

Sources

• Yuh Kobayashi and Shin-ichiro Seki, On the Length over Which k-Göbel Sequences Remain Integers, INTEGERS 26 (2026), Article A23, Section 2 (definition of g_{k,p,r}, after Matsuhira, Matsusaka, and Tsuchida, Definition 9).

Used by 5

Used byFailure of the residue sequence detects non-integrality · Periodicity of the Göbel residue sequence in the exponent · Initial value of the Göbel residue sequence · Failure of the Göbel residue sequence persists · Example value of the Göbel residue sequence

TheoremInitial value of the Göbel residue sequence#✓fully proved

For all natural numbers \(k\), \(p\), \(r\), the residue sequence satisfies \(g_{k,p,r}(1) = 2 \bmod p^r\), the residue class of \(2\) modulo \(p^r\) (represented by the remainder of \(2\) on division by \(p^r\)).

public theorem gobelResidue_one (k p r : ℕ) : gobelResidue k p r 1 = some (2 % p ^ r)

Sources

• Yuh Kobayashi and Shin-ichiro Seki, On the Length over Which k-Göbel Sequences Remain Integers, INTEGERS 26 (2026), Article A23, Section 2 (definition of g_{k,p,r}).

Uses 1

Statement usesResidue sequence of the \(k\)-Göbel sequence

TheoremFailure of the Göbel residue sequence persists#✓fully proved

For all natural numbers \(k\), \(p\), \(r\) and every \(n \ge 1\), if the residue sequence takes the failure value at \(n\), that is \(g_{k,p,r}(n) = F\), then \(g_{k,p,r}(n + 1) = F\).

public theorem gobelResidue_succ_of_eq_none (k p r n : ℕ) (hn : 1 ≤ n)
    (h : gobelResidue k p r n = none) : gobelResidue k p r (n + 1) = none

Sources

• Yuh Kobayashi and Shin-ichiro Seki, On the Length over Which k-Göbel Sequences Remain Integers, INTEGERS 26 (2026), Article A23, Section 2 (definition of g_{k,p,r}).

Uses 1

Statement usesResidue sequence of the \(k\)-Göbel sequence

TheoremExample value of the Göbel residue sequence#✓fully proved

For \(k = 2\), \(p = 3\) and \(r = 1\), the residue sequence satisfies \(g_{2,3,1}(2) = 0 \bmod 3\); in particular it is not the failure value \(F\). Indeed \(g_{2,3,1}(1) = 2\) and \((1 \cdot 2 + 2^2) \cdot 2^{-1} = 6 \cdot 2^{-1} \equiv 0 \pmod 3\).

public theorem gobelResidue_two_three_one_two : gobelResidue 2 3 1 2 = some 0

Sources

• Yuh Kobayashi and Shin-ichiro Seki, On the Length over Which k-Göbel Sequences Remain Integers, INTEGERS 26 (2026), Article A23, Section 2 (definition of g_{k,p,r}).

Uses 1

Statement usesResidue sequence of the \(k\)-Göbel sequence

TheoremFailure of the residue sequence detects non-integrality#●ready to prove

Let \(k \ge 2\) and \(r \ge 1\) be integers, let \(p\) be a prime, write \(\nu_p\) for the \(p\)-adic valuation, and let \(n \ge 1\) be an integer with \(\nu_p(n!) \le r\). Then the residue sequence \(g_{k,p,r}\) takes the failure value \(F\) at \(n\), that is \(g_{k,p,r}(n) = F\), if and only if the value \(g_{k,2}(n)\) of the \((k, 2)\)-Göbel sequence has negative \(p\)-adic valuation, that is \(g_{k,2}(n) \notin \mathbb{Z}_{(p)}\).

This is Lemma 10 of Matsuhira, Matsusaka, and Tsuchida.

public theorem_wanted gobelResidue_eq_none_iff (k p r n : ℕ) (hk : 2 ≤ k) (hr : 1 ≤ r)
    (hp : p.Prime) (hn : 1 ≤ n) (hnr : padicValNat p n.factorial ≤ r) :
    gobelResidue k p r n = none ↔ padicValRat p (gobelSequence k 2 n) < 0

Sources

• Yuh Kobayashi and Shin-ichiro Seki, On the Length over Which k-Göbel Sequences Remain Integers, INTEGERS 26 (2026), Article A23, Lemma 2.

Uses 2

Statement usesResidue sequence of the \(k\)-Göbel sequence · The (k, l)-Göbel sequence

TheoremPeriodicity of the Göbel residue sequence in the exponent#●ready to prove

Let \(p\) be a prime, \(r \ge 1\), and \(k\), \(l\) integers with \(r + 1 \le k \le l\) and \(k \equiv l \pmod{\varphi(p^r)}\), where \(\varphi\) is Euler's totient function. Write \(\nu_p\) for the \(p\)-adic valuation. Then every integer \(n \ge 1\) with \(\nu_p(n!) \le r\) satisfies \(g_{k,p,r}(n) = g_{l,p,r}(n)\), where both sides are values of the residue sequence (so either both are the failure value \(F\) or both are the same residue class).

This is Proposition 12 of Matsuhira, Matsusaka, and Tsuchida.

public theorem_wanted gobelResidue_eq_of_modEq_totient (p r k l n : ℕ) (hp : p.Prime)
    (hr : 1 ≤ r) (hk : r + 1 ≤ k) (hkl : k ≤ l) (hmod : k ≡ l [MOD (p ^ r).totient])
    (hn : 1 ≤ n) (hnr : padicValNat p n.factorial ≤ r) :
    gobelResidue k p r n = gobelResidue l p r n

Sources

• Yuh Kobayashi and Shin-ichiro Seki, On the Length over Which k-Göbel Sequences Remain Integers, INTEGERS 26 (2026), Article A23, Lemma 3.

Uses 1

Statement usesResidue sequence of the \(k\)-Göbel sequence

20 fully proved36 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.