Iterated maps and self-referential sequences

Collatz problem, EKG, Stern diatomic, Hofstadter, Golomb, Ulam, Ducci, Josephus and Conway-type sequences.

TheoremClosed form for Golomb-like sequences#✓fully proved

Let \(y\) and \(z\) be integers of opposite parity with \(y \ge 2\) and \(z \ge 2 - y\), and put \(c = (y + z - 1)/2\). There is exactly one strictly increasing function \(f\) from the positive integers to the positive integers such that \(f(1) = (y + z + 1)/2\) and \(f(f(n)) = yn + z\) for every positive integer \(n\). Moreover, for every such \(f\), every natural number \(k\) and every integer \(j\) with \(-c\,y^k \le j < c\,y^k\), the rational number

\[m = \frac{(y+1)\,c}{y-1}\, y^k - \frac{z}{y-1} + j\]

is a positive integer and

\[f(m) = \frac{2c}{y-1}\, y^{k+1} - \frac{z}{y-1} + \frac{(y+1)\,j}{2} + \frac{(y-1)\,|j|}{2}.\]

Proof: The construction tiles the positive integers by the source's blocks and verifies the two slope regimes, followed by strong-induction uniqueness, as in Cloitre–Sloane–Vandermast, Theorem Th1 and equations (Eq48a), (Eq48).

MetaMathlibExt.golomb_like_closed_form · 30 lines 
public theorem golomb_like_closed_form
    (y z : ℤ)
    (hy : 2 ≤ y)
    (hz : 2 - y ≤ z)
    (hpar : y % 2 ≠ z % 2) :
    (∃! f : ℕ+ → ℕ+,
      StrictMono f ∧
      (↑((f 1).val) : ℚ) = ((y : ℚ) + (z : ℚ) + 1) / 2 ∧
      ∀ n : ℕ+,
        (↑((f (f n)).val) : ℤ) = y * (↑n.val : ℤ) + z) ∧
    ∀ f : ℕ+ → ℕ+,
      StrictMono f →
      (↑((f 1).val) : ℚ) = ((y : ℚ) + (z : ℚ) + 1) / 2 →
      (∀ n : ℕ+,
        (↑((f (f n)).val) : ℤ) = y * (↑n.val : ℤ) + z) →
      ∀ k : ℕ, ∀ j : ℤ,
        -(((y : ℚ) + (z : ℚ) - 1) / 2) * (y : ℚ) ^ k ≤ (j : ℚ) →
        (j : ℚ) < (((y : ℚ) + (z : ℚ) - 1) / 2) * (y : ℚ) ^ k →
        ∃ m : ℕ+,
          (↑m.val : ℚ) =
              (((y : ℚ) + 1) * ((y : ℚ) + (z : ℚ) - 1) /
                (2 * ((y : ℚ) - 1))) *
                (y : ℚ) ^ k -
              (z : ℚ) / ((y : ℚ) - 1) + (j : ℚ) ∧
          (↑((f m).val) : ℚ) =
              (((y : ℚ) + (z : ℚ) - 1) / ((y : ℚ) - 1)) *
                (y : ℚ) ^ (k + 1) -
              (z : ℚ) / ((y : ℚ) - 1) +
              ((y : ℚ) + 1) * (j : ℚ) / 2 +
              ((y : ℚ) - 1) * |(j : ℚ)| / 2
Sources
  • Benoit Cloitre, N. J. A. Sloane, and Matthew J. Vandermast, "Numerical Analogues of Aronson's Sequence," Journal of Integer Sequences 6 (2003), Article 03.2.2, Theorem, equations, lines 584–603, https://cs.uwaterloo.ca/journals/JIS/VOL6/Cloitre/cloitre2.tex

TheoremHinman–Kuca–Schlesinger–Sheydvasser weak rigidity theorem for Ulam sequences#●ready to prove

