A choice-free recursion theory for Lecture VII (Scott 1981, PRG-19)

Why this file exists — we roll our own and reject mathlib's recursion theory here. Lecture VII ("Computability in effectively given domains") needs the notions recursively decidable and recursively enumerable. mathlib has these (Computable, ComputablePred, REPred, Primrec, Partrec), but in mathlib v4.30.0 essentially every correctness lemma of that development is proved with tactics (grind, lia) or wrapper lemmas that open Classical — e.g. Computable.const, Primrec.const, Nat.unpair_pair, Nat.sqrt_le, and Nat.Primrec.add/mul all audit with Classical.choice in their axiom set. This project's discipline is to keep data (and as much as possible) choice-free (⊆ {propext, Quot.sound}), so we deliberately decline mathlib's classical recursion theory and instead build the slice we need on the genuinely choice-free foundations: the raw inductives Nat.Primrec / Nat.Partrec (whose constructors are choice-free) and Nat.sqrt / Nat.pair / Nat.unpair (whose definitions are choice-free). The only tactic we lean on for arithmetic is omega, which is choice-free here (unlike grind/lia).

The pattern: a relation on integer indices is recursive (decidable) when it has a primitive-recursive characteristic function (Nat.Primrec, lifted to Nat.Partrec for the recursive/REPred analogues). Tuples are encoded with Nat.pair (choice-free), and we reprove the pairing round-trips (unpair_pair', pair_unpair') choice-free here.

Everything in this file is ⊆ {propext, Quot.sound}.

Choice-free Nat.sqrt correctness

mathlib's Nat.sqrt.iter_sq_le / Nat.sqrt.lt_iter_succ_sq are the heart of Nat.sqrt's correctness, but they use grind / lia (classical). We reprove them with omega.

theorem Domain.Recursive.amGM {a b : ℕ} : 4 * a * b ≤ (a + b) * (a + b)

AM–GM for naturals (choice-free). 4 a b ≤ (a+b)². Faithful port of mathlib's private Nat.AM_GM (no classical tactics).

theorem Domain.Recursive.iter_sq_le (n guess : ℕ) : Nat.sqrt.iter n guess * Nat.sqrt.iter n guess ≤ n

Choice-free sqrt.iter lower bound. iter n guess ² ≤ n. Faithful port of Nat.sqrt.iter_sq_le, with grind replaced by omega.

theorem Domain.Recursive.lt_of_mul_lt_mul_left' {a b c : ℕ} (h : a * b < a * c) : b < c

