The interpretation: drawing the domino system first-order

The first-order half of HALT ≤ᶠᵒ[≤] PCP: the defining formulas of an interpretation of Language.pcp in ordered machine instances, each realizing exactly the corresponding semantic predicate of DescriptiveComplexity.Problems.Pcp.Hardness.Draw – which is all the correctness proof of DescriptiveComplexity.Problems.Pcp.Hardness.Match consumes, through DescriptiveComplexity.HaltPcp.Reads.

Method

As in the QSAT machine interpretation, every static decision is taken in Lean rather than in the formula: the tags of the arguments are pattern-matched, and ⊤/⊥ close the cases the tables decide. The one genuinely recursive piece is DescriptiveComplexity.HaltPcp.specListF, which turns a word table of DescriptiveComplexity.HaltPcp.LSpec entries into a disjunction of “argument 1 is the i-th shared position and argument 2 is the specified letter” clauses – realized, by one induction over the table, as membership of the zipped table, which is verbatim the semantic letter relation DescriptiveComplexity.HaltPcp.PUAt.

@[reducible, inline]

abbrev DescriptiveComplexity.HaltPcp.haltOrd : FirstOrder.Language

The vocabulary the reduction reads: machine instances with the ambient order.

Equations

• DescriptiveComplexity.HaltPcp.haltOrd = FirstOrder.Language.turing.sum FirstOrder.Language.order

The symbols of the ordered expansion

@[reducible, inline]

abbrev DescriptiveComplexity.HaltPcp.hPosnSym : haltOrd.Relations 1

The position symbol.

Equations

• DescriptiveComplexity.HaltPcp.hPosnSym = Sum.inl FirstOrder.Language.turingRel.posn

@[reducible, inline]

abbrev DescriptiveComplexity.HaltPcp.hTrSym : haltOrd.Relations 1

The transition symbol.

Equations

• DescriptiveComplexity.HaltPcp.hTrSym = Sum.inl FirstOrder.Language.turingRel.tr

@[reducible, inline]

abbrev DescriptiveComplexity.HaltPcp.hStartSym : haltOrd.Relations 1

The start-state symbol.

Equations

• DescriptiveComplexity.HaltPcp.hStartSym = Sum.inl FirstOrder.Language.turingRel.start

@[reducible, inline]

abbrev DescriptiveComplexity.HaltPcp.hAccSym : haltOrd.Relations 1

The accepting-state symbol.

Equations

• DescriptiveComplexity.HaltPcp.hAccSym = Sum.inl FirstOrder.Language.turingRel.acc

@[reducible, inline]

abbrev DescriptiveComplexity.HaltPcp.hBlankSym : haltOrd.Relations 1

The blank symbol.

Equations

• DescriptiveComplexity.HaltPcp.hBlankSym = Sum.inl FirstOrder.Language.turingRel.blank

@[reducible, inline]

abbrev DescriptiveComplexity.HaltPcp.hRightSym : haltOrd.Relations 1

The move-right symbol.

Equations

• DescriptiveComplexity.HaltPcp.hRightSym = Sum.inl FirstOrder.Language.turingRel.right

@[reducible, inline]

abbrev DescriptiveComplexity.HaltPcp.hLeSym : haltOrd.Relations 2

The machine's order symbol.

Equations

• DescriptiveComplexity.HaltPcp.hLeSym = Sum.inl FirstOrder.Language.turingRel.le

@[reducible, inline]

abbrev DescriptiveComplexity.HaltPcp.hSrcSym : haltOrd.Relations 2

The transition-source symbol.

Equations

• DescriptiveComplexity.HaltPcp.hSrcSym = Sum.inl FirstOrder.Language.turingRel.tsrc

@[reducible, inline]

abbrev DescriptiveComplexity.HaltPcp.hReadSym : haltOrd.Relations 2

The transition-read symbol.

Equations

• DescriptiveComplexity.HaltPcp.hReadSym = Sum.inl FirstOrder.Language.turingRel.tread

@[reducible, inline]

abbrev DescriptiveComplexity.HaltPcp.hDstSym : haltOrd.Relations 2

