Exercise 4.18 (Scott 1981, PRG-19, Lecture IV)

In Example 4.3 there are many unproved assertions about N and F. These should be checked.

Example43.lean builds the natural-number domain N, the total elements n̂ = natElem n, and the structure maps succ, pred, zero with their value equations. This file discharges the remaining structural assertions Scott leaves implicit:

• Element classification (element_classification): |N| consists of exactly ⊥ and the total elements n̂ — N is genuinely the flat domain over ℕ. (This is the assertion that makes N "THE domain of integers".)
• Peano's axioms for the total elements ⟨{n̂}, 0̂, succ⟩:
  • natElem_injective / succMap_injective: distinct numerals are distinct elements, and succ is one-one;
  • natElem_zero_ne_succ / zero_ne_succMap: 0̂ is not a successor;
  • predMap_succMap_natElem (already in Example43): pred ∘ succ = id on numerals.

The classification is classical (it decides whether x contains a singleton, exactly as Example 4.3's zeroMap is classical); the injectivity / zero-is-not-a-successor facts are choice-free.

theorem Domain.Neighborhood.Exercise418.not_N_mem_empty : ¬Example43.N.mem ∅

∅ is not a neighbourhood of N.

theorem Domain.Neighborhood.Exercise418.element_classification (x : Example43.N.Element) : x = Example43.N.bot ∨ ∃ (n : ℕ), x = Example43.natElem n

Exercise 4.18 (Scott 1981, PRG-19). Element classification: every element of |N| is either the bottom ⊥ or a total element n̂. So N is the flat domain over ℕ.

theorem Domain.Neighborhood.Exercise418.natElem_injective {n m : ℕ} (h : Example43.natElem n = Example43.natElem m) : n = m

Exercise 4.18 (Scott 1981, PRG-19). The numerals are distinct: n̂ = m̂ ⟹ n = m.

theorem Domain.Neighborhood.Exercise418.succMap_injective {n m : ℕ} (h : Example43.succMap.toElementMap (Example43.natElem n) = Example43.succMap.toElementMap (Example43.natElem m)) : n = m

Exercise 4.18 (Scott 1981, PRG-19). succ is injective on the total elements.

theorem Domain.Neighborhood.Exercise418.natElem_zero_ne_succ (k : ℕ) : Example43.natElem 0 ≠ Example43.natElem (k + 1)

Exercise 4.18 (Scott 1981, PRG-19). 0̂ is not a numeral successor.

theorem Domain.Neighborhood.Exercise418.zero_ne_succMap (n : ℕ) : Example43.natElem 0 ≠ Example43.succMap.toElementMap (Example43.natElem n)

Exercise 4.18 (Scott 1981, PRG-19). 0̂ is not in the image of succ — Peano's "zero is not a successor".