The numeral segment of a certificate

An ∃SO[new] certificate for DescriptiveComplexity.CODEHALT carries numbers as invented values: a finite set with a guessed linear order on it, read as the initial segment 0, 1, …, N of ℕ. This file is that reading.

DescriptiveComplexity.CodeHalt.numOf is the number a value stands for – the count of values below it, i.e., DescriptiveComplexity.bitRank at the trivial set of positions. DescriptiveComplexity.CodeHalt.IsZ and DescriptiveComplexity.CodeHalt.IsS are “is the least value” and “is covered by”, spelled out so that a first-order kernel can state them verbatim, and the two iff lemmas say they mean 0 and + 1. That is the whole bridge: from there on a certificate is a statement about natural numbers.

The last two lemmas run the bridge the other way, on Fin (N + 1) with its own order, which is the segment a certificate is built on.

The number a value stands for

def DescriptiveComplexity.CodeHalt.IsZ {D : Type} (Le : D → D → Prop) (d : D) : Prop

d is the least value of the segment, i.e., the numeral 0.

Equations

• DescriptiveComplexity.CodeHalt.IsZ Le d = ∀ (e : D), Le d e

def DescriptiveComplexity.CodeHalt.IsS {D : Type} (Le : D → D → Prop) (d d' : D) : Prop

d' is the value just above d, i.e., its numeral is one more.

Equations

• DescriptiveComplexity.CodeHalt.IsS Le d d' = (Le d d' ∧ d ≠ d' ∧ ∀ (e : D), Le d e → Le e d' → e = d ∨ e = d')

theorem DescriptiveComplexity.CodeHalt.isZ_iff_minPos {D : Type} {Le : D → D → Prop} {d : D} : IsZ Le d ↔ MinPos Le (fun (x : D) => True) d

theorem DescriptiveComplexity.CodeHalt.isS_iff_succPos {D : Type} {Le : D → D → Prop} {d d' : D} : IsS Le d d' ↔ SuccPos Le (fun (x : D) => True) d d'

The segment a certificate is built on