Connell sequence

DefinitionRow lengths of the Connell triangle#✓fully proved

For natural numbers \(r\) and \(j\), the length of row \(j\) is \(1 + r(j - 1)\), where \(j - 1\) is read as \(0\) when \(j = 0\). For \(j \ge 1\) this is the number of entries in row \(j\) of the Connell \((m, r)\) triangle for every \(m\); the source numbers rows from one, and the value at \(j = 0\) is a convention.

def connellRowLength (r j : ℕ) : ℕ :=
  1 + r * (j - 1)

Used by 3

Used byNext position in the Connell triangle · Rows of the Connell triangle · First entries of the rows of the Connell triangle

DefinitionFirst entries of the rows of the Connell triangle#✓fully proved

For natural numbers \(m\) and \(r\), the numbers \(s_j\) are defined by \(s_0 = s_1 = 1\) and \(s_{j+1} = s_j + m(\ell_j - 1) + 1\) for \(j \ge 1\), where \(\ell_j = 1 + r(j - 1)\) is the length of row \(j\). For \(j \ge 1\), \(s_j\) is the first entry of row \(j\) of the Connell \((m, r)\) triangle: each row starts one above the last entry \(s_j + m(\ell_j - 1)\) of the row before. The source numbers rows from one, and the value \(s_0 = 1\) is a convention.

def connellRowStart (m r : ℕ) : ℕ → ℕ
  | 0 => 1
  | 1 => 1
  | j + 2 =>
      connellRowStart m r (j + 1) + m * (connellRowLength r (j + 1) - 1) + 1

Uses 1 · Used by 1

Statement usesRow lengths of the Connell triangle

Used byEntries of the Connell triangle

DefinitionEntries of the Connell triangle#✓fully proved

For natural numbers \(m\), \(r\), \(j\) and \(k\), the entry with zero-based index \(k\) in row \(j\) of the Connell \((m, r)\) triangle is \(s_j + mk\), where \(s_j\) is the first entry of row \(j\). The formula is used for every \(k\), also at or beyond the row length.

def connellEntry (m r j k : ℕ) : ℕ :=
  connellRowStart m r j + m * k

Uses 1 · Used by 2

Statement usesFirst entries of the rows of the Connell triangle

Used byRows of the Connell triangle · Connell sequence

DefinitionRows of the Connell triangle#✓fully proved

For natural numbers \(m\), \(r\) and \(j\), row \(j\) of the Connell \((m, r)\) triangle is the finite set of the numbers \(s_j + mk\) with \(0 \le k < \ell_j\), where \(s_j\) is the first entry of row \(j\) and \(\ell_j = 1 + r(j - 1)\) is its length, with \(j - 1\) read as \(0\) when \(j = 0\).

def connellRowEntries (m r j : ℕ) : Finset ℕ :=
  (Finset.range (connellRowLength r j)).image (connellEntry m r j)

Uses 2

Statement usesEntries of the Connell triangle · Row lengths of the Connell triangle

StructureConnell parameters#✓fully proved

A pair of natural numbers \((m, r)\) with \(m \ge 2\) and \(r \ge 1\); these are the admissible parameters of a Connell \((m, r)\) sequence.

structure ConnellParameters where
  m : ℕ
  r : ℕ
  two_le_m : 2 ≤ m
  pos_r : 0 < r

Used by 1

Used byConnell sequence

DefinitionNext position in the Connell triangle#✓fully proved

For a natural number \(r\), the position following row \(j\), zero-based column \(k\), is row \(j\), column \(k + 1\) if \(k + 1 < 1 + r(j - 1)\) (the length of row \(j\), with \(j - 1\) read as \(0\) when \(j = 0\)), and row \(j + 1\), column \(0\) otherwise.

def connellNext (r : ℕ) (p : ℕ × ℕ) : ℕ × ℕ :=
  if p.2 + 1 < connellRowLength r p.1 then (p.1, p.2 + 1) else (p.1 + 1, 0)

Uses 1 · Used by 1

Statement usesRow lengths of the Connell triangle

Used byPosition of a term in the Connell triangle

DefinitionPosition of a term in the Connell triangle#✓fully proved

For a natural number \(r\), the position \(p_n = (j_n, k_n)\) (row \(j_n\), zero-based column \(k_n\)) of index \(n \ge 0\) is defined by \(p_0 = (1, 0)\) and \(p_{n+1} = (j_n, k_n + 1)\) if \(k_n + 1 < 1 + r(j_n - 1)\) (the length of row \(j_n\), with \(j_n - 1\) read as \(0\) when \(j_n = 0\)), and \(p_{n+1} = (j_n + 1, 0)\) otherwise.

def connellPosition (r : ℕ) : ℕ → ℕ × ℕ
  | 0 => (1, 0)
  | n + 1 => connellNext r (connellPosition r n)

Uses 1 · Used by 1

Statement usesNext position in the Connell triangle

Used byConnell sequence

DefinitionConnell sequence#✓fully proved

For natural numbers \(m \ge 2\) and \(r \ge 1\), the Connell \((m, r)\) sequence \((a_n)_{n \ge 0}\) reads the Connell triangle row by row: row \(j \ge 1\) has \(\ell_j = 1 + r(j - 1)\) entries \(s_j, s_j + m, \dots, s_j + m(\ell_j - 1)\), where \(s_1 = 1\) and \(s_{j+1} = s_j + m(\ell_j - 1) + 1\). Thus \(a_n = s_j + mk\), where row \(j\), zero-based column \(k\) is the position reached from row \(1\), column \(0\) after \(n\) steps, each step moving one column right within a row and from the last entry of a row to the first entry of the next.

def connellSequence (p : ConnellParameters) (n : ℕ) : ℕ :=
  let pos := connellPosition p.r n
  connellEntry p.m p.r pos.1 pos.2

Uses 3

Statement usesConnell parameters · Entries of the Connell triangle · Position of a term in the Connell triangle

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.