The atoms the drawing is written with

The vocabulary a reduction from a wide machine writes its formulas in: the machine's own relations, over the ordered expansion Language.wide.sum Language.order, one shorthand each, together with the two shapes every tile formula is built from –

• a static choice on the tags, DescriptiveComplexity.TilingHard.tagIfF, which is where all the case analysis of the drawing goes;
• the machine's promises as a sentence, DescriptiveComplexity.TilingHard.wideWFF, which the start tile carries.

Everything here is about the source of the reduction, so it says nothing about tiles; the formulas that draw them are in DescriptiveComplexity.Problems.Wide.TilingHard.Draw.

@[reducible, inline]

abbrev DescriptiveComplexity.TilingHard.wideOrd : FirstOrder.Language

The vocabulary the drawing's formulas are written in: the machine's, with the order of the instance.

Equations

• DescriptiveComplexity.TilingHard.wideOrd = FirstOrder.Language.wide.sum FirstOrder.Language.order

The machine's relations, as atoms

@[reducible, inline]

abbrev DescriptiveComplexity.TilingHard.wdLeSym : wideOrd.Relations 2

The order symbol of the machine, in the drawing's vocabulary.

Equations

• DescriptiveComplexity.TilingHard.wdLeSym = Sum.inl FirstOrder.Language.wmLe

@[reducible, inline]

abbrev DescriptiveComplexity.TilingHard.wdTrSym : wideOrd.Relations 1

The transition symbol, in the drawing's vocabulary.

Equations

• DescriptiveComplexity.TilingHard.wdTrSym = Sum.inl FirstOrder.Language.wmTr

@[reducible, inline]

abbrev DescriptiveComplexity.TilingHard.wdStartSym : wideOrd.Relations 1

The start-state symbol, in the drawing's vocabulary.

Equations

• DescriptiveComplexity.TilingHard.wdStartSym = Sum.inl FirstOrder.Language.wmStart

@[reducible, inline]

abbrev DescriptiveComplexity.TilingHard.wdAccSym : wideOrd.Relations 1

The accepting-state symbol, in the drawing's vocabulary.

Equations

• DescriptiveComplexity.TilingHard.wdAccSym = Sum.inl FirstOrder.Language.wmAcc

@[reducible, inline]

abbrev DescriptiveComplexity.TilingHard.wdBlankSym : wideOrd.Relations 1

The blank symbol, in the drawing's vocabulary.

Equations

• DescriptiveComplexity.TilingHard.wdBlankSym = Sum.inl FirstOrder.Language.wmBlank

@[reducible, inline]

abbrev DescriptiveComplexity.TilingHard.wdRightSym : wideOrd.Relations 1

The right-move symbol, in the drawing's vocabulary.

Equations

• DescriptiveComplexity.TilingHard.wdRightSym = Sum.inl FirstOrder.Language.wmRight

@[reducible, inline]

abbrev DescriptiveComplexity.TilingHard.wdSrcSym : wideOrd.Relations 2

The source-state symbol, in the drawing's vocabulary.

Equations

• DescriptiveComplexity.TilingHard.wdSrcSym = Sum.inl FirstOrder.Language.wmSrc

@[reducible, inline]

abbrev DescriptiveComplexity.TilingHard.wdReadSym : wideOrd.Relations 2

The read-symbol symbol, in the drawing's vocabulary.

Equations

• DescriptiveComplexity.TilingHard.wdReadSym = Sum.inl FirstOrder.Language.wmRead

@[reducible, inline]

abbrev DescriptiveComplexity.TilingHard.wdDstSym : wideOrd.Relations 2

The destination-state symbol, in the drawing's vocabulary.

Equations

• DescriptiveComplexity.TilingHard.wdDstSym = Sum.inl FirstOrder.Language.wmDst

@[reducible, inline]

abbrev DescriptiveComplexity.TilingHard.wdWriteSym : wideOrd.Relations 2

The written-symbol symbol, in the drawing's vocabulary.

Equations

• DescriptiveComplexity.TilingHard.wdWriteSym = Sum.inl FirstOrder.Language.wmWrite