The transition-destination symbol.

Equations

• DescriptiveComplexity.HaltPcp.hDstSym = Sum.inl FirstOrder.Language.turingRel.tdst

@[reducible, inline]

abbrev DescriptiveComplexity.HaltPcp.hWriteSym : haltOrd.Relations 2

The transition-write symbol.

Equations

• DescriptiveComplexity.HaltPcp.hWriteSym = Sum.inl FirstOrder.Language.turingRel.twrite

@[reducible, inline]

abbrev DescriptiveComplexity.HaltPcp.hInpSym : haltOrd.Relations 2

The input symbol.

Equations

• DescriptiveComplexity.HaltPcp.hInpSym = Sum.inl FirstOrder.Language.turingRel.inp

@[reducible, inline]

abbrev DescriptiveComplexity.HaltPcp.hOrdSym : haltOrd.Relations 2

The ambient order symbol.

Equations

• DescriptiveComplexity.HaltPcp.hOrdSym = Sum.inr FirstOrder.Language.leSymb

The builders

def DescriptiveComplexity.HaltPcp.posnF {α : Type} (x : α) : haltOrd.Formula α

x is a position.

Equations

• DescriptiveComplexity.HaltPcp.posnF x = DescriptiveComplexity.HaltPcp.hPosnSym.formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.HaltPcp.trF {α : Type} (x : α) : haltOrd.Formula α

x is a transition.

Equations

• DescriptiveComplexity.HaltPcp.trF x = DescriptiveComplexity.HaltPcp.hTrSym.formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.HaltPcp.startF {α : Type} (x : α) : haltOrd.Formula α

x is a start state.

Equations

• DescriptiveComplexity.HaltPcp.startF x = DescriptiveComplexity.HaltPcp.hStartSym.formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.HaltPcp.accF {α : Type} (x : α) : haltOrd.Formula α

x is an accepting state.

Equations

• DescriptiveComplexity.HaltPcp.accF x = DescriptiveComplexity.HaltPcp.hAccSym.formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.HaltPcp.blankF {α : Type} (x : α) : haltOrd.Formula α

x is the blank symbol.

Equations

• DescriptiveComplexity.HaltPcp.blankF x = DescriptiveComplexity.HaltPcp.hBlankSym.formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.HaltPcp.rightF {α : Type} (x : α) : haltOrd.Formula α

x moves the head right.

Equations

• DescriptiveComplexity.HaltPcp.rightF x = DescriptiveComplexity.HaltPcp.hRightSym.formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.HaltPcp.mLeF {α : Type} (x y : α) : haltOrd.Formula α

x ≤ y in the machine's order.

Equations

• DescriptiveComplexity.HaltPcp.mLeF x y = DescriptiveComplexity.HaltPcp.hLeSym.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

def DescriptiveComplexity.HaltPcp.srcF {α : Type} (x y : α) : haltOrd.Formula α

x applies in the state y.

Equations

• DescriptiveComplexity.HaltPcp.srcF x y = DescriptiveComplexity.HaltPcp.hSrcSym.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

def DescriptiveComplexity.HaltPcp.readF {α : Type} (x y : α) : haltOrd.Formula α

x reads the symbol y.

Equations

• DescriptiveComplexity.HaltPcp.readF x y = DescriptiveComplexity.HaltPcp.hReadSym.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

def DescriptiveComplexity.HaltPcp.dstF {α : Type} (x y : α) : haltOrd.Formula α

x moves to the state y.

Equations

• DescriptiveComplexity.HaltPcp.dstF x y = DescriptiveComplexity.HaltPcp.hDstSym.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

def DescriptiveComplexity.HaltPcp.writeF {α : Type} (x y : α) : haltOrd.Formula α

x writes the symbol y.

Equations

• DescriptiveComplexity.HaltPcp.writeF x y = DescriptiveComplexity.HaltPcp.hWriteSym.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

def DescriptiveComplexity.HaltPcp.inpF {α : Type} (x y : α) : haltOrd.Formula α

The cell x initially holds the symbol y.

Equations

