The drawing, as formulas

The tile system of DescriptiveComplexity.Problems.Wide.TilingHard.Tiles written down: one formula per symbol of FirstOrder.Language.wtile and per tuple of tags, over the machine's own vocabulary with the order of the instance.

The dimension is three – a tile is a tag with a symbol, a state and a transition – and every case analysis on tags is a DescriptiveComplexity.TilingHard.tagIfF, so each formula is a fixed conjunction and the tags decide which of its parts are ⊤. The order is the only symbol needing the ambient order of the instance, through DescriptiveComplexity.lexLeF: the points that are not digits are compared lexicographically, and the digits by the machine's own order.

Each formula is checked against the predicate it draws, at an arbitrary valuation, so DescriptiveComplexity.TilingHard.tileInterp is the emitted structure of DescriptiveComplexity.TilingHard.tileStr symbol by symbol.

The coordinates of an argument

def DescriptiveComplexity.TilingHard.argSym {n : ℕ} (i : Fin n) : Fin n × Fin 3

The symbol coordinate of the i-th argument.

Equations

• DescriptiveComplexity.TilingHard.argSym i = (i, 0)

def DescriptiveComplexity.TilingHard.argState {n : ℕ} (i : Fin n) : Fin n × Fin 3

Its state coordinate.

Equations

• DescriptiveComplexity.TilingHard.argState i = (i, 1)

def DescriptiveComplexity.TilingHard.argTr {n : ℕ} (i : Fin n) : Fin n × Fin 3

Its transition coordinate.

Equations

• DescriptiveComplexity.TilingHard.argTr i = (i, 2)

def DescriptiveComplexity.TilingHard.argPt {n : ℕ} {A : Type} (v : Fin n × Fin 3 → A) (t : TileTag) (i : Fin n) : TilePt A

The tile an argument is, at a valuation and a tag.

Equations

• DescriptiveComplexity.TilingHard.argPt v t i = (t, fun (j : Fin 3) => v (i, j))

@[simp]

theorem DescriptiveComplexity.TilingHard.argPt_fst {n : ℕ} {A : Type} (v : Fin n × Fin 3 → A) (t : TileTag) (i : Fin n) : (argPt v t i).1 = t

@[simp]

theorem DescriptiveComplexity.TilingHard.tpSym_argPt {n : ℕ} {A : Type} (v : Fin n × Fin 3 → A) (t : TileTag) (i : Fin n) : tpSym (argPt v t i) = v (argSym i)

@[simp]

theorem DescriptiveComplexity.TilingHard.tpState_argPt {n : ℕ} {A : Type} (v : Fin n × Fin 3 → A) (t : TileTag) (i : Fin n) : tpState (argPt v t i) = v (argState i)

@[simp]

theorem DescriptiveComplexity.TilingHard.tpTr_argPt {n : ℕ} {A : Type} (v : Fin n × Fin 3 → A) (t : TileTag) (i : Fin n) : tpTr (argPt v t i) = v (argTr i)

The marks of one tile

noncomputable def DescriptiveComplexity.TilingHard.digF {n : ℕ} (t : TileTag) (i : Fin n) : wideOrd.Formula (Fin n × Fin 3)

x is a digit: its tag says so and its triple is diagonal.

Equations

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

noncomputable def DescriptiveComplexity.TilingHard.noHeadF {n : ℕ} (t : TileTag) (_i : Fin n) : wideOrd.Formula (Fin n × Fin 3)

x holds no head.

Equations

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

noncomputable def DescriptiveComplexity.TilingHard.tileF {n : ℕ} (t : TileTag) (i : Fin n) : wideOrd.Formula (Fin n × Fin 3)

x is a tile: a head carries a transition the machine may fire, a digit is no tile, and every other kind asks nothing.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.TilingHard.tileF DescriptiveComplexity.TileTag.dig i = ⊥
• DescriptiveComplexity.TilingHard.tileF t i = ⊤

noncomputable def DescriptiveComplexity.TilingHard.accF {n : ℕ} (t : TileTag) (i : Fin n) : wideOrd.Formula (Fin n × Fin 3)

x is an accepting tile: the head is here, in an accepting state.

Equations

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

noncomputable def DescriptiveComplexity.TilingHard.baseF {n : ℕ} (t : TileTag) (i : Fin n) : wideOrd.Formula (Fin n × Fin 3)

x is a base tile: no head, holding the blank.

Equations

• DescriptiveComplexity.TilingHard.baseF t i = DescriptiveComplexity.TilingHard.noHeadF t i ⊓ DescriptiveComplexity.TilingHard.wdBlankF (DescriptiveComplexity.TilingHard.argSym i)

noncomputable def DescriptiveComplexity.TilingHard.startF {n : ℕ} (t : TileTag) (i : Fin n) : wideOrd.Formula (Fin n × Fin 3)

x is a start tile: the head on the blank in a start state, and the machine's promises.

Equations

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

noncomputable def DescriptiveComplexity.TilingHard.edgeLF {n : ℕ} (t : TileTag) (_i : Fin n) : wideOrd.Formula (Fin n × Fin 3)

x may stand in the leftmost column.

Equations

• DescriptiveComplexity.TilingHard.edgeLF t _i = DescriptiveComplexity.TilingHard.tagIfF (t ≠ DescriptiveComplexity.TileTag.arrL)

noncomputable def DescriptiveComplexity.TilingHard.edgeRF {n : ℕ} (t : TileTag) (_i : Fin n) : wideOrd.Formula (Fin n × Fin 3)

