Exercise 1.13 (Scott 1981, PRG-19, §1) — the infinite binary system B,

revisited

Scott: "Verify all the assertions made about the system B … Draw a picture … which includes nodes for all σ ∈ Σ* … and where the total elements lie. (The picture … has to have limit nodes all along the top.)"

The "assertions about B" are exactly the content of ExampleB.lean:

• ExampleB.B is a neighbourhood system (ExampleB.nestedOrDisjoint);
• ExampleB.sigmaElt/sigmaElt_bot realize Scott's σx and σ⊥ with σx ∈ |B|;
• ExampleB.sigmaBot_le_iff is "σ₀⊥ ⊑ σ₁⊥ iff σ₀ initial segment of σ₁";
• ExampleB.mem_iff_exists_sigmaBot is "x = ⋃ₙ σₙ⊥".

This file supplies the limit nodes: for an infinite path p : ℕ → Bool we build the element branch p ∈ |B| as the ascending union (Theorem 1.11(ii)) of the finite approximations σₙ⊥ = (p↾n)⊥, show every finite approximation approximates it (branchSeq_le_branch), and prove it is a total (maximal) element (branch_isTotal). These are the nodes "along the top".

Constructive except branch_isTotal's use of B's structure (still [propext, Quot.sound]).

def Domain.Neighborhood.Exercise113.prefixSeq (p : ℕ → Bool) : ℕ → ExampleB.Str

The length-n initial segment p ↾ n = ⟨p 0, …, p (n-1)⟩ of an infinite path p.

Equations

• Domain.Neighborhood.Exercise113.prefixSeq p 0 = []
• Domain.Neighborhood.Exercise113.prefixSeq p n.succ = Domain.Neighborhood.Exercise113.prefixSeq p n ++ [p n]

@[simp]

theorem Domain.Neighborhood.Exercise113.prefixSeq_length (p : ℕ → Bool) (n : ℕ) : List.length (prefixSeq p n) = n

theorem Domain.Neighborhood.Exercise113.prefixSeq_prefix_succ (p : ℕ → Bool) (n : ℕ) : prefixSeq p n <+: prefixSeq p (n + 1)

theorem Domain.Neighborhood.Exercise113.prefixSeq_mono (p : ℕ → Bool) {n m : ℕ} (h : n ≤ m) : prefixSeq p n <+: prefixSeq p m

def Domain.Neighborhood.Exercise113.branchSeq (p : ℕ → Bool) (n : ℕ) : ExampleB.B.Element

The finite approximations σₙ⊥ = (p ↾ n)⊥ along the path p.

Equations

• Domain.Neighborhood.Exercise113.branchSeq p n = Domain.Neighborhood.ExampleB.sigmaBot (Domain.Neighborhood.Exercise113.prefixSeq p n)

theorem Domain.Neighborhood.Exercise113.branchSeq_mono (p : ℕ → Bool) : Monotone (branchSeq p)

def Domain.Neighborhood.Exercise113.branch (p : ℕ → Bool) : ExampleB.B.Element

The limit/total element of an infinite path p: the ascending union ⋃ₙ (p ↾ n)⊥ (Theorem 1.11(ii)). These are the "limit nodes all along the top" of Scott's picture.

Equations

• Domain.Neighborhood.Exercise113.branch p = Domain.Neighborhood.ExampleB.B.iUnion (Domain.Neighborhood.Exercise113.branchSeq p) ⋯

theorem Domain.Neighborhood.Exercise113.branch_mem_iff (p : ℕ → Bool) {σ : ExampleB.Str} : (branch p).mem (ExampleB.cone σ) ↔ ∃ (n : ℕ), σ <+: prefixSeq p n

cone σ ∈ branch p iff σ is an initial segment of some p ↾ n, i.e. σ lies on the path.

theorem Domain.Neighborhood.Exercise113.branchSeq_le_branch (p : ℕ → Bool) (n : ℕ) : branchSeq p n ≤ branch p

Every finite approximation (p ↾ n)⊥ approximates the limit element branch p.

theorem Domain.Neighborhood.Exercise113.prefix_comparable_of_mem {σ τ : ExampleB.Str} (y : ExampleB.B.Element) (hσ : y.mem (ExampleB.cone σ)) (hτ : y.mem (ExampleB.cone τ)) : σ <+: τ ∨ τ <+: σ

Two neighbourhoods present in a common element of |B| have comparable generating prefixes (their cones cannot be disjoint, since the intersection is a nonempty cone).

theorem Domain.Neighborhood.Exercise113.branch_isTotal (p : ℕ → Bool) : ExampleB.B.IsTotal (branch p)

Exercise 1.13 (total elements). Each infinite path p gives a total (maximal) element branch p: any y it approximates approximates it back. (These maximal elements are exactly the limit nodes along the top of the binary-tree picture.)