• DescriptiveComplexity.HaltPcp.inpF x y = DescriptiveComplexity.HaltPcp.hInpSym.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

def DescriptiveComplexity.HaltPcp.ordF {α : Type} (x y : α) : haltOrd.Formula α

x ≤ y in the ambient order.

Equations

• DescriptiveComplexity.HaltPcp.ordF x y = DescriptiveComplexity.HaltPcp.hOrdSym.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

def DescriptiveComplexity.HaltPcp.eqF {α : Type} (x y : α) : haltOrd.Formula α

x = y.

Equations

• DescriptiveComplexity.HaltPcp.eqF x y = (FirstOrder.Language.var x).equal (FirstOrder.Language.var y)

def DescriptiveComplexity.HaltPcp.ordLtF {α : Type} (x y : α) : haltOrd.Formula α

x < y in the ambient order.

Equations

• DescriptiveComplexity.HaltPcp.ordLtF x y = DescriptiveComplexity.HaltPcp.ordF x y ⊓ FirstOrder.Language.BoundedFormula.not (DescriptiveComplexity.HaltPcp.eqF x y)

def DescriptiveComplexity.HaltPcp.mLtF {α : Type} (x y : α) : haltOrd.Formula α

x < y in the machine's order.

Equations

• DescriptiveComplexity.HaltPcp.mLtF x y = DescriptiveComplexity.HaltPcp.mLeF x y ⊓ FirstOrder.Language.BoundedFormula.not (DescriptiveComplexity.HaltPcp.eqF x y)

noncomputable def DescriptiveComplexity.HaltPcp.minF {α : Type} (x : α) : haltOrd.Formula α

x is the least element of the ambient order.

Equations

• DescriptiveComplexity.HaltPcp.minF x = FirstOrder.Language.Formula.iAlls (Fin 1) (DescriptiveComplexity.HaltPcp.ordF (Sum.inl x) (Sum.inr 0))

noncomputable def DescriptiveComplexity.HaltPcp.initTapeF {α : Type} (x y : α) : haltOrd.Formula α

The cell x initially holds y: its input symbol, or the blank if it has none.

Equations

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

noncomputable def DescriptiveComplexity.HaltPcp.wfF {α : Type} : haltOrd.Formula α

Well-formedness of the machine, as a formula with unused free variables: the machine's order is linear, there is a position, the input is functional, and there is exactly one blank.

Equations

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

