6697.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

12 declarations, 1 contain sorry, 0 declared as axioms

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.

Imports (1)

FormalConjecturesUtil

Imported by 1 file

FormalConjectures/Subsets/FC100SolvedSet1.lean

def OeisA6697.morphism The morphism σ on {a, b} defined by a ↦ aab, b ↦ b, represented on Bool where false = a and true = b line 47 source
Source documentation
The morphism σ on {a, b} defined by a ↦ aab, b ↦ b, represented on Bool where false = a and true = b.

no axioms what this means
Statement uses: Bool, List
Proof uses: OeisA6697.morphism.match_1, Unit, List.cons, Bool.false, Bool.true, List.nil
```
def morphism : Bool → List Bool
  | false => [false, false, true]  -- a ↦ aab
  | true => [true]                -- b ↦ b

/-- The n-th iterate of the morphism applied to [a]. -/
```
Mentions: OeisA6697.a
def OeisA6697.finiteWord The n-th iterate of the morphism applied to [a] line 52 source
Source documentation
The n-th iterate of the morphism applied to [a].

no axioms what this means
Statement uses: Nat, List, Bool
2 instances, coercions and auxiliary constants left out.
```
def finiteWord : ℕ → List Bool
  | 0 => [false]
  | n + 1 => (finiteWord n).flatMap morphism

@[simp, category API, AMS 68]
```
Mentions: OeisA6697.morphism, AMS
lemma OeisA6697.count_false_morphism line 57 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Bool, Eq, Nat, List.count, Bool.false, OeisA6697.morphism, ite, Bool.true, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congr, congrArg, List.cons, List.nil, HAdd.hAdd, List.count_cons_self, congrFun', List.count_eq_one_of_mem, List.Nodup, And, Not, Membership.mem, List, False, Or, Bool.false_eq_true, or_self and 10 more
16 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma OeisA6697.count_true_morphism line 61 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Bool, Eq, Nat, List.count, Bool.true, OeisA6697.morphism, OfNat.ofNat
Proof uses: Bool.false, of_eq_true, Eq.trans, True, congrFun', congrArg, List.cons, List.nil, List.count_cons_of_ne, Not, False, Bool.false_eq_true, not_false_eq_true, List.count_eq_one_of_mem, List.Nodup, And, Membership.mem, List, congr, Or and 8 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma OeisA6697.count_false_finiteWord line 65 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, List.count, Bool, Bool.false, OeisA6697.finiteWord, HPow.hPow, OfNat.ofNat
16 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma OeisA6697.count_true_finiteWord line 72 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, List.count, Bool, Bool.true, OeisA6697.finiteWord, HSub.hSub, HPow.hPow, OfNat.ofNat
20 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma OeisA6697.length_finiteWord line 79 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, List.length, Bool, OeisA6697.finiteWord, HSub.hSub, HPow.hPow, OfNat.ofNat, HAdd.hAdd
Proof uses: Eq.mpr, HMul.hMul, id, congr, congrArg, Eq.trans, List.count, Bool.true, Bool.false, OeisA6697.count_true_finiteWord, OeisA6697.count_false_finiteWord, congrFun', pow_succ, Decidable.byContradiction, Not
27 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def OeisA6697.infiniteWord The infinite word w is the fixed point of the morphism starting from 'a' line 85 source
Source documentation
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.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Bool
Proof uses: GetElem.getElem, List, LT.lt, List.length, OeisA6697.finiteWord, HAdd.hAdd, OfNat.ofNat
6 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
noncomputable def infiniteWord (i : ℕ) : Bool :=
…
```
def OeisA6697.subwordAt A subword (factor) of length n starting at position i line 89 source
Source documentation
A subword (factor) of length n starting at position i.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, List, Bool
Proof uses: List.map, OeisA6697.infiniteWord, HAdd.hAdd, List.range
2 instances, coercions and auxiliary constants left out.
```
noncomputable def subwordAt (i n : ℕ) : List Bool :=
…
```
def OeisA6697.subwordsOfLength The set of all distinct subwords of length n in the infinite word line 93 source
Source documentation
The set of all distinct subwords of length n in the infinite word.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Set, List, Bool
Proof uses: Set.ofPred, Exists, Eq, OeisA6697.subwordAt
```
def subwordsOfLength (n : ℕ) : Set (List Bool) :=
…
```
def OeisA6697.a The subword complexity function: a(n) is the number of distinct subwords of length n line 97 source
Source documentation
The subword complexity function: a(n) is the number of distinct subwords of length n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Set.ncard, List, Bool, OeisA6697.subwordsOfLength
```
noncomputable def a (n : ℕ) : ℕ := (subwordsOfLength n).ncard
…
```
Mentions: OeisA6697.subwordsOfLength
theorem OeisA6697.conjecture Conjecture (A6697): The generating function for the number of subwords of length sorry line 124 source
Source documentation
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.

L4DEL explanation
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.
Sources and attribution: Pinned Lean source (1646ca16afd6)

depends on sorry what this means
Statement uses: Nat, Eq, Rat, OeisA6697.a, LinearMap, RingHom.id, PowerSeries, Unit, PowerSeries.coeff, HAdd.hAdd, Inv.inv, HSub.hSub, OfNat.ofNat, PowerSeries.X, HMul.hMul, HPow.hPow, tsum, PowerSeries.WithPiTopology.instTopologicalSpace, SummationFilter.unconditional
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
80 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem conjecture (n : ℕ) :
    a n = coeff (R := ℚ) n
…
```
Mentions: OeisA6697.a