FormalConjectures.OEIS.«6697»

/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

Subword complexity of the morphism a → aab, b → b

Let $a_n$ be the number of distinct subwords (contiguous factors) of length $n$ in the infinite word generated by the morphism $\sigma: a \mapsto aab, b \mapsto b$, starting from $a$. As shown in the references, $a_n$ is given by the formula $$ a_n = \sum_{i=0}^{n} \min(2^i,n-i+1). $$

The conjectured generating function is: $$\sum_{n \geq 0} a_n x^n = \frac{1}{1-x} + \frac{x}{(1-x)^2}\left(\frac{1}{1-x} - \sum_{k \geq 1} x^{2^k + k - 1}\right).$$

References:

A6697

J.-P. Allouche and J. Shallit, "On the subword complexity of the fixed point of a → aab, b → b, and generalizations," arXiv:1605.02361 [math.CO], 2016.

N. J. A. Sloane and Simon Plouffe, The Encyclopedia of Integer Sequences, Academic Press, 1995.


namespace OeisA6697


open PowerSeries WithPiTopology List

The morphism σ on {a, b} defined by a ↦ aab, b ↦ b, represented on Bool where false = a and true = b.

def morphism : Bool → List Bool
  | false => [false, false, true]  -- a ↦ aab
  | true => [true]                -- b ↦

The n-th iterate of the morphism applied to [a].

def finiteWord : ℕ → List Bool
  | 0 => [false]
  | n + 1 => (finiteWord n).flatMap morphism


@[simp, category API, AMS 68]
lemma count_false_morphism (b : Bool) : count false (morphism b) = if b then 0 else 2 := byb:Bool⊢ count false (morphism b) = if b = true then 0 else 2
  cases bfalse⊢ count false (morphism false) = if false = true then 0 else 2true⊢ count false (morphism true) = if true = true then 0 else 2 <;>false⊢ count false (morphism false) = if false = true then 0 else 2true⊢ count false (morphism true) = if true = true then 0 else 2 simp [morphism]All goals completed! 🐙


@[simp, category API, AMS 68]
lemma count_true_morphism (b : Bool) : count true (morphism b) = 1 := byb:Bool⊢ count true (morphism b) = 1
  cases bfalse⊢ count true (morphism false) = 1true⊢ count true (morphism true) = 1 <;>false⊢ count true (morphism false) = 1true⊢ count true (morphism true) = 1 simp [morphism]All goals completed! 🐙


@[simp, category API, AMS 68]
lemma count_false_finiteWord : ∀ n, (finiteWord n).count false = 2 ^ n
  | 0 => rfl
  | n + 1 =>n:ℕ⊢ count false (finiteWord (n + 1)) = 2 ^ (n + 1) byn:ℕ⊢ count false (finiteWord (n + 1)) = 2 ^ (n + 1)
    simp [finiteWord, count_flatMap, Function.comp_def, sum_map_ite, ← Bool.beq_eq_decide_eq,
      -beq_false, ← count_eq_length_filter, count_false_finiteWord, pow_succ]All goals completed! 🐙


@[simp, category API, AMS 68]
lemma count_true_finiteWord : ∀ n, (finiteWord n).count true = 2 ^ n - 1
  | 0 => rfl
  | n + 1 =>n:ℕ⊢ count true (finiteWord (n + 1)) = 2 ^ (n + 1) - 1 byn:ℕ⊢ count true (finiteWord (n + 1)) = 2 ^ (n + 1) - 1
    simp [finiteWord, List.count_flatMap, Function.comp_def, ← count_true_add_count_false,
      count_true_finiteWord, pow_succ]n:ℕ⊢ 2 ^ n - 1 + 2 ^ n = 2 ^ n * 2 - 1; omegaAll goals completed! 🐙


@[simp, category API, AMS 68]
lemma length_finiteWord (n : ℕ) : (finiteWord n).length = 2 ^ (n + 1) - 1 := byn:ℕ⊢ (finiteWord n).length = 2 ^ (n + 1) - 1
  simp [← count_true_add_count_false, count_true_finiteWord, pow_succ]n:ℕ⊢ 2 ^ n - 1 + 2 ^ n = 2 ^ n * 2 - 1; omegaAll goals completed! 🐙

The infinite word w is the fixed point of the morphism starting from 'a'. We define it as the limit: w(i) is the i-th symbol, which stabilizes after sufficiently many iterations.

noncomputable def infiniteWord (i : ℕ) : Bool :=
  (finiteWord (i + 1))[i]'(byi:ℕ⊢ i < (finiteWord (i + 1)).length grw [length_finiteWord, ← Nat.lt_two_pow_self]i:ℕ⊢ i < i + 1 + 1 - 1; simpAll goals completed! 🐙)

A subword (factor) of length n starting at position i.

noncomputable def subwordAt (i n : ℕ) : List Bool :=
  (List.range n).map fun j => infiniteWord (i + j)

The set of all distinct subwords of length n in the infinite word.

def subwordsOfLength (n : ℕ) : Set (List Bool) :=
  {w | ∃ i, w = subwordAt i n}

The subword complexity function: a(n) is the number of distinct subwords of length n.

noncomputable def a (n : ℕ) : ℕ := (subwordsOfLength n).ncard

Conjecture (A6697): The generating function for the number of subwords of length $n$ in the infinite word generated by $a \mapsto aab, b \mapsto b$ is $$\sum_{n \geq 0} a_n x^n = 1 + \frac{1}{1-x} + \frac{1}{(1-x)^2}\left(\frac{1}{1-x} - \sum_{k \geq 0} x^{2^{k+1} + k}\right).$$

Equivalently, a(n) equals the n-th coefficient of this generating function.

However, the reference quoted in the OEIS sequence

J.-P. Allouche and J. Shallit, "On the subword complexity of the fixed point of a → aab, b → b, and generalizations," arXiv:1605.02361 [math.CO], 2016.

provides an explicit formula $$ a_n = \sum_{i=0}^{n} \min(2^i,n-i+1). $$

If one takes this as a definition of a(n) instead, it becomes straightforward to prove the conjecture. See https://github.com/AxiomMath/gdm-formal-conjectures/blob/main/docs/OeisA6697.md for a formal proof of the generating function using this definition.

Hence, a formalization of arXiv:1605.02361 would complete a formal proof as below.

@[category research solved, formal_proof using lean4 at "https://github.com/AxiomMath/gdm-formal-conjectures/blob/main/OeisA6697/solution.lean", AMS 68]
theorem declaration uses 'sorry'conjecture (n : ℕ) :
    a n = coeff (R := ℚ) n
      ((1 - X)⁻¹ + X * (1 - X)⁻¹ ^ 2 * ((1 - X)⁻¹ - ∑' k, X ^ (2 ^ (k + 1) + k))) := byn:ℕ⊢ ↑(a n) = (coeff n) ((1 - X)⁻¹ + X * (1 - X)⁻¹ ^ 2 * ((1 - X)⁻¹ - ∑' (k : ℕ), X ^ (2 ^ (k + 1) + k)))
  sorryAll goals completed! 🐙


end OeisA6697