The drawn instance is a well-formed machine embedding the simulator

The semantic half of the correctness of the drawing: the drawn structure's machine data is well-formed (DescriptiveComplexity.HaltHard.wellFormed_halt), and its machine predicates are exactly the images of DescriptiveComplexity.HaltHard.simTM's along the embedding that places each machine element on the canonically padded bottom tuple (DescriptiveComplexity.HaltHard.tmEmbed_halt). The enumeration of the cells and the initial tape are the next file's business; this one only speaks about tags and tuples.

Canonical tuples

theorem DescriptiveComplexity.HaltHard.eq_botTup_of_canon0 {L : FirstOrder.Language} {V : L.FinVocab} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {w : Fin (dimOf V) → A} (h : Canon 0 w) : w = botTup V A

A tuple canonical at 0 is the bottom tuple.

noncomputable def DescriptiveComplexity.HaltHard.mEl {L : FirstOrder.Language} {V : L.FinVocab} {cF cP : Turing.ToPartrec.Code} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (u : SimU (allCode cF cP)) : (haltTuringInterp V cF cP).Map A

The machine element u, as the point of the drawn instance with the bottom tuple.

Equations

• DescriptiveComplexity.HaltHard.mEl u = DescriptiveComplexity.HaltHard.hPt (Sum.inl u) (DescriptiveComplexity.botTup V A)

The embedding of the simulating machine

theorem DescriptiveComplexity.HaltHard.unary_embed_iff {L : FirstOrder.Language} {V : L.FinVocab} {cF cP : Turing.ToPartrec.Code} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (Q : SimU (allCode cF cP) → Prop) (R : FirstOrder.Language.turingRel 1) (hR : ∀ (ts : Fin 1 → HTag V cF cP), (haltTuringInterp V cF cP).relFormula R ts = mUnaryF V cF cP Q (ts 0)) (b : (haltTuringInterp V cF cP).Map A) : FirstOrder.Language.Structure.RelMap (have this := R; this) ![b] ↔ ∃ (u : SimU (allCode cF cP)), b = mEl u ∧ Q u

