Theorem 7.4 (Scott 1981, PRG-19, §7) — + and × preserve effective givenness

Following Dana Scott, Lectures on a Mathematical Theory of Computation, PRG-19, Lecture VII.

Theorem 7.4. If 𝒟₀ and 𝒟₁ are effectively given, then so are (𝒟₀ + 𝒟₁) and (𝒟₀ × 𝒟₁). Moreover the combinators inᵢ, outᵢ, projᵢ are all computable; further, if f and g are computable maps, then so are f + g and f × g.

This file: the product (×) half. Scott takes 𝒟₀ × 𝒟₁ = {Xₙ⁰ ∪ Xₘ¹ ∣ n, m} with a one-one pairing function r(n, m) and W_k = X⁰_{p(k)} ∪ X¹_{q(k)}; we realize r = Nat.pair, p = ·.unpair.1, q = ·.unpair.2, and the project's prodNbhd/prod (over α ⊕ β, Product.lean). The product is uniform (no tag analysis), so both of Scott's relations decompose into conjunctions of the components' relations under index reindexing, handled entirely by the choice-free closure layer of Recursive.lean (RecDecidable.and/.comp/.of_iff):

• prodPresentation, prod_isEffectivelyGiven — the product is effectively given;
• proj₀_isComputable, proj₁_isComputable — (Xₙ⁰ ∪ Xₘ¹) projᵢ Z ↔ (component) ⊆ Z is recursively decidable (a slice of incl_computable), hence r.e.;
• paired_isComputable — ⟨f, g⟩ is computable when f, g are (conjunction of two r.e. relations);
• prodMap_isComputable — f × g is computable, via f × g = ⟨f ∘ p₀, g ∘ p₁⟩ (Exercise 3.19) and comp_isComputable (Proposition 7.3).

The sum (+) half — which needs tag analysis, hence a little more choice-free recursion theory (truncated subtraction, equality/disjunction deciders) — is in the companion development.

Everything here is ⊆ {propext, Quot.sound} (choice-free).

theorem Domain.Neighborhood.prodNbhd_eq_iff {α : Type u_1} {β : Type u_2} {X X' : Set α} {Y Y' : Set β} : prodNbhd X Y = prodNbhd X' Y' ↔ X = X' ∧ Y = Y'

The product representation is determined by its two components (the ↔ form of prodNbhd_injective).

def Domain.Neighborhood.prodEnum {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) (t : ℕ) : Set (α ⊕ β)

Scott's W_k = X⁰_{p(k)} ∪ X¹_{q(k)} with p = ·.unpair.1, q = ·.unpair.2.

Equations

• Domain.Neighborhood.prodEnum P₀ P₁ t = Domain.Neighborhood.prodNbhd (P₀.X (Nat.unpair t).1) (P₁.X (Nat.unpair t).2)

@[simp]

theorem Domain.Neighborhood.prodEnum_apply {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) (t : ℕ) : prodEnum P₀ P₁ t = prodNbhd (P₀.X (Nat.unpair t).1) (P₁.X (Nat.unpair t).2)

def Domain.Neighborhood.prodPresentation {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) : ComputablePresentation (prod V₀ V₁)

Theorem 7.4 (Scott 1981, PRG-19) — 𝒟₀ × 𝒟₁ is effectively given. The presentation W_k = X⁰_{p k} ∪ X¹_{q k}. Scott's 7.1(i) and (ii) each split, via prodNbhd_inter / prodNbhd_subset_iff, into the conjunction of the two factors' relations on the projected indices — recursively decidable by RecDecidable.and/.comp/.of_iff.

Equations

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

@[simp]

theorem Domain.Neighborhood.prodPresentation_X {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) (t : ℕ) : (prodPresentation P₀ P₁).X t = prodNbhd (P₀.X (Nat.unpair t).1) (P₁.X (Nat.unpair t).2)

