The arithmetic a certificate for CODEHALT has to speak

Everything the ∃SO[new] certificate of DescriptiveComplexity.CODEHALT needs to know about Nat.Partrec.Code, stated over ℕ alone – no logic, no structures. Three groups:

• codes are numbers. DescriptiveComplexity.CodeHalt.dec decodes a number into a code, and the four dec_pair/dec_comp/dec_prec/dec_rfind lemmas read the shape of a code off the arithmetic of its number: a pair is a 4 * ⟨e₁, e₂⟩ + 4, a prec a + 5, a comp a + 6, an rfind' a 4 * e + 7. This is what lets the certificate carry codes as numerals rather than as nodes of the instance, and it is what makes decoding unambiguous without asking the instance to be well-formed.
• Nat.pair has a successor rule. DescriptiveComplexity.CodeHalt.NextP names the four ways the pair enumerated next after ⟨a, b⟩ arises, and DescriptiveComplexity.CodeHalt.pair_next / DescriptiveComplexity.CodeHalt.exists_next make it a recurrence. A guessed pairing relation checked against that recurrence is Nat.pair, which is much cheaper than guessing addition and multiplication and building the closed form out of them.
• bounded evaluation unfolds. One mem_evaln_*_iff per constructor, plus DescriptiveComplexity.CodeHalt.evaln_rfind'_spec, which turns the step-by-step search of evaln on an rfind' into the bounded universal statement a first-order kernel can make: the answer is a place where the argument returns 0 and every earlier place returns something nonzero. Finally DescriptiveComplexity.CodeHalt.valBound bounds every value a bounded evaluation can produce, which is what makes the numeral segment of a certificate finite.

Codes as numbers

def DescriptiveComplexity.CodeHalt.dec (e : ℕ) : Nat.Partrec.Code

The code a number denotes.

Equations

• DescriptiveComplexity.CodeHalt.dec e = Denumerable.ofNat Nat.Partrec.Code e

@[simp]

theorem DescriptiveComplexity.CodeHalt.dec_encodeCode (c : Nat.Partrec.Code) : dec c.encodeCode = c

@[simp]

theorem DescriptiveComplexity.CodeHalt.encodeCode_dec (e : ℕ) : (dec e).encodeCode = e

theorem DescriptiveComplexity.CodeHalt.encodeCode_pair (cf cg : Nat.Partrec.Code) : (cf.pair cg).encodeCode = 4 * Nat.pair cf.encodeCode cg.encodeCode + 4

theorem DescriptiveComplexity.CodeHalt.encodeCode_comp (cf cg : Nat.Partrec.Code) : (cf.comp cg).encodeCode = 4 * Nat.pair cf.encodeCode cg.encodeCode + 6

theorem DescriptiveComplexity.CodeHalt.encodeCode_prec (cf cg : Nat.Partrec.Code) : (cf.prec cg).encodeCode = 4 * Nat.pair cf.encodeCode cg.encodeCode + 5

theorem DescriptiveComplexity.CodeHalt.encodeCode_rfind' (cf : Nat.Partrec.Code) : cf.rfind'.encodeCode = 4 * cf.encodeCode + 7

@[simp]

theorem DescriptiveComplexity.CodeHalt.dec_zero : dec 0 = Nat.Partrec.Code.zero

@[simp]

theorem DescriptiveComplexity.CodeHalt.dec_one : dec 1 = Nat.Partrec.Code.succ

@[simp]

theorem DescriptiveComplexity.CodeHalt.dec_two : dec 2 = Nat.Partrec.Code.left

@[simp]

theorem DescriptiveComplexity.CodeHalt.dec_three : dec 3 = Nat.Partrec.Code.right

theorem DescriptiveComplexity.CodeHalt.dec_pair (a b : ℕ) : dec (4 * Nat.pair a b + 4) = (dec a).pair (dec b)

theorem DescriptiveComplexity.CodeHalt.dec_comp (a b : ℕ) : dec (4 * Nat.pair a b + 6) = (dec a).comp (dec b)

theorem DescriptiveComplexity.CodeHalt.dec_prec (a b : ℕ) : dec (4 * Nat.pair a b + 5) = (dec a).prec (dec b)

theorem DescriptiveComplexity.CodeHalt.dec_rfind (a : ℕ) : dec (4 * a + 7) = (dec a).rfind'

theorem DescriptiveComplexity.CodeHalt.lt_of_pair_encode (a b : ℕ) : a < 4 * Nat.pair a b + 4 ∧ b < 4 * Nat.pair a b + 4

The number of a proper subcode is smaller: this is the well-founded measure the soundness of a certificate runs on.

The successor rule of Nat.pair

