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

def DescriptiveComplexity.HaltHard.CellTag.key {L : FirstOrder.Language} (V : L.FinVocab) : CellTag V → Fin 10 × Fin (V.numSyms + 1)

An injective numbering of the cell tags, for finiteness.

Equations

• DescriptiveComplexity.HaltHard.CellTag.key V DescriptiveComplexity.HaltHard.CellTag.cEndL = (0, 0)
• DescriptiveComplexity.HaltHard.CellTag.key V (DescriptiveComplexity.HaltHard.CellTag.cBit i) = (1, i.castSucc)
• DescriptiveComplexity.HaltHard.CellTag.key V (DescriptiveComplexity.HaltHard.CellTag.cFold i) = (2, i.castSucc)
• DescriptiveComplexity.HaltHard.CellTag.key V DescriptiveComplexity.HaltHard.CellTag.cProc = (3, 0)
• DescriptiveComplexity.HaltHard.CellTag.key V DescriptiveComplexity.HaltHard.CellTag.cMid = (4, 0)
• DescriptiveComplexity.HaltHard.CellTag.key V DescriptiveComplexity.HaltHard.CellTag.cGap = (5, 0)
• DescriptiveComplexity.HaltHard.CellTag.key V DescriptiveComplexity.HaltHard.CellTag.cComL = (6, 0)
• DescriptiveComplexity.HaltHard.CellTag.key V DescriptiveComplexity.HaltHard.CellTag.cOne = (7, 0)
• DescriptiveComplexity.HaltHard.CellTag.key V DescriptiveComplexity.HaltHard.CellTag.cComR = (8, 0)
• DescriptiveComplexity.HaltHard.CellTag.key V DescriptiveComplexity.HaltHard.CellTag.cEndR = (9, 0)

theorem DescriptiveComplexity.HaltHard.CellTag.key_injective {L : FirstOrder.Language} (V : L.FinVocab) : Function.Injective (key V)

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

theorem DescriptiveComplexity.HaltHard.CellTag.used_le_dimOf {L : FirstOrder.Language} (V : L.FinVocab) (c : CellTag V) : used V c ≤ dimOf V

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

theorem DescriptiveComplexity.HaltHard.uCode_injective (cF cP : Turing.ToPartrec.Code) : Function.Injective (uCode cF cP)

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

theorem DescriptiveComplexity.HaltHard.tag_eq_of_idx {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) {t t' : HTag V cF cP} (hb : blockIdx V cF cP t = blockIdx V cF cP t') (hs : subIdx V cF cP t = subIdx V cF cP t') : t = t'

The pair of indices determines the tag.

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 DescriptiveComplexity.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.irrefl {A : Type} [LinearOrder A] {D : ℕ} {u : Fin D → A} (h : RevLexLt u u) : False

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

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

theorem DescriptiveComplexity.HaltHard.revLexLt_trichotomy {A : Type} [LinearOrder A] {D : ℕ} (u w : Fin D → A) : RevLexLt u w ∨ u = w ∨ RevLexLt w u

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.

theorem DescriptiveComplexity.HaltHard.isLinOrd_hLe {L : FirstOrder.Language} (V : L.FinVocab) (cF cP : Turing.ToPartrec.Code) {A : Type} [LinearOrder A] : IsLinOrd (HLe V cF cP)

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

theorem DescriptiveComplexity.HaltHard.hLe_def {L : FirstOrder.Language} {V : L.FinVocab} {cF cP : Turing.ToPartrec.Code} {A : Type} [LinearOrder A] (t t' : HTag V cF cP) (w w' : Fin (dimOf V) → A) : HLe V cF cP (t, w) (t', w') ↔ blockIdx V cF cP t < blockIdx V cF cP t' ∨ blockIdx V cF cP t = blockIdx V cF cP t' ∧ (RevLexLt w' w ∨ w = w' ∧ subIdx V cF cP t ≤ subIdx V cF cP t')

The order, with the projections of the point reduced.

theorem DescriptiveComplexity.HaltHard.realize_revLexLtF {L : FirstOrder.Language} {V : L.FinVocab} {A : Type} [L.Structure A] [LinearOrder A] {γ : Type} {p q : Fin (dimOf V) → γ} {v : γ → A} : (revLexLtF V p q).Realize v ↔ RevLexLt (fun (j : Fin (dimOf V)) => v (p j)) fun (j : Fin (dimOf V)) => v (q j)

theorem DescriptiveComplexity.HaltHard.relMap_posn {L : FirstOrder.Language} {V : L.FinVocab} {cF cP : Turing.ToPartrec.Code} {A : Type} [L.Structure A] [LinearOrder A] (t : HTag V cF cP) (w : Fin (dimOf V) → A) : TMPosn (hPt t w) ↔ ∃ (c : CellTag V), t = Sum.inr c ∧ Canon (CellTag.used V c) w

theorem DescriptiveComplexity.HaltHard.relMap_unary {L : FirstOrder.Language} {V : L.FinVocab} {cF cP : Turing.ToPartrec.Code} {A : Type} [L.Structure A] [LinearOrder 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)) (t : HTag V cF cP) (w : Fin (dimOf V) → A) : FirstOrder.Language.Structure.RelMap (have this := R; this) ![hPt t w] ↔ (∃ (u : SimU (allCode cF cP)), t = Sum.inl u ∧ Q u) ∧ Canon 0 w

theorem DescriptiveComplexity.HaltHard.relMap_binary {L : FirstOrder.Language} {V : L.FinVocab} {cF cP : Turing.ToPartrec.Code} {A : Type} [L.Structure A] [LinearOrder 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)) (t t' : HTag V cF cP) (w w' : Fin (dimOf V) → A) : FirstOrder.Language.Structure.RelMap (have this := R; this) ![hPt t w, hPt t' w'] ↔ (∃ (u : SimU (allCode cF cP)) (u' : SimU (allCode cF cP)), t = Sum.inl u ∧ t' = Sum.inl u' ∧ Q u u') ∧ Canon 0 w ∧ Canon 0 w'

theorem DescriptiveComplexity.HaltHard.relMap_le {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) : TMLe (hPt t w) (hPt t' w') ↔ HLe V cF cP (t, w) (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

theorem DescriptiveComplexity.HaltHard.relMap_inp {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) : TMInp (hPt t w) (hPt t' w') ↔ ∃ (c : CellTag V) (u : SimU (allCode cF cP)), t = Sum.inr c ∧ t' = Sum.inl u ∧ Canon (CellTag.used V c) w ∧ Canon 0 w' ∧ InpOn V cF cP c u w