There exist sequences of integers \((a_k)\), \((b_k)\), \((c_k)\), \((d_k)\) indexed by \(k \in \mathbb{N}\) with the following property. For every real \(C > 0\) there is a natural number \(N > 0\) such that for every natural number \(n \ge N\) with \(n > 1\), and every sequence of natural numbers \(u_0, u_1, u_2, \dots\) with \(u_0 = 1\) and \(u_1 = n\) that is strictly increasing and in which, for every \(t \ge 2\), \(u_t\) is the least natural number \(m > u_{t-1}\) for which there is exactly one pair of indices \((i, j)\) with \(i < j < t\) and \(u_i + u_j = m\), the following holds: for every natural number \(x\) with \(1 \le x \le Cn\), \(x\) is a term of the sequence \(u\) if and only if \(a_k n + b_k \le x \le c_k n + d_k\) for some \(k \in \mathbb{N}\).

Source identifiers (stable): - canonical_name: Hinman-Kuca-Schlesinger-Sheydvasser weak rigidity theorem for Ulam sequences - concept_id: jis_dep_b6bd02b67460015658284d14 - grounded_candidate_id: jis_grounded_4a3f4c32b68e2308906fe08d - source_url: https://cs.uwaterloo.ca/journals/JIS/VOL24/Sheydvasser/sheyd3.tex - source lines: 150-155 - source_sha256: ee0e4d944870bbfc4ebf49a21dc3a129f9857c6c19b0fffc73a7c923d4baed68 - source_text_sha256: 03e5dd3a6e1e0d117dd2ca2e2724758fc7ee26ac232c48855b404c8ff267e4fe - label: Weak Rigidity Theorem; cite: Theorem 1.1 of HKSS_2019_1 - corrected mentions/papers/proof-uses: 6/1/1

theorem_wanted hinman_kuca_schlesinger_sheydvasser_weak_rigidity : ∃ a b c d : ℕ → ℤ, ∀ C : ℝ, 0 <
  C → ∃ N : ℕ, 0 < N ∧ ∀ n : ℕ, N ≤ n → 1 < n → ∀ u : ℕ → ℕ, u 0 = 1 → u 1 = n → StrictMono u →
  (∀ t : ℕ, 2 ≤ t → IsLeast
  {m : ℕ | u (t - 1) < m ∧ ∃! ij : Fin t × Fin t, (ij.1 : ℕ) < (ij.2 : ℕ) ∧ u ij.1 + u ij.2 = m}
  (u t)) → ∀ x : ℕ, 1 ≤ x → (x : ℝ) ≤ C * n →
  (x ∈ Set.range u ↔ ∃ i : ℕ, a i * (n : ℤ) + b i ≤ (x : ℤ) ∧ (x : ℤ) ≤ c i * (n : ℤ) + d i)
Sources
  • Weak Rigidity Theorem, Theorem 1.1 of HKSS_2019_1, as stated in Sheydvasser, JIS VOL24, lines 150-155.

DefinitionThe EKG sequence#✓fully proved

A sequence \(a_0, a_1, a_2, \dots\) of natural numbers is an EKG sequence when \(a_0 = 1\), \(a_1 = 2\), and for every \(n \ge 0\) the term \(a_{n+2}\) is positive, differs from each of \(a_0, \dots, a_{n+1}\), satisfies \(\gcd(a_{n+1}, a_{n+2}) > 1\), and satisfies \(a_{n+2} \le m\) for every positive integer \(m\) that differs from each of \(a_0, \dots, a_{n+1}\) and has \(\gcd(a_{n+1}, m) > 1\). Thus every term from \(a_2\) on is the least positive integer not used before that shares a factor greater than \(1\) with the previous term.

The indexing starts at \(0\), so the source's \(a_1 = 1\) and \(a_2 = 2\) are \(a_0\) and \(a_1\) here. The sequence begins \(1, 2, 4, 6, 3, 9, 12, 8, 10, 5, \dots\)

public def IsEKGSequence (a : ℕ → ℕ) : Prop :=
  a 0 = 1 ∧
    a 1 = 2 ∧
      ∀ n : ℕ,
        0 < a (n + 2) ∧
          (∀ i : ℕ, i < n + 2 → a i ≠ a (n + 2)) ∧
            Nat.gcd (a (n + 1)) (a (n + 2)) > 1 ∧
              ∀ m : ℕ,
                0 < m →
                  (∀ i : ℕ, i < n + 2 → a i ≠ m) →
                    Nat.gcd (a (n + 1)) m > 1 → a (n + 2) ≤ m
Sources
2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.