theorem Domain.Neighborhood.prod_isEffectivelyGiven {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (h₀ : V₀.IsEffectivelyGiven) (h₁ : V₁.IsEffectivelyGiven) : (prod V₀ V₁).IsEffectivelyGiven

Theorem 7.4 (Scott 1981, PRG-19). The product of effectively given domains is effectively given.

theorem Domain.Neighborhood.proj₀_isComputable {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) : IsComputableMap (prodPresentation P₀ P₁) P₀ (proj₀ V₀ V₁)

Theorem 7.4 (Scott 1981, PRG-19) — proj₀ is computable. (Xₙ⁰ ∪ Xₘ¹) p₀ X⁰_k ↔ Xₙ⁰ ⊆ X⁰_k, a recursive slice of incl_computable, hence r.e.

theorem Domain.Neighborhood.proj₁_isComputable {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) : IsComputableMap (prodPresentation P₀ P₁) P₁ (proj₁ V₀ V₁)

Theorem 7.4 (Scott 1981, PRG-19) — proj₁ is computable. (Xₙ⁰ ∪ Xₘ¹) p₁ X¹_k ↔ Xₘ¹ ⊆ X¹_k (Scott's worked example), a recursive slice of incl_computable.

theorem Domain.Neighborhood.paired_isComputable {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {P₂ : ComputablePresentation V₂} {P₀ : ComputablePresentation V₀} {P₁ : ComputablePresentation V₁} {a : ApproximableMap V₂ V₀} {b : ApproximableMap V₂ V₁} (ha : IsComputableMap P₂ P₀ a) (hb : IsComputableMap P₂ P₁ b) : IsComputableMap P₂ (prodPresentation P₀ P₁) (paired a b)

Theorem 7.4 (Scott 1981, PRG-19) — the paired map ⟨f, g⟩ is computable. Zₙ ⟨f, g⟩ (X⁰_k ∪ X¹_l) ↔ Zₙ f X⁰_k ∧ Zₙ g X¹_l, the conjunction of two r.e. relations.

theorem Domain.Neighborhood.prodMap_isComputable {α : Type u_1} {β : Type u_2} {α' : Type u_4} {β' : Type u_5} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₀' : NeighborhoodSystem α'} {V₁' : NeighborhoodSystem β'} {P₀ : ComputablePresentation V₀} {P₁ : ComputablePresentation V₁} {P₀' : ComputablePresentation V₀'} {P₁' : ComputablePresentation V₁'} {f : ApproximableMap V₀ V₀'} {g : ApproximableMap V₁ V₁'} (hf : IsComputableMap P₀ P₀' f) (hg : IsComputableMap P₁ P₁' g) : IsComputableMap (prodPresentation P₀ P₁) (prodPresentation P₀' P₁') (prodMap f g)

Theorem 7.4 (Scott 1981, PRG-19) — the product functor f × g is computable. Using f × g = ⟨f ∘ p₀, g ∘ p₁⟩ (Exercise 3.19) together with computability of projᵢ and comp (Proposition 7.3).

The sum (+) half of Theorem 7.4

The sum 𝒟₀ + 𝒟₁ (Exercise318.lean, over Option (α ⊕ β)) has three kinds of neighbourhood — the master {Λ}∪0Δ₀∪1Δ₁, the left copies 0X, the right copies 1Y — so its presentation deciders require a genuine tag analysis (Scott: "the neighbourhood relations have to be worked out in terms of the indices … recursively enumerable relations … closure under conjunctions, disjunctions, …"). We enumerate with a Nat.pair tag: tag 0 ↦ 0X⁰ₖ, tag 1 ↦ 1X¹ₖ, tag ≥ 2 ↦ master.

theorem Domain.Neighborhood.tag_trichotomy (n : ℕ) : n = 0 ∨ n = 1 ∨ n ≠ 0 ∧ n ≠ 1

Choice-free three-way split of a tag n ∈ {0, 1, ≥2} (via Nat.decEq, not classical em).

def Domain.Neighborhood.sumEnum {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) (t : ℕ) : Set (Option (α ⊕ β))

Scott's Z₀ = Δ, Z_{2n+1} = X⁰ₙ, Z_{2n+2} = X¹ₙ, realized with a Nat.pair tag: tag = 0 ↦ 0X⁰, tag = 1 ↦ 1X¹, else the master.

Equations

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

@[simp]

theorem Domain.Neighborhood.sumEnum_zero {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {P₀ : ComputablePresentation V₀} {P₁ : ComputablePresentation V₁} {t : ℕ} (h : (Nat.unpair t).1 = 0) : sumEnum P₀ P₁ t = inj₀ (P₀.X (Nat.unpair t).2)

@[simp]

theorem Domain.Neighborhood.sumEnum_one {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {P₀ : ComputablePresentation V₀} {P₁ : ComputablePresentation V₁} {t : ℕ} (h : (Nat.unpair t).1 = 1) : sumEnum P₀ P₁ t = inj₁ (P₁.X (Nat.unpair t).2)

theorem Domain.Neighborhood.sumEnum_master {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {P₀ : ComputablePresentation V₀} {P₁ : ComputablePresentation V₁} {t : ℕ} (h0 : (Nat.unpair t).1 ≠ 0) (h1 : (Nat.unpair t).1 ≠ 1) : sumEnum P₀ P₁ t = sumMaster V₀ V₁

theorem Domain.Neighborhood.sumEnum_mem {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} {P₀ : ComputablePresentation V₀} {P₁ : ComputablePresentation V₁} (t : ℕ) : (sum V₀ V₁ h₀ h₁).mem (sumEnum P₀ P₁ t)

theorem Domain.Neighborhood.sumEnum_nonempty {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} {P₀ : ComputablePresentation V₀} {P₁ : ComputablePresentation V₁} (t : ℕ) : (sumEnum P₀ P₁ t).Nonempty

Distinctness of the three neighbourhood kinds (uses non-emptiness).

theorem Domain.Neighborhood.inj₀_eq_iff {α : Type u_1} {β : Type u_2} {A B : Set α} : inj₀ A = inj₀ B ↔ A = B

theorem Domain.Neighborhood.inj₁_eq_iff {α : Type u_1} {β : Type u_2} {A B : Set β} : inj₁ A = inj₁ B ↔ A = B

theorem Domain.Neighborhood.inj₀_ne_sumMaster {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {A : Set α} : inj₀ A ≠ sumMaster V₀ V₁

theorem Domain.Neighborhood.inj₁_ne_sumMaster {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {B : Set β} : inj₁ B ≠ sumMaster V₀ V₁

theorem Domain.Neighborhood.inj₀_ne_inj₁_of_nonempty {α : Type u_1} {β : Type u_2} {A : Set α} {B : Set β} (hB : B.Nonempty) : inj₀ A ≠ inj₁ B

theorem Domain.Neighborhood.sumEnum_eq_iff {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} {P₀ : ComputablePresentation V₀} {P₁ : ComputablePresentation V₁} (x y : ℕ) : sumEnum P₀ P₁ x = sumEnum P₀ P₁ y ↔ ((Nat.unpair x).1 ≠ 0 ∧ (Nat.unpair x).1 ≠ 1) ∧ (Nat.unpair y).1 ≠ 0 ∧ (Nat.unpair y).1 ≠ 1 ∨ ((Nat.unpair x).1 = 0 ∧ (Nat.unpair y).1 = 0) ∧ P₀.X (Nat.unpair x).2 = P₀.X (Nat.unpair y).2 ∨ ((Nat.unpair x).1 = 1 ∧ (Nat.unpair y).1 = 1) ∧ P₁.X (Nat.unpair x).2 = P₁.X (Nat.unpair y).2

Equality of two sum-neighbourhoods, in the indices. Both master, or same tag with equal component.

theorem Domain.Neighborhood.recDec_setEq₀ {α : Type u_1} {V₀ : NeighborhoodSystem α} {P₀ : ComputablePresentation V₀} {f g : ℕ → ℕ} (hf : Nat.Primrec f) (hg : Nat.Primrec g) : Recursive.RecDecidable fun (u : ℕ) => P₀.X (f u) = P₀.X (g u)

Equality of two enumerated 𝒟₀-neighbourhoods is recursively decidable (antisymmetry of ⊆, decided by incl_computable).

theorem Domain.Neighborhood.recDec_setEq₁ {β : Type u_2} {V₁ : NeighborhoodSystem β} {P₁ : ComputablePresentation V₁} {f g : ℕ → ℕ} (hf : Nat.Primrec f) (hg : Nat.Primrec g) : Recursive.RecDecidable fun (u : ℕ) => P₁.X (f u) = P₁.X (g u)

theorem Domain.Neighborhood.eqSEdec {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} {P₀ : ComputablePresentation V₀} {P₁ : ComputablePresentation V₁} : Recursive.RecDecidable fun (u : ℕ) => sumEnum P₀ P₁ (Nat.unpair u).1 = sumEnum P₀ P₁ (Nat.unpair u).2

sumEnum u.1 = sumEnum u.2 is recursively decidable (the of_iff translation of sumEnum_eq_iff into the tag/component deciders).

theorem Domain.Neighborhood.inj₀_eq_inj₁_elim {α : Type u_1} {β : Type u_2} {A : Set α} {B : Set β} (hA : A.Nonempty) (h : inj₀ A = inj₁ B) : False

A nonempty left copy cannot equal a right copy.

theorem Domain.Neighborhood.sumEnum_subset_sumMaster {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {P₀ : ComputablePresentation V₀} {P₁ : ComputablePresentation V₁} (n : ℕ) : sumEnum P₀ P₁ n ⊆ sumMaster V₀ V₁

Every enumerated sum-neighbourhood lies under the master (no non-emptiness needed).

theorem Domain.Neighborhood.sumMaster_inter_sumEnum {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {P₀ : ComputablePresentation V₀} {P₁ : ComputablePresentation V₁} (m : ℕ) : sumMaster V₀ V₁ ∩ sumEnum P₀ P₁ m = sumEnum P₀ P₁ m

M ∩ Z = Z: the master absorbs on the left.

theorem Domain.Neighborhood.sumEnum_inter_sumMaster {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {P₀ : ComputablePresentation V₀} {P₁ : ComputablePresentation V₁} (n : ℕ) : sumEnum P₀ P₁ n ∩ sumMaster V₀ V₁ = sumEnum P₀ P₁ n

Z ∩ M = Z: the master absorbs on the right.

theorem Domain.Neighborhood.sumPresentation_interEq_computable {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} {P₀ : ComputablePresentation V₀} {P₁ : ComputablePresentation V₁} : Recursive.RecDecidable₃ fun (n m k : ℕ) => sumEnum P₀ P₁ n ∩ sumEnum P₀ P₁ m = sumEnum P₀ P₁ k

Decidability of the sum-presentation intersection equality relation.

theorem Domain.Neighborhood.sumPresentation_cons_computable {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} {P₀ : ComputablePresentation V₀} {P₁ : ComputablePresentation V₁} : Recursive.RecDecidable₂ fun (n m : ℕ) => ∃ (k : ℕ), sumEnum P₀ P₁ k ⊆ sumEnum P₀ P₁ n ∩ sumEnum P₀ P₁ m

Decidability of the sum-presentation consistency relation.

def Domain.Neighborhood.sumInter {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) (n m : ℕ) : ℕ

Primitive-recursive index chosen for sum intersections.

Equations

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

theorem Domain.Neighborhood.sumInter_primrec {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {P₀ : ComputablePresentation V₀} {P₁ : ComputablePresentation V₁} : Nat.Primrec fun (t : ℕ) => sumInter P₀ P₁ (Nat.unpair t).1 (Nat.unpair t).2

The sum-presentation intersection index is primitive recursive.

theorem Domain.Neighborhood.sumInter_spec {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} {P₀ : ComputablePresentation V₀} {P₁ : ComputablePresentation V₁} {n m : ℕ} (h : ∃ (k : ℕ), sumEnum P₀ P₁ k ⊆ sumEnum P₀ P₁ n ∩ sumEnum P₀ P₁ m) : sumEnum P₀ P₁ (sumInter P₀ P₁ n m) = sumEnum P₀ P₁ n ∩ sumEnum P₀ P₁ m

The sum-presentation intersection index specifies the actual intersection when consistent.

theorem Domain.Neighborhood.sumPresentation_masterIdx_spec {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} {P₀ : ComputablePresentation V₀} {P₁ : ComputablePresentation V₁} : sumEnum P₀ P₁ (Nat.pair 2 0) = (sum V₀ V₁ h₀ h₁).master

The master index of the sum presentation denotes the sum master.

def Domain.Neighborhood.sumPresentation {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) : ComputablePresentation (sum V₀ V₁ h₀ h₁)

Theorem 7.4 (Scott 1981, PRG-19) — 𝒟₀ + 𝒟₁ is effectively given. The tag enumeration Z (pair 0 n) = 0X⁰ₙ, Z (pair 1 n) = 1X¹ₙ, Z (pair (≥2) _) = M. Scott's 7.1(i)/(ii) follow the intersection table: master absorbs, 0X ∩ 0X' = 0(X∩X') reduces to 𝒟₀, 0X ∩ 1Y = ∅ is impossible (non-emptiness). The deciders are assembled from eqSEdec, the tag deciders (natEq/not/and/or), and the components' interEq/cons.

Equations

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

theorem Domain.Neighborhood.sum_isEffectivelyGiven {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} (g₀ : V₀.IsEffectivelyGiven) (g₁ : V₁.IsEffectivelyGiven) : (sum V₀ V₁ h₀ h₁).IsEffectivelyGiven

Theorem 7.4 (Scott 1981, PRG-19). The sum of effectively given domains is effectively given.

@[simp]

theorem Domain.Neighborhood.sumPresentation_X {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) (t : ℕ) : (sumPresentation P₀ P₁).X t = sumEnum P₀ P₁ t

theorem Domain.Neighborhood.inMap₀_isComputable {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) : IsComputableMap P₀ (sumPresentation P₀ P₁) inMap₀

Theorem 7.4 (Scott 1981, PRG-19) — in₀ is computable. X⁰ₙ (in₀) Z_m ↔ 0X⁰ₙ ⊆ Z_m, which tag-decodes to (m = 0X⁰ ∧ X⁰ₙ ⊆ X⁰_{m.2}) ∨ (m = master) (m = 1X¹ is impossible as X⁰ₙ ≠ ∅).

theorem Domain.Neighborhood.inMap₁_isComputable {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) : IsComputableMap P₁ (sumPresentation P₀ P₁) inMap₁

Theorem 7.4 (Scott 1981, PRG-19) — in₁ is computable. Symmetric to in₀.

theorem Domain.Neighborhood.outMap₀_isComputable {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) : IsComputableMap (sumPresentation P₀ P₁) P₀ outMap₀

Theorem 7.4 (Scott 1981, PRG-19) — out₀ is computable. Z_n (out₀) X⁰_m ↔ leftPart Z_n ⊆ X⁰_m; tag-decoded, leftPart is X⁰_{n.2} on a left copy and Δ₀ on a right copy/master, so the relation is incl against either n.2 or the master index k₀ (X⁰_{k₀} = Δ₀).

theorem Domain.Neighborhood.outMap₁_isComputable {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) : IsComputableMap (sumPresentation P₀ P₁) P₁ outMap₁

Theorem 7.4 (Scott 1981, PRG-19) — out₁ is computable. Symmetric to out₀ via rightPart.

theorem Domain.Neighborhood.sumMap_isComputable {α : Type u_1} {β : Type u_2} {α' : Type u_4} {β' : Type u_5} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} {P₀ : ComputablePresentation V₀} {P₁ : ComputablePresentation V₁} {V₀' : NeighborhoodSystem α'} {V₁' : NeighborhoodSystem β'} {h₀' : ∀ (X : Set α'), V₀'.mem X → X.Nonempty} {h₁' : ∀ (Y : Set β'), V₁'.mem Y → Y.Nonempty} (Q₀ : ComputablePresentation V₀') (Q₁ : ComputablePresentation V₁') {f : ApproximableMap V₀ V₀'} {g : ApproximableMap V₁ V₁'} (hf : IsComputableMap P₀ Q₀ f) (hg : IsComputableMap P₁ Q₁ g) : IsComputableMap (sumPresentation P₀ P₁) (sumPresentation Q₀ Q₁) (sumMap f g)

Theorem 7.4 (Scott 1981, PRG-19) — f + g is computable. Tag-decoding the sum relation, Zₙ (f+g) W_m holds iff W_m is the codomain master (decidable in m's tag), or both are left copies (tag 0) with X⁰_{n.2} f Y⁰_{m.2}, or both are right copies (tag 1) with X¹_{n.2} g Y¹_{m.2}. The three disjuncts are r.e. (REPred.or): each copy case conjoins a decidable tag test with the reindexed r.e. relation of f/g.