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

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.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

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 FirstOrder.Language.tupleIdx of the coordinates read through the numbering. One direction is proved arithmetically; the other falls out of trichotomy and injectivity.

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_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.tupleIdx_eq_zero {c : ℕ} {l : List ℕ} : (∀ a ∈ l, a = 0) → FirstOrder.Language.tupleIdx c l = 0

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.

Membership: the cells are exactly the positions

The initial letters

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)

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.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

The enumeration and the initial tape

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.replicate_rotate {α : Type} (a : α) (n : ℕ) (l : List α) : List.replicate n a ++ a :: l = a :: (List.replicate n a ++ l)