Fractal sequences

StructureRegular fractal sequence#✓fully proved

A regular fractal sequence is a sequence \((x_n)_{n \ge 0}\) of positive integers together with a position array \((p_i(j))_{i, j \ge 0}\) of natural numbers such that: for every \(i \ge 0\), the strictly increasing sequence \(p_i(0) < p_i(1) < \cdots\) lists exactly the positions \(n\) with \(x_n = i + 1\) (so every positive integer occurs infinitely often); for all \(i\) and \(n\) with \(x_n = i + 2\), some \(m < n\) has \(x_m = i + 1\); for all \(h\), \(i\) and \(j\) with \(h < i\), exactly one \(k\) satisfies \(p_i(j) < p_h(k) < p_i(j + 1)\); and for every \(j\), \(p_i(j)\) is strictly increasing in \(i\).

Source JIS VOL25/Kimberling, https://cs.uwaterloo.ca/journals/JIS/VOL25/Kimberling/kimber16.tex, lines 103–219.

Source positive value i + 1 is represented directly as the natural i + 1, and pos i j is the zero-based position of its j-th occurrence.

MetaMathlibExt.FractalSequence · 19 lines

public structure FractalSequence where
  /-- The positive-valued sequence. -/
  seq : ℕ → ℕ
  seq_pos : ∀ n, 0 < seq n
  /-- `pos i j` is the zero-based index of the `j`-th occurrence of value `i + 1`. -/
  pos : ℕ → ℕ → ℕ
  /-- Occurrence positions for a fixed value increase strictly. -/
  pos_strict : ∀ i, StrictMono (pos i)
  /-- Every recorded occurrence position contains the corresponding value. -/
  pos_sound : ∀ i j, seq (pos i j) = i + 1
  /-- Every occurrence of a value appears in its position row. -/
  pos_complete : ∀ i n, seq n = i + 1 → ∃ j, pos i j = n
  /-- Source condition (F2), shifted to zero-based value indices. -/
  cond_F2 : ∀ n i, seq n = i + 2 → ∃ m, m < n ∧ seq m = i + 1
  /-- Source condition (F3): exactly one smaller-value position lies strictly
  between consecutive positions of a larger value. -/
  cond_F3 : ∀ h i j, h < i → ∃! k, pos i j < pos h k ∧ pos h k < pos i (j + 1)
  /-- Regularity: every column of the position array increases strictly. -/
  pos_column_strict : ∀ j, StrictMono (fun i => pos i j)

Used by 2

Used byEvery value occurs infinitely often in a regular fractal sequence · Occurrence positions are distinct

TheoremOccurrence positions are distinct#✓fully proved

In a regular fractal sequence with position array \(p\), for every \(i \ge 0\) the map \(j \mapsto p_i(j)\), sending \(j\) to the position of the \(j\)-th occurrence of \(i + 1\) (counting from \(j = 0\)), is injective.

public theorem FractalSequence.pos_injective (X : FractalSequence) (i : ℕ) :
    Function.Injective (X.pos i)

Uses 1

Statement usesRegular fractal sequence

TheoremEvery value occurs infinitely often in a regular fractal sequence#✓fully proved

Let \((x_n)_{n \ge 0}\) be a regular fractal sequence. Then for every positive integer \(k\) there are infinitely many \(n\) with \(x_n = k\).

public theorem FractalSequence.infinite_occurrences (X : FractalSequence) (i : ℕ) :
    Set.Infinite {n | X.seq n = i + 1}

Uses 1

Statement usesRegular fractal sequence

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.