noncomputable def DescriptiveComplexity.HaltPcp.existsMoveF {α : Type} (right : Bool) (q a b q' : α) : haltOrd.Formula α

Some transition with the given attributes exists; the direction of the move is a static decision.

Equations

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

Realization of the builders

@[simp]

theorem DescriptiveComplexity.HaltPcp.realize_posnF {α A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {v : α → A} {x : α} : (posnF x).Realize v ↔ TMPosn (v x)

@[simp]

theorem DescriptiveComplexity.HaltPcp.realize_trF {α A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {v : α → A} {x : α} : (trF x).Realize v ↔ TMTr (v x)

@[simp]

theorem DescriptiveComplexity.HaltPcp.realize_startF {α A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {v : α → A} {x : α} : (startF x).Realize v ↔ TMStart (v x)

@[simp]

theorem DescriptiveComplexity.HaltPcp.realize_accF {α A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {v : α → A} {x : α} : (accF x).Realize v ↔ TMAcc (v x)

@[simp]

theorem DescriptiveComplexity.HaltPcp.realize_blankF {α A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {v : α → A} {x : α} : (blankF x).Realize v ↔ TMBlank (v x)

@[simp]

theorem DescriptiveComplexity.HaltPcp.realize_rightF {α A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {v : α → A} {x : α} : (rightF x).Realize v ↔ TMRight (v x)

@[simp]

theorem DescriptiveComplexity.HaltPcp.realize_mLeF {α A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {v : α → A} {x y : α} : (mLeF x y).Realize v ↔ TMLe (v x) (v y)

@[simp]

theorem DescriptiveComplexity.HaltPcp.realize_srcF {α A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {v : α → A} {x y : α} : (srcF x y).Realize v ↔ TMSrc (v x) (v y)

@[simp]

theorem DescriptiveComplexity.HaltPcp.realize_readF {α A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {v : α → A} {x y : α} : (readF x y).Realize v ↔ TMRead (v x) (v y)

@[simp]

theorem DescriptiveComplexity.HaltPcp.realize_dstF {α A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {v : α → A} {x y : α} : (dstF x y).Realize v ↔ TMDst (v x) (v y)

@[simp]

theorem DescriptiveComplexity.HaltPcp.realize_writeF {α A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {v : α → A} {x y : α} : (writeF x y).Realize v ↔ TMWrite (v x) (v y)

@[simp]

theorem DescriptiveComplexity.HaltPcp.realize_inpF {α A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {v : α → A} {x y : α} : (inpF x y).Realize v ↔ TMInp (v x) (v y)

@[simp]

theorem DescriptiveComplexity.HaltPcp.realize_ordF {α A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {v : α → A} {x y : α} : (ordF x y).Realize v ↔ v x ≤ v y

@[simp]

theorem DescriptiveComplexity.HaltPcp.realize_eqF {α A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {v : α → A} {x y : α} : (eqF x y).Realize v ↔ v x = v y

@[simp]

theorem DescriptiveComplexity.HaltPcp.realize_ordLtF {α A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {v : α → A} {x y : α} : (ordLtF x y).Realize v ↔ v x < v y

@[simp]

theorem DescriptiveComplexity.HaltPcp.realize_mLtF {α A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {v : α → A} {x y : α} : (mLtF x y).Realize v ↔ MLt (v x) (v y)

@[simp]

theorem DescriptiveComplexity.HaltPcp.realize_minF {α A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {v : α → A} {x : α} : (minF x).Realize v ↔ ∀ (a : A), v x ≤ a

@[simp]

theorem DescriptiveComplexity.HaltPcp.realize_initTapeF {α A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {v : α → A} {x y : α} : (initTapeF x y).Realize v ↔ (tmData A).InitTape (v x) (v y)

@[simp]

theorem DescriptiveComplexity.HaltPcp.realize_wfF {α A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {v : α → A} : wfF.Realize v ↔ (tmData A).WellFormed

@[simp]

theorem DescriptiveComplexity.HaltPcp.realize_existsMoveF {α A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {v : α → A} {right : Bool} {q a b q' : α} : (existsMoveF right q a b q').Realize v ↔ ∃ (τ : A), TMTr τ ∧ (if right = true then TMRight τ else ¬TMRight τ) ∧ TMSrc τ (v q) ∧ TMRead τ (v a) ∧ TMDst τ (v q') ∧ TMWrite τ (v b)

The letter formulas

The word tables of DescriptiveComplexity.Problems.Pcp.Hardness.Draw are turned into formulas entry by entry: “argument 1 is the i-th shared position and argument 2 is the specified letter”.

def DescriptiveComplexity.HaltPcp.posTagN : ℕ → PTag

The tag of the i-th shared position.

Equations

• DescriptiveComplexity.HaltPcp.posTagN 0 = DescriptiveComplexity.HaltPcp.PTag.pos0
• DescriptiveComplexity.HaltPcp.posTagN 1 = DescriptiveComplexity.HaltPcp.PTag.pos1
• DescriptiveComplexity.HaltPcp.posTagN 2 = DescriptiveComplexity.HaltPcp.PTag.pos2
• DescriptiveComplexity.HaltPcp.posTagN 3 = DescriptiveComplexity.HaltPcp.PTag.pos3
• DescriptiveComplexity.HaltPcp.posTagN 4 = DescriptiveComplexity.HaltPcp.PTag.pos4
• DescriptiveComplexity.HaltPcp.posTagN 5 = DescriptiveComplexity.HaltPcp.PTag.pos5
• DescriptiveComplexity.HaltPcp.posTagN 6 = DescriptiveComplexity.HaltPcp.PTag.pos6
• DescriptiveComplexity.HaltPcp.posTagN x✝ = DescriptiveComplexity.HaltPcp.PTag.pos7

theorem DescriptiveComplexity.HaltPcp.posE_eq {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (i : ℕ) : posE i = cstE (posTagN i)

The shared positions are the constants of their tags.

noncomputable def DescriptiveComplexity.HaltPcp.minAllF (k : Fin 3) : haltOrd.Formula (Fin 3 × Fin 5)

All five coordinates of the argument k are minimal.

Equations

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

noncomputable def DescriptiveComplexity.HaltPcp.minTailF (k : Fin 3) : haltOrd.Formula (Fin 3 × Fin 5)

The four last coordinates of the argument k are minimal.

Equations

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

noncomputable def DescriptiveComplexity.HaltPcp.cstLF (s tc : PTag) : haltOrd.Formula (Fin 3 × Fin 5)

The letter argument is the constant letter of the tag s.

Equations

• DescriptiveComplexity.HaltPcp.cstLF s tc = if tc = s then DescriptiveComplexity.HaltPcp.minAllF 2 else ⊥

noncomputable def DescriptiveComplexity.HaltPcp.idxLF (s : PTag) (j : Fin 5) (tc : PTag) : haltOrd.Formula (Fin 3 × Fin 5)

The letter argument carries the j-th coordinate of the domino argument.

Equations

• DescriptiveComplexity.HaltPcp.idxLF s j tc = if tc = s then DescriptiveComplexity.HaltPcp.eqF (2, 0) (0, j) ⊓ DescriptiveComplexity.HaltPcp.minTailF 2 else ⊥

noncomputable def DescriptiveComplexity.HaltPcp.specF : LSpec → PTag → haltOrd.Formula (Fin 3 × Fin 5)

The formula of one table entry.

Equations

• DescriptiveComplexity.HaltPcp.specF (DescriptiveComplexity.HaltPcp.LSpec.cst s) x✝ = DescriptiveComplexity.HaltPcp.cstLF s x✝
• DescriptiveComplexity.HaltPcp.specF (DescriptiveComplexity.HaltPcp.LSpec.idx s j) x✝ = DescriptiveComplexity.HaltPcp.idxLF s j x✝

noncomputable def DescriptiveComplexity.HaltPcp.posIsF (i : ℕ) (tp : PTag) : haltOrd.Formula (Fin 3 × Fin 5)

The position argument is the i-th shared position.

Equations

• DescriptiveComplexity.HaltPcp.posIsF i tp = if tp = DescriptiveComplexity.HaltPcp.posTagN i then DescriptiveComplexity.HaltPcp.minAllF 1 else ⊥

noncomputable def DescriptiveComplexity.HaltPcp.specListF : List LSpec → ℕ → PTag → PTag → haltOrd.Formula (Fin 3 × Fin 5)

The formula of a word table, entry by entry from the i-th shared position on.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.HaltPcp.specListF [] x✝² x✝¹ x✝ = ⊥

noncomputable def DescriptiveComplexity.HaltPcp.uAtF (td tp tc : PTag) : haltOrd.Formula (Fin 3 × Fin 5)

The formula of the top word of a domino tag.

Equations

• DescriptiveComplexity.HaltPcp.uAtF td tp tc = DescriptiveComplexity.HaltPcp.specListF (DescriptiveComplexity.HaltPcp.uSpec td) 0 tp tc

noncomputable def DescriptiveComplexity.HaltPcp.startBotF (tp tc : PTag) : haltOrd.Formula (Fin 3 × Fin 5)

The formula of the start domino's bottom word, by the tag of the position.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.HaltPcp.startBotF tp tc = ⊥

noncomputable def DescriptiveComplexity.HaltPcp.vAtF (td tp tc : PTag) : haltOrd.Formula (Fin 3 × Fin 5)

The formula of the bottom word of a domino tag.

Equations

• DescriptiveComplexity.HaltPcp.vAtF DescriptiveComplexity.HaltPcp.PTag.dStart tp tc = DescriptiveComplexity.HaltPcp.startBotF tp tc
• DescriptiveComplexity.HaltPcp.vAtF td tp tc = DescriptiveComplexity.HaltPcp.specListF (DescriptiveComplexity.HaltPcp.vSpec td) 0 tp tc

The domino and order formulas

noncomputable def DescriptiveComplexity.HaltPcp.domF : PTag → haltOrd.Formula (Fin 1 × Fin 5)

The formula marking the dominoes: well-formedness of the machine and the side condition of the tag.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.HaltPcp.domF DescriptiveComplexity.HaltPcp.PTag.dStart = DescriptiveComplexity.HaltPcp.wfF
• DescriptiveComplexity.HaltPcp.domF DescriptiveComplexity.HaltPcp.PTag.dClose = DescriptiveComplexity.HaltPcp.wfF
• DescriptiveComplexity.HaltPcp.domF DescriptiveComplexity.HaltPcp.PTag.dCopySep = DescriptiveComplexity.HaltPcp.wfF
• DescriptiveComplexity.HaltPcp.domF DescriptiveComplexity.HaltPcp.PTag.dCopyLft = DescriptiveComplexity.HaltPcp.wfF
• DescriptiveComplexity.HaltPcp.domF DescriptiveComplexity.HaltPcp.PTag.dCopyRgt = DescriptiveComplexity.HaltPcp.wfF
• DescriptiveComplexity.HaltPcp.domF DescriptiveComplexity.HaltPcp.PTag.dCopyBoot = DescriptiveComplexity.HaltPcp.wfF
• DescriptiveComplexity.HaltPcp.domF DescriptiveComplexity.HaltPcp.PTag.dCopyHalt = DescriptiveComplexity.HaltPcp.wfF
• DescriptiveComplexity.HaltPcp.domF DescriptiveComplexity.HaltPcp.PTag.dCopySym = DescriptiveComplexity.HaltPcp.wfF
• DescriptiveComplexity.HaltPcp.domF DescriptiveComplexity.HaltPcp.PTag.dCopyState = DescriptiveComplexity.HaltPcp.wfF
• DescriptiveComplexity.HaltPcp.domF DescriptiveComplexity.HaltPcp.PTag.dEraseSymL = DescriptiveComplexity.HaltPcp.wfF
• DescriptiveComplexity.HaltPcp.domF DescriptiveComplexity.HaltPcp.PTag.dEraseLft = DescriptiveComplexity.HaltPcp.wfF
• DescriptiveComplexity.HaltPcp.domF DescriptiveComplexity.HaltPcp.PTag.dEraseSymR = DescriptiveComplexity.HaltPcp.wfF
• DescriptiveComplexity.HaltPcp.domF DescriptiveComplexity.HaltPcp.PTag.dEraseRgt = DescriptiveComplexity.HaltPcp.wfF
• DescriptiveComplexity.HaltPcp.domF DescriptiveComplexity.HaltPcp.PTag.dBoot = DescriptiveComplexity.HaltPcp.wfF ⊓ DescriptiveComplexity.HaltPcp.startF (0, 0)
• DescriptiveComplexity.HaltPcp.domF DescriptiveComplexity.HaltPcp.PTag.dAcc = DescriptiveComplexity.HaltPcp.wfF ⊓ DescriptiveComplexity.HaltPcp.accF (0, 0)
• DescriptiveComplexity.HaltPcp.domF DescriptiveComplexity.HaltPcp.PTag.dMoveR = DescriptiveComplexity.HaltPcp.wfF ⊓ DescriptiveComplexity.HaltPcp.existsMoveF true (0, 0) (0, 1) (0, 2) (0, 3)
• DescriptiveComplexity.HaltPcp.domF DescriptiveComplexity.HaltPcp.PTag.dMoveL = DescriptiveComplexity.HaltPcp.wfF ⊓ DescriptiveComplexity.HaltPcp.existsMoveF false (0, 0) (0, 1) (0, 2) (0, 3)
• DescriptiveComplexity.HaltPcp.domF x✝ = ⊥

noncomputable def DescriptiveComplexity.HaltPcp.tupLeF : haltOrd.Formula (Fin 2 × Fin 5)

The ambient lexicographic order of the last four coordinates, as a formula.

Equations

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

noncomputable def DescriptiveComplexity.HaltPcp.leF (t t' : PTag) : haltOrd.Formula (Fin 2 × Fin 5)

The order of the drawn instance: the static comparisons are decided in Lean, the dynamic ones written out.

Equations

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

noncomputable def DescriptiveComplexity.HaltPcp.haltPcpInterp : FOInterpretation haltOrd FirstOrder.Language.pcp PTag 5

The interpretation of the PCP vocabulary in an ordered machine instance.

Equations

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

Realization of the letter formulas

theorem DescriptiveComplexity.HaltPcp.realize_minAllF {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {v : Fin 3 × Fin 5 → A} {k : Fin 3} {w : Fin 5 → A} (hv : ∀ (j : Fin 5), v (k, j) = w j) : (minAllF k).Realize v ↔ w = fun (x : Fin 5) => pbot

theorem DescriptiveComplexity.HaltPcp.realize_minTailF {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {v : Fin 3 × Fin 5 → A} {k : Fin 3} {w : Fin 5 → A} (hv : ∀ (j : Fin 5), v (k, j) = w j) : (minTailF k).Realize v ↔ w 1 = pbot ∧ w 2 = pbot ∧ w 3 = pbot ∧ w 4 = pbot

theorem DescriptiveComplexity.HaltPcp.eq_cstE_iff {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {t t' : PTag} {w : Fin 5 → A} : (t, w) = cstE t' ↔ t = t' ∧ w = fun (x : Fin 5) => pbot

A pair with the right tag is a constant element exactly when its tuple is padding.

theorem DescriptiveComplexity.HaltPcp.eq_idxE_iff {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {t t' : PTag} {w : Fin 5 → A} {a : A} : (t, w) = idxE t' a ↔ t = t' ∧ w 0 = a ∧ w 1 = pbot ∧ w 2 = pbot ∧ w 3 = pbot ∧ w 4 = pbot

A pair with the right tag carries an element exactly when its head coordinate is it and its tail is padding.

theorem DescriptiveComplexity.HaltPcp.realize_cstLF {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {v : Fin 3 × Fin 5 → A} {wc : Fin 5 → A} {s tc : PTag} (hv2 : ∀ (j : Fin 5), v (2, j) = wc j) : (cstLF s tc).Realize v ↔ (tc, wc) = cstE s

theorem DescriptiveComplexity.HaltPcp.realize_idxLF {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {v : Fin 3 × Fin 5 → A} {wd wc : Fin 5 → A} {s : PTag} {j : Fin 5} {tc : PTag} (hv0 : ∀ (i : Fin 5), v (0, i) = wd i) (hv2 : ∀ (i : Fin 5), v (2, i) = wc i) : (idxLF s j tc).Realize v ↔ (tc, wc) = idxE s (wd j)

theorem DescriptiveComplexity.HaltPcp.realize_specF {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {v : Fin 3 × Fin 5 → A} {wd wc : Fin 5 → A} {sp : LSpec} {tc : PTag} (hv0 : ∀ (i : Fin 5), v (0, i) = wd i) (hv2 : ∀ (i : Fin 5), v (2, i) = wc i) : (specF sp tc).Realize v ↔ (tc, wc) = LSpec.eval wd sp

theorem DescriptiveComplexity.HaltPcp.realize_posIsF {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {v : Fin 3 × Fin 5 → A} {wp : Fin 5 → A} {i : ℕ} {tp : PTag} (hv1 : ∀ (j : Fin 5), v (1, j) = wp j) : (posIsF i tp).Realize v ↔ (tp, wp) = posE i

theorem DescriptiveComplexity.HaltPcp.realize_specListF {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {v : Fin 3 × Fin 5 → A} {wd wp wc : Fin 5 → A} {specs : List LSpec} {i : ℕ} {tp tc : PTag} (hv0 : ∀ (j : Fin 5), v (0, j) = wd j) (hv1 : ∀ (j : Fin 5), v (1, j) = wp j) (hv2 : ∀ (j : Fin 5), v (2, j) = wc j) : (specListF specs i tp tc).Realize v ↔ ((tp, wp), tc, wc) ∈ (List.map posE (List.range' i specs.length)).zip (List.map (LSpec.eval wd) specs)

theorem DescriptiveComplexity.HaltPcp.pUAt_iff_range' {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {d p c : PV A} : PUAt d p c ↔ (p, c) ∈ (List.map posE (List.range' 0 (uSpec d.1).length)).zip (List.map (LSpec.eval d.2) (uSpec d.1))

The top table relation, in terms of List.range'.

theorem DescriptiveComplexity.HaltPcp.realize_uAtF {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {v : Fin 3 × Fin 5 → A} {wd wp wc : Fin 5 → A} {td tp tc : PTag} (hv0 : ∀ (j : Fin 5), v (0, j) = wd j) (hv1 : ∀ (j : Fin 5), v (1, j) = wp j) (hv2 : ∀ (j : Fin 5), v (2, j) = wc j) : (uAtF td tp tc).Realize v ↔ PUAt (td, wd) (tp, wp) (tc, wc)

theorem DescriptiveComplexity.HaltPcp.pVAt_iff_range' {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {d p c : PV A} (hne : d.1 ≠ PTag.dStart) : PVAt d p c ↔ (p, c) ∈ (List.map posE (List.range' 0 (vSpec d.1).length)).zip (List.map (LSpec.eval d.2) (vSpec d.1))

The bottom table relation, in terms of List.range'.

theorem DescriptiveComplexity.HaltPcp.realize_startBotF {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {v : Fin 3 × Fin 5 → A} {wp wc : Fin 5 → A} {tp tc : PTag} (hv1 : ∀ (j : Fin 5), v (1, j) = wp j) (hv2 : ∀ (j : Fin 5), v (2, j) = wc j) : (startBotF tp tc).Realize v ↔ StartBotAt (tp, wp) (tc, wc)

theorem DescriptiveComplexity.HaltPcp.realize_vAtF {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {v : Fin 3 × Fin 5 → A} {wd wp wc : Fin 5 → A} {td tp tc : PTag} (hv0 : ∀ (j : Fin 5), v (0, j) = wd j) (hv1 : ∀ (j : Fin 5), v (1, j) = wp j) (hv2 : ∀ (j : Fin 5), v (2, j) = wc j) : (vAtF td tp tc).Realize v ↔ PVAt (td, wd) (tp, wp) (tc, wc)

Realization of the domino and order formulas

theorem DescriptiveComplexity.HaltPcp.realize_domF {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {t : PTag} {v : Fin 1 × Fin 5 → A} {wd : Fin 5 → A} (hv : ∀ (j : Fin 5), v (0, j) = wd j) : (domF t).Realize v ↔ PDom (t, wd)

theorem DescriptiveComplexity.HaltPcp.realize_tupLeF {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {v : Fin 2 × Fin 5 → A} {w w' : Fin 5 → A} (hv0 : ∀ (j : Fin 5), v (0, j) = w j) (hv1 : ∀ (j : Fin 5), v (1, j) = w' j) : tupLeF.Realize v ↔ TupLe w w'

theorem DescriptiveComplexity.HaltPcp.realize_leF {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {t t' : PTag} {v : Fin 2 × Fin 5 → A} {w w' : Fin 5 → A} (hv0 : ∀ (j : Fin 5), v (0, j) = w j) (hv1 : ∀ (j : Fin 5), v (1, j) = w' j) : (leF t t').Realize v ↔ PLe (t, w) (t', w')

The reads

theorem DescriptiveComplexity.HaltPcp.reads_haltPcp (A : Type) [FirstOrder.Language.turing.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : Reads (Equiv.refl (PV A))

The interpreted structure reads as the drawn instance: each relation of Language.pcp, realized through the defining formulas, is the semantic predicate of the drawing.

theorem DescriptiveComplexity.HaltPcp.pcp_map_iff (A : Type) [FirstOrder.Language.turing.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : PCP.Holds (haltPcpInterp.Map A) ↔ (tmData A).WellFormed ∧ (tmData A).AcceptsU

The image is a yes-instance exactly when the machine halts.