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

noncomputable def DescriptiveComplexity.CodeHalt.numOf {D : Type} (Le : D → D → Prop) (d : D) : ℕ

The number a value of the numeral segment stands for: how many values lie strictly below it.

Equations

• DescriptiveComplexity.CodeHalt.numOf Le d = DescriptiveComplexity.bitRank Le (fun (x : D) => True) d

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.numOf_lt {D : Type} {Le : D → D → Prop} [Finite D] (hlin : IsLinOrd Le) {x y : D} (hle : Le x y) (hne : x ≠ y) : numOf Le x < numOf Le y

theorem DescriptiveComplexity.CodeHalt.le_of_numOf_lt {D : Type} {Le : D → D → Prop} [Finite D] (hlin : IsLinOrd Le) {x y : D} (h : numOf Le x < numOf Le y) : Le x y ∧ x ≠ y

theorem DescriptiveComplexity.CodeHalt.numOf_injective {D : Type} {Le : D → D → Prop} [Finite D] (hlin : IsLinOrd Le) {x y : D} (h : numOf Le x = numOf Le y) : x = y

theorem DescriptiveComplexity.CodeHalt.le_iff_numOf_le {D : Type} {Le : D → D → Prop} [Finite D] (hlin : IsLinOrd Le) {x y : D} : Le x y ↔ numOf Le x ≤ numOf Le y

theorem DescriptiveComplexity.CodeHalt.isZ_iff {D : Type} {Le : D → D → Prop} [Finite D] (hlin : IsLinOrd Le) {d : D} : IsZ Le d ↔ numOf Le d = 0

theorem DescriptiveComplexity.CodeHalt.isS_iff {D : Type} {Le : D → D → Prop} [Finite D] (hlin : IsLinOrd Le) {d d' : D} : IsS Le d d' ↔ numOf Le d' = numOf Le d + 1

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'

theorem DescriptiveComplexity.CodeHalt.exists_numOf {D : Type} {Le : D → D → Prop} [Finite D] (hlin : IsLinOrd Le) (Y : ℕ) (y : D) : numOf Le y = Y → ∀ w ≤ Y, ∃ (x : D), numOf Le x = w

Every number below a reached one is reached: the values of the segment are an initial segment of ℕ. This is what lets a bounded universal over the segment be read as a bounded universal over ℕ.

The segment a certificate is built on

theorem DescriptiveComplexity.CodeHalt.isZ_fin {N : ℕ} {i : Fin (N + 1)} : IsZ (fun (x1 x2 : Fin (N + 1)) => x1 ≤ x2) i ↔ ↑i = 0

theorem DescriptiveComplexity.CodeHalt.isS_fin {N : ℕ} {i j : Fin (N + 1)} : IsS (fun (x1 x2 : Fin (N + 1)) => x1 ≤ x2) i j ↔ ↑j = ↑i + 1