Drawing the simulating machine and its input page

The interpretation of the reduction P ≤ᶠᵒ[≤] HALT: the states, symbols and transitions of the simulating machine are tags – constant at every instance size – and the cells of its initial tape are tagged tuples of the source structure: one bit cell and one fold cell per tuple of each source relation (the chain of DescriptiveComplexity.HaltHard.inputChain), and a handful of constant cells for the markers and the spelled initial value [0, n].

The one order key of the whole universe, junk included: the block index of the tag, then the tuple in descending lexicographic order with the last coordinate most significant – matching the little-endian significance of FirstOrder.Language.tupleIdx, so that position-ascending order reads the flattened relation table reversed, which is the order the chain folds – and a static sub-index that interleaves each bit cell with its fold cell. Unused coordinates are pinned to the minimum (DescriptiveComplexity.Canon), so cells enumerate exactly once.

The cell tags

inductive DescriptiveComplexity.HaltHard.CellTag {L : FirstOrder.Language} (V : L.FinVocab) : Type

The tags of the input cells: the left marker, one bit cell and one fold cell per source symbol (carrying a tuple of its arity), the procedure cell, the middle marker, the inner blank, and the spelled initial value [0, n] – a separator, one digit cell per element, a separator, and the right marker.

• cEndL {L : FirstOrder.Language} {V : L.FinVocab} : CellTag V

  The cell of endL.

• cBit {L : FirstOrder.Language} {V : L.FinVocab} (i : Fin V.numSyms) : CellTag V

  A bit cell of the chain: one per tuple of the source symbol i.

• cFold {L : FirstOrder.Language} {V : L.FinVocab} (i : Fin V.numSyms) : CellTag V

  The fold cell paired with a bit cell.

• cProc {L : FirstOrder.Language} {V : L.FinVocab} : CellTag V

  The cell of the final comp header, the semi-decision procedure.

• cMid {L : FirstOrder.Language} {V : L.FinVocab} : CellTag V

  The cell of mid.

• cGap {L : FirstOrder.Language} {V : L.FinVocab} : CellTag V

  The one blank of the inner gap.

• cComL {L : FirstOrder.Language} {V : L.FinVocab} : CellTag V

  The separator left of the digits.

• cOne {L : FirstOrder.Language} {V : L.FinVocab} : CellTag V

  A digit cell of the spelled size: one per element.

• cComR {L : FirstOrder.Language} {V : L.FinVocab} : CellTag V

  The separator right of the digits.

• cEndR {L : FirstOrder.Language} {V : L.FinVocab} : CellTag V

  The cell of endR.

instance DescriptiveComplexity.HaltHard.CellTag.instFinite {L : FirstOrder.Language} (V : L.FinVocab) : Finite (CellTag V)

instance DescriptiveComplexity.HaltHard.CellTag.instNonempty {L : FirstOrder.Language} (V : L.FinVocab) : Nonempty (CellTag V)

def DescriptiveComplexity.HaltHard.CellTag.used {L : FirstOrder.Language} (V : L.FinVocab) : CellTag V → ℕ

The coordinates a cell tag uses; the rest are pinned to the minimum.

Equations

• DescriptiveComplexity.HaltHard.CellTag.used V (DescriptiveComplexity.HaltHard.CellTag.cBit i) = V.arity i
• DescriptiveComplexity.HaltHard.CellTag.used V (DescriptiveComplexity.HaltHard.CellTag.cFold i) = V.arity i
• DescriptiveComplexity.HaltHard.CellTag.used V DescriptiveComplexity.HaltHard.CellTag.cOne = 1
• DescriptiveComplexity.HaltHard.CellTag.used V x✝ = 0

The tags of the drawn instance

@[reducible, inline]

abbrev DescriptiveComplexity.HaltHard.HTag {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) : Type

The tags of the drawn instance: a machine element – a state, a symbol or a transition of the simulating machine – or an input cell.

Equations

• DescriptiveComplexity.HaltHard.HTag V cF cP = (DescriptiveComplexity.HaltHard.SimU (DescriptiveComplexity.HaltHard.allCode cF cP) ⊕ DescriptiveComplexity.HaltHard.CellTag V)

instance DescriptiveComplexity.HaltHard.instFiniteHTag {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) : Finite (HTag V cF cP)

instance DescriptiveComplexity.HaltHard.instNonemptyHTag {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) : Nonempty (HTag V cF cP)

def DescriptiveComplexity.HaltHard.HTag.used {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) : HTag V cF cP → ℕ

The coordinates a tag uses.

Equations

• DescriptiveComplexity.HaltHard.HTag.used V cF cP (Sum.inl val) = 0
• DescriptiveComplexity.HaltHard.HTag.used V cF cP (Sum.inr c) = DescriptiveComplexity.HaltHard.CellTag.used V c

