Proposition 7.7 (Scott 1981, PRG-19, §7) — D^§ is effectively given

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

Proposition 7.7. For any effectively given domain D, the domain D^§ is also effectively given, and all the combinators of Example 6.1 prove to be computable.

Scott transposes everything back to ℕ and gives the enumeration of D^§ (Example 6.1's tree algebra, Example61.Dsharp) by a course-of-values recursion. In our model D^§ lives over List Bool × α (Example 6.1), so the enumeration is V : ℕ → Set (List Bool × α):

• V 0 = Γ (the master neighbourhood of D^§);
• V (2n+1) = 0·Xₙ (embZero of the n-th D-neighbourhood Xₙ = P.X n);
• V (2n+2) = 1·V_{p n} ∪ 2·V_{q n} (embPair of two earlier neighbourhoods).

Here p n = n.unpair.1 and q n = n.unpair.2 are Scott's p, q (inverse pairing): both are ≤ n, hence the subscripts p n, q n of V_{2n+2} are < 2n+2, so the recursion is well-founded and membership stays recursive — exactly Scott's observation.

This file builds the construction in milestones:

• Foundational layer (this commit): Vsharp and its core math — mem_X (each V k ∈ 𝒟^§), surj (every 𝒟^§-neighbourhood is some V k), nonemptiness. All choice-free.

A left bound for Nat.unpair (local, to keep Recursive.lean's cache

warm).

theorem Domain.Neighborhood.Proposition77.unpair_fst_le (n : ℕ) : (Nat.unpair n).1 ≤ n

n.unpair.1 ≤ n (choice-free); the decreasing measure for Vsharp's left child.

theorem Domain.Neighborhood.Proposition77.nat_shape (n : ℕ) : n = 0 ∨ (∃ (a : ℕ), n = 2 * a + 1) ∨ ∃ (a : ℕ), n = 2 * a + 2

The three index shapes: 0 (master Γ), 2a+1 (leaf), 2a+2 (node). Choice-free.

Nat.pair is strictly monotone on strict componentwise order.

Needed so the node∩node recursive child code pair (a.1) (b.1) is < pair (2a+2) (2b+2), hence present in the memo table. Proof via max² ≤ pair _ _ < (max+1)².

theorem Domain.Neighborhood.Proposition77.pair_lt_pair_of_lt {x y i j : ℕ} (hx : x < i) (hy : y < j) : Nat.pair x y < Nat.pair i j

The enumeration V : ℕ → 𝒫(List Bool × α).

@[irreducible]

def Domain.Neighborhood.Proposition77.Vsharp {α : Type u_1} (D : NeighborhoodSystem α) (P : ComputablePresentation D) : ℕ → Set (List Bool × α)

Proposition 7.7 (Scott 1981, PRG-19). Scott's enumeration of D^§: V₀ = Γ, V_{2n+1} = 0·Xₙ, V_{2n+2} = 1·V_{p n} ∪ 2·V_{q n} (p = unpair.1, q = unpair.2).

Equations

• One or more equations did not get rendered due to their size.
• Domain.Neighborhood.Proposition77.Vsharp D P 0 = Domain.Neighborhood.Example61.Gamma D

theorem Domain.Neighborhood.Proposition77.Vsharp_zero {α : Type u_1} {D : NeighborhoodSystem α} (P : ComputablePresentation D) : Vsharp D P 0 = Example61.Gamma D

theorem Domain.Neighborhood.Proposition77.Vsharp_succ {α : Type u_1} {D : NeighborhoodSystem α} (P : ComputablePresentation D) (k : ℕ) : Vsharp D P (k + 1) = if (k + 1) % 2 = 1 then Example61.embZero (P.X (k / 2)) else Example61.embPair (Vsharp D P (Nat.unpair ((k - 1) / 2)).1) (Vsharp D P (Nat.unpair ((k - 1) / 2)).2)

One-step unfolding of Vsharp at a successor index.

theorem Domain.Neighborhood.Proposition77.Vsharp_odd {α : Type u_1} {D : NeighborhoodSystem α} (P : ComputablePresentation D) (n : ℕ) : Vsharp D P (2 * n + 1) = Example61.embZero (P.X n)

theorem Domain.Neighborhood.Proposition77.Vsharp_even {α : Type u_1} {D : NeighborhoodSystem α} (P : ComputablePresentation D) (n : ℕ) : Vsharp D P (2 * n + 2) = Example61.embPair (Vsharp D P (Nat.unpair n).1) (Vsharp D P (Nat.unpair n).2)

mem_X, surj, nonemptiness.

theorem Domain.Neighborhood.Proposition77.Vsharp_mem {α : Type u_1} {D : NeighborhoodSystem α} (P : ComputablePresentation D) (k : ℕ) : Example61.MemS D (Vsharp D P k)

Every V k is a neighbourhood of D^§.

theorem Domain.Neighborhood.Proposition77.Vsharp_surj {α : Type u_1} {D : NeighborhoodSystem α} (P : ComputablePresentation D) {W : Set (List Bool × α)} (hW : Example61.MemS D W) : ∃ (k : ℕ), Vsharp D P k = W

Every neighbourhood of D^§ is enumerated as some V k (surjectivity of V).

theorem Domain.Neighborhood.Proposition77.Vsharp_nonempty {α : Type u_1} {D : NeighborhoodSystem α} (P : ComputablePresentation D) (hD : ∀ (X : Set α), D.mem X → X.Nonempty) (k : ℕ) : (Vsharp D P k).Nonempty

Under ∅ ∉ 𝒟, no V k is empty.

Per-parity intersection identities.

These are the choice-free heart of Scott's "the reader has to check that 7.1(i)–(ii) hold for the Vₖ. The idea is that any such check is either (1) trivial, or (2) something already assumed about D and the Xₙ, or (3) can be thrown back to some sets Vₘ with strictly smaller subscripts."

• V₀ = Γ is the identity for ∩ (cases (1));
• odd ∩ odd reduces to D's own intersection Xₐ ∩ X_b (case (2));
• odd ∩ even (and even ∩ odd) are ∅ — inconsistent (case (1), and ∅ ∉ 𝒟^§);
• even ∩ even is embPair of the component intersections, whose subscripts unpair.1 / unpair.2 are strictly smaller (case (3)).

theorem Domain.Neighborhood.Proposition77.Vsharp_zero_inter {α : Type u_1} {D : NeighborhoodSystem α} (P : ComputablePresentation D) (m : ℕ) : Vsharp D P 0 ∩ Vsharp D P m = Vsharp D P m

theorem Domain.Neighborhood.Proposition77.Vsharp_inter_zero {α : Type u_1} {D : NeighborhoodSystem α} (P : ComputablePresentation D) (n : ℕ) : Vsharp D P n ∩ Vsharp D P 0 = Vsharp D P n

theorem Domain.Neighborhood.Proposition77.Vsharp_odd_inter_odd {α : Type u_1} {D : NeighborhoodSystem α} (P : ComputablePresentation D) (a b : ℕ) : Vsharp D P (2 * a + 1) ∩ Vsharp D P (2 * b + 1) = Example61.embZero (P.X a ∩ P.X b)

theorem Domain.Neighborhood.Proposition77.Vsharp_odd_inter_even {α : Type u_1} {D : NeighborhoodSystem α} (P : ComputablePresentation D) (a b : ℕ) : Vsharp D P (2 * a + 1) ∩ Vsharp D P (2 * b + 2) = ∅

theorem Domain.Neighborhood.Proposition77.Vsharp_even_inter_odd {α : Type u_1} {D : NeighborhoodSystem α} (P : ComputablePresentation D) (a b : ℕ) : Vsharp D P (2 * a + 2) ∩ Vsharp D P (2 * b + 1) = ∅

theorem Domain.Neighborhood.Proposition77.Vsharp_even_inter_even {α : Type u_1} {D : NeighborhoodSystem α} (P : ComputablePresentation D) (a b : ℕ) : Vsharp D P (2 * a + 2) ∩ Vsharp D P (2 * b + 2) = Example61.embPair (Vsharp D P (Nat.unpair a).1 ∩ Vsharp D P (Nat.unpair b).1) (Vsharp D P (Nat.unpair a).2 ∩ Vsharp D P (Nat.unpair b).2)

MemS-subset inversions and the consistency-via-subset equivalences.

A nonempty D^§-neighbourhood contained in embZero Y must itself be an embZero (its tokens have empty {1,2}-path); contained in embPair A B, an embPair. These give the bridge between Scott's consistency relation on D^§ (∃ l, V_l ⊆ V_n ∩ V_m) and the recursive sub-checks: embZero consistency reduces to D's, and embPair consistency to the two components'.

theorem Domain.Neighborhood.Proposition77.memS_sub_embZero {α : Type u_1} {D : NeighborhoodSystem α} (hD : ∀ (X : Set α), D.mem X → X.Nonempty) {W : Set (List Bool × α)} {Y : Set α} (hW : Example61.MemS D W) (hsub : W ⊆ Example61.embZero Y) : ∃ (Z : Set α), D.mem Z ∧ W = Example61.embZero Z

theorem Domain.Neighborhood.Proposition77.memS_sub_embPair {α : Type u_1} {D : NeighborhoodSystem α} (hD : ∀ (X : Set α), D.mem X → X.Nonempty) {W A B : Set (List Bool × α)} (hW : Example61.MemS D W) (hsub : W ⊆ Example61.embPair A B) : ∃ (Pp : Set (List Bool × α)) (Qq : Set (List Bool × α)), Example61.MemS D Pp ∧ Example61.MemS D Qq ∧ W = Example61.embPair Pp Qq

theorem Domain.Neighborhood.Proposition77.exists_sub_embZero_iff {α : Type u_1} {D : NeighborhoodSystem α} (P : ComputablePresentation D) (hD : ∀ (X : Set α), D.mem X → X.Nonempty) (Y : Set α) : (∃ (l : ℕ), Vsharp D P l ⊆ Example61.embZero Y) ↔ ∃ (k : ℕ), P.X k ⊆ Y

theorem Domain.Neighborhood.Proposition77.exists_sub_embPair_iff {α : Type u_1} {D : NeighborhoodSystem α} (P : ComputablePresentation D) (hD : ∀ (X : Set α), D.mem X → X.Nonempty) (A B : Set (List Bool × α)) : (∃ (l : ℕ), Vsharp D P l ⊆ Example61.embPair A B) ↔ (∃ (l : ℕ), Vsharp D P l ⊆ A) ∧ ∃ (l : ℕ), Vsharp D P l ⊆ B

theorem Domain.Neighborhood.Proposition77.Vsharp_eq_Gamma_iff {α : Type u_1} {D : NeighborhoodSystem α} (P : ComputablePresentation D) (hD : ∀ (X : Set α), D.mem X → X.Nonempty) (j : ℕ) : Vsharp D P j = Example61.Gamma D ↔ j = 0

A primitive-recursive course-of-values memo evaluator.

The D^§ deciders (cons, inter, equality) recurse on the index trees: e.g. inter(2a+2, 2b+2) recurses on inter(a.1, b.1) and inter(a.2, b.2). The combined measure w = Nat.pair n m strictly decreases on every recursive call, so each decider is a unary course-of-values recursion on w. We realise course-of-values by a primitive-recursive memo table: rtbl step w codes the reverse list [g(w-1), …, g 0] (g v = step (pair v (table for v))), built by a single Nat.Primrec.prec whose step is a cons. To read g v for v < w inside step, we look up position w-1-v of the reverse table via listGet. All choice-free.

def Domain.Neighborhood.Proposition77.listGetStp (t : ℕ) : ℕ

One step of the list-indexing fold: state pair countdown value; capture the current element when countdown = 1, else carry the value and decrement.

Equations

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

def Domain.Neighborhood.Proposition77.listGet (c i : ℕ) : ℕ

listGet c i = (decodeList c).getD i 0: the i-th entry of the list coded by c.

Equations

• Domain.Neighborhood.Proposition77.listGet c i = (Nat.unpair (Domain.Recursive.foldCode Domain.Neighborhood.Proposition77.listGetStp 0 (Nat.pair (i + 1) 0) c)).2

theorem Domain.Neighborhood.Proposition77.listGet_encodeList (l : List ℕ) (i : ℕ) : listGet (Recursive.encodeList l) i = l.getD i 0

Correctness of listGet on a coded list.

theorem Domain.Neighborhood.Proposition77.primrec_listGet : Nat.Primrec fun (p : ℕ) => listGet (Nat.unpair p).1 (Nat.unpair p).2

listGet is primitive recursive (on the Nat.pair coding of c, i).

def Domain.Neighborhood.Proposition77.rtbl (step : ℕ → ℕ) : ℕ → ℕ

The reverse memo table: rtbl step w codes [g(w-1), …, g 0].

Equations

• Domain.Neighborhood.Proposition77.rtbl step 0 = 0
• Domain.Neighborhood.Proposition77.rtbl step k.succ = Nat.pair (step (Nat.pair k (Domain.Neighborhood.Proposition77.rtbl step k))) (Domain.Neighborhood.Proposition77.rtbl step k) + 1

def Domain.Neighborhood.Proposition77.gOf (step : ℕ → ℕ) (w : ℕ) : ℕ

The course-of-values value at w: g w = step (pair w (table of g below w)).

Equations

• Domain.Neighborhood.Proposition77.gOf step w = step (Nat.pair w (Domain.Neighborhood.Proposition77.rtbl step w))

theorem Domain.Neighborhood.Proposition77.gOf_def (step : ℕ → ℕ) (w : ℕ) : gOf step w = step (Nat.pair w (rtbl step w))

def Domain.Neighborhood.Proposition77.gList (step : ℕ → ℕ) : ℕ → List ℕ

The reverse list of memo values [g(w-1), …, g 0].

Equations

• Domain.Neighborhood.Proposition77.gList step 0 = []
• Domain.Neighborhood.Proposition77.gList step k.succ = Domain.Neighborhood.Proposition77.gOf step k :: Domain.Neighborhood.Proposition77.gList step k

theorem Domain.Neighborhood.Proposition77.rtbl_eq_encode (step : ℕ → ℕ) (w : ℕ) : rtbl step w = Recursive.encodeList (gList step w)

theorem Domain.Neighborhood.Proposition77.gList_length (step : ℕ → ℕ) (w : ℕ) : (gList step w).length = w

theorem Domain.Neighborhood.Proposition77.getD_gList (step : ℕ → ℕ) (w p : ℕ) : p < w → (gList step w).getD p 0 = gOf step (w - 1 - p)

theorem Domain.Neighborhood.Proposition77.listGet_rtbl (step : ℕ → ℕ) {v w : ℕ} (hv : v < w) : listGet (rtbl step w) (w - 1 - v) = gOf step v

The course-of-values lookup. Inside step at w, position w-1-v of the reverse table is exactly g v, for any earlier v < w.

theorem Domain.Neighborhood.Proposition77.primrec_rtbl {step : ℕ → ℕ} (hstep : Nat.Primrec step) : Nat.Primrec (rtbl step)

rtbl step is primitive recursive when step is (a single prec whose step is a cons).

theorem Domain.Neighborhood.Proposition77.primrec_gOf {step : ℕ → ℕ} (hstep : Nat.Primrec step) : Nat.Primrec (gOf step)

gOf step is primitive recursive when step is.

theorem Domain.Neighborhood.Proposition77.primrec_listGet₂ {c i : ℕ → ℕ} (hc : Nat.Primrec c) (hi : Nat.Primrec i) : Nat.Primrec fun (p : ℕ) => listGet (c p) (i p)

listGet as a binary primrec composite.

The combined D^§ decider step (eq/cons/inter triple).

All three D^§ deciders recurse the same way on (i, j), so we compute them together as a packed triple packT eqBit consBit interIdx. The step dsharpStep fcons feq finter is fed Scott's three D-level primitive-recursive functions: fcons/feq are the extracted {0,1} characteristic functions of P.cons_computable/P.eq_computable, and finter is P.inter (on Nat.pair codes). The combined index is w = Nat.pair i j; in the node∩node case the children's results are read from the memo table by listGet.

def Domain.Neighborhood.Proposition77.packT (e c ii : ℕ) : ℕ

Pack the triple (eqBit, consBit, interIdx) into one natural.

Equations

• Domain.Neighborhood.Proposition77.packT e c ii = Nat.pair e (Nat.pair c ii)

def Domain.Neighborhood.Proposition77.eqB (r : ℕ) : ℕ

Equality bit of a packed triple.

Equations

• Domain.Neighborhood.Proposition77.eqB r = (Nat.unpair r).1

def Domain.Neighborhood.Proposition77.consB (r : ℕ) : ℕ

Consistency bit of a packed triple.

Equations

• Domain.Neighborhood.Proposition77.consB r = (Nat.unpair (Nat.unpair r).2).1

def Domain.Neighborhood.Proposition77.intI (r : ℕ) : ℕ

Intersection index of a packed triple.

Equations

• Domain.Neighborhood.Proposition77.intI r = (Nat.unpair (Nat.unpair r).2).2

@[simp]

theorem Domain.Neighborhood.Proposition77.eqB_packT (e c ii : ℕ) : eqB (packT e c ii) = e

@[simp]

theorem Domain.Neighborhood.Proposition77.consB_packT (e c ii : ℕ) : consB (packT e c ii) = c

@[simp]

theorem Domain.Neighborhood.Proposition77.intI_packT (e c ii : ℕ) : intI (packT e c ii) = ii

def Domain.Neighborhood.Proposition77.dsharpStep (fcons feq finter : ℕ → ℕ) (p : ℕ) : ℕ

The D^§ decider step. p = pair (pair i j) tbl. Returns packT eqBit consBit interIdx, case-splitting on i = 0 / j = 0 (the Γ identity), then on parities (leaf 2a+1 vs node 2a+2). Leaf∩leaf delegates to D's deciders; node∩node ANDs/combines the two children read from the memo table tbl.

Equations

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

theorem Domain.Neighborhood.Proposition77.dsharpStep_i0 (fcons feq finter : ℕ → ℕ) (j tbl : ℕ) : dsharpStep fcons feq finter (Nat.pair (Nat.pair 0 j) tbl) = packT (1 - j) 1 j

theorem Domain.Neighborhood.Proposition77.dsharpStep_j0 (fcons feq finter : ℕ → ℕ) {i : ℕ} (tbl : ℕ) (hi : i ≠ 0) : dsharpStep fcons feq finter (Nat.pair (Nat.pair i 0) tbl) = packT (1 - i) 1 i

theorem Domain.Neighborhood.Proposition77.dsharpStep_ll (fcons feq finter : ℕ → ℕ) (a b tbl : ℕ) : dsharpStep fcons feq finter (Nat.pair (Nat.pair (2 * a + 1) (2 * b + 1)) tbl) = packT (feq (Nat.pair a b)) (fcons (Nat.pair a b)) (2 * finter (Nat.pair a b) + 1)

theorem Domain.Neighborhood.Proposition77.dsharpStep_ln (fcons feq finter : ℕ → ℕ) (a b tbl : ℕ) : dsharpStep fcons feq finter (Nat.pair (Nat.pair (2 * a + 1) (2 * b + 2)) tbl) = packT 0 0 0

theorem Domain.Neighborhood.Proposition77.dsharpStep_nl (fcons feq finter : ℕ → ℕ) (a b tbl : ℕ) : dsharpStep fcons feq finter (Nat.pair (Nat.pair (2 * a + 2) (2 * b + 1)) tbl) = packT 0 0 0

theorem Domain.Neighborhood.Proposition77.dsharpStep_nn (fcons feq finter : ℕ → ℕ) (a b tbl : ℕ) : dsharpStep fcons feq finter (Nat.pair (Nat.pair (2 * a + 2) (2 * b + 2)) tbl) = packT (eqB (listGet tbl (Nat.pair (2 * a + 2) (2 * b + 2) - 1 - Nat.pair (Nat.unpair a).1 (Nat.unpair b).1)) * eqB (listGet tbl (Nat.pair (2 * a + 2) (2 * b + 2) - 1 - Nat.pair (Nat.unpair a).2 (Nat.unpair b).2))) (consB (listGet tbl (Nat.pair (2 * a + 2) (2 * b + 2) - 1 - Nat.pair (Nat.unpair a).1 (Nat.unpair b).1)) * consB (listGet tbl (Nat.pair (2 * a + 2) (2 * b + 2) - 1 - Nat.pair (Nat.unpair a).2 (Nat.unpair b).2))) (2 * Nat.pair (intI (listGet tbl (Nat.pair (2 * a + 2) (2 * b + 2) - 1 - Nat.pair (Nat.unpair a).1 (Nat.unpair b).1))) (intI (listGet tbl (Nat.pair (2 * a + 2) (2 * b + 2) - 1 - Nat.pair (Nat.unpair a).2 (Nat.unpair b).2))) + 2)

theorem Domain.Neighborhood.Proposition77.primrec_dsharpStep (fcons feq finter : ℕ → ℕ) (hfcons : Nat.Primrec fcons) (hfeq : Nat.Primrec feq) (hfinter : Nat.Primrec finter) : Nat.Primrec (dsharpStep fcons feq finter)

The decider step is primitive recursive when the D-level functions are.

Correctness of the decider step (strong induction on the combined code).

Given that fcons/feq/finter correctly decide D-consistency / D-equality / D-intersection, the packed triple gOf (dsharpStep …) correctly decides D^§-consistency, computes the D^§-intersection index, and decides D^§-equality. Proved together by strong induction on the combined code Nat.pair i j; the node∩node case recurses to strictly smaller codes (present in the memo table by pair_lt_pair_of_lt).

theorem Domain.Neighborhood.Proposition77.dsharp_decider_spec {α : Type u_1} {D : NeighborhoodSystem α} (P : ComputablePresentation D) (fcons feq finter : ℕ → ℕ) (hD : ∀ (X : Set α), D.mem X → X.Nonempty) (hcons : ∀ (a b : ℕ), fcons (Nat.pair a b) = 1 ↔ ∃ (l : ℕ), P.X l ⊆ P.X a ∩ P.X b) (heq : ∀ (a b : ℕ), feq (Nat.pair a b) = 1 ↔ P.X a = P.X b) (hinter : ∀ (a b : ℕ), (∃ (l : ℕ), P.X l ⊆ P.X a ∩ P.X b) → P.X (finter (Nat.pair a b)) = P.X a ∩ P.X b) (i j : ℕ) : (consB (gOf (dsharpStep fcons feq finter) (Nat.pair i j)) = 1 ↔ ∃ (l : ℕ), Vsharp D P l ⊆ Vsharp D P i ∩ Vsharp D P j) ∧ ((∃ (l : ℕ), Vsharp D P l ⊆ Vsharp D P i ∩ Vsharp D P j) → Vsharp D P (intI (gOf (dsharpStep fcons feq finter) (Nat.pair i j))) = Vsharp D P i ∩ Vsharp D P j) ∧ (eqB (gOf (dsharpStep fcons feq finter) (Nat.pair i j)) = 1 ↔ Vsharp D P i = Vsharp D P j)

theorem Domain.Neighborhood.Proposition77.dsharp_intI_correct {α : Type u_1} {D : NeighborhoodSystem α} (P : ComputablePresentation D) (fcons feq finter : ℕ → ℕ) (hD : ∀ (X : Set α), D.mem X → X.Nonempty) (hinter : ∀ (a b : ℕ), (∃ (l : ℕ), P.X l ⊆ P.X a ∩ P.X b) → P.X (finter (Nat.pair a b)) = P.X a ∩ P.X b) (i j : ℕ) : (∃ (l : ℕ), Vsharp D P l ⊆ Vsharp D P i ∩ Vsharp D P j) → Vsharp D P (intI (gOf (dsharpStep fcons feq finter) (Nat.pair i j))) = Vsharp D P i ∩ Vsharp D P j

Intersection-index correctness in isolation. The intI component of gOf (dsharpStep …) is independent of the eq/cons bits (fcons/feq), so it is correct assuming only that finter correctly intersects in D. This lets the inter data field be built with dummy fcons/feq while staying choice-free.

theorem Domain.Neighborhood.Proposition77.dsharp_interEq_iff {α : Type u_1} {D : NeighborhoodSystem α} (P : ComputablePresentation D) (fcons feq finter : ℕ → ℕ) (hD : ∀ (X : Set α), D.mem X → X.Nonempty) (hcons : ∀ (a b : ℕ), fcons (Nat.pair a b) = 1 ↔ ∃ (l : ℕ), P.X l ⊆ P.X a ∩ P.X b) (heq : ∀ (a b : ℕ), feq (Nat.pair a b) = 1 ↔ P.X a = P.X b) (hinter : ∀ (a b : ℕ), (∃ (l : ℕ), P.X l ⊆ P.X a ∩ P.X b) → P.X (finter (Nat.pair a b)) = P.X a ∩ P.X b) (n m k : ℕ) : Vsharp D P n ∩ Vsharp D P m = Vsharp D P k ↔ consB (gOf (dsharpStep fcons feq finter) (Nat.pair n m)) * eqB (gOf (dsharpStep fcons feq finter) (Nat.pair (intI (gOf (dsharpStep fcons feq finter) (Nat.pair n m))) k)) = 1

Decidability of 7.1(i) for D^§. Vₙ ∩ Vₘ = V_k iff (n,m) is consistent and the computed intersection index agrees with k under D^§-equality. Inconsistency forces the product to 0 (and then Vₙ ∩ Vₘ = ∅ ≠ V_k, since V_k is nonempty), so the single product decider is correct on the nose.

Proposition 7.7: D^§ is effectively given.

Assembling the pieces into a ComputablePresentation (Dsharp D hD). The enumeration is Vsharp; relation 7.1(ii) (consistency) and 7.1(i) (intersection-equality) are decided by the packed-triple deciders; the primitive-recursive intersection function reads the intI component (built with dummy eq/cons bits, which it does not depend on). Choice-free: the Prop fields obtain D's existential deciders, the data fields use only P.inter (data).

def Domain.Neighborhood.Proposition77.dsharpPresentation {α : Type u_1} {D : NeighborhoodSystem α} (P : ComputablePresentation D) (hD : ∀ (X : Set α), D.mem X → X.Nonempty) : ComputablePresentation (Example61.Dsharp D hD)

Proposition 7.7 (Scott 1981, PRG-19). A computable presentation of D^§ from one of D.

Equations

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

theorem Domain.Neighborhood.Proposition77.dsharp_isEffectivelyGiven {α : Type u_1} {D : NeighborhoodSystem α} (P : ComputablePresentation D) (hD : ∀ (X : Set α), D.mem X → X.Nonempty) : (Example61.Dsharp D hD).IsEffectivelyGiven

Proposition 7.7 (Scott 1981, PRG-19). If D is effectively given, so is D^§.