Choice-free left-cancellation for < under * (mathlib's Nat.lt_of_mul_lt_mul_left is classical). From a*b < a*c deduce b < c, by the contrapositive c ≤ b → a*c ≤ a*b.

theorem Domain.Recursive.lt_iter_succ_sq (n guess : ℕ) (hn : n < (guess + 1) * (guess + 1)) : n < (Nat.sqrt.iter n guess + 1) * (Nat.sqrt.iter n guess + 1)

Choice-free sqrt.iter upper bound. If n < (guess+1)² then n < (iter n guess + 1)². Faithful port of Nat.sqrt.lt_iter_succ_sq, with lia replaced by omega.

theorem Domain.Recursive.sqrt_le (n : ℕ) : n.sqrt * n.sqrt ≤ n

sqrt n squared is ≤ n (choice-free; mathlib's Nat.sqrt_le is classical).

theorem Domain.Recursive.lt_succ_sqrt (n : ℕ) : n < (n.sqrt + 1) * (n.sqrt + 1)

n < (sqrt n + 1)² (choice-free; mathlib's Nat.lt_succ_sqrt is classical). The initial guess 2 ^ (log₂ n / 2 + 1) over-shoots √n, which feeds lt_iter_succ_sq.

theorem Domain.Recursive.sqrt_eq_of {m q : ℕ} (h1 : q * q ≤ m) (h2 : m < (q + 1) * (q + 1)) : m.sqrt = q

The square-root characterization (choice-free). If q² ≤ m < (q+1)² then sqrt m = q. The uniqueness step is omega from the two bounds plus sqrt_le/lt_succ_sqrt.

theorem Domain.Recursive.sqrt_add_eq (q a : ℕ) (h : a ≤ q + q) : (q * q + a).sqrt = q

sqrt (q² + a) = q whenever a ≤ 2q (choice-free; mathlib's Nat.sqrt_add_eq is classical).

Choice-free pairing round-trip

Nat.pair/Nat.unpair are themselves choice-free definitions; only mathlib's unpair_pair lemma (via sqrt_add_eq) is classical. We reprove the round-trip on our choice-free sqrt.

theorem Domain.Recursive.unpair_pair (a b : ℕ) : Nat.unpair (Nat.pair a b) = (a, b)

unpair ∘ pair = id (choice-free). Mirrors Nat.unpair_pair.

theorem Domain.Recursive.unpair_pair_fst (a b : ℕ) : (Nat.unpair (Nat.pair a b)).1 = a

First projection of the pairing round-trip.

theorem Domain.Recursive.unpair_pair_snd (a b : ℕ) : (Nat.unpair (Nat.pair a b)).2 = b

Second projection of the pairing round-trip.

theorem Domain.Recursive.sqrt_le_add (n : ℕ) : n ≤ n.sqrt * n.sqrt + n.sqrt + n.sqrt

n ≤ (sqrt n)² + 2·sqrt n (choice-free; needed for pair_unpair).

theorem Domain.Recursive.pair_unpair (n : ℕ) : Nat.pair (Nat.unpair n).1 (Nat.unpair n).2 = n

pair ∘ unpair = id (choice-free). Mirrors Nat.pair_unpair.

Choice-free primitive-recursive arithmetic

mathlib's Nat.Primrec.id/add/mul are proved with by simp, which silently applies the classical @[simp] Nat.unpair_pair; so they audit with Classical.choice. We reprove the few we need using the choice-free round-trips above. The constructors of Nat.Primrec (zero/succ/left/right/pair/comp/prec) are choice-free and used directly.

theorem Domain.Recursive.primrec_id : Nat.Primrec id

id is primitive recursive (choice-free).

theorem Domain.Recursive.primrec_add : Nat.Primrec (Nat.unpaired fun (x1 x2 : ℕ) => x1 + x2)

Addition is primitive recursive (choice-free).

theorem Domain.Recursive.primrec_mul : Nat.Primrec (Nat.unpaired fun (x1 x2 : ℕ) => x1 * x2)

Multiplication is primitive recursive (choice-free).

theorem Domain.Recursive.primrec_pred : Nat.Primrec fun (n : ℕ) => n - 1

Predecessor n ↦ n - 1 is primitive recursive (choice-free; mathlib's Nat.Primrec.pred is classical).

theorem Domain.Recursive.primrec_sub : Nat.Primrec (Nat.unpaired fun (x1 x2 : ℕ) => x1 - x2)

Truncated subtraction is primitive recursive (choice-free; mathlib's Nat.Primrec.sub is classical).

theorem Domain.Recursive.nat_mul_eq_one {a b : ℕ} : a * b = 1 ↔ a = 1 ∧ b = 1

a * b = 1 ↔ a = 1 ∧ b = 1 over ℕ (choice-free; avoids the classical generic mul_eq_one).

Pointwise primitive-recursive arithmetic combinators

primrec_add/mul/sub are Nat.unpaired forms; the ₂ variants below take two primitive recursive functions f, g and build fun n => f n ⋆ g n directly (composing through Nat.pair). These cut the Nat.pair/unpair plumbing in larger constructions (sum's intersection function and the list-fold engine). All choice-free.

theorem Domain.Recursive.primrec_add₂ {f g : ℕ → ℕ} (hf : Nat.Primrec f) (hg : Nat.Primrec g) : Nat.Primrec fun (n : ℕ) => f n + g n

fun n => f n + g n is primitive recursive.

theorem Domain.Recursive.primrec_mul₂ {f g : ℕ → ℕ} (hf : Nat.Primrec f) (hg : Nat.Primrec g) : Nat.Primrec fun (n : ℕ) => f n * g n

fun n => f n * g n is primitive recursive.

theorem Domain.Recursive.primrec_sub₂ {f g : ℕ → ℕ} (hf : Nat.Primrec f) (hg : Nat.Primrec g) : Nat.Primrec fun (n : ℕ) => f n - g n

fun n => f n - g n (truncated) is primitive recursive.

def Domain.Recursive.selectFn (c a b : ℕ) : ℕ

Choice-free primitive-recursive selection: selectFn c a b = a if c = 1, = b if c = 0 (for a {0,1}-valued c), via c * a + (1 - c) * b.

Equations

• Domain.Recursive.selectFn c a b = c * a + (1 - c) * b

@[simp]

theorem Domain.Recursive.selectFn_one (a b : ℕ) : selectFn 1 a b = a

@[simp]

theorem Domain.Recursive.selectFn_zero (a b : ℕ) : selectFn 0 a b = b

theorem Domain.Recursive.primrec_selectFn {c a b : ℕ → ℕ} (hc : Nat.Primrec c) (ha : Nat.Primrec a) (hb : Nat.Primrec b) : Nat.Primrec fun (n : ℕ) => selectFn (c n) (a n) (b n)

selectFn of primitive-recursive c, a, b is primitive recursive.

@[simp]

theorem Domain.Recursive.selectFn_ite {c : Prop} [Decidable c] (a b : ℕ) : selectFn (if c then 1 else 0) a b = if c then a else b

selectFn driven by a decidable test through its {0,1} indicator is an if-then-else.

theorem Domain.Recursive.geTwo_bit (a : ℕ) : 1 - (2 - a) = if 2 ≤ a then 1 else 0

The {0,1} indicator of 2 ≤ a, written via truncated subtraction.

theorem Domain.Recursive.eqZero_bit (a : ℕ) : 1 - a = if a = 0 then 1 else 0

The {0,1} indicator of a = 0, written via truncated subtraction.

"Recursively decidable" predicates (Scott's notion, Definition 7.1)

A predicate is recursively decidable when it has a primitive-recursive {0,1}-valued characteristic function. Tuples are coded by Nat.pair. These are the building blocks Scott's Definition 7.1 needs (relations on indices), and the closure lemmas (of_iff, comp = reindex, and) let us derive the inclusion- and equality-deciders. All choice-free.

def Domain.Recursive.RecDecidable (p : ℕ → Prop) : Prop

A unary predicate p : ℕ → Prop is recursively decidable.

Equations

• Domain.Recursive.RecDecidable p = ∃ (f : ℕ → ℕ), Nat.Primrec f ∧ ∀ (n : ℕ), p n ↔ f n = 1

def Domain.Recursive.RecDecidable₂ (r : ℕ → ℕ → Prop) : Prop

A binary relation is recursively decidable when its Nat.pair-coding is.

Equations

• Domain.Recursive.RecDecidable₂ r = Domain.Recursive.RecDecidable fun (t : ℕ) => r (Nat.unpair t).1 (Nat.unpair t).2

def Domain.Recursive.RecDecidable₃ (r : ℕ → ℕ → ℕ → Prop) : Prop

A ternary relation is recursively decidable when its Nat.pair-coding (pair n (pair m k)) is.

Equations

• Domain.Recursive.RecDecidable₃ r = Domain.Recursive.RecDecidable fun (t : ℕ) => r (Nat.unpair t).1 (Nat.unpair (Nat.unpair t).2).1 (Nat.unpair (Nat.unpair t).2).2

theorem Domain.Recursive.RecDecidable.of_iff {p q : ℕ → Prop} (h : ∀ (n : ℕ), q n ↔ p n) (hp : RecDecidable p) : RecDecidable q

Recursive decidability transfers across a pointwise logical equivalence.

theorem Domain.Recursive.RecDecidable.comp {p : ℕ → Prop} (hp : RecDecidable p) {g : ℕ → ℕ} (hg : Nat.Primrec g) : RecDecidable fun (n : ℕ) => p (g n)

Reindexing. If p is recursively decidable and g is primitive recursive, then fun n => p (g n) is recursively decidable.

theorem Domain.Recursive.RecDecidable.and {p q : ℕ → Prop} (hp : RecDecidable p) (hq : RecDecidable q) : RecDecidable fun (n : ℕ) => p n ∧ q n

Conjunction. Recursive decidability is closed under ∧ (multiply the {0,1} deciders).

theorem Domain.Recursive.recDecidable_of_forall {p : ℕ → Prop} (h : ∀ (n : ℕ), p n) : RecDecidable p

An always-true predicate is recursively decidable (constant decider 1).

theorem Domain.Recursive.RecDecidable.natEq {a b : ℕ → ℕ} (ha : Nat.Primrec a) (hb : Nat.Primrec b) : RecDecidable fun (t : ℕ) => a t = b t

Equality of two primitive-recursive functions is recursively decidable. The {0,1}-valued characteristic function is 1 - ((a t - b t) + (b t - a t)) (truncated subtraction), which is 1 exactly when a t = b t; primitive recursive via primrec_sub/primrec_add, and the biconditional is omega (which understands truncated subtraction).

theorem Domain.Recursive.RecDecidable.not {p : ℕ → Prop} (hp : RecDecidable p) : RecDecidable fun (n : ℕ) => ¬p n

Negation. Recursive decidability is closed under ¬ (negate the {0,1} decider).

theorem Domain.Recursive.RecDecidable.em {p : ℕ → Prop} (hp : RecDecidable p) (n : ℕ) : p n ∨ ¬p n

Every recursively decidable predicate is decidable (the decider is f n = 1, decidable equality on ℕ); useful for choice-free De Morgan.

theorem Domain.Recursive.RecDecidable.or {p q : ℕ → Prop} (hp : RecDecidable p) (hq : RecDecidable q) : RecDecidable fun (n : ℕ) => p n ∨ q n

Disjunction. Recursive decidability is closed under ∨, via choice-free De Morgan p ∨ q ↔ ¬(¬p ∧ ¬q) (the non-constructive direction uses RecDecidable.em).

"Recursively enumerable" predicates (Scott's notion, Definition 7.2)

Scott's Definition 7.2 asks for the neighbourhood relation Xₙ f Yₘ to be recursively enumerable. We model "recursively enumerable" choice-free as a projection of a recursively decidable relation: p is r.e. iff there is a recursively decidable q with p n ↔ ∃ i, q ⟨i, n⟩ (the search variable i is paired with n via Nat.pair). This is the standard equivalent of Scott's prose description — "there is a primitive recursive r with y = {Y_{r(i)} ∣ i ∈ ℕ}": the projection form additionally represents the empty set (take q identically false), exactly as r.e. sets require. Every recursively decidable predicate is r.e. (RecDecidable.re, dropping the search variable), and r.e.-ness transfers across pointwise equivalence (REPred.of_iff). All choice-free.

def Domain.Recursive.REPred (p : ℕ → Prop) : Prop

A unary predicate p : ℕ → Prop is recursively enumerable: it is the projection of a recursively decidable relation, p n ↔ ∃ i, q (Nat.pair i n).

Equations

• Domain.Recursive.REPred p = ∃ (q : ℕ → Prop), Domain.Recursive.RecDecidable q ∧ ∀ (n : ℕ), p n ↔ ∃ (i : ℕ), q (Nat.pair i n)

def Domain.Recursive.REPred₂ (r : ℕ → ℕ → Prop) : Prop

A binary relation is recursively enumerable when its Nat.pair-coding is.

Equations

• Domain.Recursive.REPred₂ r = Domain.Recursive.REPred fun (t : ℕ) => r (Nat.unpair t).1 (Nat.unpair t).2

theorem Domain.Recursive.RecDecidable.re {p : ℕ → Prop} (hp : RecDecidable p) : REPred p

Every recursively decidable predicate is recursively enumerable. Use the decider as the relation q ⟨i, n⟩ := p n (a reindex of p along unpair.2, dropping the search variable i); the witness i = 0 makes the projection trivial.

theorem Domain.Recursive.RecDecidable₂.re {r : ℕ → ℕ → Prop} (hr : RecDecidable₂ r) : REPred₂ r

A recursively decidable binary relation is recursively enumerable.

theorem Domain.Recursive.REPred.of_iff {p q : ℕ → Prop} (h : ∀ (n : ℕ), q n ↔ p n) (hp : REPred p) : REPred q

Recursive enumerability transfers across a pointwise logical equivalence.

theorem Domain.Recursive.rePred_of_forall {p : ℕ → Prop} (h : ∀ (n : ℕ), p n) : REPred p

An always-true predicate is recursively enumerable.

Closure properties of r.e. predicates (for Proposition 7.3 and Theorem

7.4)

The projection-of-decidable form makes r.e.-ness closed under primitive-recursive reindexing (REPred.comp), conjunction (REPred.and, pairing the two search variables), and existential projection over ℕ (REPred.proj, absorbing the projected variable into the search variable). These are exactly the moves Scott's g ∘ f needs: X (g∘f) Z ↔ ∃ Y, X f Y ∧ Y g Z.

theorem Domain.Recursive.REPred.comp {p : ℕ → Prop} (hp : REPred p) {g : ℕ → ℕ} (hg : Nat.Primrec g) : REPred fun (n : ℕ) => p (g n)

Reindexing. If p is r.e. and g is primitive recursive, then fun n => p (g n) is r.e. (absorb g into the decidable relation along unpair.2).

theorem Domain.Recursive.REPred.and {p q : ℕ → Prop} (hp : REPred p) (hq : REPred q) : REPred fun (n : ℕ) => p n ∧ q n

Conjunction. Recursive enumerability is closed under ∧: combine the two decidable relations and run the two searches in parallel (pairing the search variables i, j into a single w).

theorem Domain.Recursive.REPred.proj {p : ℕ → Prop} (hp : REPred p) : REPred fun (n : ℕ) => ∃ (i : ℕ), p (Nat.pair i n)

Existential projection. If p is r.e. then so is fun n => ∃ i, p ⟨i, n⟩: fold the new existential variable i into the search variable (pairing it with the decidable relation's own search variable j).

theorem Domain.Recursive.REPred.or {p q : ℕ → Prop} (hp : REPred p) (hq : REPred q) : REPred fun (n : ℕ) => p n ∨ q n

Disjunction of r.e. predicates is r.e. A witness w carries a tag w.1 ∈ {0,1} selecting which disjunct's search index w.2 to use; the underlying relation is recursively decidable by RecDecidable.or/.and/.natEq. (Used for the sum-mapping f + g of Theorem 7.4.)

A choice-free primitive-recursive fold engine over Nat-coded lists

Scott's function-space deciders (Theorem 7.5) range over finite lists of neighborhood indices. To stay choice-free we encode such a list as a single natural via encodeList and process it with a genuinely primitive-recursive foldCode. The key results are:

• encodeList — List ℕ → ℕ, with l.length ≤ encodeList l (encodeList_length_le);
• foldCode stp p z c — folds the list coded by c, threading an accumulator and a fixed parameter p, with stp the (coded) step function;
• foldCode_eq — foldCode on encodeList l equals the corresponding List.foldl;
• primrec_foldCode — foldCode is primitive recursive in all of its (primrec) inputs.

foldStep walks one entry: the state is pair remainingCode accumulator; an empty remaining code (= 0) is a fixed point, otherwise it pops the head and applies stp.

theorem Domain.Recursive.le_pair_right (a b : ℕ) : b ≤ Nat.pair a b

b ≤ pair a b (choice-free; avoids mathlib's Nat.right_le_pair to keep the axiom set clean).

def Domain.Recursive.encodeList : List ℕ → ℕ

Encode a list of naturals as a single natural: [] ↦ 0, a :: l ↦ pair a (encodeList l) + 1. The +1 keeps the empty list (code 0) distinguishable from any nonempty list.

Equations

• Domain.Recursive.encodeList [] = 0
• Domain.Recursive.encodeList (a :: l) = Nat.pair a (Domain.Recursive.encodeList l) + 1

theorem Domain.Recursive.encodeList_length_le (l : List ℕ) : l.length ≤ encodeList l

The length of a list is bounded by its code; this is the fuel bound that lets a c-fold iterate enough times to consume the whole list coded by c.

def Domain.Recursive.foldStep (stp : ℕ → ℕ) (params s : ℕ) : ℕ

One step of the code-walking fold. The state s = pair rc acc carries the remaining code rc and accumulator acc. If rc = 0 the state is a fixed point; otherwise rc - 1 = pair head tail, and the step pops head, recurses on tail, and updates acc := stp (pair head (pair acc params)).

Equations

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

theorem Domain.Recursive.foldStep_zero (stp : ℕ → ℕ) (params acc : ℕ) : foldStep stp params (Nat.pair 0 acc) = Nat.pair 0 acc

Empty remaining code: the fold state is unchanged.

theorem Domain.Recursive.foldStep_pos (stp : ℕ → ℕ) (params a t acc : ℕ) : foldStep stp params (Nat.pair (Nat.pair a t + 1) acc) = Nat.pair t (stp (Nat.pair a (Nat.pair acc params)))

Nonempty remaining code pair a t + 1: pop a, recurse on t, update the accumulator.

def Domain.Recursive.foldCode (stp : ℕ → ℕ) (params z c : ℕ) : ℕ

Fold the list coded by c, threading accumulator z and parameter params. Implemented as c-fold iteration of foldStep from the initial state pair c z, projecting out the accumulator.

Equations

• Domain.Recursive.foldCode stp params z c = (Nat.unpair ((Domain.Recursive.foldStep stp params)^[c] (Nat.pair c z))).2

theorem Domain.Recursive.rec_const_iterate (f : ℕ → ℕ) (s k : ℕ) : Nat.rec s (fun (x ih : ℕ) => f ih) k = f^[k] s

Nat.rec with a counter-independent step is just function iteration (choice-free). Needed to bridge the Nat.Primrec.prec form (a Nat.rec) with foldCode's Function.iterate form.

theorem Domain.Recursive.foldStep_iterate (stp : ℕ → ℕ) (params k : ℕ) (l : List ℕ) (acc : ℕ) : l.length ≤ k → (Nat.unpair ((foldStep stp params)^[k] (Nat.pair (encodeList l) acc))).2 = List.foldl (fun (acc x : ℕ) => stp (Nat.pair x (Nat.pair acc params))) acc l

Core correctness of the iteration: starting from pair (encodeList l) acc, after at least l.length steps the accumulator equals the List.foldl of the step over l.

theorem Domain.Recursive.foldCode_eq (stp : ℕ → ℕ) (params z : ℕ) (l : List ℕ) : foldCode stp params z (encodeList l) = List.foldl (fun (acc x : ℕ) => stp (Nat.pair x (Nat.pair acc params))) z l

Correctness of foldCode. Folding the code of l equals the corresponding List.foldl.

theorem Domain.Recursive.unpair_snd_le (n : ℕ) : (Nat.unpair n).2 ≤ n

n.unpair.2 ≤ n (choice-free); the decreasing measure for decodeList.

@[irreducible]

def Domain.Recursive.decodeList : ℕ → List ℕ

Decode a natural back into a list of naturals, inverting encodeList. Well-founded on the remaining code (c.unpair.2 ≤ c < c + 1).

Equations

• Domain.Recursive.decodeList 0 = []
• Domain.Recursive.decodeList c.succ = (Nat.unpair c).1 :: Domain.Recursive.decodeList (Nat.unpair c).2

theorem Domain.Recursive.decodeList_zero : decodeList 0 = []

theorem Domain.Recursive.decodeList_succ (c : ℕ) : decodeList (c + 1) = (Nat.unpair c).1 :: decodeList (Nat.unpair c).2

theorem Domain.Recursive.encodeList_decodeList (c : ℕ) : encodeList (decodeList c) = c

encodeList ∘ decodeList = id: every natural is the code of its decoded list.

theorem Domain.Recursive.decodeList_length_le (c : ℕ) : (decodeList c).length ≤ c

The decoded list is no longer than its code.

theorem Domain.Recursive.foldCode_eq' (stp : ℕ → ℕ) (params z c : ℕ) : foldCode stp params z c = List.foldl (fun (acc x : ℕ) => stp (Nat.pair x (Nat.pair acc params))) z (decodeList c)

Correctness of foldCode on an arbitrary code. foldCode over any natural c equals the List.foldl over the list c decodes to.

theorem Domain.Recursive.primrec_foldStepPacked {stp : ℕ → ℕ} (hstp : Nat.Primrec stp) : Nat.Primrec fun (w : ℕ) => foldStep stp (Nat.unpair w).1 (Nat.unpair w).2

foldStep (with the parameter packed into the state as pair params state) is primitive recursive whenever the step stp is. This is the workhorse for primrec_foldCode.

theorem Domain.Recursive.primrec_foldCode {stp : ℕ → ℕ} (hstp : Nat.Primrec stp) {params z c : ℕ → ℕ} (hp : Nat.Primrec params) (hz : Nat.Primrec z) (hc : Nat.Primrec c) : Nat.Primrec fun (n : ℕ) => foldCode stp (params n) (z n) (c n)

foldCode is primitive recursive in all of its (primitive-recursive) inputs.

Primitive-recursive exponentiation (for the 2^q subset bound)

The funSpace consistency decider quantifies over all 2^q subsets of a q-element step-list, so it needs 2^q as a primitive-recursive bound. Choice-free (mathlib's Nat.Primrec lemmas for ^ route through classical simp).

theorem Domain.Recursive.recPow_eq (b e : ℕ) : Nat.rec 1 (fun (x ih : ℕ) => ih * b) e = b ^ e

Nat.rec 1 (· * b) computes b ^ e (choice-free).

theorem Domain.Recursive.primrec_pow : Nat.Primrec (Nat.unpaired fun (b e : ℕ) => b ^ e)

Exponentiation is primitive recursive (unpaired (b, e) ↦ b ^ e), choice-free.

theorem Domain.Recursive.primrec_two_pow {g : ℕ → ℕ} (hg : Nat.Primrec g) : Nat.Primrec fun (n : ℕ) => 2 ^ g n

n ↦ 2 ^ g n is primitive recursive when g is.

Halving (/2, %2) for per-subset bit extraction

The funSpace consistency fold walks a step-list while consuming a subset bitmask b one bit at a time: at each entry it reads b % 2 (is this entry in the subset?) and recurses on b / 2. Only division/modulus by the literal 2 is needed — which omega discharges directly — so this stays choice-free without a general div/mod. Computed jointly by halfParity n = pair (n/2) (n%2).

def Domain.Recursive.halfParity (n : ℕ) : ℕ

halfParity n = pair (n / 2) (n % 2), built by structural recursion: from (h, p) for n, the value for n+1 is (h + p, 1 - p) (carry on odd→even).

Equations

• Domain.Recursive.halfParity n = Nat.rec 0 (fun (x ih : ℕ) => Nat.pair ((Nat.unpair ih).1 + (Nat.unpair ih).2) (1 - (Nat.unpair ih).2)) n

theorem Domain.Recursive.halfParity_spec (n : ℕ) : halfParity n = Nat.pair (n / 2) (n % 2)

theorem Domain.Recursive.primrec_halfParity : Nat.Primrec halfParity

theorem Domain.Recursive.primrec_div2 : Nat.Primrec fun (n : ℕ) => n / 2

theorem Domain.Recursive.primrec_mod2 : Nat.Primrec fun (n : ℕ) => n % 2

Bounded quantifiers for recursively decidable predicates

Scott's function-space consistency decider (Theorem 7.5) is a bounded universal statement: a list of step-pairs is consistent iff for every subset (coded by a bitmask b < 2^q) a component condition holds. Bounded quantification of a recursively decidable predicate is again recursively decidable — choice-free, via an explicit Nat.rec fold of the {0,1} indicator.

def Domain.Recursive.isOne (v : ℕ) : ℕ

Indicator of v = 1, as a {0,1}-valued primitive-recursive function.

Equations

• Domain.Recursive.isOne v = 1 - (v - 1 + (1 - v))

theorem Domain.Recursive.isOne_le_one (v : ℕ) : isOne v ≤ 1

theorem Domain.Recursive.isOne_eq_one_iff (v : ℕ) : isOne v = 1 ↔ v = 1

theorem Domain.Recursive.primrec_isOne : Nat.Primrec isOne

def Domain.Recursive.bForallFn (g : ℕ → ℕ) (n N : ℕ) : ℕ

The {0,1}-valued bounded-∀ indicator: 1 iff g (pair i n) = 1 for all i < N. Folded right-to-left with selectFn so the result stays in {0,1}.

Equations

• Domain.Recursive.bForallFn g n N = Nat.rec 1 (fun (i ih : ℕ) => Domain.Recursive.selectFn ih (Domain.Recursive.isOne (g (Nat.pair i n))) 0) N

theorem Domain.Recursive.bForallFn_le_one (g : ℕ → ℕ) (n N : ℕ) : bForallFn g n N ≤ 1

theorem Domain.Recursive.bForallFn_eq_one_iff (g : ℕ → ℕ) (n N : ℕ) : bForallFn g n N = 1 ↔ ∀ i < N, g (Nat.pair i n) = 1

theorem Domain.Recursive.RecDecidable.bForall {p : ℕ → Prop} (hp : RecDecidable p) {bound : ℕ → ℕ} (hb : Nat.Primrec bound) : RecDecidable fun (n : ℕ) => ∀ i < bound n, p (Nat.pair i n)

Bounded universal quantifier preserves recursive decidability. If p is recursively decidable and bound is primitive recursive, then fun n => ∀ i < bound n, p (pair i n) is recursively decidable (choice-free).

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

decodeList ∘ encodeList = id (the round-trip the other way from encodeList_decodeList).

Bounded universal quantification of an r.e. predicate over a coded list

The "computable elements = computable maps" half of Theorem 7.5 needs r.e.-ness closed under ∀ e ∈ decodeList c, p e for an r.e. p. Classically this is the standard "bounded ∀ of r.e. is r.e."; choice-free we realise the search for the finite tuple of witnesses as a single code w whose decoded list supplies one witness per list entry, threaded through a foldCode.

def Domain.Recursive.reForallF (qc : ℕ → ℕ) (acc x : ℕ) : ℕ

The pure (set-theoretic) witness-threading fold step. The accumulator is pair remWitness flag: at the list head x we pop a witness i (the decodeList head of remWitness, i.e. (remWitness - 1).unpair.1) with new remaining code (remWitness - 1).unpair.2, and AND the flag with isOne (qc ⟨i, x⟩).

Equations

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

def Domain.Recursive.reForallStp (qc : ℕ → ℕ) (w : ℕ) : ℕ

The foldCode-form step (parameter unused), used to package reForallF primitive-recursively.

Equations

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

def Domain.Recursive.reForallChar (qc : ℕ → ℕ) (w c : ℕ) : ℕ

The {0,1}-flag computed by threading witness code w through the list coded by c.

Equations

• Domain.Recursive.reForallChar qc w c = (Nat.unpair (Domain.Recursive.foldCode (Domain.Recursive.reForallStp qc) 0 (Nat.pair w 1) c)).2

theorem Domain.Recursive.reForallStp_eq (qc : ℕ → ℕ) (acc x : ℕ) : reForallStp qc (Nat.pair x (Nat.pair acc 0)) = reForallF qc acc x

theorem Domain.Recursive.reForallChar_eq (qc : ℕ → ℕ) (w c : ℕ) : reForallChar qc w c = (Nat.unpair (List.foldl (reForallF qc) (Nat.pair w 1) (decodeList c))).2

theorem Domain.Recursive.reForallF_foldl_eq_one_iff (qc : ℕ → ℕ) (l : List ℕ) (w flag : ℕ) : flag ≤ 1 → ((Nat.unpair (List.foldl (reForallF qc) (Nat.pair w flag) l)).2 = 1 ↔ flag = 1 ∧ ∀ k < l.length, qc (Nat.pair ((decodeList w).getD k 0) (l.getD k 0)) = 1)

Core induction. Threading witness code w through l, the final flag is 1 iff the start flag was 1 and, position by position, the k-th witness of decodeList w satisfies qc.

theorem Domain.Recursive.reForallChar_eq_one_iff (qc : ℕ → ℕ) (w c : ℕ) : reForallChar qc w c = 1 ↔ ∀ k < (decodeList c).length, qc (Nat.pair ((decodeList w).getD k 0) ((decodeList c).getD k 0)) = 1

theorem Domain.Recursive.primrec_reForallStp {qc : ℕ → ℕ} (hqc : Nat.Primrec qc) : Nat.Primrec (reForallStp qc)

theorem Domain.Recursive.primrec_reForallChar {qc : ℕ → ℕ} (hqc : Nat.Primrec qc) : Nat.Primrec fun (t : ℕ) => reForallChar qc (Nat.unpair t).1 (Nat.unpair t).2

theorem Domain.Recursive.REPred.forall_mem_decodeList {p : ℕ → Prop} (hp : REPred p) : REPred fun (c : ℕ) => ∀ e ∈ decodeList c, p e

Bounded ∀ over a coded list preserves recursive enumerability. If p is r.e. then so is fun c => ∀ e ∈ decodeList c, p e: the finite tuple of per-entry witnesses is packed into a single search code w, and the {0,1} flag reForallChar makes the body recursively decidable.

Bounded ∀ over a coded list with a parameter (for curry, Theorem 7.5)

curry's neighbourhood relation is a bounded ∀ e ∈ decodeList c, p n e whose body depends on a parameter n (the 𝒟₀-index) as well as the list entry e. We reduce this to REPred.forall_mem_decodeList by primitively-recursively re-coding the list decodeList c into the list of pairs ⟨n, e⟩ (order is irrelevant under ∀ ∈), so the parameterised body becomes the plain fun s => p s.1 s.2 over the re-coded list.

def Domain.Recursive.mapPairStep (n acc x : ℕ) : ℕ

Prepend the pair ⟨n, x⟩ onto the list coded by acc.

Equations

• Domain.Recursive.mapPairStep n acc x = Nat.pair (Nat.pair n x) acc + 1

def Domain.Recursive.mapPairStp (w : ℕ) : ℕ

foldCode-shaped wrapper of mapPairStep (parameter n threaded via the params slot).

Equations

• Domain.Recursive.mapPairStp w = Domain.Recursive.mapPairStep (Nat.unpair (Nat.unpair w).2).2 (Nat.unpair (Nat.unpair w).2).1 (Nat.unpair w).1

theorem Domain.Recursive.mapPairStp_eq (n acc x : ℕ) : mapPairStp (Nat.pair x (Nat.pair acc n)) = mapPairStep n acc x

theorem Domain.Recursive.decodeList_mapPairStep (n acc x : ℕ) : decodeList (mapPairStep n acc x) = Nat.pair n x :: decodeList acc

theorem Domain.Recursive.decodeList_foldl_mapPairStp (n : ℕ) (el : List ℕ) (acc : ℕ) : decodeList (List.foldl (fun (acc x : ℕ) => mapPairStp (Nat.pair x (Nat.pair acc n))) acc el) = (List.map (fun (x : ℕ) => Nat.pair n x) el).reverse ++ decodeList acc

def Domain.Recursive.mapPairCode (n c : ℕ) : ℕ

mapPairCode n c codes the list (decodeList c).map ⟨n, ·⟩ (reversed).

Equations

• Domain.Recursive.mapPairCode n c = Domain.Recursive.foldCode Domain.Recursive.mapPairStp n 0 c

theorem Domain.Recursive.decodeList_mapPairCode (n c : ℕ) : decodeList (mapPairCode n c) = (List.map (fun (x : ℕ) => Nat.pair n x) (decodeList c)).reverse

theorem Domain.Recursive.primrec_mapPairStp : Nat.Primrec mapPairStp

theorem Domain.Recursive.primrec_mapPairCode : Nat.Primrec fun (t : ℕ) => mapPairCode (Nat.unpair t).1 (Nat.unpair t).2

theorem Domain.Recursive.REPred.forall_mem_decodeList₂ {p : ℕ → ℕ → Prop} (hp : REPred₂ p) : REPred fun (t : ℕ) => ∀ e ∈ decodeList (Nat.unpair t).2, p (Nat.unpair t).1 e

Parameterised bounded ∀ over a coded list preserves recursive enumerability. If p is an r.e. binary relation then fun t => ∀ e ∈ decodeList t.2, p t.1 e is r.e.: re-code the list into the pairs ⟨t.1, e⟩ (mapPairCode) and apply the unparameterised forall_mem_decodeList.