Tiling a square is existential second-order definable

The membership half of the problem's completeness: a tiling is a certificate, and checking it is local. The Σ₁ definition guesses one ternary relation variable R x y t, read as “the cell in column x and row y carries the tile t”, and its first-order kernel says what a tiling is:

• every cell of the grid carries exactly one tile, and that tile is one of the instance's;
• the bottom row is one the description allows, and the two edge columns carry tiles allowed there;
• horizontal and vertical neighbors are compatible;
• some cell carries an accepting tile;

together with the well-formedness the yes-instances fold in – the order is linear and there is a position.

The guess has to be functional where a coloring's need not be (DescriptiveComplexity.paletteKernel): the accepting condition asks for a cell that carries an accepting tile, so a cell holding two tiles could satisfy the compatibility clauses by one and the acceptance by the other, which no tiling does.

The grid is indexed by the positions of the instance, so this is an n × n tiling and the definition is a Σ₁ one. Read over an exponential expansion the same sentence asks about a 2ⁿ × 2ⁿ square.

The guessed tiling

def DescriptiveComplexity.tileGuessBlock : SOBlock

The single existential block of the Σ₁ definition: one ternary relation variable, read as “the cell in this column and this row carries this tile”.

Equations

• DescriptiveComplexity.tileGuessBlock = { ι := Unit, ιFinite := ⋯, arity := fun (x : Unit) => 3 }

def DescriptiveComplexity.tgTileRel : tileGuessBlock.lang.Relations 3

The symbol of the guessed tiling.

Equations

• DescriptiveComplexity.tgTileRel = ⟨(), DescriptiveComplexity.tgTileRel._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.tileSOLang : FirstOrder.Language

The vocabulary of the kernel: tile systems together with the guessed tiling.

Equations

• DescriptiveComplexity.tileSOLang = FirstOrder.Language.tiling.sum DescriptiveComplexity.tileGuessBlock.lang

@[reducible, inline]

abbrev DescriptiveComplexity.tsPosn : tileSOLang.Relations 1

The position symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.tsPosn = Sum.inl FirstOrder.Language.tlPosn

@[reducible, inline]

abbrev DescriptiveComplexity.tsTile : tileSOLang.Relations 1

The tile symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.tsTile = Sum.inl FirstOrder.Language.tlTile

@[reducible, inline]

abbrev DescriptiveComplexity.tsAcc : tileSOLang.Relations 1

The accepting-tile symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.tsAcc = Sum.inl FirstOrder.Language.tlAcc

@[reducible, inline]

abbrev DescriptiveComplexity.tsLe : tileSOLang.Relations 2

The order symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.tsLe = Sum.inl FirstOrder.Language.tlLe

@[reducible, inline]

abbrev DescriptiveComplexity.tsHoriz : tileSOLang.Relations 2

The horizontal-compatibility symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.tsHoriz = Sum.inl FirstOrder.Language.tlHoriz

@[reducible, inline]

abbrev DescriptiveComplexity.tsVert : tileSOLang.Relations 2

The vertical-compatibility symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.tsVert = Sum.inl FirstOrder.Language.tlVert

@[reducible, inline]

abbrev DescriptiveComplexity.tsFirst : tileSOLang.Relations 2

The bottom-row symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.tsFirst = Sum.inl FirstOrder.Language.tlFirst

@[reducible, inline]

abbrev DescriptiveComplexity.tsBase : tileSOLang.Relations 1

The base-tile symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.tsBase = Sum.inl FirstOrder.Language.tlBase

@[reducible, inline]

abbrev DescriptiveComplexity.tsStart : tileSOLang.Relations 1

The start-tile symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.tsStart = Sum.inl FirstOrder.Language.tlStart

@[reducible, inline]

abbrev DescriptiveComplexity.tsEdgeL : tileSOLang.Relations 1

The left-edge symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.tsEdgeL = Sum.inl FirstOrder.Language.tlEdgeL

@[reducible, inline]

abbrev DescriptiveComplexity.tsEdgeR : tileSOLang.Relations 1

The right-edge symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.tsEdgeR = Sum.inl FirstOrder.Language.tlEdgeR

@[reducible, inline]

abbrev DescriptiveComplexity.tsRel : tileSOLang.Relations 3