noncomputable def DescriptiveComplexity.HaltHard.uCode (cF cP : Turing.ToPartrec.Code) : SimU (allCode cF cP) → ℕ

A chosen injective numbering of the machine elements, for the order on the junk.

Equations

• DescriptiveComplexity.HaltHard.uCode cF cP = ⋯.choose

noncomputable def DescriptiveComplexity.HaltHard.blockIdx {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) : HTag V cF cP → ℕ

The block index of a tag – the primary component of the one order key. The chain blocks descend along the symbols, each shared by the bit and fold tags; the machine elements sit above everything, ordered by the chosen numbering.

Equations

• DescriptiveComplexity.HaltHard.blockIdx V cF cP (Sum.inr DescriptiveComplexity.HaltHard.CellTag.cEndL) = 0
• DescriptiveComplexity.HaltHard.blockIdx V cF cP (Sum.inr (DescriptiveComplexity.HaltHard.CellTag.cBit i)) = 1 + (V.numSyms - 1 - ↑i)
• DescriptiveComplexity.HaltHard.blockIdx V cF cP (Sum.inr (DescriptiveComplexity.HaltHard.CellTag.cFold i)) = 1 + (V.numSyms - 1 - ↑i)
• DescriptiveComplexity.HaltHard.blockIdx V cF cP (Sum.inr DescriptiveComplexity.HaltHard.CellTag.cProc) = V.numSyms + 1
• DescriptiveComplexity.HaltHard.blockIdx V cF cP (Sum.inr DescriptiveComplexity.HaltHard.CellTag.cMid) = V.numSyms + 2
• DescriptiveComplexity.HaltHard.blockIdx V cF cP (Sum.inr DescriptiveComplexity.HaltHard.CellTag.cGap) = V.numSyms + 3
• DescriptiveComplexity.HaltHard.blockIdx V cF cP (Sum.inr DescriptiveComplexity.HaltHard.CellTag.cComL) = V.numSyms + 4
• DescriptiveComplexity.HaltHard.blockIdx V cF cP (Sum.inr DescriptiveComplexity.HaltHard.CellTag.cOne) = V.numSyms + 5
• DescriptiveComplexity.HaltHard.blockIdx V cF cP (Sum.inr DescriptiveComplexity.HaltHard.CellTag.cComR) = V.numSyms + 6
• DescriptiveComplexity.HaltHard.blockIdx V cF cP (Sum.inr DescriptiveComplexity.HaltHard.CellTag.cEndR) = V.numSyms + 7
• DescriptiveComplexity.HaltHard.blockIdx V cF cP (Sum.inl u) = V.numSyms + 8 + DescriptiveComplexity.HaltHard.uCode cF cP u

def DescriptiveComplexity.HaltHard.subIdx {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) : HTag V cF cP → ℕ

The sub-index breaking the tie inside a chain block: the fold cell sits right of its bit cell.

Equations

• DescriptiveComplexity.HaltHard.subIdx V cF cP (Sum.inr (DescriptiveComplexity.HaltHard.CellTag.cFold i)) = 1
• DescriptiveComplexity.HaltHard.subIdx V cF cP x✝ = 0

The reversed lexicographic order on tuples

def DescriptiveComplexity.HaltHard.RevLexLt {A : Type} [LinearOrder A] {D : ℕ} (u w : Fin D → A) : Prop

u is below w in the reversed lexicographic order: they differ, and at the highest differing coordinate u is smaller. Matching the little-endian significance of FirstOrder.Language.tupleIdx, this is comparison of tuple numbers.

Equations