def DescriptiveComplexity.CodeHalt.NextP (a' b' a b : ℕ) : Prop

(a, b) is the pair enumerated just after (a', b'). The four cases are: move up inside a shell, close a shell, move along a shell, and open the next one.

Equations

• DescriptiveComplexity.CodeHalt.NextP a' b' a b = (a' < b' ∧ a = a' + 1 ∧ a < b' ∧ b = b' ∨ b' = a' + 1 ∧ a = b' ∧ b = 0 ∨ b' ≤ a' ∧ b = b' + 1 ∧ b ≤ a' ∧ a = a' ∨ a' = b' ∧ a = 0 ∧ b = b' + 1)

theorem DescriptiveComplexity.CodeHalt.pair_next {a' b' a b : ℕ} (h : NextP a' b' a b) : Nat.pair a b = Nat.pair a' b' + 1

theorem DescriptiveComplexity.CodeHalt.exists_next (a' b' : ℕ) : ∃ (a : ℕ) (b : ℕ), NextP a' b' a b

theorem DescriptiveComplexity.CodeHalt.pair_eq_zero {a b : ℕ} (h : Nat.pair a b = 0) : a = 0 ∧ b = 0

theorem DescriptiveComplexity.CodeHalt.exists_pred_pair {a b : ℕ} (h : Nat.pair a b ≠ 0) : ∃ (a' : ℕ) (b' : ℕ), Nat.pair a' b' + 1 = Nat.pair a b ∧ NextP a' b' a b

The predecessor of a nonzero pair, together with the step relating them: the completeness half of the recurrence.

Unfolding bounded evaluation

theorem DescriptiveComplexity.CodeHalt.mem_evaln_zero_iff {k n v : ℕ} : v ∈ Nat.Partrec.Code.evaln (k + 1) Nat.Partrec.Code.zero n ↔ n ≤ k ∧ v = 0

theorem DescriptiveComplexity.CodeHalt.mem_evaln_succ_iff {k n v : ℕ} : v ∈ Nat.Partrec.Code.evaln (k + 1) Nat.Partrec.Code.succ n ↔ n ≤ k ∧ v = n + 1

theorem DescriptiveComplexity.CodeHalt.mem_evaln_left_iff {k n v : ℕ} : v ∈ Nat.Partrec.Code.evaln (k + 1) Nat.Partrec.Code.left n ↔ n ≤ k ∧ v = (Nat.unpair n).1

theorem DescriptiveComplexity.CodeHalt.mem_evaln_right_iff {k n v : ℕ} : v ∈ Nat.Partrec.Code.evaln (k + 1) Nat.Partrec.Code.right n ↔ n ≤ k ∧ v = (Nat.unpair n).2

theorem DescriptiveComplexity.CodeHalt.mem_evaln_pair_iff {k n v : ℕ} {cf cg : Nat.Partrec.Code} : v ∈ Nat.Partrec.Code.evaln (k + 1) (cf.pair cg) n ↔ n ≤ k ∧ ∃ (x : ℕ) (y : ℕ), x ∈ Nat.Partrec.Code.evaln (k + 1) cf n ∧ y ∈ Nat.Partrec.Code.evaln (k + 1) cg n ∧ Nat.pair x y = v

theorem DescriptiveComplexity.CodeHalt.mem_evaln_comp_iff {k n v : ℕ} {cf cg : Nat.Partrec.Code} : v ∈ Nat.Partrec.Code.evaln (k + 1) (cf.comp cg) n ↔ n ≤ k ∧ ∃ y ∈ Nat.Partrec.Code.evaln (k + 1) cg n, v ∈ Nat.Partrec.Code.evaln (k + 1) cf y

theorem DescriptiveComplexity.CodeHalt.mem_evaln_prec_zero_iff {k v : ℕ} {cf cg : Nat.Partrec.Code} {a : ℕ} : v ∈ Nat.Partrec.Code.evaln (k + 1) (cf.prec cg) (Nat.pair a 0) ↔ Nat.pair a 0 ≤ k ∧ v ∈ Nat.Partrec.Code.evaln (k + 1) cf a

theorem DescriptiveComplexity.CodeHalt.mem_evaln_prec_succ_iff {k v : ℕ} {cf cg : Nat.Partrec.Code} {a j : ℕ} : v ∈ Nat.Partrec.Code.evaln (k + 1) (cf.prec cg) (Nat.pair a (j + 1)) ↔ Nat.pair a (j + 1) ≤ k ∧ ∃ i ∈ Nat.Partrec.Code.evaln k (cf.prec cg) (Nat.pair a j), v ∈ Nat.Partrec.Code.evaln (k + 1) cg (Nat.pair a (Nat.pair j i))

