Conway–Hofstadter sequences

DefinitionOne-based residue#✓fully proved

For natural numbers \(a\) and \(m\), the one-based residue of \(a\) modulo \(m\) is \(a \bmod m\) if this is nonzero, and \(m\) if \(a \bmod m = 0\) (here \(a \bmod 0 = a\)). This is the residue convention used in Pelesko's recurrence.

def conwayHofstadterResidue (a m : ℕ) : ℕ :=
  if a % m = 0 then m else a % m

Used by 1

Used byConway–Hofstadter-like sequence

DefinitionConway–Hofstadter-like sequence#✓fully proved

Let \(k\) be a natural number. A sequence \(c : \mathbb{N} \to \mathbb{N}\) is a Conway–Hofstadter-like sequence of order \(k\) when \(c(1) = c(2) = 1\) and, for every \(n \ge 3\),

\[c(n) = c(i_n) + c(n - i_n),\]

where \(i_n\) is the one-based residue of \(k \, c(n-1)\) modulo \(n - 1\): it equals \(k \, c(n-1) \bmod (n-1)\) when this is nonzero, and \(n - 1\) otherwise.

The value \(c(0)\) is not constrained.

def IsConwayHofstadterLikeSequence (k : ℕ) (c : ℕ → ℕ) : Prop :=
  c 1 = 1 ∧ c 2 = 1 ∧ ∀ n : ℕ, 3 ≤ n →
    let i := conwayHofstadterResidue (k * c (n - 1)) (n - 1)
    c n = c i + c (n - i)

Uses 1

Statement usesOne-based residue

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.