• DescriptiveComplexity.HaltHard.RevLexLt u w = ∃ (j : Fin D), u j < w j ∧ ∀ (j' : Fin D), j < j' → u j' = w j'

theorem DescriptiveComplexity.HaltHard.RevLexLt.trans {A : Type} [LinearOrder A] {D : ℕ} {u w x : Fin D → A} (h : RevLexLt u w) (h' : RevLexLt w x) : RevLexLt u x

The one order of the whole universe

noncomputable def DescriptiveComplexity.HaltHard.HLe {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) {A : Type} [LinearOrder A] (x y : HTag V cF cP × (Fin (dimOf V) → A)) : Prop

The order of the drawn universe, junk included: block index of the tag, then the tuple – descending along the reversed lexicographic order, so that ascending positions read descending tuple numbers – then the sub-index.

Equations

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

The defining formulas

noncomputable def DescriptiveComplexity.HaltHard.revLexLtF {L : FirstOrder.Language} (V : L.FinVocab) {γ : Type} (p q : Fin (dimOf V) → γ) : (L.sum FirstOrder.Language.order).Formula γ

The reversed lexicographic comparison, as a formula: p is below q.

Equations

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

noncomputable def DescriptiveComplexity.HaltHard.hPosnF {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) (t : HTag V cF cP) : (L.sum FirstOrder.Language.order).Formula (Fin 1 × Fin (dimOf V))

Being a position: a cell tag on a canonically padded tuple.

Equations

• DescriptiveComplexity.HaltHard.hPosnF V cF cP (Sum.inl val) = ⊥
• DescriptiveComplexity.HaltHard.hPosnF V cF cP (Sum.inr c) = DescriptiveComplexity.canonF (DescriptiveComplexity.HaltHard.CellTag.used V c) (DescriptiveComplexity.CodeProgRed.sel₀ V)

noncomputable def DescriptiveComplexity.HaltHard.mUnaryF {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) (Q : SimU (allCode cF cP) → Prop) (t : HTag V cF cP) : (L.sum FirstOrder.Language.order).Formula (Fin 1 × Fin (dimOf V))

A unary machine predicate: the tag is a machine element satisfying it, canonically padded.

Equations

• DescriptiveComplexity.HaltHard.mUnaryF V cF cP Q (Sum.inl val) = if Q val then DescriptiveComplexity.canonF 0 (DescriptiveComplexity.CodeProgRed.sel₀ V) else ⊥
• DescriptiveComplexity.HaltHard.mUnaryF V cF cP Q (Sum.inr c) = ⊥

noncomputable def DescriptiveComplexity.HaltHard.mBinaryF {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) (Q : SimU (allCode cF cP) → SimU (allCode cF cP) → Prop) (t t' : HTag V cF cP) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin (dimOf V))

A binary machine predicate: two machine elements satisfying it, canonically padded.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.HaltHard.mBinaryF V cF cP Q t t' = ⊥

noncomputable def DescriptiveComplexity.HaltHard.hLeF {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) (t t' : HTag V cF cP) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin (dimOf V))

The order, by the one key: block index, then the reversed lexicographic order descending, then the sub-index.

Equations

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

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

The letter a cell initially holds, semantically: the marker of its tag, and on a bit cell the pushed bit reads the source relation.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.HaltHard.InpOn V cF cP DescriptiveComplexity.HaltHard.CellTag.cEndL u w = (u = DescriptiveComplexity.HaltHard.sts DescriptiveComplexity.HaltHard.SimSym.endL)
• DescriptiveComplexity.HaltHard.InpOn V cF cP DescriptiveComplexity.HaltHard.CellTag.cMid u w = (u = DescriptiveComplexity.HaltHard.sts DescriptiveComplexity.HaltHard.SimSym.mid)
• DescriptiveComplexity.HaltHard.InpOn V cF cP DescriptiveComplexity.HaltHard.CellTag.cGap u w = (u = DescriptiveComplexity.HaltHard.sts DescriptiveComplexity.HaltHard.SimSym.bk)
• DescriptiveComplexity.HaltHard.InpOn V cF cP DescriptiveComplexity.HaltHard.CellTag.cComL u w = (u = DescriptiveComplexity.HaltHard.sts DescriptiveComplexity.HaltHard.SimSym.com)
• DescriptiveComplexity.HaltHard.InpOn V cF cP DescriptiveComplexity.HaltHard.CellTag.cOne u w = (u = DescriptiveComplexity.HaltHard.sts DescriptiveComplexity.HaltHard.SimSym.one)
• DescriptiveComplexity.HaltHard.InpOn V cF cP DescriptiveComplexity.HaltHard.CellTag.cComR u w = (u = DescriptiveComplexity.HaltHard.sts DescriptiveComplexity.HaltHard.SimSym.com)
• DescriptiveComplexity.HaltHard.InpOn V cF cP DescriptiveComplexity.HaltHard.CellTag.cEndR u w = (u = DescriptiveComplexity.HaltHard.sts DescriptiveComplexity.HaltHard.SimSym.endR)

noncomputable def DescriptiveComplexity.HaltHard.inpBodyF {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) (c : CellTag V) (u : SimU (allCode cF cP)) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin (dimOf V))

The body of the initial-tape relation, per cell tag and letter.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.HaltHard.inpBodyF V cF cP DescriptiveComplexity.HaltHard.CellTag.cEndL u = if u = DescriptiveComplexity.HaltHard.sts DescriptiveComplexity.HaltHard.SimSym.endL then ⊤ else ⊥
• DescriptiveComplexity.HaltHard.inpBodyF V cF cP DescriptiveComplexity.HaltHard.CellTag.cMid u = if u = DescriptiveComplexity.HaltHard.sts DescriptiveComplexity.HaltHard.SimSym.mid then ⊤ else ⊥
• DescriptiveComplexity.HaltHard.inpBodyF V cF cP DescriptiveComplexity.HaltHard.CellTag.cGap u = if u = DescriptiveComplexity.HaltHard.sts DescriptiveComplexity.HaltHard.SimSym.bk then ⊤ else ⊥
• DescriptiveComplexity.HaltHard.inpBodyF V cF cP DescriptiveComplexity.HaltHard.CellTag.cComL u = if u = DescriptiveComplexity.HaltHard.sts DescriptiveComplexity.HaltHard.SimSym.com then ⊤ else ⊥
• DescriptiveComplexity.HaltHard.inpBodyF V cF cP DescriptiveComplexity.HaltHard.CellTag.cOne u = if u = DescriptiveComplexity.HaltHard.sts DescriptiveComplexity.HaltHard.SimSym.one then ⊤ else ⊥
• DescriptiveComplexity.HaltHard.inpBodyF V cF cP DescriptiveComplexity.HaltHard.CellTag.cComR u = if u = DescriptiveComplexity.HaltHard.sts DescriptiveComplexity.HaltHard.SimSym.com then ⊤ else ⊥
• DescriptiveComplexity.HaltHard.inpBodyF V cF cP DescriptiveComplexity.HaltHard.CellTag.cEndR u = if u = DescriptiveComplexity.HaltHard.sts DescriptiveComplexity.HaltHard.SimSym.endR then ⊤ else ⊥

noncomputable def DescriptiveComplexity.HaltHard.hInpF {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) (t t' : HTag V cF cP) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin (dimOf V))

The initial-tape relation: a cell and a canonically padded symbol element, related by the body.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.HaltHard.hInpF V cF cP t t' = ⊥

noncomputable def DescriptiveComplexity.HaltHard.haltTuringInterp {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) : FOInterpretation (L.sum FirstOrder.Language.order) FirstOrder.Language.turing (HTag V cF cP) (dimOf V)

The interpretation: machine elements and input cells as tagged tuples, the machine relations read off DescriptiveComplexity.HaltHard.simTM at the tags, the input page reading the source relations.

Equations

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

Characterization of the interpreted relations

def DescriptiveComplexity.HaltHard.hPt {L : FirstOrder.Language} {V : L.FinVocab} {cF cP : Turing.ToPartrec.Code} {A : Type} (t : HTag V cF cP) (w : Fin (dimOf V) → A) : (haltTuringInterp V cF cP).Map A

The element of the drawn instance with a given tag and tuple.

Equations

• DescriptiveComplexity.HaltHard.hPt t w = (t, w)

theorem DescriptiveComplexity.HaltHard.exists_hPt {L : FirstOrder.Language} {V : L.FinVocab} {cF cP : Turing.ToPartrec.Code} {A : Type} (x : (haltTuringInterp V cF cP).Map A) : ∃ (t : HTag V cF cP) (w : Fin (dimOf V) → A), x = hPt t w

@[simp]

theorem DescriptiveComplexity.HaltHard.val_sel₀ {L : FirstOrder.Language} {V : L.FinVocab} {cF cP : Turing.ToPartrec.Code} {A : Type} (t : HTag V cF cP) (w : Fin (dimOf V) → A) (j : Fin (dimOf V)) : (![hPt t w] (CodeProgRed.sel₀ V j).1).2 (CodeProgRed.sel₀ V j).2 = w j

@[simp]

theorem DescriptiveComplexity.HaltHard.val_selA {L : FirstOrder.Language} {V : L.FinVocab} {cF cP : Turing.ToPartrec.Code} {A : Type} (t t' : HTag V cF cP) (w w' : Fin (dimOf V) → A) (j : Fin (dimOf V)) : (![hPt t w, hPt t' w'] (CodeProgRed.selA V j).1).2 (CodeProgRed.selA V j).2 = w j

@[simp]

theorem DescriptiveComplexity.HaltHard.val_selB {L : FirstOrder.Language} {V : L.FinVocab} {cF cP : Turing.ToPartrec.Code} {A : Type} (t t' : HTag V cF cP) (w w' : Fin (dimOf V) → A) (j : Fin (dimOf V)) : (![hPt t w, hPt t' w'] (CodeProgRed.selB V j).1).2 (CodeProgRed.selB V j).2 = w' j

theorem DescriptiveComplexity.HaltHard.posBit_true_ne_false {cF cP : Turing.ToPartrec.Code} : posBit cF cP true ≠ posBit cF cP false

theorem DescriptiveComplexity.HaltHard.posBit_false_ne_true {cF cP : Turing.ToPartrec.Code} : posBit cF cP false ≠ posBit cF cP true