The guessed tiling's symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.tsRel = Sum.inr DescriptiveComplexity.tgTileRel

The atoms, at an arbitrary index of free variables

noncomputable def DescriptiveComplexity.tlPosnF {γ : Type} (x : γ) : tileSOLang.Formula γ

x is a position.

Equations

• DescriptiveComplexity.tlPosnF x = DescriptiveComplexity.tsPosn.formula₁ (FirstOrder.Language.var x)

noncomputable def DescriptiveComplexity.tlTileF {γ : Type} (t : γ) : tileSOLang.Formula γ

t is a tile.

Equations

• DescriptiveComplexity.tlTileF t = DescriptiveComplexity.tsTile.formula₁ (FirstOrder.Language.var t)

noncomputable def DescriptiveComplexity.tlAccF {γ : Type} (t : γ) : tileSOLang.Formula γ

t is an accepting tile.

Equations

• DescriptiveComplexity.tlAccF t = DescriptiveComplexity.tsAcc.formula₁ (FirstOrder.Language.var t)

noncomputable def DescriptiveComplexity.tlLeF {γ : Type} (x y : γ) : tileSOLang.Formula γ

x is at most y.

Equations

• DescriptiveComplexity.tlLeF x y = DescriptiveComplexity.tsLe.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

noncomputable def DescriptiveComplexity.tlHorizF {γ : Type} (t t' : γ) : tileSOLang.Formula γ

t' may stand immediately to the right of t.

Equations

• DescriptiveComplexity.tlHorizF t t' = DescriptiveComplexity.tsHoriz.formula₂ (FirstOrder.Language.var t) (FirstOrder.Language.var t')

noncomputable def DescriptiveComplexity.tlVertF {γ : Type} (t t' : γ) : tileSOLang.Formula γ

t' may stand immediately above t.

Equations

• DescriptiveComplexity.tlVertF t t' = DescriptiveComplexity.tsVert.formula₂ (FirstOrder.Language.var t) (FirstOrder.Language.var t')

noncomputable def DescriptiveComplexity.tlFirstF {γ : Type} (x t : γ) : tileSOLang.Formula γ

The bottom row's cell in column x may carry t.

Equations

• DescriptiveComplexity.tlFirstF x t = DescriptiveComplexity.tsFirst.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var t)

noncomputable def DescriptiveComplexity.tlBaseF {γ : Type} (t : γ) : tileSOLang.Formula γ

t is a base tile.

Equations

• DescriptiveComplexity.tlBaseF t = DescriptiveComplexity.tsBase.formula₁ (FirstOrder.Language.var t)

noncomputable def DescriptiveComplexity.tlStartF {γ : Type} (t : γ) : tileSOLang.Formula γ

t is a start tile.

Equations

• DescriptiveComplexity.tlStartF t = DescriptiveComplexity.tsStart.formula₁ (FirstOrder.Language.var t)

noncomputable def DescriptiveComplexity.tlEdgeLF {γ : Type} (t : γ) : tileSOLang.Formula γ

t may stand in the leftmost column.

Equations

• DescriptiveComplexity.tlEdgeLF t = DescriptiveComplexity.tsEdgeL.formula₁ (FirstOrder.Language.var t)

noncomputable def DescriptiveComplexity.tlEdgeRF {γ : Type} (t : γ) : tileSOLang.Formula γ

t may stand in the rightmost column.

Equations

• DescriptiveComplexity.tlEdgeRF t = DescriptiveComplexity.tsEdgeR.formula₁ (FirstOrder.Language.var t)

noncomputable def DescriptiveComplexity.tlRelF {γ : Type} (x y t : γ) : tileSOLang.Formula γ

The cell in column x and row y carries the tile t.

Equations

• DescriptiveComplexity.tlRelF x y t = DescriptiveComplexity.tsRel.formula ![FirstOrder.Language.var x, FirstOrder.Language.var y, FirstOrder.Language.var t]

noncomputable def DescriptiveComplexity.tlEqF {γ : Type} (x y : γ) : tileSOLang.Formula γ

x and y are the same element.

Equations

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

What the kernel says

@[simp]

theorem DescriptiveComplexity.realize_tlPosnF {A : Type} [FirstOrder.Language.tiling.Structure A] {γ : Type} (ρ : tileGuessBlock.Assignment A) {v : γ → A} (x : γ) : (tlPosnF x).Realize v ↔ TLPosn (v x)