theorem DescriptiveComplexity.HaltHard.binary_embed_iff {L : FirstOrder.Language} {V : L.FinVocab} {cF cP : Turing.ToPartrec.Code} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (Q : SimU (allCode cF cP) → SimU (allCode cF cP) → Prop) (R : FirstOrder.Language.turingRel 2) (hR : ∀ (ts : Fin 2 → HTag V cF cP), (haltTuringInterp V cF cP).relFormula R ts = mBinaryF V cF cP Q (ts 0) (ts 1)) (b b' : (haltTuringInterp V cF cP).Map A) : FirstOrder.Language.Structure.RelMap (have this := R; this) ![b, b'] ↔ ∃ (u : SimU (allCode cF cP)) (u' : SimU (allCode cF cP)), b = mEl u ∧ b' = mEl u' ∧ Q u u'

theorem DescriptiveComplexity.HaltHard.tmEmbed_halt {L : FirstOrder.Language} {V : L.FinVocab} {cF cP : Turing.ToPartrec.Code} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : TMEmbed mEl (simTM (allCode cF cP)) (tmData ((haltTuringInterp V cF cP).Map A))

The drawn machine embeds the simulating machine: every machine predicate of the drawn structure is the image of simTM's along mEl.

The letter of a cell is unique

theorem DescriptiveComplexity.HaltHard.inpOn_functional {L : FirstOrder.Language} {V : L.FinVocab} {cF cP : Turing.ToPartrec.Code} {A : Type} [L.Structure A] [LinearOrder A] {c : CellTag V} {u u' : SimU (allCode cF cP)} {w : Fin (dimOf V) → A} (h : InpOn V cF cP c u w) (h' : InpOn V cF cP c u' w) : u = u'

The letter DescriptiveComplexity.HaltHard.InpOn relates to a cell is unique.

The drawn machine is well-formed

theorem DescriptiveComplexity.HaltHard.wellFormed_halt {L : FirstOrder.Language} {V : L.FinVocab} {cF cP : Turing.ToPartrec.Code} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : (tmData ((haltTuringInterp V cF cP).Map A)).WellFormed

The drawn machine data is well-formed.

Tuple numbers

The reversed lexicographic order on tuples is comparison of their numbers – the little-endian DescriptiveComplexity.tupleIdx of the coordinates read through the numbering. One direction is proved arithmetically; the other falls out of trichotomy and injectivity.

theorem DescriptiveComplexity.HaltHard.tupleIdx_append (c : ℕ) (l₁ l₂ : List ℕ) : FirstOrder.Language.tupleIdx c (l₁ ++ l₂) = FirstOrder.Language.tupleIdx c l₁ + c ^ l₁.length * FirstOrder.Language.tupleIdx c l₂

Splitting the number of a concatenation.

noncomputable def DescriptiveComplexity.HaltHard.tupN {L : FirstOrder.Language} {V : L.FinVocab} {A : Type} [LinearOrder A] (k : ℕ) (e : Fin (k + 1) ≃o A) (w : Fin (dimOf V) → A) : ℕ

The number of a tuple, read through the numbering.

Equations

• DescriptiveComplexity.HaltHard.tupN k e w = FirstOrder.Language.tupleIdx (k + 1) (List.ofFn fun (j : Fin (DescriptiveComplexity.dimOf V)) => ↑(e.symm (w j)))

theorem DescriptiveComplexity.HaltHard.tupN_lt {L : FirstOrder.Language} {V : L.FinVocab} {A : Type} [LinearOrder A] (k : ℕ) (e : Fin (k + 1) ≃o A) (w : Fin (dimOf V) → A) : tupN k e w < (k + 1) ^ dimOf V

theorem DescriptiveComplexity.HaltHard.tupN_lt_of_revLexLt {L : FirstOrder.Language} {V : L.FinVocab} {A : Type} [LinearOrder A] (k : ℕ) (e : Fin (k + 1) ≃o A) {u w : Fin (dimOf V) → A} (h : RevLexLt u w) : tupN k e u < tupN k e w

Reversed lexicographic comparison is comparison of the numbers.

theorem DescriptiveComplexity.HaltHard.tupN_inj {L : FirstOrder.Language} {V : L.FinVocab} {A : Type} [LinearOrder A] (k : ℕ) (e : Fin (k + 1) ≃o A) {u w : Fin (dimOf V) → A} (h : tupN k e u = tupN k e w) : u = w

theorem DescriptiveComplexity.HaltHard.revLexLt_of_tupN_lt {L : FirstOrder.Language} {V : L.FinVocab} {A : Type} [LinearOrder A] (k : ℕ) (e : Fin (k + 1) ≃o A) {u w : Fin (dimOf V) → A} (h : tupN k e u < tupN k e w) : RevLexLt u w

The cells of the input page

theorem DescriptiveComplexity.HaltHard.eSymm_botOrd {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (k : ℕ) (e : Fin (k + 1) ≃o A) : e.symm (botOrd A) = 0

noncomputable def DescriptiveComplexity.HaltHard.tupOf {L : FirstOrder.Language} (V : L.FinVocab) {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (k : ℕ) (e : Fin (k + 1) ≃o A) (i : Fin V.numSyms) (t : ℕ) : Fin (dimOf V) → A

The tuple of the bit cell numbered t in the block of symbol i.

Equations

• DescriptiveComplexity.HaltHard.tupOf V k e i t = DescriptiveComplexity.pad (DescriptiveComplexity.botOrd A) fun (j : Fin (V.arity i)) => e ⟨FirstOrder.Language.digitAt (k + 1) t ↑j, ⋯⟩

theorem DescriptiveComplexity.HaltHard.canon_tupOf {L : FirstOrder.Language} (V : L.FinVocab) {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (k : ℕ) (e : Fin (k + 1) ≃o A) (i : Fin V.numSyms) (t : ℕ) : Canon (V.arity i) (tupOf V k e i t)

theorem DescriptiveComplexity.HaltHard.tupN_tupOf {L : FirstOrder.Language} (V : L.FinVocab) {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (k : ℕ) (e : Fin (k + 1) ≃o A) (i : Fin V.numSyms) {t : ℕ} (ht : t < (k + 1) ^ V.arity i) : tupN k e (tupOf V k e i t) = t

The number of a bit cell's tuple is its index.

theorem DescriptiveComplexity.HaltHard.tupleIdx_eq_zero {c : ℕ} {l : List ℕ} : (∀ a ∈ l, a = 0) → FirstOrder.Language.tupleIdx c l = 0

theorem DescriptiveComplexity.HaltHard.tupN_lt_cap_of_canon {L : FirstOrder.Language} (V : L.FinVocab) {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (k : ℕ) (e : Fin (k + 1) ≃o A) {i : Fin V.numSyms} {w : Fin (dimOf V) → A} (hcan : Canon (V.arity i) w) : tupN k e w < (k + 1) ^ V.arity i

The number of a tuple canonical at an arity stays below the block cap.

theorem DescriptiveComplexity.HaltHard.eq_tupOf_of_canon {L : FirstOrder.Language} (V : L.FinVocab) {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (k : ℕ) (e : Fin (k + 1) ≃o A) {i : Fin V.numSyms} {w : Fin (dimOf V) → A} (hcan : Canon (V.arity i) w) : w = tupOf V k e i (tupN k e w)

A tuple canonical at an arity is the tuple of its number's bit cell.

def DescriptiveComplexity.HaltHard.bitIdx {L : FirstOrder.Language} (V : L.FinVocab) (k : ℕ) : List (Fin V.numSyms × ℕ)

The chain indices, in tape order: symbols descending, tuple numbers descending inside each block.

Equations

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

theorem DescriptiveComplexity.HaltHard.mem_bitIdx {L : FirstOrder.Language} (V : L.FinVocab) (k : ℕ) {p : Fin V.numSyms × ℕ} : p ∈ bitIdx V k ↔ p.2 < (k + 1) ^ V.arity p.1

noncomputable def DescriptiveComplexity.HaltHard.pairCells {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (k : ℕ) (e : Fin (k + 1) ≃o A) (p : Fin V.numSyms × ℕ) : List ((haltTuringInterp V cF cP).Map A)

The two chain cells of a bit.

Equations

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

noncomputable def DescriptiveComplexity.HaltHard.chainCells {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (k : ℕ) (e : Fin (k + 1) ≃o A) : List ((haltTuringInterp V cF cP).Map A)

The chain cells, in tape order.

Equations

• DescriptiveComplexity.HaltHard.chainCells V cF cP k e = List.flatMap (DescriptiveComplexity.HaltHard.pairCells V cF cP k e) (DescriptiveComplexity.HaltHard.bitIdx V k)

noncomputable def DescriptiveComplexity.HaltHard.oneCells {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (k : ℕ) (e : Fin (k + 1) ≃o A) : List ((haltTuringInterp V cF cP).Map A)

The digit cells of the spelled size, in tape order – elements descending.

Equations

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

noncomputable def DescriptiveComplexity.HaltHard.psH {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (k : ℕ) (e : Fin (k + 1) ≃o A) : List ((haltTuringInterp V cF cP).Map A)

The cells of the drawn instance, in tape order.

Equations

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

Membership: the cells are exactly the positions

theorem DescriptiveComplexity.HaltHard.posn_of_mem_psH {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (k : ℕ) (e : Fin (k + 1) ≃o A) {p : (haltTuringInterp V cF cP).Map A} (hp : p ∈ psH V cF cP k e) : (tmData ((haltTuringInterp V cF cP).Map A)).Posn p

Every listed cell is a position.

theorem DescriptiveComplexity.HaltHard.mem_psH_of_posn {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (k : ℕ) (e : Fin (k + 1) ≃o A) {p : (haltTuringInterp V cF cP).Map A} (hp : (tmData ((haltTuringInterp V cF cP).Map A)).Posn p) : p ∈ psH V cF cP k e

Every position is a listed cell.

The initial letters

noncomputable def DescriptiveComplexity.HaltHard.bitAt {L : FirstOrder.Language} (V : L.FinVocab) {A : Type} [L.Structure A] [LinearOrder A] (k : ℕ) (e : Fin (k + 1) ≃o A) [(n : ℕ) → (R : L.Relations n) → (x : Fin n → A) → Decidable (FirstOrder.Language.Structure.RelMap R x)] (i : Fin V.numSyms) (t : ℕ) : Bool

The bit drawn at a bit cell: the table entry of the presentation.

Equations

• DescriptiveComplexity.HaltHard.bitAt V k e i t = decide (FirstOrder.Language.Structure.RelMap (V.sym i) fun (j : Fin (V.arity i)) => e ⟨FirstOrder.Language.digitAt (k + 1) t ↑j, ⋯⟩)

theorem DescriptiveComplexity.HaltHard.bitAt_iff_bitOf {L : FirstOrder.Language} (V : L.FinVocab) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (k : ℕ) (e : Fin (k + 1) ≃o A) [(n : ℕ) → (R : L.Relations n) → (x : Fin n → A) → Decidable (FirstOrder.Language.Structure.RelMap R x)] (i : Fin V.numSyms) (t : ℕ) : bitAt V k e i t = true ↔ bitOf V i (tupOf V k e i t)

The drawn bit reads the source relation at the cell's tuple.

noncomputable def DescriptiveComplexity.HaltHard.inpH {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (k : ℕ) (e : Fin (k + 1) ≃o A) [(n : ℕ) → (R : L.Relations n) → (x : Fin n → A) → Decidable (FirstOrder.Language.Structure.RelMap R x)] : List ((haltTuringInterp V cF cP).Map A)

The initial letters, cell by cell.

Equations

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

The enumeration is strictly ordered

def DescriptiveComplexity.HaltHard.SLt {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) {A : Type} [L.Structure A] [LinearOrder A] (p q : (haltTuringInterp V cF cP).Map A) : Prop

The strict order of the drawn machine.

Equations

• DescriptiveComplexity.HaltHard.SLt V cF cP p q = ((DescriptiveComplexity.tmData ((DescriptiveComplexity.HaltHard.haltTuringInterp V cF cP).Map A)).Le p q ∧ p ≠ q)

theorem DescriptiveComplexity.HaltHard.sLt_intro {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) {A : Type} [L.Structure A] [LinearOrder A] {t t' : HTag V cF cP} {w w' : Fin (dimOf V) → A} (hle : HLe V cF cP (t, w) (t', w')) (hne : t ≠ t' ∨ w ≠ w') : SLt V cF cP (hPt t w) (hPt t' w')

theorem DescriptiveComplexity.HaltHard.sLt_of_blockLt {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) {A : Type} [L.Structure A] [LinearOrder A] {t t' : HTag V cF cP} (h : blockIdx V cF cP t < blockIdx V cF cP t') (w w' : Fin (dimOf V) → A) : SLt V cF cP (hPt t w) (hPt t' w')

theorem DescriptiveComplexity.HaltHard.sLt_of_revLex {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) {A : Type} [L.Structure A] [LinearOrder A] {t t' : HTag V cF cP} (hb : blockIdx V cF cP t = blockIdx V cF cP t') {w w' : Fin (dimOf V) → A} (h : RevLexLt w' w) : SLt V cF cP (hPt t w) (hPt t' w')

theorem DescriptiveComplexity.HaltHard.sLt_bit_fold {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) {A : Type} [L.Structure A] [LinearOrder A] (i : Fin V.numSyms) (w : Fin (dimOf V) → A) : SLt V cF cP (hPt (Sum.inr (CellTag.cBit i)) w) (hPt (Sum.inr (CellTag.cFold i)) w)

theorem DescriptiveComplexity.HaltHard.sLt_one {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (k : ℕ) (e : Fin (k + 1) ≃o A) {a a' : Fin (k + 1)} (h : a' < a) : SLt V cF cP (hPt (Sum.inr CellTag.cOne) (pad (botOrd A) fun (x : Fin 1) => e a)) (hPt (Sum.inr CellTag.cOne) (pad (botOrd A) fun (x : Fin 1) => e a'))

theorem DescriptiveComplexity.HaltHard.pairwise_flatMap {α β : Type} {R : β → β → Prop} {f : α → List β} {l : List α} : (∀ a ∈ l, List.Pairwise R (f a)) → List.Pairwise (fun (a b : α) => ∀ x ∈ f a, ∀ y ∈ f b, R x y) l → List.Pairwise R (List.flatMap f l)

Pairwise over a flatMap, from pairwise inside each image and pairwise across the images.

def DescriptiveComplexity.HaltHard.BitLt {L : FirstOrder.Language} (V : L.FinVocab) (p q : Fin V.numSyms × ℕ) : Prop

Later chain indices are smaller: symbols descending, tuple numbers descending inside a symbol.

Equations

• DescriptiveComplexity.HaltHard.BitLt V p q = (↑q.1 < ↑p.1 ∨ q.1 = p.1 ∧ q.2 < p.2)

theorem DescriptiveComplexity.HaltHard.pairwise_bitIdx {L : FirstOrder.Language} (V : L.FinVocab) (k : ℕ) : List.Pairwise (BitLt V) (bitIdx V k)

theorem DescriptiveComplexity.HaltHard.pairwise_chainCells {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (k : ℕ) (e : Fin (k + 1) ≃o A) : List.Pairwise (SLt V cF cP) (chainCells V cF cP k e)

theorem DescriptiveComplexity.HaltHard.pairwise_oneCells {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (k : ℕ) (e : Fin (k + 1) ≃o A) : List.Pairwise (SLt V cF cP) (oneCells V cF cP k e)

theorem DescriptiveComplexity.HaltHard.tag_of_mem_chainCells {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (k : ℕ) (e : Fin (k + 1) ≃o A) {x : (haltTuringInterp V cF cP).Map A} (hx : x ∈ chainCells V cF cP k e) : ∃ (i : Fin V.numSyms) (w : Fin (dimOf V) → A), x = hPt (Sum.inr (CellTag.cBit i)) w ∨ x = hPt (Sum.inr (CellTag.cFold i)) w

theorem DescriptiveComplexity.HaltHard.tag_of_mem_oneCells {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (k : ℕ) (e : Fin (k + 1) ≃o A) {x : (haltTuringInterp V cF cP).Map A} (hx : x ∈ oneCells V cF cP k e) : ∃ (w : Fin (dimOf V) → A), x = hPt (Sum.inr CellTag.cOne) w

theorem DescriptiveComplexity.HaltHard.blockIdx_cEndL {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) : blockIdx V cF cP (Sum.inr CellTag.cEndL) = 0

theorem DescriptiveComplexity.HaltHard.blockIdx_cBit {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) (i : Fin V.numSyms) : blockIdx V cF cP (Sum.inr (CellTag.cBit i)) = 1 + (V.numSyms - 1 - ↑i)

theorem DescriptiveComplexity.HaltHard.blockIdx_cFold {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) (i : Fin V.numSyms) : blockIdx V cF cP (Sum.inr (CellTag.cFold i)) = 1 + (V.numSyms - 1 - ↑i)

theorem DescriptiveComplexity.HaltHard.blockIdx_cProc {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) : blockIdx V cF cP (Sum.inr CellTag.cProc) = V.numSyms + 1

theorem DescriptiveComplexity.HaltHard.blockIdx_cMid {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) : blockIdx V cF cP (Sum.inr CellTag.cMid) = V.numSyms + 2

theorem DescriptiveComplexity.HaltHard.blockIdx_cGap {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) : blockIdx V cF cP (Sum.inr CellTag.cGap) = V.numSyms + 3

theorem DescriptiveComplexity.HaltHard.blockIdx_cComL {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) : blockIdx V cF cP (Sum.inr CellTag.cComL) = V.numSyms + 4

theorem DescriptiveComplexity.HaltHard.blockIdx_cOne {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) : blockIdx V cF cP (Sum.inr CellTag.cOne) = V.numSyms + 5

theorem DescriptiveComplexity.HaltHard.blockIdx_cComR {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) : blockIdx V cF cP (Sum.inr CellTag.cComR) = V.numSyms + 6

theorem DescriptiveComplexity.HaltHard.blockIdx_cEndR {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) : blockIdx V cF cP (Sum.inr CellTag.cEndR) = V.numSyms + 7

theorem DescriptiveComplexity.HaltHard.pairwise_psH {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (k : ℕ) (e : Fin (k + 1) ≃o A) : List.Pairwise (SLt V cF cP) (psH V cF cP k e)

The cells are strictly ordered as listed.

The enumeration and the initial tape

theorem DescriptiveComplexity.HaltHard.isPosEnum_psH {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (k : ℕ) (e : Fin (k + 1) ≃o A) : HaltPcp.IsPosEnum (tmData ((haltTuringInterp V cF cP).Map A)) (psH V cF cP k e)

The listed cells enumerate the positions in the machine's order.

theorem DescriptiveComplexity.HaltHard.forall₂_flatMap {α β γ : Type} {R : β → γ → Prop} {f : α → List β} {g : α → List γ} {l : List α} : (∀ a ∈ l, List.Forall₂ R (f a) (g a)) → List.Forall₂ R (List.flatMap f l) (List.flatMap g l)

theorem DescriptiveComplexity.HaltHard.forall₂_map_replicate {α β γ : Type} {R : β → γ → Prop} {F : α → β} {c : γ} {l : List α} : (∀ a ∈ l, R (F a) c) → List.Forall₂ R (List.map F l) (List.replicate l.length c)

theorem DescriptiveComplexity.HaltHard.forall₂_initTape {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] [(n : ℕ) → (R : L.Relations n) → (x : Fin n → A) → Decidable (FirstOrder.Language.Structure.RelMap R x)] (k : ℕ) (e : Fin (k + 1) ≃o A) : List.Forall₂ (tmData ((haltTuringInterp V cF cP).Map A)).InitTape (psH V cF cP k e) (inpH V cF cP k e)

The listed letters are the initial tape of the listed cells.

theorem DescriptiveComplexity.HaltHard.reverse_flatMap {α β : Type} (f : α → List β) (l : List α) : (List.flatMap f l).reverse = List.flatMap (fun (a : α) => (f a).reverse) l.reverse

theorem DescriptiveComplexity.HaltHard.table_flatten_reverse_eq {L : FirstOrder.Language} (V : L.FinVocab) {A : Type} [L.Structure A] [LinearOrder A] [L.IsRelational] [(n : ℕ) → (R : L.Relations n) → (x : Fin n → A) → Decidable (FirstOrder.Language.Structure.RelMap R x)] (k : ℕ) (e : Fin (k + 1) ≃o A) : (FirstOrder.Language.FinStruct.ofEquiv V k e.toEquiv).table.flatten.reverse = List.map (fun (p : Fin V.numSyms × ℕ) => bitAt V k e p.1 p.2) (bitIdx V k)

The reversed flattened table is the drawn bit sequence.

theorem DescriptiveComplexity.HaltHard.replicate_rotate {α : Type} (a : α) (n : ℕ) (l : List α) : List.replicate n a ++ a :: l = a :: (List.replicate n a ++ l)

theorem DescriptiveComplexity.HaltHard.inpH_eq {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] [(n : ℕ) → (R : L.Relations n) → (x : Fin n → A) → Decidable (FirstOrder.Language.Structure.RelMap R x)] (k : ℕ) (e : Fin (k + 1) ≃o A) : inpH V cF cP k e = List.map mEl (List.map sts (SimSym.endL :: (List.flatMap (fun (b : Bool) => [SimSym.hComp (posBit cF cP b), SimSym.hComp (posFold cF cP)]) (List.map (fun (p : Fin V.numSyms × ℕ) => bitAt V k e p.1 p.2) (bitIdx V k)) ++ [SimSym.hComp (posProc cF cP)] ++ SimSym.mid :: valR [0, k + 1] 0 0)))

The listed letters are the image of the spelled initial word.

theorem DescriptiveComplexity.HaltHard.holds_haltMap_iff {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] [L.IsRelational] (k : ℕ) (e : Fin (k + 1) ≃o A) {P : DecisionProblem L} (hF : ∀ (v : List.Vector ℕ 3), cF.eval ↑v = pure <$> foldSpec v) (hP : ∀ (N n : ℕ), (cP.eval [N, n]).Dom ↔ P.toPred V (structOfBits V (n - 1) N)) : HALT.Holds ((haltTuringInterp V cF cP).Map A) ↔ P.Holds A

Correctness of the drawing: the drawn instance is a yes-instance of the halting problem exactly when the source structure is one.