@[reducible, inline]

abbrev DescriptiveComplexity.TilingHard.wdInpSym : wideOrd.Relations 2

The input symbol, in the drawing's vocabulary.

Equations

• DescriptiveComplexity.TilingHard.wdInpSym = Sum.inl FirstOrder.Language.wmInp

noncomputable def DescriptiveComplexity.TilingHard.wdLeF {γ : Type} (x y : γ) : wideOrd.Formula γ

x ≤ y in the machine's own order.

Equations

• DescriptiveComplexity.TilingHard.wdLeF x y = DescriptiveComplexity.TilingHard.wdLeSym.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

noncomputable def DescriptiveComplexity.TilingHard.wdTrF {γ : Type} (t : γ) : wideOrd.Formula γ

t is a transition.

Equations

• DescriptiveComplexity.TilingHard.wdTrF t = DescriptiveComplexity.TilingHard.wdTrSym.formula₁ (FirstOrder.Language.var t)

noncomputable def DescriptiveComplexity.TilingHard.wdStartF {γ : Type} (q : γ) : wideOrd.Formula γ

q is a start state.

Equations

• DescriptiveComplexity.TilingHard.wdStartF q = DescriptiveComplexity.TilingHard.wdStartSym.formula₁ (FirstOrder.Language.var q)

noncomputable def DescriptiveComplexity.TilingHard.wdAccF {γ : Type} (q : γ) : wideOrd.Formula γ

q is an accepting state.

Equations

• DescriptiveComplexity.TilingHard.wdAccF q = DescriptiveComplexity.TilingHard.wdAccSym.formula₁ (FirstOrder.Language.var q)

noncomputable def DescriptiveComplexity.TilingHard.wdBlankF {γ : Type} (a : γ) : wideOrd.Formula γ

a is the blank symbol.

Equations

• DescriptiveComplexity.TilingHard.wdBlankF a = DescriptiveComplexity.TilingHard.wdBlankSym.formula₁ (FirstOrder.Language.var a)

noncomputable def DescriptiveComplexity.TilingHard.wdRightF {γ : Type} (t : γ) : wideOrd.Formula γ

t moves the head to the right.

Equations

• DescriptiveComplexity.TilingHard.wdRightF t = DescriptiveComplexity.TilingHard.wdRightSym.formula₁ (FirstOrder.Language.var t)

noncomputable def DescriptiveComplexity.TilingHard.wdSrcF {γ : Type} (t q : γ) : wideOrd.Formula γ

t applies in the state q.

Equations

• DescriptiveComplexity.TilingHard.wdSrcF t q = DescriptiveComplexity.TilingHard.wdSrcSym.formula₂ (FirstOrder.Language.var t) (FirstOrder.Language.var q)

noncomputable def DescriptiveComplexity.TilingHard.wdReadF {γ : Type} (t a : γ) : wideOrd.Formula γ

t applies on the symbol a.

Equations

• DescriptiveComplexity.TilingHard.wdReadF t a = DescriptiveComplexity.TilingHard.wdReadSym.formula₂ (FirstOrder.Language.var t) (FirstOrder.Language.var a)

noncomputable def DescriptiveComplexity.TilingHard.wdDstF {γ : Type} (t q : γ) : wideOrd.Formula γ

t moves to the state q.

Equations

• DescriptiveComplexity.TilingHard.wdDstF t q = DescriptiveComplexity.TilingHard.wdDstSym.formula₂ (FirstOrder.Language.var t) (FirstOrder.Language.var q)

noncomputable def DescriptiveComplexity.TilingHard.wdWriteF {γ : Type} (t a : γ) : wideOrd.Formula γ

t writes the symbol a.

Equations

• DescriptiveComplexity.TilingHard.wdWriteF t a = DescriptiveComplexity.TilingHard.wdWriteSym.formula₂ (FirstOrder.Language.var t) (FirstOrder.Language.var a)

noncomputable def DescriptiveComplexity.TilingHard.wdInpF {γ : Type} (x a : γ) : wideOrd.Formula γ

The cell of x starts holding a.

Equations