@[simp]

theorem DescriptiveComplexity.realize_tlTileF {A : Type} [FirstOrder.Language.tiling.Structure A] {γ : Type} (ρ : tileGuessBlock.Assignment A) {v : γ → A} (t : γ) : (tlTileF t).Realize v ↔ TLTile (v t)

@[simp]

theorem DescriptiveComplexity.realize_tlAccF {A : Type} [FirstOrder.Language.tiling.Structure A] {γ : Type} (ρ : tileGuessBlock.Assignment A) {v : γ → A} (t : γ) : (tlAccF t).Realize v ↔ TLAcc (v t)

@[simp]

theorem DescriptiveComplexity.realize_tlLeF {A : Type} [FirstOrder.Language.tiling.Structure A] {γ : Type} (ρ : tileGuessBlock.Assignment A) {v : γ → A} (x y : γ) : (tlLeF x y).Realize v ↔ TLLe (v x) (v y)

@[simp]

theorem DescriptiveComplexity.realize_tlHorizF {A : Type} [FirstOrder.Language.tiling.Structure A] {γ : Type} (ρ : tileGuessBlock.Assignment A) {v : γ → A} (t t' : γ) : (tlHorizF t t').Realize v ↔ TLHoriz (v t) (v t')

@[simp]

theorem DescriptiveComplexity.realize_tlVertF {A : Type} [FirstOrder.Language.tiling.Structure A] {γ : Type} (ρ : tileGuessBlock.Assignment A) {v : γ → A} (t t' : γ) : (tlVertF t t').Realize v ↔ TLVert (v t) (v t')

@[simp]

theorem DescriptiveComplexity.realize_tlFirstF {A : Type} [FirstOrder.Language.tiling.Structure A] {γ : Type} (ρ : tileGuessBlock.Assignment A) {v : γ → A} (x t : γ) : (tlFirstF x t).Realize v ↔ TLFirst (v x) (v t)

@[simp]

theorem DescriptiveComplexity.realize_tlBaseF {A : Type} [FirstOrder.Language.tiling.Structure A] {γ : Type} (ρ : tileGuessBlock.Assignment A) {v : γ → A} (t : γ) : (tlBaseF t).Realize v ↔ TLBase (v t)

@[simp]

theorem DescriptiveComplexity.realize_tlStartF {A : Type} [FirstOrder.Language.tiling.Structure A] {γ : Type} (ρ : tileGuessBlock.Assignment A) {v : γ → A} (t : γ) : (tlStartF t).Realize v ↔ TLStart (v t)

@[simp]

theorem DescriptiveComplexity.realize_tlEdgeLF {A : Type} [FirstOrder.Language.tiling.Structure A] {γ : Type} (ρ : tileGuessBlock.Assignment A) {v : γ → A} (t : γ) : (tlEdgeLF t).Realize v ↔ TLEdgeL (v t)

@[simp]

theorem DescriptiveComplexity.realize_tlEdgeRF {A : Type} [FirstOrder.Language.tiling.Structure A] {γ : Type} (ρ : tileGuessBlock.Assignment A) {v : γ → A} (t : γ) : (tlEdgeRF t).Realize v ↔ TLEdgeR (v t)

@[simp]

theorem DescriptiveComplexity.realize_tlRelF {A : Type} [FirstOrder.Language.tiling.Structure A] {γ : Type} (ρ : tileGuessBlock.Assignment A) {v : γ → A} (x y t : γ) : (tlRelF x y t).Realize v ↔ ρ () ![v x, v y, v t]

@[simp]

theorem DescriptiveComplexity.realize_tlEqF {A : Type} [FirstOrder.Language.tiling.Structure A] {γ : Type} (ρ : tileGuessBlock.Assignment A) {v : γ → A} (x y : γ) : (tlEqF x y).Realize v ↔ v x = v y

The two order guards, as formulas

noncomputable def DescriptiveComplexity.tlMinPosF {γ : Type} (y : γ) : tileSOLang.Formula γ

y is the least position.

Equations

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

noncomputable def DescriptiveComplexity.tlMaxPosF {γ : Type} (y : γ) : tileSOLang.Formula γ

y is the greatest position.

Equations

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

noncomputable def DescriptiveComplexity.tlSuccPosF {γ : Type} (x x' : γ) : tileSOLang.Formula γ

x' is the position immediately above x.

Equations

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

@[simp]

theorem DescriptiveComplexity.realize_tlMinPosF {γ A : Type} [FirstOrder.Language.tiling.Structure A] (ρ : tileGuessBlock.Assignment A) {v : γ → A} (y : γ) : (tlMinPosF y).Realize v ↔ MinPos (tileData A).Le (tileData A).Posn (v y)

@[simp]

theorem DescriptiveComplexity.realize_tlMaxPosF {γ A : Type} [FirstOrder.Language.tiling.Structure A] (ρ : tileGuessBlock.Assignment A) {v : γ → A} (y : γ) : (tlMaxPosF y).Realize v ↔ MaxPos (tileData A).Le (tileData A).Posn (v y)

@[simp]

theorem DescriptiveComplexity.realize_tlSuccPosF {γ A : Type} [FirstOrder.Language.tiling.Structure A] (ρ : tileGuessBlock.Assignment A) {v : γ → A} (x x' : γ) : (tlSuccPosF x x').Realize v ↔ SuccPos (tileData A).Le (tileData A).Posn (v x) (v x')

The clauses of the kernel

noncomputable def DescriptiveComplexity.tileWfC : tileSOLang.Sentence

The order is linear and there is a position: the well-formedness the yes-instances fold in.

Equations

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

noncomputable def DescriptiveComplexity.tileTotalC : tileSOLang.Sentence

Every cell of the grid carries a tile of the instance.

Equations

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

noncomputable def DescriptiveComplexity.tileFuncC : tileSOLang.Sentence

A cell carries at most one tile.

Equations

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

noncomputable def DescriptiveComplexity.tileFirstC : tileSOLang.Sentence

The bottom row is one the description allows: the tiles it names in that column, or a base tile where it names none.

Equations

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

noncomputable def DescriptiveComplexity.tileEdgeLC : tileSOLang.Sentence

The leftmost column carries tiles allowed there.

Equations

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

noncomputable def DescriptiveComplexity.tileEdgeRC : tileSOLang.Sentence

And the rightmost column those allowed there.

Equations

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

noncomputable def DescriptiveComplexity.tileHorizC : tileSOLang.Sentence

Horizontal neighbors are compatible.

Equations

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

noncomputable def DescriptiveComplexity.tileVertC : tileSOLang.Sentence

Vertical neighbors are compatible.

Equations

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

noncomputable def DescriptiveComplexity.tileAccC : tileSOLang.Sentence

Some cell of the grid carries an accepting tile.

Equations

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

noncomputable def DescriptiveComplexity.tileKernel : tileSOLang.Sentence

The first-order kernel of the Σ₁ definition: the tiling the block guesses is a tiling of the square, and the instance is well-formed.

Equations

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

What each clause says

theorem DescriptiveComplexity.realize_tileWfC {A : Type} [FirstOrder.Language.tiling.Structure A] (ρ : tileGuessBlock.Assignment A) : A ⊨ tileWfC ↔ (tileData A).WellFormed

theorem DescriptiveComplexity.realize_tileTotalC {A : Type} [FirstOrder.Language.tiling.Structure A] (ρ : tileGuessBlock.Assignment A) : A ⊨ tileTotalC ↔ ∀ (x y : A), TLPosn x → TLPosn y → ∃ (t : A), ρ () ![x, y, t] ∧ TLTile t

theorem DescriptiveComplexity.realize_tlTileFuncC {A : Type} [FirstOrder.Language.tiling.Structure A] (ρ : tileGuessBlock.Assignment A) : A ⊨ tileFuncC ↔ ∀ (x y t t' : A), ρ () ![x, y, t] → ρ () ![x, y, t'] → t = t'

theorem DescriptiveComplexity.realize_tlTileFirstC {A : Type} [FirstOrder.Language.tiling.Structure A] (ρ : tileGuessBlock.Assignment A) : A ⊨ tileFirstC ↔ ∀ (x y t : A), TLPosn x → MinPos (tileData A).Le (tileData A).Posn y → ρ () ![x, y, t] → (MinPos (tileData A).Le (tileData A).Posn x → TLStart t) ∧ (¬MinPos (tileData A).Le (tileData A).Posn x → (tileData A).FirstTile x t)

theorem DescriptiveComplexity.realize_tileEdgeLC {A : Type} [FirstOrder.Language.tiling.Structure A] (ρ : tileGuessBlock.Assignment A) : A ⊨ tileEdgeLC ↔ ∀ (x y t : A), TLPosn y → MinPos (tileData A).Le (tileData A).Posn x → ρ () ![x, y, t] → TLEdgeL t

theorem DescriptiveComplexity.realize_tileEdgeRC {A : Type} [FirstOrder.Language.tiling.Structure A] (ρ : tileGuessBlock.Assignment A) : A ⊨ tileEdgeRC ↔ ∀ (x y t : A), TLPosn y → MaxPos (tileData A).Le (tileData A).Posn x → ρ () ![x, y, t] → TLEdgeR t

theorem DescriptiveComplexity.realize_tileHorizC {A : Type} [FirstOrder.Language.tiling.Structure A] (ρ : tileGuessBlock.Assignment A) : A ⊨ tileHorizC ↔ ∀ (x x' y t t' : A), SuccPos (tileData A).Le (tileData A).Posn x x' → TLPosn y → ρ () ![x, y, t] → ρ () ![x', y, t'] → TLHoriz t t'

theorem DescriptiveComplexity.realize_tileVertC {A : Type} [FirstOrder.Language.tiling.Structure A] (ρ : tileGuessBlock.Assignment A) : A ⊨ tileVertC ↔ ∀ (x y y' t t' : A), TLPosn x → SuccPos (tileData A).Le (tileData A).Posn y y' → ρ () ![x, y, t] → ρ () ![x, y', t'] → TLVert t t'

theorem DescriptiveComplexity.realize_tileAccC {A : Type} [FirstOrder.Language.tiling.Structure A] (ρ : tileGuessBlock.Assignment A) : A ⊨ tileAccC ↔ ∃ (x : A) (y : A) (t : A), TLPosn x ∧ TLPosn y ∧ ρ () ![x, y, t] ∧ TLAcc t

The definition

theorem DescriptiveComplexity.realize_tileKernel {A : Type} [FirstOrder.Language.tiling.Structure A] (ρ : tileGuessBlock.Assignment A) : A ⊨ tileKernel ↔ (tileData A).WellFormed ∧ (∀ (x y : A), TLPosn x → TLPosn y → ∃ (t : A), ρ () ![x, y, t] ∧ TLTile t) ∧ (∀ (x y t t' : A), ρ () ![x, y, t] → ρ () ![x, y, t'] → t = t') ∧ (∀ (x y t : A), TLPosn x → MinPos (tileData A).Le (tileData A).Posn y → ρ () ![x, y, t] → (MinPos (tileData A).Le (tileData A).Posn x → TLStart t) ∧ (¬MinPos (tileData A).Le (tileData A).Posn x → (tileData A).FirstTile x t)) ∧ (∀ (x y t : A), TLPosn y → MinPos (tileData A).Le (tileData A).Posn x → ρ () ![x, y, t] → TLEdgeL t) ∧ (∀ (x y t : A), TLPosn y → MaxPos (tileData A).Le (tileData A).Posn x → ρ () ![x, y, t] → TLEdgeR t) ∧ (∀ (x x' y t t' : A), SuccPos (tileData A).Le (tileData A).Posn x x' → TLPosn y → ρ () ![x, y, t] → ρ () ![x', y, t'] → TLHoriz t t') ∧ (∀ (x y y' t t' : A), TLPosn x → SuccPos (tileData A).Le (tileData A).Posn y y' → ρ () ![x, y, t] → ρ () ![x, y', t'] → TLVert t t') ∧ ∃ (x : A) (y : A) (t : A), TLPosn x ∧ TLPosn y ∧ ρ () ![x, y, t] ∧ TLAcc t

What the kernel says, at an assignment of the guessed tiling: the instance is well-formed and the guess is a tiling of the square, read as a relation.

theorem DescriptiveComplexity.tiling_sigmaSODefinable : SigmaSODefinable 1 TILING

Tiling a square is Σ₁-definable: guess the tiling as one ternary relation, and check first-order that it is one. Since NP is Σ₁-definability, this is the membership half of the problem's completeness.

theorem DescriptiveComplexity.tiling_mem_NP : NP.Mem TILING

Tiling a square is in NP.