Theorem 7.5 (Scott 1981, PRG-19, §7) — (𝒟₀ → 𝒟₁) is effectively given

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

Theorem 7.5. If 𝒟₀ and 𝒟₁ are effectively given, then so is (𝒟₀ → 𝒟₁). The combinators eval and curry are computable, provided all the domains involved are effectively given. The computable elements f ∈ |𝒟₀ → 𝒟₁| are exactly the computable maps f : 𝒟₀ → 𝒟₁.

This file builds the theorem in green, audited, choice-free milestones (see HANDOFF.md).

Milestone 1 — Proposition 3.9(i), the consistency condition (forward,

choice-free)

The keystone is Scott's 3.9(i): a function-space neighbourhood ⋂[Xᵢ,Yᵢ] is non-empty iff for every subset I of indices with {Xᵢ ∣ i∈I} consistent in 𝒟₀, the outputs {Yᵢ ∣ i∈I} are consistent in 𝒟₁. We model a subset by a sublist sub ⊑ L (this is what the eventual primitive-recursive decider enumerates, one entry/bit at a time), and the intersection of a finite list of neighbourhoods by interList. The forward direction — non-empty ⟹ the subset condition — is choice-free: given a witness map f ∈ stepFun L and a common lower neighbourhood Z of the selected inputs, f relates Z to the intersection of the selected outputs (a finite inter_right fold over the explicit selection, so no undecidable X ⊆ Xᵢ case-split is needed), whence that intersection is a neighbourhood by f.rel_cod.

(The reverse direction is genuinely decidable only relative to the presentations — it needs 𝒟₀-inclusion to be decidable to single out {i ∣ X ⊆ Xᵢ} — and is developed with the decider.)

interList — the intersection of a finite list of neighbourhoods (with a

base).

def Domain.Neighborhood.interList {β : Type u_2} (base : Set β) : List (Set β) → Set β

The intersection of the sets in M, taken inside the base set base (so the empty list gives base, matching the convention 1.1a where the empty intersection is Δ).

Equations

• Domain.Neighborhood.interList base [] = base
• Domain.Neighborhood.interList base (Y :: M) = Y ∩ Domain.Neighborhood.interList base M

@[simp]

theorem Domain.Neighborhood.interList_nil {β : Type u_2} (base : Set β) : interList base [] = base

theorem Domain.Neighborhood.interList_cons {β : Type u_2} (base Y : Set β) (M : List (Set β)) : interList base (Y :: M) = Y ∩ interList base M

theorem Domain.Neighborhood.mem_interList {β : Type u_2} {base : Set β} {M : List (Set β)} {z : β} : z ∈ interList base M ↔ z ∈ base ∧ ∀ Y ∈ M, z ∈ Y

theorem Domain.Neighborhood.interList_subset_base {β : Type u_2} {base : Set β} {M : List (Set β)} : interList base M ⊆ base

Milestone 1 — the forward direction of 3.9(i), choice-free.

