Exercise 5.16 follow-up (Scott 1981, PRG-19, Lecture V) — the Thue–Morse

sequence t

The unfinished tail of Exercise 5.16. Returning to the domain C of finite/infinite binary sequences (Example 4.4), Scott studies the element

t = 0·merge(neg t, tail t),

the least fixed point of Φ(x) = 0·merge(neg x, tail x), and (Lambek's observation) identifies its n-th digit with the parity of the binary digits of n — the Thue–Morse sequence.

This module formalizes:

• Step 0 — the element and its unfolding. tElt := Φ.fixElement and tElt_unfold proving t = 0·merge(neg t, tail t).
• The Thue–Morse morphism expand (the substitution 0 ↦ 01, 1 ↦ 10) and the key bridge Phi_strBot_expand: applied to a partial element (0σ)⊥, the operator Φ is exactly expand. Consequently the finite approximants of the least fixed point are Φⁿ⁺¹(⊥) = (expandⁿ[0])⊥ (iterElem_succ_eq).
• The parity bit-function tm with tm n = ⊕ (binary digits of n) (via Nat.bits), its recurrences tm (2n) = tm n, tm (2n+1) = ¬ tm n, and the bridge expand_iterate_eq showing the approximant strings are precisely the Thue–Morse parity prefixes tmList (2ⁿ).
• Property (a) — the digit characterization. tElt_mem_cone_iff: a finite string σ is a prefix of t iff σ is the length-σ.length Thue–Morse prefix (σ = tmList σ.length); and the digit reading tElt_digit : (tmList n ++ [tm n])⊥ ≤ t, i.e. the n-th digit of t is tm n, the parity of the binary digits of n (Lambek).

The tElt data is choice-free; the Prop-level digit facts may use Classical.choice (through the project's eq_of_toElementMap_principal and the truth-domain primitives), exactly like the existing uniqueness lemmas. Overlap-freeness (property (b)) is a self-contained word-combinatorics theorem and lives in its own module.

The Thue–Morse morphism expand (0 ↦ 01, 1 ↦ 10).

def Domain.Neighborhood.Exercise516.expand : ExampleB.Str → ExampleB.Str

The Thue–Morse substitution applied letterwise: each bit b is replaced by b (¬b).

Equations

• Domain.Neighborhood.Exercise516.expand [] = []
• Domain.Neighborhood.Exercise516.expand (b :: σ) = b :: (!b) :: Domain.Neighborhood.Exercise516.expand σ

@[simp]

theorem Domain.Neighborhood.Exercise516.expand_nil : expand [] = []

@[simp]

theorem Domain.Neighborhood.Exercise516.expand_cons (b : Bool) (σ : ExampleB.Str) : expand (b :: σ) = b :: (!b) :: expand σ

theorem Domain.Neighborhood.Exercise516.expand_append (σ τ : ExampleB.Str) : expand (σ ++ τ) = expand σ ++ expand τ

expand distributes over append (it is a monoid morphism Σ* → Σ*).

Φ on a partial element computes by interleaving — and equals expand.

theorem Domain.Neighborhood.Exercise516.mergeVal_snd_false (σ τ : ExampleB.Str) (b₁ : Bool) : (mergeVal σ false τ b₁).2 = false

The second (total/partial-flag) component of an interleaving with a partial first input is always false: a partial input keeps the output partial.

theorem Domain.Neighborhood.Exercise516.weave_head (h : Bool) (ρ : ExampleB.Str) : (mergeVal (h :: flip ρ) false ρ false).1 = h :: expand ρ

The interleaving of h :: flip ρ with ρ (both starting after a common head h) is h :: expand ρ. This is the heart of why Φ is the Thue–Morse morphism on the trajectory.

def Domain.Neighborhood.Exercise516.tmOp : ApproximableMap Example44.C Example44.C

Exercise 5.16 (the operator Φ). Φ(x) = 0·merge(neg x, tail x) as an approximable map.

Equations

• One or more equations did not get rendered due to their size.

theorem Domain.Neighborhood.Exercise516.tmOp_strBot (σ : ExampleB.Str) : tmOp.toElementMap (Example44.strBot σ) = Example44.strBot (false :: (mergeVal (flip σ) false (List.tail σ) false).1)

The value of Φ on a partial element σ⊥ is (0 · weave σ)⊥, the leading 0 prepended to the interleaving of (flip σ)⊥ and (tail σ)⊥.

theorem Domain.Neighborhood.Exercise516.tmOp_strBot_expand (ρ : ExampleB.Str) : tmOp.toElementMap (Example44.strBot (false :: ρ)) = Example44.strBot (expand (false :: ρ))

The Thue–Morse trajectory. On a partial element whose string starts with 0, Φ acts as the Thue–Morse morphism expand.

The finite approximants of the least fixed point are the morphism

iterates.

theorem Domain.Neighborhood.Exercise516.iterElem_zero' {α : Type u_1} {V : NeighborhoodSystem α} (f : ApproximableMap V V) : f.iterElem 0 = V.bot

The base of the iterated bottom element: f⁰(⊥) = ⊥.

theorem Domain.Neighborhood.Exercise516.iterElem_succ {α : Type u_1} {V : NeighborhoodSystem α} (f : ApproximableMap V V) (n : ℕ) : f.iterElem (n + 1) = f.toElementMap (f.iterElem n)

A one-step unfolding of the iterated bottom element: fⁿ⁺¹(⊥) = f(fⁿ(⊥)).

theorem Domain.Neighborhood.Exercise516.iterate_expand_cons (k : ℕ) : ∃ (ρ : List Bool), expand^[k] [false] = false :: ρ

Every iterate of expand from [0] starts with 0 (so Φ keeps acting as expand).

theorem Domain.Neighborhood.Exercise516.strBot_nil : Example44.strBot [] = Example44.C.bot

⊥ = []⊥ in C (the cone of Λ is the master).

theorem Domain.Neighborhood.Exercise516.iterElem_succ_eq (k : ℕ) : tmOp.iterElem (k + 1) = Example44.strBot (expand^[k] [false])

Exercise 5.16 (the approximants). The (k+1)-st approximant of the least fixed point is the partial element of the k-fold Thue–Morse morphism iterate of [0]: Φᵏ⁺¹(⊥) = (expandᵏ[0])⊥.

The parity bit-function tm and its prefixes.

def Domain.Neighborhood.Exercise516.tm (n : ℕ) : Bool

The Thue–Morse bit-function: tm n = ⊕(binary digits of n), the parity of the number of 1s in the binary expansion of n (Lambek's description).

Equations

• Domain.Neighborhood.Exercise516.tm n = List.foldr xor false n.bits

@[simp]

theorem Domain.Neighborhood.Exercise516.tm_zero : tm 0 = false

theorem Domain.Neighborhood.Exercise516.tm_two_mul (n : ℕ) : tm (2 * n) = tm n

The even recurrence tm (2n) = tm n (appending a 0-digit does not change the parity).

theorem Domain.Neighborhood.Exercise516.tm_two_mul_add_one (n : ℕ) : tm (2 * n + 1) = !tm n

The odd recurrence tm (2n+1) = ¬ tm n (appending a 1-digit flips the parity).

def Domain.Neighborhood.Exercise516.tmList (n : ℕ) : ExampleB.Str

The length-n Thue–Morse prefix [tm 0, tm 1, …, tm (n-1)].

Equations

• Domain.Neighborhood.Exercise516.tmList n = List.map Domain.Neighborhood.Exercise516.tm (List.range n)

@[simp]

theorem Domain.Neighborhood.Exercise516.tmList_zero : tmList 0 = []

theorem Domain.Neighborhood.Exercise516.tmList_succ (n : ℕ) : tmList (n + 1) = tmList n ++ [tm n]

theorem Domain.Neighborhood.Exercise516.tmList_length (n : ℕ) : List.length (tmList n) = n

theorem Domain.Neighborhood.Exercise516.tmList_prefix {n m : ℕ} (h : n ≤ m) : tmList n <+: tmList m

Thue–Morse prefixes are nested in the prefix order.

theorem Domain.Neighborhood.Exercise516.expand_tmList (m : ℕ) : expand (tmList m) = tmList (2 * m)

The morphism step on prefixes. expand (tmList m) = tmList (2m): applying the Thue–Morse morphism to a length-m prefix yields the length-2m prefix — this is exactly the even/odd parity recurrence in disguise.

theorem Domain.Neighborhood.Exercise516.expand_iterate_eq (k : ℕ) : expand^[k] [false] = tmList (2 ^ k)

The bridge. The k-fold morphism iterate of [0] is the Thue–Morse parity prefix of length 2ᵏ: expandᵏ[0] = tmList (2ᵏ).

Step 0 — the element t and its unfolding.

def Domain.Neighborhood.Exercise516.tElt : Example44.C.Element

Exercise 5.16 (Scott 1981, PRG-19). Scott's Thue–Morse element t = 0·merge(neg t, tail t), the least fixed point of Φ.

Equations

• Domain.Neighborhood.Exercise516.tElt = Domain.Neighborhood.Exercise516.tmOp.fixElement

theorem Domain.Neighborhood.Exercise516.tElt_unfold : (Example44.consMap false).toElementMap (mergeMap.toElementMap (pair (negMap.toElementMap tElt) (tailMap.toElementMap tElt))) = tElt

Exercise 5.16 — the defining unfolding. t = 0·merge(neg t, tail t).

Property (a) — the digit characterization.

theorem Domain.Neighborhood.Exercise516.strBot_mem_cone {σ τ : ExampleB.Str} : (Example44.strBot τ).mem (ExampleB.cone σ) ↔ σ <+: τ

(strBot τ) has the cone of σ as a neighbourhood iff σ is a prefix of τ.

theorem Domain.Neighborhood.Exercise516.cone_univ_iff {σ : ExampleB.Str} : ExampleB.cone σ = Set.univ ↔ σ = []

σΣ* = Σ* iff σ = Λ.

theorem Domain.Neighborhood.Exercise516.iterElem_le_fixElement {α : Type u_1} {V : NeighborhoodSystem α} (f : ApproximableMap V V) (n : ℕ) : f.iterElem n ≤ f.fixElement

Each approximant is below the least fixed point.

theorem Domain.Neighborhood.Exercise516.tmList_le_tElt (n : ℕ) : Example44.strBot (tmList n) ≤ tElt

Property (a), prefix form. Every Thue–Morse parity prefix is a prefix of t: (tmList n)⊥ ⊑ t for all n.

theorem Domain.Neighborhood.Exercise516.tElt_mem_cone_iff (σ : ExampleB.Str) : tElt.mem (ExampleB.cone σ) ↔ σ = tmList (List.length σ)

Property (a) (Scott 1981, PRG-19; Lambek). The finite-prefix characterization of t: a string σ is a prefix of t iff it is the length-σ.length Thue–Morse parity prefix. Reading off position n, the n-th digit of t is tm n, the parity of the binary digits of n.

theorem Domain.Neighborhood.Exercise516.tElt_digit (n : ℕ) : Example44.strBot (tmList n ++ [tm n]) ≤ tElt

Property (a), digit form. The n-th digit of t is tm n (the parity of the binary digits of n): the length-(n+1) prefix of t is tmList n ++ [tm n].