Exercise 5.16 follow-up (Scott 1981, PRG-19, Lecture V) — overlap-freeness of

t

The second Thue–Morse property Scott asks for: t is overlap-free, t ≠ u·a·a·a·v for any finite u and nonempty a. This is a self-contained theorem of combinatorics on words (Thue 1912); it uses no domain theory (only the parity recurrences tm (2n) = tm n, tm (2n+1) = ¬ tm n of the bit-function tm from Exercise516ThueMorse) and has no leverage from Mathlib, so it is proved from scratch here.

We phrase an overlap of period p ≥ 1 at offset i as a factor of length 2p+1 with period p: Overlap i p := 1 ≤ p ∧ ∀ k ≤ p, tm (i+k) = tm (i+p+k). The main theorem no_overlap shows no overlap exists, and overlap_free is Scott's literal cube form t ≠ u·a·a·a·v (an overlap is weaker than a cube, so the cube form follows).

The proof is the classical descent: the two base facts are no three consecutive equal symbols (no_three_consec, the period-1 case) and a direct period-3 computation; an even period 2q contracts to a period-q overlap via the substitution structure, and an odd period ≥ 5 forces a run of three equal symbols.

The two basic facts about consecutive symbols.

theorem Domain.Neighborhood.Exercise516.tm_two_mul_ne (x : ℕ) : tm (2 * x) ≠ tm (2 * x + 1)

An even-indexed symbol differs from its successor: tm (2x) ≠ tm (2x+1).

theorem Domain.Neighborhood.Exercise516.odd_of_consec_eq {x : ℕ} (h : tm x = tm (x + 1)) : Odd x

tm x = tm (x+1) forces x to be odd: equal consecutive symbols only straddle a block boundary (2m+1, 2m+2), never a block (2m, 2m+1).

theorem Domain.Neighborhood.Exercise516.no_three_consec (j : ℕ) : ¬(tm j = tm (j + 1) ∧ tm (j + 1) = tm (j + 2))

No three consecutive equal symbols (the period-1 case): ¬ (tm j = tm (j+1) ∧ tm (j+1) = tm (j+2)). If both held, j and j+1 would both be odd.

Index reductions for tm.

theorem Domain.Neighborhood.Exercise516.tm_of_eq_two_mul {x y : ℕ} (h : x = 2 * y) : tm x = tm y

theorem Domain.Neighborhood.Exercise516.tm_of_eq_two_mul_add_one {x y : ℕ} (h : x = 2 * y + 1) : tm x = !tm y

Overlaps.

def Domain.Neighborhood.Exercise516.Overlap (i p : ℕ) : Prop

An overlap of period p ≥ 1 at offset i: a factor of length 2p+1 with period p.

Equations

• Domain.Neighborhood.Exercise516.Overlap i p = (1 ≤ p ∧ ∀ k ≤ p, Domain.Neighborhood.Exercise516.tm (i + k) = Domain.Neighborhood.Exercise516.tm (i + p + k))

theorem Domain.Neighborhood.Exercise516.no_overlap (p i : ℕ) : ¬Overlap i p

Overlap-freeness of the Thue–Morse sequence (Scott 1981, PRG-19; Thue 1912). No overlap exists at any offset and period.

Cube-freeness — Scott's literal form t ≠ u·a·a·a·v.

theorem Domain.Neighborhood.Exercise516.no_cube (i p : ℕ) (hp : 1 ≤ p) : ¬∀ k < 2 * p, tm (i + k) = tm (i + p + k)

The Thue–Morse sequence is cube-free. A cube of period p ≥ 1 (the factor a·a·a with |a| = p) is in particular an overlap, so none exists.

theorem Domain.Neighborhood.Exercise516.tmListGetElemOptional {n j : ℕ} (h : j < n) : (tmList n)[j]? = some (tm j)

The j-th bit of the length-n Thue–Morse prefix is tm j.

theorem Domain.Neighborhood.Exercise516.append_three_period {α : Type u_1} (a : List α) (m : ℕ) (hm : m < 2 * a.length) : (a ++ (a ++ a))[m]? = (a ++ (a ++ a))[m + a.length]?

Positions differing by |a| inside a ++ (a ++ a) carry the same symbol, for indices < 2|a| (the three copies of a are identical).

theorem Domain.Neighborhood.Exercise516.tElt_cube_free (u a : ExampleB.Str) (ha : a ≠ []) : ¬Example44.strBot (u ++ a ++ a ++ a) ≤ tElt

Exercise 5.16 (Scott 1981, PRG-19) — t is cube-free. Scott's literal statement: t is not of the form u·a·a·a·v for any finite prefix u and nonempty finite block a. (v is whatever follows; we phrase "u·a·a·a is a prefix of t" as (u·a·a·a)⊥ ⊑ t.)