• DescriptiveComplexity.TilingHard.wdInpF x a = DescriptiveComplexity.TilingHard.wdInpSym.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var a)

noncomputable def DescriptiveComplexity.TilingHard.wdEqF {γ : Type} (x y : γ) : wideOrd.Formula γ

x and y are the same element.

Equations

• DescriptiveComplexity.TilingHard.wdEqF x y = (FirstOrder.Language.var x).equal (FirstOrder.Language.var y)

@[simp]

theorem DescriptiveComplexity.TilingHard.realize_wdLeF {γ A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] {v : γ → A} (x y : γ) : (wdLeF x y).Realize v ↔ WMLe (v x) (v y)

@[simp]

theorem DescriptiveComplexity.TilingHard.realize_wdTrF {γ A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] {v : γ → A} (t : γ) : (wdTrF t).Realize v ↔ WMTr (v t)

@[simp]

theorem DescriptiveComplexity.TilingHard.realize_wdStartF {γ A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] {v : γ → A} (q : γ) : (wdStartF q).Realize v ↔ WMStart (v q)

@[simp]

theorem DescriptiveComplexity.TilingHard.realize_wdAccF {γ A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] {v : γ → A} (q : γ) : (wdAccF q).Realize v ↔ WMAcc (v q)

@[simp]

theorem DescriptiveComplexity.TilingHard.realize_wdBlankF {γ A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] {v : γ → A} (a : γ) : (wdBlankF a).Realize v ↔ WMBlank (v a)

@[simp]

theorem DescriptiveComplexity.TilingHard.realize_wdRightF {γ A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] {v : γ → A} (t : γ) : (wdRightF t).Realize v ↔ WMRight (v t)

@[simp]

theorem DescriptiveComplexity.TilingHard.realize_wdSrcF {γ A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] {v : γ → A} (t q : γ) : (wdSrcF t q).Realize v ↔ WMSrc (v t) (v q)

@[simp]

theorem DescriptiveComplexity.TilingHard.realize_wdReadF {γ A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] {v : γ → A} (t a : γ) : (wdReadF t a).Realize v ↔ WMRead (v t) (v a)

@[simp]

theorem DescriptiveComplexity.TilingHard.realize_wdDstF {γ A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] {v : γ → A} (t q : γ) : (wdDstF t q).Realize v ↔ WMDst (v t) (v q)

@[simp]

theorem DescriptiveComplexity.TilingHard.realize_wdWriteF {γ A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] {v : γ → A} (t a : γ) : (wdWriteF t a).Realize v ↔ WMWrite (v t) (v a)

@[simp]

theorem DescriptiveComplexity.TilingHard.realize_wdInpF {γ A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] {v : γ → A} (x a : γ) : (wdInpF x a).Realize v ↔ WMInp (v x) (v a)

@[simp]

theorem DescriptiveComplexity.TilingHard.realize_wdEqF {γ A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] {v : γ → A} (x y : γ) : (wdEqF x y).Realize v ↔ v x = v y

The two shapes every tile formula is built from

noncomputable def DescriptiveComplexity.TilingHard.tagIfF {γ : Type} (b : Prop) : wideOrd.Formula γ

A static choice on the tags: the truth value a tag decides, as a formula. Every case analysis the drawing does on tags is one of these, so the formulas themselves stay small.

Equations

• DescriptiveComplexity.TilingHard.tagIfF b = if b then ⊤ else ⊥

noncomputable def DescriptiveComplexity.TilingHard.wideWFF {γ : Type} : wideOrd.Formula γ

The machine's promises: the order is linear, the input is functional, and there is exactly one blank. This is DescriptiveComplexity.WideWF written out, and the start tile is where the drawing carries it – a no-instance whose promises fail has no start tile, hence no tiling.

Equations

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

@[simp]

theorem DescriptiveComplexity.TilingHard.realize_tagIfF {γ A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] {v : γ → A} (b : Prop) : (tagIfF b).Realize v ↔ b

@[simp]

theorem DescriptiveComplexity.TilingHard.realize_wideWFF {γ A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] {v : γ → A} : wideWFF.Realize v ↔ WideWF A