theorem Domain.Neighborhood.rel_interList_of_selection {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {f : ApproximableMap V₀ V₁} {Z : Set α} (hZ : V₀.mem Z) {sub : List (Set α × Set β)} (hmem : ∀ p ∈ sub, f.rel p.1 p.2) (hZle : ∀ p ∈ sub, Z ⊆ p.1) : f.rel Z (interList V₁.master (List.map Prod.snd sub))

A witness map f ∈ stepFun L relates a common lower neighbourhood Z of the selected inputs to the intersection of the selected outputs. The selection sub is processed entry-by-entry with inter_right, so the proof is choice-free (no inclusion case-split).

theorem Domain.Neighborhood.interList_mem_of_stepFun_nonempty {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {L : List (Set α × Set β)} (h : (stepFun L).Nonempty) {sub : List (Set α × Set β)} (hsub : sub.Sublist L) {Z : Set α} (hZ : V₀.mem Z) (hZle : ∀ p ∈ sub, Z ⊆ p.1) : V₁.mem (interList V₁.master (List.map Prod.snd sub))

Proposition 3.9(i) (Scott 1981, PRG-19), forward direction — choice-free. If the function-space neighbourhood stepFun L is non-empty, then for every selection sub ⊑ L whose inputs admit a common lower neighbourhood Z ∈ 𝒟₀, the intersection of the selected outputs is a neighbourhood of 𝒟₁.

Milestone 2 — the consistency characterization over coded entry-lists.

A function-space neighbourhood is presented by a list el : List ℕ of entry codes: each e ∈ el codes a step pair [X_{e.1}, Y_{e.2}] via Nat.pair. funListOf turns el into the list of step pairs, and stepFun (funListOf el) is the neighbourhood ⋂[X_{eᵢ.1}, Y_{eᵢ.2}].

The characterization stepFun_funListOf_nonempty_iff is Scott's 3.9(i): the neighbourhood is non-empty iff for every sub-selection sub ⊑ el whose inputs have a common lower neighbourhood Z ∈ 𝒟₀, the intersection of the selected outputs is a neighbourhood of 𝒟₁. The reverse direction builds the least map leastMap; its consistency hypothesis is discharged input-by-input by filtering el with the (choice-free) decidable 𝒟₀-inclusion test supplied by the presentation P₀, so it stays ⊆ {propext, Quot.sound}.

def Domain.Neighborhood.funPair {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) (e : ℕ) : Set α × Set β

The step pair coded by an entry e: (X_{e.unpair.1}, Y_{e.unpair.2}).

Equations

• Domain.Neighborhood.funPair P₀ P₁ e = (P₀.X (Nat.unpair e).1, P₁.X (Nat.unpair e).2)

@[simp]

theorem Domain.Neighborhood.funPair_fst {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) (e : ℕ) : (funPair P₀ P₁ e).1 = P₀.X (Nat.unpair e).1

@[simp]

theorem Domain.Neighborhood.funPair_snd {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) (e : ℕ) : (funPair P₀ P₁ e).2 = P₁.X (Nat.unpair e).2

def Domain.Neighborhood.funListOf {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) (el : List ℕ) : List (Set α × Set β)

The list of step pairs coded by an entry-list el.

Equations

• Domain.Neighborhood.funListOf P₀ P₁ el = List.map (Domain.Neighborhood.funPair P₀ P₁) el

theorem Domain.Neighborhood.funListOf_valid {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) (el : List ℕ) (p : Set α × Set β) : p ∈ funListOf P₀ P₁ el → V₀.mem p.1 ∧ V₁.mem p.2

theorem Domain.Neighborhood.stepFun_funListOf_nonempty_iff {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) (el : List ℕ) : (stepFun (funListOf P₀ P₁ el)).Nonempty ↔ ∀ (sub : List ℕ), sub.Sublist el → (∃ (Z : Set α), V₀.mem Z ∧ ∀ e ∈ sub, Z ⊆ P₀.X (Nat.unpair e).1) → V₁.mem (interList V₁.master (List.map (fun (e : ℕ) => P₁.X (Nat.unpair e).2) sub))

Proposition 3.9(i) (Scott 1981, PRG-19), over coded entry-lists — choice-free. The function-space neighbourhood ⋂[X_{eᵢ}, Y_{eᵢ}] coded by el is non-empty iff for every sub-selection sub ⊑ el whose inputs {X_{e} ∣ e ∈ sub} admit a common lower neighbourhood Z ∈ 𝒟₀, the intersection of the selected outputs {Y_{e} ∣ e ∈ sub} is a neighbourhood of 𝒟₁.

• (⟹) is interList_mem_of_stepFun_nonempty (Milestone 1), pushed through funPair.
• (<=) builds leastMap; its consistency hypothesis hcons is discharged for each input X' by filtering el with the decidable 𝒟₀-inclusion X' ⊆ X_e (supplied choice-free by P₀), so that interYs Δ₁ (funListOf el) X' is exactly the intersection of the selected outputs.

Milestone 3a — deciding consistency of a finite index set via the

inter-chain.

To decide whether a finite list of neighbourhood indices js is consistent in 𝒟 (i.e. whether ⋂{X_j ∣ j ∈ js} is a neighbourhood) we fold the presentation's primitive-recursive inter along js, starting from masterIdx, to obtain an index idxchain js. The crisp characterization is:

js is consistent iff X_{idxchain js} ⊆ X_j for every j ∈ js.

The point is that X_{idxchain js} is always a neighbourhood (mem_X), so if it sits inside every X_j it witnesses consistency; conversely, when consistent, inter's spec (and the fact that a subset of a consistent set is consistent) makes the chain compute the genuine intersection. This replaces any consistency-flag bookkeeping by a single inter-fold plus a bounded inclusion check — all choice-free.

def Domain.Neighborhood.interFrom {α : Type u_1} {V : NeighborhoodSystem α} (P : ComputablePresentation V) (A : Set α) : List ℕ → Set α

The running intersection of A with the neighbourhoods X_j (j ∈ js), left-accumulated to match List.foldl.

Equations

• Domain.Neighborhood.interFrom P A [] = A
• Domain.Neighborhood.interFrom P A (j :: js) = Domain.Neighborhood.interFrom P (A ∩ P.X j) js

theorem Domain.Neighborhood.mem_interFrom {α : Type u_1} {V : NeighborhoodSystem α} (P : ComputablePresentation V) {A : Set α} {js : List ℕ} {z : α} : z ∈ interFrom P A js ↔ z ∈ A ∧ ∀ j ∈ js, z ∈ P.X j

theorem Domain.Neighborhood.interFrom_subset {α : Type u_1} {V : NeighborhoodSystem α} (P : ComputablePresentation V) {A : Set α} {js : List ℕ} : interFrom P A js ⊆ A

theorem Domain.Neighborhood.interFrom_mem_of_witness {α : Type u_1} {V : NeighborhoodSystem α} (P : ComputablePresentation V) {A : Set α} {js : List ℕ} {Z : Set α} (hZ : V.mem Z) (hZsub : Z ⊆ interFrom P A js) (hA : V.mem A) : V.mem (interFrom P A js)

A finite running intersection with a neighbourhood inside it is itself a neighbourhood.

theorem Domain.Neighborhood.interFrom_eq_of_foldl {α : Type u_1} {V : NeighborhoodSystem α} (P : ComputablePresentation V) (js : List ℕ) (A : Set α) (a : ℕ) : P.X a = A → V.mem A → V.mem (interFrom P A js) → P.X (List.foldl (fun (acc j : ℕ) => P.inter acc j) a js) = interFrom P A js

The fold of inter along js (starting from a, with X a = A) computes the running intersection interFrom A js — provided that intersection is consistent (so each prefix is too, by inter_spec).

def Domain.Neighborhood.idxchain {α : Type u_1} {V : NeighborhoodSystem α} (P : ComputablePresentation V) (js : List ℕ) : ℕ

The inter-chain index of js: inter-fold from masterIdx.

Equations

• Domain.Neighborhood.idxchain P js = List.foldl (fun (acc j : ℕ) => P.inter acc j) P.masterIdx js

theorem Domain.Neighborhood.idxchain_spec {α : Type u_1} {V : NeighborhoodSystem α} (P : ComputablePresentation V) {js : List ℕ} (h : V.mem (interFrom P V.master js)) : P.X (idxchain P js) = interFrom P V.master js

When js is consistent, the inter-chain index genuinely indexes ⋂{X_j ∣ j ∈ js}.

theorem Domain.Neighborhood.consChain_iff {α : Type u_1} {V : NeighborhoodSystem α} (P : ComputablePresentation V) (js : List ℕ) : (∀ j ∈ js, P.X (idxchain P js) ⊆ P.X j) ↔ V.mem (interFrom P V.master js)

Consistency via the inter-chain (choice-free). A finite index set js is consistent — i.e. ⋂{X_j ∣ j ∈ js} is a neighbourhood — exactly when the always-a-neighbourhood X_{idxchain js} sits inside every X_j (j ∈ js).

Milestone 3b — bitmask sublist selection.

The eventual decider enumerates the subsets of an entry-list one bit at a time: bitSelect L b keeps the entries of L whose position is set in the binary expansion of b (low bit = head). Every sublist arises as some bitSelect L b with b < 2 ^ L.length (exists_bitSelect_lt), so a universal statement over sublists is a bounded universal statement over bitmasks (forall_sublist_iff_forall_bitmask) — and bounded-∀ of a recursively decidable predicate is recursively decidable (RecDecidable.bForall). All choice-free.

def Domain.Neighborhood.bitSelect : List ℕ → ℕ → List ℕ

The sublist of L selected by the bitmask b (low bit = head).

Equations

• Domain.Neighborhood.bitSelect [] x✝ = []
• Domain.Neighborhood.bitSelect (e :: L) x✝ = if x✝ % 2 = 1 then e :: Domain.Neighborhood.bitSelect L (x✝ / 2) else Domain.Neighborhood.bitSelect L (x✝ / 2)

@[simp]

theorem Domain.Neighborhood.bitSelect_nil (b : ℕ) : bitSelect [] b = []

theorem Domain.Neighborhood.bitSelect_cons (e : ℕ) (L : List ℕ) (b : ℕ) : bitSelect (e :: L) b = if b % 2 = 1 then e :: bitSelect L (b / 2) else bitSelect L (b / 2)

theorem Domain.Neighborhood.bitSelect_sublist (L : List ℕ) (b : ℕ) : (bitSelect L b).Sublist L

theorem Domain.Neighborhood.exists_bitSelect_lt {L sub : List ℕ} (hsub : sub.Sublist L) : ∃ b < 2 ^ L.length, bitSelect L b = sub

theorem Domain.Neighborhood.forall_sublist_iff_forall_bitmask (c : ℕ) (p : List ℕ → Prop) : (∀ (sub : List ℕ), sub.Sublist (Recursive.decodeList c) → p sub) ↔ ∀ b < 2 ^ c, p (bitSelect (Recursive.decodeList c) b)

A universal statement over all sublists of decodeList c is a bounded universal over bitmasks b < 2 ^ c (using (decodeList c).length ≤ c).

Milestone 3c — the single-pass consistency fold (section ConsFold,

generic over P).

To decide whether a bitmask-selected sublist of an index list is consistent, we fold once over the list threading a state s = pair b (pair idx flag): b the remaining bitmask, idx an index of the running intersection ⋂{X_j ∣ j selected so far}, and flag ∈ {0,1} recording whether every prefix has been consistent. At a selected entry we set idx := P.inter idx (projFn x) and flag := flag ∧ [P.cons_computable says X_idx ∩ X_{projFn x} is consistent]. The headline consUpd_foldl_spec shows the final flag is 1 iff the selected intersection is a neighbourhood (using inter_spec to keep X_idx exact along the consistent prefix, and the fact that the full intersection being a neighbourhood forces every prefix to be one). All choice-free.

def Domain.Neighborhood.consUpd {α : Type u_1} {V : NeighborhoodSystem α} (P : ComputablePresentation V) (projFn fc : ℕ → ℕ) (s x : ℕ) : ℕ

One fold step (see the section doc). projFn extracts the relevant component index from an entry; fc is P.cons_computable's {0,1} consistency tester.

Equations

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

theorem Domain.Neighborhood.consUpd_eval {α : Type u_1} {V : NeighborhoodSystem α} (P : ComputablePresentation V) (projFn fc : ℕ → ℕ) (b idx flag x : ℕ) : consUpd P projFn fc (Nat.pair b (Nat.pair idx flag)) x = Recursive.selectFn (b % 2) (Nat.pair (b / 2) (Nat.pair (P.inter idx (projFn x)) (Recursive.selectFn flag (Recursive.isOne (fc (Nat.pair idx (projFn x)))) 0))) (Nat.pair (b / 2) (Nat.pair idx flag))

theorem Domain.Neighborhood.consUpd_foldl_flag_zero {α : Type u_1} {V : NeighborhoodSystem α} (P : ComputablePresentation V) (projFn fc : ℕ → ℕ) (el : List ℕ) (b a : ℕ) : (Nat.unpair (Nat.unpair (List.foldl (fun (s x : ℕ) => consUpd P projFn fc s x) (Nat.pair b (Nat.pair a 0)) el)).2).2 = 0

Once the flag is 0, the fold keeps it 0 (inconsistency persists).

theorem Domain.Neighborhood.consUpd_foldl_spec {α : Type u_1} {V : NeighborhoodSystem α} (P : ComputablePresentation V) (projFn fc : ℕ → ℕ) (hfc : ∀ (s : ℕ), fc s = 1 ↔ ∃ (k : ℕ), P.X k ⊆ P.X (Nat.unpair s).1 ∩ P.X (Nat.unpair s).2) (el : List ℕ) (b a : ℕ) : (Nat.unpair (Nat.unpair (List.foldl (fun (s x : ℕ) => consUpd P projFn fc s x) (Nat.pair b (Nat.pair a 1)) el)).2).2 = 1 ↔ V.mem (interFrom P (P.X a) (List.map projFn (bitSelect el b)))

Single-pass consistency fold — correctness. Starting from index a (an index of X a) with flag 1, the final flag is 1 iff the running intersection of X a with the selected components is a neighbourhood. Choice-free.

def Domain.Neighborhood.consStp {α : Type u_1} {V : NeighborhoodSystem α} (P : ComputablePresentation V) (projFn fc : ℕ → ℕ) (w : ℕ) : ℕ

foldCode-shaped wrapper of consUpd (state lives in w.unpair.2.unpair.1, entry in w.unpair.1).

Equations

• Domain.Neighborhood.consStp P projFn fc w = Domain.Neighborhood.consUpd P projFn fc (Nat.unpair (Nat.unpair w).2).1 (Nat.unpair w).1

def Domain.Neighborhood.consCharAt {α : Type u_1} {V : NeighborhoodSystem α} (P : ComputablePresentation V) (projFn fc : ℕ → ℕ) (w : ℕ) : ℕ

The {0,1} characteristic function of the bitmask-selected-sublist consistency test, packaged through foldCode so it is primitive recursive. Input w = pair b c (bitmask b, list code c).

Equations

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

theorem Domain.Neighborhood.consCharAt_spec {α : Type u_1} {V : NeighborhoodSystem α} (P : ComputablePresentation V) (projFn fc : ℕ → ℕ) (hfc : ∀ (s : ℕ), fc s = 1 ↔ ∃ (k : ℕ), P.X k ⊆ P.X (Nat.unpair s).1 ∩ P.X (Nat.unpair s).2) (w : ℕ) : consCharAt P projFn fc w = 1 ↔ V.mem (interFrom P V.master (List.map projFn (bitSelect (Recursive.decodeList (Nat.unpair w).2) (Nat.unpair w).1)))

theorem Domain.Neighborhood.primrec_consStp {α : Type u_1} {V : NeighborhoodSystem α} (P : ComputablePresentation V) {projFn fc : ℕ → ℕ} (hprojp : Nat.Primrec projFn) (hfcp : Nat.Primrec fc) : Nat.Primrec (consStp P projFn fc)

theorem Domain.Neighborhood.primrec_consCharAt {α : Type u_1} {V : NeighborhoodSystem α} (P : ComputablePresentation V) {projFn fc : ℕ → ℕ} (hprojp : Nat.Primrec projFn) (hfcp : Nat.Primrec fc) : Nat.Primrec (consCharAt P projFn fc)

theorem Domain.Neighborhood.consFold_decidable {α : Type u_1} {V : NeighborhoodSystem α} (P : ComputablePresentation V) (projFn fc : ℕ → ℕ) (hfc : ∀ (s : ℕ), fc s = 1 ↔ ∃ (k : ℕ), P.X k ⊆ P.X (Nat.unpair s).1 ∩ P.X (Nat.unpair s).2) (hprojp : Nat.Primrec projFn) (hfcp : Nat.Primrec fc) : Recursive.RecDecidable fun (w : ℕ) => V.mem (interFrom P V.master (List.map projFn (bitSelect (Recursive.decodeList (Nat.unpair w).2) (Nat.unpair w).1)))

Consistency of the bitmask-selected sublist is recursively decidable. Choice-free.

Milestone 3d — assembling the function-space consistency decider

funCons_decidable.

stepFun_funListOf_nonempty_iff (Milestone 2) characterises non-emptiness as a universal statement over sublists; forall_sublist_iff_forall_bitmask turns it into a bounded universal over bitmasks b < 2^c; antecedent_cons_iff / funConsequent_eq rewrite the per-bitmask antecedent and consequent into the interFrom form decided by consFold_decidable. The implication of two recursively decidable predicates is recursively decidable (.not/.or/.em, choice-free), and a bounded universal of a recursively decidable predicate is recursively decidable (RecDecidable.bForall).

theorem Domain.Neighborhood.interList_X_eq_interFrom {α : Type u_1} {V : NeighborhoodSystem α} (P : ComputablePresentation V) (js : List ℕ) : interList V.master (List.map (fun (j : ℕ) => P.X j) js) = interFrom P V.master js

interList over js.map X is the same set as the interFrom-chain over js.

theorem Domain.Neighborhood.antecedent_cons_iff {α : Type u_1} {V₀ : NeighborhoodSystem α} (P₀ : ComputablePresentation V₀) (sub : List ℕ) : (∃ (Z : Set α), V₀.mem Z ∧ ∀ e ∈ sub, Z ⊆ P₀.X (Nat.unpair e).1) ↔ V₀.mem (interFrom P₀ V₀.master (List.map (fun (e : ℕ) => (Nat.unpair e).1) sub))

The antecedent of Prop 3.9(i) — {X_{e.1} ∣ e ∈ sub} admits a common lower neighbourhood — is exactly consistency of {e.1 ∣ e ∈ sub} in 𝒟₀ (in interFrom form). Choice-free.

theorem Domain.Neighborhood.funConsequent_eq {β : Type u_2} {V₁ : NeighborhoodSystem β} (P₁ : ComputablePresentation V₁) (sub : List ℕ) : interList V₁.master (List.map (fun (e : ℕ) => P₁.X (Nat.unpair e).2) sub) = interFrom P₁ V₁.master (List.map (fun (e : ℕ) => (Nat.unpair e).2) sub)

The consequent of Prop 3.9(i), rewritten from interList to interFrom form.

theorem Domain.Neighborhood.funCons_iff {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) (c : ℕ) : (stepFun (funListOf P₀ P₁ (Recursive.decodeList c))).Nonempty ↔ ∀ b < 2 ^ c, V₀.mem (interFrom P₀ V₀.master (List.map (fun (e : ℕ) => (Nat.unpair e).1) (bitSelect (Recursive.decodeList c) b))) → V₁.mem (interFrom P₁ V₁.master (List.map (fun (e : ℕ) => (Nat.unpair e).2) (bitSelect (Recursive.decodeList c) b)))

Proposition 3.9(i) as a bounded bitmask quantifier. The function-space neighbourhood coded by decodeList c is non-empty iff for every bitmask b < 2^c, consistency of the selected inputs in 𝒟₀ forces consistency of the selected outputs in 𝒟₁. Choice-free.

theorem Domain.Neighborhood.funCons_decidable {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) (fc0 fc1 : ℕ → ℕ) (hfc0 : ∀ (s : ℕ), fc0 s = 1 ↔ ∃ (k : ℕ), P₀.X k ⊆ P₀.X (Nat.unpair s).1 ∩ P₀.X (Nat.unpair s).2) (hfc1 : ∀ (s : ℕ), fc1 s = 1 ↔ ∃ (k : ℕ), P₁.X k ⊆ P₁.X (Nat.unpair s).1 ∩ P₁.X (Nat.unpair s).2) (hfc0p : Nat.Primrec fc0) (hfc1p : Nat.Primrec fc1) : Recursive.RecDecidable fun (c : ℕ) => (stepFun (funListOf P₀ P₁ (Recursive.decodeList c))).Nonempty

The function-space consistency relation is recursively decidable. Given the binary consistency deciders fc0/fc1 of the two presentations, (stepFun (funListOf (decodeList c))) is non-empty is recursively decidable in c. Choice-free.

Milestone 4 — appendCode (list append on entry codes).

X n ∩ X m = stepFun (L_n ++ L_m), so the presentation's inter will splice two entry-lists. We fold one code onto another (prepending each entry), giving appendCode a b whose decoded list is (decodeList b).reverse ++ decodeList a; since stepFun is an intersection (order- and duplicate-invariant), this codes X a ∩ X b regardless of the reversal. All choice-free.

def Domain.Neighborhood.appendStep (acc x : ℕ) : ℕ

Prepend the entry x onto the list coded by acc.

Equations

• Domain.Neighborhood.appendStep acc x = Nat.pair x acc + 1

def Domain.Neighborhood.appendStp (w : ℕ) : ℕ

foldCode-shaped wrapper of appendStep.

Equations

• Domain.Neighborhood.appendStp w = Domain.Neighborhood.appendStep (Nat.unpair (Nat.unpair w).2).1 (Nat.unpair w).1

theorem Domain.Neighborhood.appendStp_eq (x acc : ℕ) : appendStp (Nat.pair x (Nat.pair acc 0)) = appendStep acc x

theorem Domain.Neighborhood.decodeList_appendStep (acc x : ℕ) : Recursive.decodeList (appendStep acc x) = x :: Recursive.decodeList acc

theorem Domain.Neighborhood.decodeList_foldl_appendStp (el : List ℕ) (acc : ℕ) : Recursive.decodeList (List.foldl (fun (acc x : ℕ) => appendStp (Nat.pair x (Nat.pair acc 0))) acc el) = el.reverse ++ Recursive.decodeList acc

def Domain.Neighborhood.appendCode (a b : ℕ) : ℕ

appendCode a b codes (decodeList b).reverse ++ decodeList a.

Equations

• Domain.Neighborhood.appendCode a b = Domain.Recursive.foldCode Domain.Neighborhood.appendStp 0 a b

theorem Domain.Neighborhood.decodeList_appendCode (a b : ℕ) : Recursive.decodeList (appendCode a b) = (Recursive.decodeList b).reverse ++ Recursive.decodeList a

theorem Domain.Neighborhood.primrec_appendCode : Nat.Primrec fun (t : ℕ) => appendCode (Nat.unpair t).1 (Nat.unpair t).2

theorem Domain.Neighborhood.funListOf_append {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) (la lb : List ℕ) : funListOf P₀ P₁ (la ++ lb) = funListOf P₀ P₁ la ++ funListOf P₀ P₁ lb

theorem Domain.Neighborhood.stepFun_funListOf_appendCode {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) (a b : ℕ) : stepFun (funListOf P₀ P₁ (Recursive.decodeList (appendCode a b))) = stepFun (funListOf P₀ P₁ (Recursive.decodeList a)) ∩ stepFun (funListOf P₀ P₁ (Recursive.decodeList b))

stepFun (funListOf (decodeList (appendCode a b))) is exactly X a ∩ X b at the level of the underlying step-intersections.

Milestone 5 — the function-space inclusion characterization (choice-free).

stepFun La ⊆ stepFun Lb iff ∀ (X',Y') ∈ Lb, ⋂{Y ∣ X' ⊆ X, (X,Y)∈La} ⊆ Y' (Scott, via the least map leastMap/3.9(ii)). The forward direction is choice-free (test the least map). The backward direction needs f.rel X' (interYs Δ₁ La X') for arbitrary f ∈ stepFun La — the library rel_interYs proves this classically (by_cases X' ⊆ Xᵢ), so we re-prove it choice-free for the presented list funListOf el, replacing the case split by P₀.incl_computable's recursive decidability (.em).

theorem Domain.Neighborhood.funListOf_cons {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) (e : ℕ) (el : List ℕ) : funListOf P₀ P₁ (e :: el) = funPair P₀ P₁ e :: funListOf P₀ P₁ el

theorem Domain.Neighborhood.rel_interYs_funList {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) {f : ApproximableMap V₀ V₁} {el : List ℕ} (hf : f ∈ stepFun (funListOf P₀ P₁ el)) (n' : ℕ) : f.rel (P₀.X n') (interYs V₁.master (funListOf P₀ P₁ el) (P₀.X n'))

Choice-free rel_interYs for a presented list. Any f ∈ stepFun (funListOf el) relates each X₀_{n'} to the intersection of the relevant outputs interYs Δ₁ (funListOf el) (X₀_{n'}). The case split on X₀_{n'} ⊆ X₀_{e.1} is discharged by P₀.incl_computable.em (no Classical.choice).

theorem Domain.Neighborhood.interYs_funList_mem_of_nonempty {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) {ea : List ℕ} (h : (stepFun (funListOf P₀ P₁ ea)).Nonempty) {X : Set α} (hX : V₀.mem X) : V₁.mem (interYs V₁.master (funListOf P₀ P₁ ea) X)

If stepFun (funListOf ea) is non-empty, then interYs Δ₁ (funListOf ea) X is a neighbourhood of 𝒟₁ for every X ∈ 𝒟₀ (the consistency hypothesis needed by leastMap). Choice-free.

theorem Domain.Neighborhood.stepFun_funListOf_subset_iff {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) {ea eb : List ℕ} (hcons : ∀ {X : Set α}, V₀.mem X → V₁.mem (interYs V₁.master (funListOf P₀ P₁ ea) X)) : stepFun (funListOf P₀ P₁ ea) ⊆ stepFun (funListOf P₀ P₁ eb) ↔ ∀ e' ∈ eb, interYs V₁.master (funListOf P₀ P₁ ea) (P₀.X (Nat.unpair e').1) ⊆ P₁.X (Nat.unpair e').2

Function-space inclusion characterisation (choice-free). With ea consistent (so the least map exists), stepFun (funListOf ea) ⊆ stepFun (funListOf eb) iff for every entry e' ∈ eb, the intersection of the ea-outputs relevant to the input X₀_{e'.1} is contained in X₁_{e'.2}.

Milestone 5b — the function-space inclusion / equality / consistency

deciders.

We now turn the choice-free characterization of Milestone 5a into recursive deciders for the function-space presentation. Two small generic facts first; then the interYs-index fold (a conditional inter-chain over 𝒟₁, gated by the decidable 𝒟₀-inclusion test); then the deciders themselves. All choice-free.

theorem Domain.Neighborhood.selectFn_isOne (v a b : ℕ) : Recursive.selectFn (Recursive.isOne v) a b = if v = 1 then a else b

selectFn driven by isOne is a Nat-equality if (choice-free; decEq on ℕ).

theorem Domain.Neighborhood.decodeList_encodeList (l : List ℕ) : Recursive.decodeList (Recursive.encodeList l) = l

decodeList inverts encodeList: every list is the decoding of its code.

The interYs-index fold: a conditional inter-chain over 𝒟₁.

For a presented list funListOf (decodeList a) and a 𝒟₀-index k, the set interYs Δ₁ (funListOf (decodeList a)) (X₀_k) is the intersection of the outputs X₁_{e.2} over the entries e of decodeList a whose input dominates X₀_k (X₀_k ⊆ X₀_{e.1}). We compute an index of it by folding P₁.inter over decodeList a, intersecting at an entry exactly when the (decidable) inclusion test fires. condSet k A el is the running set; interYsFoldl_spec is the index correctness (when the result is consistent), mirroring interFrom_eq_of_foldl.

def Domain.Neighborhood.condSet {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) (k : ℕ) (A : Set β) (el : List ℕ) : Set β

The running set of the conditional inter-chain: A intersected with the outputs X₁_{e.2} of the entries e ∈ el whose input dominates X₀_k.

Equations

• Domain.Neighborhood.condSet P₀ P₁ k A el = {z : β | z ∈ A ∧ ∀ e ∈ el, P₀.X k ⊆ P₀.X (Nat.unpair e).1 → z ∈ P₁.X (Nat.unpair e).2}

theorem Domain.Neighborhood.mem_condSet {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) {k : ℕ} {A : Set β} {el : List ℕ} {z : β} : z ∈ condSet P₀ P₁ k A el ↔ z ∈ A ∧ ∀ e ∈ el, P₀.X k ⊆ P₀.X (Nat.unpair e).1 → z ∈ P₁.X (Nat.unpair e).2

theorem Domain.Neighborhood.condSet_nil {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) (k : ℕ) (A : Set β) : condSet P₀ P₁ k A [] = A

theorem Domain.Neighborhood.condSet_subset {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) (k : ℕ) (A : Set β) (el : List ℕ) : condSet P₀ P₁ k A el ⊆ A

theorem Domain.Neighborhood.condSet_cons_pos {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) {k : ℕ} {A : Set β} {e : ℕ} {el : List ℕ} (h : P₀.X k ⊆ P₀.X (Nat.unpair e).1) : condSet P₀ P₁ k A (e :: el) = condSet P₀ P₁ k (A ∩ P₁.X (Nat.unpair e).2) el

condSet cons-step when the input dominates the head entry's input: intersect A with the head's output.

theorem Domain.Neighborhood.condSet_cons_neg {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) {k : ℕ} {A : Set β} {e : ℕ} {el : List ℕ} (h : ¬P₀.X k ⊆ P₀.X (Nat.unpair e).1) : condSet P₀ P₁ k A (e :: el) = condSet P₀ P₁ k A el

condSet cons-step when the input does not dominate the head entry's input: drop the head.

theorem Domain.Neighborhood.condSet_eq_interYs {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) (k : ℕ) (el : List ℕ) : condSet P₀ P₁ k V₁.master el = interYs V₁.master (funListOf P₀ P₁ el) (P₀.X k)

condSet k Δ₁ el is exactly interYs Δ₁ (funListOf el) (X₀_k).

def Domain.Neighborhood.interYsStp {β : Type u_2} {V₁ : NeighborhoodSystem β} (P₁ : ComputablePresentation V₁) (incl0 : ℕ → ℕ) (w : ℕ) : ℕ

One step of the interYs-index fold. State pair entry (pair acc k): entry e = w.unpair.1, running 𝒟₁-index acc = w.unpair.2.unpair.1, input index k = w.unpair.2.unpair.2 (the foldCode parameter). Intersects acc with e's output index when the inclusion test fires.

Equations

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

def Domain.Neighborhood.interYsIdx {β : Type u_2} {V₁ : NeighborhoodSystem β} (P₁ : ComputablePresentation V₁) (incl0 : ℕ → ℕ) (a k : ℕ) : ℕ

The index of interYs Δ₁ (funListOf (decodeList a)) (X₀_k): a conditional inter-fold over decodeList a from masterIdx, with k carried as the foldCode parameter.

Equations

• Domain.Neighborhood.interYsIdx P₁ incl0 a k = Domain.Recursive.foldCode (Domain.Neighborhood.interYsStp P₁ incl0) k P₁.masterIdx a

theorem Domain.Neighborhood.condFoldl_spec {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) (incl0 : ℕ → ℕ) (hincl0 : ∀ (s : ℕ), incl0 s = 1 ↔ P₀.X (Nat.unpair s).1 ⊆ P₀.X (Nat.unpair s).2) (k : ℕ) (el : List ℕ) (A : Set β) (a : ℕ) : P₁.X a = A → V₁.mem A → V₁.mem (condSet P₀ P₁ k A el) → P₁.X (List.foldl (fun (acc x : ℕ) => if incl0 (Nat.pair k (Nat.unpair x).1) = 1 then P₁.inter acc (Nat.unpair x).2 else acc) a el) = condSet P₀ P₁ k A el

Correctness of the conditional inter-fold (if-form). When the running set is consistent, the fold computes an index of it, by induction with inter_spec (mirrors interFrom_eq_of_foldl).

theorem Domain.Neighborhood.interYsIdx_spec {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) (incl0 : ℕ → ℕ) (hincl0 : ∀ (s : ℕ), incl0 s = 1 ↔ P₀.X (Nat.unpair s).1 ⊆ P₀.X (Nat.unpair s).2) (a k : ℕ) (hcons : V₁.mem (interYs V₁.master (funListOf P₀ P₁ (Recursive.decodeList a)) (P₀.X k))) : P₁.X (interYsIdx P₁ incl0 a k) = interYs V₁.master (funListOf P₀ P₁ (Recursive.decodeList a)) (P₀.X k)

interYsIdx indexes interYs Δ₁ (funListOf (decodeList a)) (X₀_k) (when that is consistent, which it is whenever stepFun (funListOf (decodeList a)) is non-empty). Choice-free.

theorem Domain.Neighborhood.primrec_interYsStp {β : Type u_2} {V₁ : NeighborhoodSystem β} (P₁ : ComputablePresentation V₁) (incl0 : ℕ → ℕ) (hincl0p : Nat.Primrec incl0) : Nat.Primrec (interYsStp P₁ incl0)

theorem Domain.Neighborhood.primrec_interYsIdx {β : Type u_2} {V₁ : NeighborhoodSystem β} (P₁ : ComputablePresentation V₁) (incl0 : ℕ → ℕ) (hincl0p : Nat.Primrec incl0) : Nat.Primrec fun (t : ℕ) => interYsIdx P₁ incl0 (Nat.unpair t).1 (Nat.unpair t).2

A concrete {0,1} characteristic function for function-space

consistency.

funCons_decidable already shows consistency is recursively decidable, but to use it in data (the function-space enumeration branches on it) we need a concrete primitive-recursive char rather than one extracted from an existential (extraction needs choice). We build it explicitly from the component presentations' consistency chars fc0/fc1, and prove its spec via funCons_iff.

theorem Domain.Neighborhood.selectFn_one_iff_imp {A B : ℕ} (hA : A ≤ 1) : Recursive.selectFn A B 1 = 1 ↔ A = 1 → B = 1

selectFn A B 1 = 1 decides the implication A = 1 → B = 1 for A ∈ {0,1}.

def Domain.Neighborhood.funImpChar {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) (fc0 fc1 : ℕ → ℕ) (w : ℕ) : ℕ

The per-bitmask implication char: cons₀(selected inputs) → cons₁(selected outputs).

Equations

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

def Domain.Neighborhood.funConsChar {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) (fc0 fc1 : ℕ → ℕ) (c : ℕ) : ℕ

The concrete {0,1} characteristic function of function-space consistency.

Equations

• Domain.Neighborhood.funConsChar P₀ P₁ fc0 fc1 c = Domain.Recursive.bForallFn (Domain.Neighborhood.funImpChar P₀ P₁ fc0 fc1) c (2 ^ c)

theorem Domain.Neighborhood.funConsChar_spec {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) (fc0 fc1 : ℕ → ℕ) (hfc0 : ∀ (s : ℕ), fc0 s = 1 ↔ ∃ (k : ℕ), P₀.X k ⊆ P₀.X (Nat.unpair s).1 ∩ P₀.X (Nat.unpair s).2) (hfc1 : ∀ (s : ℕ), fc1 s = 1 ↔ ∃ (k : ℕ), P₁.X k ⊆ P₁.X (Nat.unpair s).1 ∩ P₁.X (Nat.unpair s).2) (c : ℕ) : funConsChar P₀ P₁ fc0 fc1 c = 1 ↔ (stepFun (funListOf P₀ P₁ (Recursive.decodeList c))).Nonempty

theorem Domain.Neighborhood.primrec_funImpChar {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) (fc0 fc1 : ℕ → ℕ) (hfc0p : Nat.Primrec fc0) (hfc1p : Nat.Primrec fc1) : Nat.Primrec (funImpChar P₀ P₁ fc0 fc1)

theorem Domain.Neighborhood.primrec_funConsChar {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) (fc0 fc1 : ℕ → ℕ) (hfc0p : Nat.Primrec fc0) (hfc1p : Nat.Primrec fc1) : Nat.Primrec (funConsChar P₀ P₁ fc0 fc1)

A generic list-AND and the stepFun-inclusion decider subChar.

theorem Domain.Neighborhood.andFoldl_eq_one_iff (g : ℕ → ℕ) (el : List ℕ) (a : ℕ) : a ≤ 1 → (List.foldl (fun (acc x : ℕ) => Recursive.selectFn acc (Recursive.isOne (g x)) 0) a el = 1 ↔ a = 1 ∧ ∀ e ∈ el, g e = 1)

A {0,1} left-fold AND of isOne ∘ g over a list, started from a ∈ {0,1}.

theorem Domain.Neighborhood.andFoldl_one (g : ℕ → ℕ) (el : List ℕ) : List.foldl (fun (acc x : ℕ) => Recursive.selectFn acc (Recursive.isOne (g x)) 0) 1 el = 1 ↔ ∀ e ∈ el, g e = 1

def Domain.Neighborhood.subStp {β : Type u_2} {V₁ : NeighborhoodSystem β} (P₁ : ComputablePresentation V₁) (incl0 incl1 : ℕ → ℕ) (w : ℕ) : ℕ

One step of the stepFun-inclusion fold over decodeList b: test interYs-index ⊆ output.

Equations

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

def Domain.Neighborhood.subChar {β : Type u_2} {V₁ : NeighborhoodSystem β} (P₁ : ComputablePresentation V₁) (incl0 incl1 : ℕ → ℕ) (a b : ℕ) : ℕ

The {0,1} characteristic function of stepFun (funListOf (decodeList a)) ⊆ stepFun (funListOf (decodeList b)) (correct when a is consistent). a is the foldCode parameter, b the code.

Equations

• Domain.Neighborhood.subChar P₁ incl0 incl1 a b = Domain.Recursive.foldCode (Domain.Neighborhood.subStp P₁ incl0 incl1) a 1 b

theorem Domain.Neighborhood.subChar_spec {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) (incl0 incl1 : ℕ → ℕ) (hincl0 : ∀ (s : ℕ), incl0 s = 1 ↔ P₀.X (Nat.unpair s).1 ⊆ P₀.X (Nat.unpair s).2) (hincl1 : ∀ (s : ℕ), incl1 s = 1 ↔ P₁.X (Nat.unpair s).1 ⊆ P₁.X (Nat.unpair s).2) {a : ℕ} (hane : (stepFun (funListOf P₀ P₁ (Recursive.decodeList a))).Nonempty) (b : ℕ) : subChar P₁ incl0 incl1 a b = 1 ↔ stepFun (funListOf P₀ P₁ (Recursive.decodeList a)) ⊆ stepFun (funListOf P₀ P₁ (Recursive.decodeList b))

theorem Domain.Neighborhood.primrec_subStp {β : Type u_2} {V₁ : NeighborhoodSystem β} (P₁ : ComputablePresentation V₁) (incl0 incl1 : ℕ → ℕ) (hincl0p : Nat.Primrec incl0) (hincl1p : Nat.Primrec incl1) : Nat.Primrec (subStp P₁ incl0 incl1)

theorem Domain.Neighborhood.primrec_subChar {β : Type u_2} {V₁ : NeighborhoodSystem β} (P₁ : ComputablePresentation V₁) (incl0 incl1 : ℕ → ℕ) (hincl0p : Nat.Primrec incl0) (hincl1p : Nat.Primrec incl1) : Nat.Primrec fun (t : ℕ) => subChar P₁ incl0 incl1 (Nat.unpair t).1 (Nat.unpair t).2

The trivial test: stepFun (funListOf el) = univ iff every output is Δ₁`.

def Domain.Neighborhood.botMap {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} : ApproximableMap V₀ V₁

The least map of the empty step-list — the function-space bottom: it relates every 𝒟₀ neighbourhood only to Δ₁.

Equations

• Domain.Neighborhood.botMap = Domain.Neighborhood.leastMap [] ⋯

theorem Domain.Neighborhood.botMap_rel {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {X : Set α} {Y : Set β} : botMap.rel X Y ↔ V₀.mem X ∧ V₁.mem Y ∧ V₁.master ⊆ Y

theorem Domain.Neighborhood.stepFun_funListOf_eq_univ_iff {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) (el : List ℕ) : stepFun (funListOf P₀ P₁ el) = Set.univ ↔ ∀ e ∈ el, P₁.X (Nat.unpair e).2 = V₁.master

stepFun (funListOf el) is everything iff every output neighbourhood is Δ₁. Forward: the bottom map botMap lies in univ, and botMap.rel X Y forces Y = Δ₁. Backward: [X, Δ₁] is satisfied by every map. Choice-free.

def Domain.Neighborhood.trivStp {β : Type u_2} {V₁ : NeighborhoodSystem β} (P₁ : ComputablePresentation V₁) (eq1 : ℕ → ℕ) (w : ℕ) : ℕ

One step of the trivial-test fold: is this entry's output index equal to masterIdx?

Equations

• Domain.Neighborhood.trivStp P₁ eq1 w = Domain.Recursive.selectFn (Nat.unpair (Nat.unpair w).2).1 (Domain.Recursive.isOne (eq1 (Nat.pair (Nat.unpair (Nat.unpair w).1).2 P₁.masterIdx))) 0

def Domain.Neighborhood.trivialChar {β : Type u_2} {V₁ : NeighborhoodSystem β} (P₁ : ComputablePresentation V₁) (eq1 : ℕ → ℕ) (a : ℕ) : ℕ

The {0,1} characteristic function of stepFun (funListOf (decodeList a)) = univ.

Equations

• Domain.Neighborhood.trivialChar P₁ eq1 a = Domain.Recursive.foldCode (Domain.Neighborhood.trivStp P₁ eq1) 0 1 a

theorem Domain.Neighborhood.trivialChar_spec {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) (eq1 : ℕ → ℕ) (heq1 : ∀ (s : ℕ), eq1 s = 1 ↔ P₁.X (Nat.unpair s).1 = P₁.X (Nat.unpair s).2) (a : ℕ) : trivialChar P₁ eq1 a = 1 ↔ stepFun (funListOf P₀ P₁ (Recursive.decodeList a)) = Set.univ

theorem Domain.Neighborhood.primrec_trivStp {β : Type u_2} {V₁ : NeighborhoodSystem β} (P₁ : ComputablePresentation V₁) (eq1 : ℕ → ℕ) (heq1p : Nat.Primrec eq1) : Nat.Primrec (trivStp P₁ eq1)

theorem Domain.Neighborhood.primrec_trivialChar {β : Type u_2} {V₁ : NeighborhoodSystem β} (P₁ : ComputablePresentation V₁) (eq1 : ℕ → ℕ) (heq1p : Nat.Primrec eq1) : Nat.Primrec (trivialChar P₁ eq1)

The function-space enumeration Xenum and its consistency-pair decider.

def Domain.Neighborhood.Xenum {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) (gN : ℕ → ℕ) (c : ℕ) : Set (ApproximableMap V₀ V₁)

The function-space enumeration: a code c lists step-pairs; if they are consistent (gN c = 1, where gN is the consistency char) the neighbourhood is stepFun (funListOf (decodeList c)), otherwise we send the junk code to the master neighbourhood univ. Choice-free as data because the branch is a Nat-equality if.

Equations

• Domain.Neighborhood.Xenum P₀ P₁ gN c = if gN c = 1 then Domain.Neighborhood.stepFun (Domain.Neighborhood.funListOf P₀ P₁ (Domain.Recursive.decodeList c)) else Set.univ

theorem Domain.Neighborhood.Xenum_pos {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) {gN : ℕ → ℕ} {c : ℕ} (h : gN c = 1) : Xenum P₀ P₁ gN c = stepFun (funListOf P₀ P₁ (Recursive.decodeList c))

theorem Domain.Neighborhood.Xenum_neg {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) {gN : ℕ → ℕ} {c : ℕ} (h : gN c ≠ 1) : Xenum P₀ P₁ gN c = Set.univ

theorem Domain.Neighborhood.Xenum_mem {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) (gN : ℕ → ℕ) (hgN : ∀ (c : ℕ), gN c = 1 ↔ (stepFun (funListOf P₀ P₁ (Recursive.decodeList c))).Nonempty) (c : ℕ) : (funSpace V₀ V₁).mem (Xenum P₀ P₁ gN c)

theorem Domain.Neighborhood.Xenum_nonempty {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) (gN : ℕ → ℕ) (hgN : ∀ (c : ℕ), gN c = 1 ↔ (stepFun (funListOf P₀ P₁ (Recursive.decodeList c))).Nonempty) (c : ℕ) : (Xenum P₀ P₁ gN c).Nonempty

def Domain.Neighborhood.interIdx (gN : ℕ → ℕ) (n m : ℕ) : ℕ

The canonical code of the intersection Xenum n ∩ Xenum m: appendCode when both are consistent, otherwise the consistent side (the other being univ).

Equations

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

theorem Domain.Neighborhood.Xenum_inter_eq {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) (gN : ℕ → ℕ) (hgN : ∀ (c : ℕ), gN c = 1 ↔ (stepFun (funListOf P₀ P₁ (Recursive.decodeList c))).Nonempty) (n m : ℕ) (hne : (Xenum P₀ P₁ gN n ∩ Xenum P₀ P₁ gN m).Nonempty) : Xenum P₀ P₁ gN (interIdx gN n m) = Xenum P₀ P₁ gN n ∩ Xenum P₀ P₁ gN m

interIdx codes the intersection whenever it is non-empty (and the result is in the enumeration).

def Domain.Neighborhood.consPairChar (gN : ℕ → ℕ) (n m : ℕ) : ℕ

The {0,1} characteristic function of Scott's consistency relation (ii) for the function space: ∃ k, Xenum k ⊆ Xenum n ∩ Xenum m.

Equations

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

theorem Domain.Neighborhood.consPairChar_spec {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) (gN : ℕ → ℕ) (hgN : ∀ (c : ℕ), gN c = 1 ↔ (stepFun (funListOf P₀ P₁ (Recursive.decodeList c))).Nonempty) (n m : ℕ) : consPairChar gN n m = 1 ↔ ∃ (k : ℕ), Xenum P₀ P₁ gN k ⊆ Xenum P₀ P₁ gN n ∩ Xenum P₀ P₁ gN m

theorem Domain.Neighborhood.primrec_consPairChar (gN : ℕ → ℕ) (hgNp : Nat.Primrec gN) : Nat.Primrec fun (t : ℕ) => consPairChar gN (Nat.unpair t).1 (Nat.unpair t).2

theorem Domain.Neighborhood.primrec_interIdx (gN : ℕ → ℕ) (hgNp : Nat.Primrec gN) : Nat.Primrec fun (t : ℕ) => interIdx gN (Nat.unpair t).1 (Nat.unpair t).2

The equality decider eqEnumChar and Scott's relation (i) interEqChar.

theorem Domain.Neighborhood.selectFn_mul_iff (c d : ℕ) : Recursive.selectFn c d 0 = 1 ↔ c = 1 ∧ d = 1

selectFn c d 0 = 1 decides the conjunction c = 1 ∧ d = 1.

def Domain.Neighborhood.eqEnumChar {β : Type u_2} {V₁ : NeighborhoodSystem β} (P₁ : ComputablePresentation V₁) (gN incl0 incl1 eq1 : ℕ → ℕ) (a b : ℕ) : ℕ

The {0,1} characteristic function of Xenum a = Xenum b. Both consistent → inclusion both ways (subChar); one consistent, one junk (univ) → the consistent side is the trivial neighbourhood (trivialChar); both junk → equal.

Equations

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

theorem Domain.Neighborhood.eqEnumChar_spec {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) (gN incl0 incl1 eq1 : ℕ → ℕ) (hgN : ∀ (c : ℕ), gN c = 1 ↔ (stepFun (funListOf P₀ P₁ (Recursive.decodeList c))).Nonempty) (hincl0 : ∀ (s : ℕ), incl0 s = 1 ↔ P₀.X (Nat.unpair s).1 ⊆ P₀.X (Nat.unpair s).2) (hincl1 : ∀ (s : ℕ), incl1 s = 1 ↔ P₁.X (Nat.unpair s).1 ⊆ P₁.X (Nat.unpair s).2) (heq1 : ∀ (s : ℕ), eq1 s = 1 ↔ P₁.X (Nat.unpair s).1 = P₁.X (Nat.unpair s).2) (a b : ℕ) : eqEnumChar P₁ gN incl0 incl1 eq1 a b = 1 ↔ Xenum P₀ P₁ gN a = Xenum P₀ P₁ gN b

theorem Domain.Neighborhood.primrec_eqEnumChar {β : Type u_2} {V₁ : NeighborhoodSystem β} (P₁ : ComputablePresentation V₁) (gN incl0 incl1 eq1 : ℕ → ℕ) (hgNp : Nat.Primrec gN) (hincl0p : Nat.Primrec incl0) (hincl1p : Nat.Primrec incl1) (heq1p : Nat.Primrec eq1) : Nat.Primrec fun (t : ℕ) => eqEnumChar P₁ gN incl0 incl1 eq1 (Nat.unpair t).1 (Nat.unpair t).2

def Domain.Neighborhood.interEqChar {β : Type u_2} {V₁ : NeighborhoodSystem β} (P₁ : ComputablePresentation V₁) (gN incl0 incl1 eq1 : ℕ → ℕ) (n m k : ℕ) : ℕ

The {0,1} characteristic function of Scott's relation (i) for the function space: Xenum n ∩ Xenum m = Xenum k.

Equations

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

theorem Domain.Neighborhood.interEqChar_spec {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) (gN incl0 incl1 eq1 : ℕ → ℕ) (hgN : ∀ (c : ℕ), gN c = 1 ↔ (stepFun (funListOf P₀ P₁ (Recursive.decodeList c))).Nonempty) (hincl0 : ∀ (s : ℕ), incl0 s = 1 ↔ P₀.X (Nat.unpair s).1 ⊆ P₀.X (Nat.unpair s).2) (hincl1 : ∀ (s : ℕ), incl1 s = 1 ↔ P₁.X (Nat.unpair s).1 ⊆ P₁.X (Nat.unpair s).2) (heq1 : ∀ (s : ℕ), eq1 s = 1 ↔ P₁.X (Nat.unpair s).1 = P₁.X (Nat.unpair s).2) (n m k : ℕ) : interEqChar P₁ gN incl0 incl1 eq1 n m k = 1 ↔ Xenum P₀ P₁ gN n ∩ Xenum P₀ P₁ gN m = Xenum P₀ P₁ gN k

theorem Domain.Neighborhood.primrec_interEqChar {β : Type u_2} {V₁ : NeighborhoodSystem β} (P₁ : ComputablePresentation V₁) (gN incl0 incl1 eq1 : ℕ → ℕ) (hgNp : Nat.Primrec gN) (hincl0p : Nat.Primrec incl0) (hincl1p : Nat.Primrec incl1) (heq1p : Nat.Primrec eq1) : Nat.Primrec fun (t : ℕ) => interEqChar P₁ gN incl0 incl1 eq1 (Nat.unpair t).1 (Nat.unpair (Nat.unpair t).2).1 (Nat.unpair (Nat.unpair t).2).2

Milestone 6 — assembling the function-space presentation.

Theorem 7.5 (existence part): (𝒟₀ → 𝒟₁) is effectively given. We package the deciders above into a ComputablePresentation (funSpace V₀ V₁), with X = Xenum, inter = interIdx and masterIdx = 0 (the empty step-list, whose neighbourhood is univ = Δ). The concrete characteristic functions are obtained choice-free from the component presentations' relations inside the Nonempty proof of funSpace_isEffectivelyGiven (extraction into a Prop goal needs no choice).

theorem Domain.Neighborhood.exists_funListOf {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) {L : List (Set α × Set β)} (hL : ∀ p ∈ L, V₀.mem p.1 ∧ V₁.mem p.2) : ∃ (el : List ℕ), funListOf P₀ P₁ el = L

Every valid finite step-list is funListOf of some entry-list (choice-free: Exists.elim of P₀.surj/P₁.surj, entry by entry).

def Domain.Neighborhood.funPresentation {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) (gN incl0 incl1 eq1 : ℕ → ℕ) (hgN : ∀ (c : ℕ), gN c = 1 ↔ (stepFun (funListOf P₀ P₁ (Recursive.decodeList c))).Nonempty) (hgNp : Nat.Primrec gN) (hincl0 : ∀ (s : ℕ), incl0 s = 1 ↔ P₀.X (Nat.unpair s).1 ⊆ P₀.X (Nat.unpair s).2) (hincl0p : Nat.Primrec incl0) (hincl1 : ∀ (s : ℕ), incl1 s = 1 ↔ P₁.X (Nat.unpair s).1 ⊆ P₁.X (Nat.unpair s).2) (hincl1p : Nat.Primrec incl1) (heq1 : ∀ (s : ℕ), eq1 s = 1 ↔ P₁.X (Nat.unpair s).1 = P₁.X (Nat.unpair s).2) (heq1p : Nat.Primrec eq1) : ComputablePresentation (funSpace V₀ V₁)

The function-space presentation. Built from explicit characteristic functions for the component presentations' relations (gN = function-space consistency, incl0/incl1 = inclusion, eq1 = equality), so it is choice-free given those concrete functions.

Equations

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

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

Theorem 7.5 (existence part) (Scott 1981, PRG-19). If 𝒟₀ and 𝒟₁ are effectively given, then so is the function space (𝒟₀ → 𝒟₁). Choice-free.

Milestone 8 — computable elements of (𝒟₀ → 𝒟₁) are exactly the

computable maps.

Scott (Theorem 7.5): "The computable elements f ∈ |𝒟₀ → 𝒟₁| are exactly the computable maps f : 𝒟₀ → 𝒟₁." Under the completeness isomorphism toApproxMap (Theorem 3.10), a filter φ of the function space corresponds to the approximable map f̂ = toApproxMap φ, and φ.mem [X, Y] ↔ X f̂ Y. The enumeration Xenum c of a consistent code is the finite intersection ⋂[X₀_{eᵢ}, X₁_{eᵢ}], so φ ∋ Xenum c ↔ ∀ eᵢ, φ ∋ [X₀_{eᵢ}, X₁_{eᵢ}] (the generation lemma mem_stepFun_iff); junk codes map to univ, always in φ. Hence the element index set {c ∣ Xenum c ∈ φ} is r.e. iff the single-step relation {⟨n,m⟩ ∣ [X₀ₙ, X₁ₘ] ∈ φ} is — the map's neighbourhood relation. The map ⟹ element half is the choice-free bounded-∀ over a coded list closure REPred.forall_mem_decodeList.

theorem Domain.Neighborhood.mem_Xenum_iff {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) (gN : ℕ → ℕ) (φ : (funSpace V₀ V₁).Element) (c : ℕ) : φ.mem (Xenum P₀ P₁ gN c) ↔ gN c = 1 → ∀ e ∈ Recursive.decodeList c, φ.mem (step (P₀.X (Nat.unpair e).1) (P₁.X (Nat.unpair e).2))

Bridge. φ ∋ Xenum c iff, when c is consistent, φ contains every constituent step.

theorem Domain.Neighborhood.Xenum_isComputableElement_iff {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) (gN : ℕ → ℕ) (hgNp : Nat.Primrec gN) (hgN : ∀ (c : ℕ), gN c = 1 ↔ (stepFun (funListOf P₀ P₁ (Recursive.decodeList c))).Nonempty) (φ : (funSpace V₀ V₁).Element) : (Recursive.REPred fun (c : ℕ) => φ.mem (Xenum P₀ P₁ gN c)) ↔ IsComputableMap P₀ P₁ (toApproxMap φ)

Theorem 7.5 (Scott 1981, PRG-19) — computable elements = computable maps (choice-free). For the function-space enumeration Xenum built from a consistency char gN, an element φ has an r.e. index set iff the corresponding approximable map toApproxMap φ is computable.

theorem Domain.Neighborhood.isComputableElement_funPresentation_iff {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) (gN incl0 incl1 eq1 : ℕ → ℕ) (hgN : ∀ (c : ℕ), gN c = 1 ↔ (stepFun (funListOf P₀ P₁ (Recursive.decodeList c))).Nonempty) (hgNp : Nat.Primrec gN) (hincl0 : ∀ (s : ℕ), incl0 s = 1 ↔ P₀.X (Nat.unpair s).1 ⊆ P₀.X (Nat.unpair s).2) (hincl0p : Nat.Primrec incl0) (hincl1 : ∀ (s : ℕ), incl1 s = 1 ↔ P₁.X (Nat.unpair s).1 ⊆ P₁.X (Nat.unpair s).2) (hincl1p : Nat.Primrec incl1) (heq1 : ∀ (s : ℕ), eq1 s = 1 ↔ P₁.X (Nat.unpair s).1 = P₁.X (Nat.unpair s).2) (heq1p : Nat.Primrec eq1) (φ : (funSpace V₀ V₁).Element) : IsComputableElement (funPresentation P₀ P₁ gN incl0 incl1 eq1 hgN hgNp hincl0 hincl0p hincl1 hincl1p heq1 heq1p) φ ↔ IsComputableMap P₀ P₁ (toApproxMap φ)

Theorem 7.5 (Scott 1981, PRG-19), packaged for funPresentation. An element of the function-space presentation is a computable element iff it is (the filter of) a computable map.

Milestone 7 — eval is computable.

Scott (Theorem 7.5): "The combinators eval and curry are computable, provided all the domains involved are effectively given." The evaluation map eval : (𝒟₀ → 𝒟₁) × 𝒟₀ → 𝒟₁ sends (F, X) to Y iff every map f ∈ F relates X to Y (Theorem 3.11), i.e. F ⊆ [X, Y] (the step neighbourhood, viewed as the set of maps relating X to Y). On the product presentation prodPresentation funPresentation P₀, the neighbourhood at index k is Xenum_{k.1} × X₀_{k.2}, so

(Xenum c, X₀ⱼ) eval Y₁ₘ ↔ Xenum c ⊆ [X₀ⱼ, Y₁ₘ].

The single step [X₀ⱼ, Y₁ₘ] is itself a one-entry function-space neighbourhood — Xenum of the (always consistent) code ⟨⟨j, m⟩, 0⟩ + 1 — so the relation is exactly the decidable function-space inclusion funPresentation.incl_computable, re-indexed by a primitive-recursive code map. This is Scott's observation that eval is a recursive set; r.e.-ness (hence computability) and choice-freeness follow.

theorem Domain.Neighborhood.Xenum_singleton {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) (gN : ℕ → ℕ) (hgN : ∀ (c : ℕ), gN c = 1 ↔ (stepFun (funListOf P₀ P₁ (Recursive.decodeList c))).Nonempty) (j m : ℕ) : Xenum P₀ P₁ gN (Nat.pair (Nat.pair j m) 0 + 1) = step (P₀.X j) (P₁.X m)

The step neighbourhood [X₀ⱼ, Y₁ₘ] as a one-entry Xenum. The code ⟨⟨j, m⟩, 0⟩ + 1 decodes to the singleton entry-list [⟨j, m⟩], which is always consistent (the step map itself is a witness), so Xenum of it is stepFun [(X₀ⱼ, Y₁ₘ)] = [X₀ⱼ, Y₁ₘ].

theorem Domain.Neighborhood.evalMap_rel_prodNbhd_iff {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {F : Set (ApproximableMap V₀ V₁)} (hF : (funSpace V₀ V₁).mem F) {X : Set α} (hX : V₀.mem X) {Y : Set β} (hY : V₁.mem Y) : (evalMap V₀ V₁).rel (prodNbhd F X) Y ↔ F ⊆ step X Y

Evaluation against a product neighbourhood. (F, X) eval Y ↔ F ⊆ [X, Y], for any function-space neighbourhood F and basic neighbourhoods X, Y: every map in F relates X to Y exactly when F is contained in the step set [X, Y] = {f ∣ f X Y}.

theorem Domain.Neighborhood.evalMap_isComputable {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) (gN incl0 incl1 eq1 : ℕ → ℕ) (hgN : ∀ (c : ℕ), gN c = 1 ↔ (stepFun (funListOf P₀ P₁ (Recursive.decodeList c))).Nonempty) (hgNp : Nat.Primrec gN) (hincl0 : ∀ (s : ℕ), incl0 s = 1 ↔ P₀.X (Nat.unpair s).1 ⊆ P₀.X (Nat.unpair s).2) (hincl0p : Nat.Primrec incl0) (hincl1 : ∀ (s : ℕ), incl1 s = 1 ↔ P₁.X (Nat.unpair s).1 ⊆ P₁.X (Nat.unpair s).2) (hincl1p : Nat.Primrec incl1) (heq1 : ∀ (s : ℕ), eq1 s = 1 ↔ P₁.X (Nat.unpair s).1 = P₁.X (Nat.unpair s).2) (heq1p : Nat.Primrec eq1) : IsComputableMap (prodPresentation (funPresentation P₀ P₁ gN incl0 incl1 eq1 hgN hgNp hincl0 hincl0p hincl1 hincl1p heq1 heq1p) P₀) P₁ (evalMap V₀ V₁)

Theorem 7.5 (Scott 1981, PRG-19) — eval is computable (choice-free). Relative to the function-space presentation funPresentation (and the product/codomain presentations), the evaluation map eval : (𝒟₀ → 𝒟₁) × 𝒟₀ → 𝒟₁ is computable: its neighbourhood relation is the recursively decidable function-space inclusion Xenum c ⊆ [X₀ⱼ, Y₁ₘ], hence recursively enumerable.

Milestone 9 — curry is computable.

Scott (Theorem 7.5): "The combinators eval and curry are computable." For a map g : 𝒟₀ × 𝒟₁ → 𝒟₂, curry g : 𝒟₀ → (𝒟₁ → 𝒟₂) sends X to the (filter generated by the) section map gᴬ = gSection g X, with gᴬ Y Z ↔ X ∪ Y g Z (Theorem 3.12). On the codomain presentation funPresentation P₁ P₂, (X₀ₙ) curry(g) (Xenum c) holds iff the section map lies in Xenum c, i.e. (for consistent c) ∀ ⟨j, k⟩ ∈ decodeList c, X₀ₙ ∪ X₁ⱼ g X₂ₖ — a bounded ∀ over the coded list, with the 𝒟₀-parameter n of the r.e. relation of g. This is r.e. by the parameterised closure REPred.forall_mem_decodeList₂; junk codes go to univ (always satisfied). Choice-free.

theorem Domain.Neighborhood.mem_Xenum_iff_map {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) (gN : ℕ → ℕ) (f : ApproximableMap V₀ V₁) (c : ℕ) : f ∈ Xenum P₀ P₁ gN c ↔ gN c = 1 → ∀ e ∈ Recursive.decodeList c, f.rel (P₀.X (Nat.unpair e).1) (P₁.X (Nat.unpair e).2)

Membership in Xenum for a single map. A map f lies in Xenum c iff (when c is consistent) it relates every coded step ⟨X₀ᵢ, X₁ⱼ⟩; junk codes give univ. (The single-map analogue of mem_Xenum_iff.)

theorem Domain.Neighborhood.curry_rel_Xenum_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) {V₂ : NeighborhoodSystem γ} (P₂ : ComputablePresentation V₂) (gN : ℕ → ℕ) (hgN : ∀ (c : ℕ), gN c = 1 ↔ (stepFun (funListOf P₁ P₂ (Recursive.decodeList c))).Nonempty) (g : ApproximableMap (prod V₀ V₁) V₂) (n c : ℕ) : (curry g).rel (P₀.X n) (Xenum P₁ P₂ gN c) ↔ gN c = 1 → ∀ e ∈ Recursive.decodeList c, g.rel (prodNbhd (P₀.X n) (P₁.X (Nat.unpair e).1)) (P₂.X (Nat.unpair e).2)

Bridge for curry. (X₀ₙ) curry(g) (Xenum c) iff, when c is consistent, g relates X₀ₙ ∪ X₁_{e.1} to X₂_{e.2} for every coded entry e.

theorem Domain.Neighborhood.curry_isComputable {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (P₀ : ComputablePresentation V₀) (P₁ : ComputablePresentation V₁) {V₂ : NeighborhoodSystem γ} (P₂ : ComputablePresentation V₂) (gN incl0 incl1 eq1 : ℕ → ℕ) (hgN : ∀ (c : ℕ), gN c = 1 ↔ (stepFun (funListOf P₁ P₂ (Recursive.decodeList c))).Nonempty) (hgNp : Nat.Primrec gN) (hincl0 : ∀ (s : ℕ), incl0 s = 1 ↔ P₁.X (Nat.unpair s).1 ⊆ P₁.X (Nat.unpair s).2) (hincl0p : Nat.Primrec incl0) (hincl1 : ∀ (s : ℕ), incl1 s = 1 ↔ P₂.X (Nat.unpair s).1 ⊆ P₂.X (Nat.unpair s).2) (hincl1p : Nat.Primrec incl1) (heq1 : ∀ (s : ℕ), eq1 s = 1 ↔ P₂.X (Nat.unpair s).1 = P₂.X (Nat.unpair s).2) (heq1p : Nat.Primrec eq1) {g : ApproximableMap (prod V₀ V₁) V₂} (hg : IsComputableMap (prodPresentation P₀ P₁) P₂ g) : IsComputableMap P₀ (funPresentation P₁ P₂ gN incl0 incl1 eq1 hgN hgNp hincl0 hincl0p hincl1 hincl1p heq1 heq1p) (curry g)

Theorem 7.5 (Scott 1981, PRG-19) — curry is computable (choice-free). If g : 𝒟₀ × 𝒟₁ → 𝒟₂ is computable then so is curry g : 𝒟₀ → (𝒟₁ → 𝒟₂): its neighbourhood relation is the parameterised bounded ∀ (REPred.forall_mem_decodeList₂) over the r.e. relation of g, guarded by the decidable consistency flag.