x may stand in the rightmost column.

Equations

• DescriptiveComplexity.TilingHard.edgeRF t _i = DescriptiveComplexity.TilingHard.tagIfF (t ≠ DescriptiveComplexity.TileTag.arrR)

@[simp]

theorem DescriptiveComplexity.TilingHard.realize_digF {n : ℕ} {A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] {v : Fin n × Fin 3 → A} {t : TileTag} {i : Fin n} : (digF t i).Realize v ↔ TPDig (argPt v t i)

@[simp]

theorem DescriptiveComplexity.TilingHard.realize_noHeadF {n : ℕ} {A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] {v : Fin n × Fin 3 → A} {t : TileTag} {i : Fin n} : (noHeadF t i).Realize v ↔ TPNoHead (argPt v t i)

@[simp]

theorem DescriptiveComplexity.TilingHard.realize_tileF {n : ℕ} {A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] {v : Fin n × Fin 3 → A} {t : TileTag} {i : Fin n} : (tileF t i).Realize v ↔ TPTile (argPt v t i)

@[simp]

theorem DescriptiveComplexity.TilingHard.realize_accF {n : ℕ} {A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] {v : Fin n × Fin 3 → A} {t : TileTag} {i : Fin n} : (accF t i).Realize v ↔ TPAcc (argPt v t i)

@[simp]

theorem DescriptiveComplexity.TilingHard.realize_baseF {n : ℕ} {A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] {v : Fin n × Fin 3 → A} {t : TileTag} {i : Fin n} : (baseF t i).Realize v ↔ TPBase (argPt v t i)

@[simp]

theorem DescriptiveComplexity.TilingHard.realize_startF {n : ℕ} {A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] {v : Fin n × Fin 3 → A} {t : TileTag} {i : Fin n} : (startF t i).Realize v ↔ TPStart (argPt v t i)

@[simp]

theorem DescriptiveComplexity.TilingHard.realize_edgeLF {n : ℕ} {A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] {v : Fin n × Fin 3 → A} {t : TileTag} {i : Fin n} : (edgeLF t i).Realize v ↔ TPEdgeL (argPt v t i)

@[simp]

theorem DescriptiveComplexity.TilingHard.realize_edgeRF {n : ℕ} {A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] {v : Fin n × Fin 3 → A} {t : TileTag} {i : Fin n} : (edgeRF t i).Realize v ↔ TPEdgeR (argPt v t i)

The relations between two tiles

noncomputable def DescriptiveComplexity.TilingHard.leF (t₁ t₂ : TileTag) : wideOrd.Formula (Fin 2 × Fin 3)

The order the drawing emits: the digits last, in the machine's own order, and everything else lexicographically.

Equations

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

noncomputable def DescriptiveComplexity.TilingHard.firstF (t₁ t₂ : TileTag) : wideOrd.Formula (Fin 2 × Fin 3)

The bottom row: the cell of a digit may carry a tile holding that element's input symbol, and no head.

Equations

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

noncomputable def DescriptiveComplexity.TilingHard.firstRF (t₁ t₂ : TileTag) : wideOrd.Formula (Fin 2 × Fin 3)

The bottom row at the ruler: the cell of a digit carries that element's input symbol, or the blank where it has none.

Equations

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

noncomputable def DescriptiveComplexity.TilingHard.horizF (t₁ t₂ : TileTag) : wideOrd.Formula (Fin 2 × Fin 3)

What may stand immediately to the right of a tile: an announced head is the neighbor's arrival and an arrival is a neighboring head, so a row keeps to one head.

Equations

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

noncomputable def DescriptiveComplexity.TilingHard.vertF (t₁ t₂ : TileTag) : wideOrd.Formula (Fin 2 × Fin 3)

What may stand immediately above a tile: the head writes, an arrival becomes the head, and every other cell copies itself.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.TilingHard.vertF DescriptiveComplexity.TileTag.dig t₂ = ⊥

@[simp]

theorem DescriptiveComplexity.TilingHard.realize_leF {A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] {v : Fin 2 × Fin 3 → A} {t₁ t₂ : TileTag} : (leF t₁ t₂).Realize v ↔ tpLe (argPt v t₁ 0) (argPt v t₂ 1)

@[simp]

theorem DescriptiveComplexity.TilingHard.realize_firstF {A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] {v : Fin 2 × Fin 3 → A} {t₁ t₂ : TileTag} : (firstF t₁ t₂).Realize v ↔ TPFirst (argPt v t₁ 0) (argPt v t₂ 1)

@[simp]

theorem DescriptiveComplexity.TilingHard.realize_firstRF {A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] {v : Fin 2 × Fin 3 → A} {t₁ t₂ : TileTag} : (firstRF t₁ t₂).Realize v ↔ TPFirstR (argPt v t₁ 0) (argPt v t₂ 1)

@[simp]

theorem DescriptiveComplexity.TilingHard.realize_horizF {A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] {v : Fin 2 × Fin 3 → A} {t₁ t₂ : TileTag} : (horizF t₁ t₂).Realize v ↔ TPHoriz (argPt v t₁ 0) (argPt v t₂ 1)

@[simp]

theorem DescriptiveComplexity.TilingHard.realize_vertF {A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] {v : Fin 2 × Fin 3 → A} {t₁ t₂ : TileTag} : (vertF t₁ t₂).Realize v ↔ TPVert (argPt v t₁ 0) (argPt v t₂ 1)