theorem DescriptiveComplexity.CodeHalt.mem_evaln_rfind'_iff {k v : ℕ} {cf : Nat.Partrec.Code} {a m : ℕ} : v ∈ Nat.Partrec.Code.evaln (k + 1) cf.rfind' (Nat.pair a m) ↔ Nat.pair a m ≤ k ∧ ∃ x ∈ Nat.Partrec.Code.evaln (k + 1) cf (Nat.pair a m), if x = 0 then v = m else v ∈ Nat.Partrec.Code.evaln k cf.rfind' (Nat.pair a (m + 1))

theorem DescriptiveComplexity.CodeHalt.evaln_rfind'_spec (k : ℕ) {cf : Nat.Partrec.Code} {a m v : ℕ} : v ∈ Nat.Partrec.Code.evaln k cf.rfind' (Nat.pair a m) → m ≤ v ∧ 0 ∈ Nat.Partrec.Code.evaln k cf (Nat.pair a v) ∧ ∀ (w : ℕ), m ≤ w → w < v → ∃ (u : ℕ), u ≠ 0 ∧ u ∈ Nat.Partrec.Code.evaln k cf (Nat.pair a w)

The search an rfind' performs, read as a bounded universal statement. A bounded evaluation of rfind' cf on ⟨a, m⟩ returns some v ≥ m such that cf returns 0 at ⟨a, v⟩ and something nonzero at every ⟨a, w⟩ with m ≤ w < v – and all of that within the same budget, which is what lets a first-order kernel state the search without a chain.

Introduction rules for evaluation

One per constructor: what has to hold of the arguments for a value to be in the evaluation of a code. They are what the soundness of a certificate discharges its case analysis with.

theorem DescriptiveComplexity.CodeHalt.mem_eval_zero {n : ℕ} : 0 ∈ Nat.Partrec.Code.zero.eval n

theorem DescriptiveComplexity.CodeHalt.mem_eval_succ {n : ℕ} : n + 1 ∈ Nat.Partrec.Code.succ.eval n

theorem DescriptiveComplexity.CodeHalt.mem_eval_left {n : ℕ} : (Nat.unpair n).1 ∈ Nat.Partrec.Code.left.eval n

theorem DescriptiveComplexity.CodeHalt.mem_eval_right {n : ℕ} : (Nat.unpair n).2 ∈ Nat.Partrec.Code.right.eval n

theorem DescriptiveComplexity.CodeHalt.mem_eval_pair {cf cg : Nat.Partrec.Code} {n a b : ℕ} (ha : a ∈ cf.eval n) (hb : b ∈ cg.eval n) : Nat.pair a b ∈ (cf.pair cg).eval n

theorem DescriptiveComplexity.CodeHalt.mem_eval_comp {cf cg : Nat.Partrec.Code} {n y v : ℕ} (hy : y ∈ cg.eval n) (hv : v ∈ cf.eval y) : v ∈ (cf.comp cg).eval n

theorem DescriptiveComplexity.CodeHalt.mem_eval_prec_zero {cf cg : Nat.Partrec.Code} {a v : ℕ} (h : v ∈ cf.eval a) : v ∈ (cf.prec cg).eval (Nat.pair a 0)

theorem DescriptiveComplexity.CodeHalt.mem_eval_prec_succ {cf cg : Nat.Partrec.Code} {a j i v : ℕ} (hi : i ∈ (cf.prec cg).eval (Nat.pair a j)) (hv : v ∈ cg.eval (Nat.pair a (Nat.pair j i))) : v ∈ (cf.prec cg).eval (Nat.pair a (j + 1))

theorem DescriptiveComplexity.CodeHalt.mem_eval_rfind' {cf : Nat.Partrec.Code} {a m v : ℕ} (hmv : m ≤ v) (h0 : 0 ∈ cf.eval (Nat.pair a v)) (hlt : ∀ (w : ℕ), m ≤ w → w < v → ∃ (u : ℕ), u ≠ 0 ∧ u ∈ cf.eval (Nat.pair a w)) : v ∈ cf.rfind'.eval (Nat.pair a m)

The evaluation of an rfind', from the bounded universal shape of the search: v is a place at or above m where cf returns 0, and every place in between returns something nonzero.

A bound on the values a bounded evaluation produces

def DescriptiveComplexity.CodeHalt.valBound (E k : ℕ) : ℕ

Every value a bounded evaluation with budget k of a code numbered at most E can produce. The numeral segment of a certificate is an initial segment of ℕ reaching this far, which is what makes it finite.

Equations

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

theorem DescriptiveComplexity.CodeHalt.le_valBound {E k e x v : ℕ} (he : e ≤ E) (hv : v ∈ Nat.Partrec.Code.evaln k (dec e) x) : v ≤ valBound E k