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

@[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)

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

Unfolding bounded evaluation

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.

A bound on the values a bounded evaluation produces