The wide tiling as an exponential expansion

What makes DescriptiveComplexity.WideTiling a member of NEXPTIME, and nothing about resources: the address expansion (DescriptiveComplexity.AddrExp.addrExp) at the vocabulary of ordinary tile systems. Read on an instance A, it produces exactly the tile system whose positions are the addresses of A – so a wide tiling is an ordinary tiling, one exponential up, and membership is the composition TILING ∘ expansion, exactly as DescriptiveComplexity.wideAccept_mem_NEXPTIME is NTMAccept ∘ expansion.

Each of the symbols is a static choice on the two tags followed by one of the address expansion's five sentences: a mark of the instance for the tiles and the accepting ones, a binary attribute for the two compatibilities, the binary-number order for the order, and the initial-segment reading for the bottom row.

The defining sentences, at the tags

@[reducible, inline]

abbrev DescriptiveComplexity.WideTile.wtOrd : FirstOrder.Language

The ordered vocabulary of wide tile-system instances.

Equations

• DescriptiveComplexity.WideTile.wtOrd = DescriptiveComplexity.AddrExp.aeOrd FirstOrder.Language.wtile

@[reducible, inline]

abbrev DescriptiveComplexity.WideTile.wtile1 : FirstOrder.Language

The base vocabulary expanded by one copy of the block.

Equations

• DescriptiveComplexity.WideTile.wtile1 = DescriptiveComplexity.AddrExp.aeLang1 FirstOrder.Language.wtile

@[reducible, inline]

abbrev DescriptiveComplexity.WideTile.wtile2 : FirstOrder.Language

The base vocabulary expanded by two copies of the block.

Equations

• DescriptiveComplexity.WideTile.wtile2 = DescriptiveComplexity.AddrExp.aeLang2 FirstOrder.Language.wtile

noncomputable def DescriptiveComplexity.WideTile.posnT : AddrExp.WTag → wtile1.Sentence

Being a position: an address of digits is one, a tile is not.

Equations

• DescriptiveComplexity.WideTile.posnT DescriptiveComplexity.AddrExp.WTag.addr = DescriptiveComplexity.AddrExp.subsetS FirstOrder.Language.wtDig
• DescriptiveComplexity.WideTile.posnT DescriptiveComplexity.AddrExp.WTag.ctrl = ⊥

noncomputable def DescriptiveComplexity.WideTile.markT (r : FirstOrder.Language.wtile.Relations 1) : AddrExp.WTag → wtile1.Sentence

A mark of the instance, at a tag: only the elements carry it.

Equations

• DescriptiveComplexity.WideTile.markT r DescriptiveComplexity.AddrExp.WTag.addr = ⊥
• DescriptiveComplexity.WideTile.markT r DescriptiveComplexity.AddrExp.WTag.ctrl = DescriptiveComplexity.AddrExp.markS r

noncomputable def DescriptiveComplexity.WideTile.binT (r : FirstOrder.Language.wtile.Relations 2) : AddrExp.WTag → AddrExp.WTag → wtile2.Sentence

A binary attribute of the instance, at a pair of tags.

Equations

• DescriptiveComplexity.WideTile.binT r DescriptiveComplexity.AddrExp.WTag.ctrl DescriptiveComplexity.AddrExp.WTag.ctrl = DescriptiveComplexity.AddrExp.binS r
• DescriptiveComplexity.WideTile.binT r x✝¹ x✝ = ⊥

noncomputable def DescriptiveComplexity.WideTile.leT : AddrExp.WTag → AddrExp.WTag → wtile2.Sentence

The order of the tiling, at a pair of tags: the addresses come first, in the binary-number order, then the tiles in the instance's order.

Equations

• DescriptiveComplexity.WideTile.leT DescriptiveComplexity.AddrExp.WTag.addr DescriptiveComplexity.AddrExp.WTag.addr = DescriptiveComplexity.AddrExp.addrLeS FirstOrder.Language.wtLe
• DescriptiveComplexity.WideTile.leT DescriptiveComplexity.AddrExp.WTag.addr DescriptiveComplexity.AddrExp.WTag.ctrl = ⊤
• DescriptiveComplexity.WideTile.leT DescriptiveComplexity.AddrExp.WTag.ctrl DescriptiveComplexity.AddrExp.WTag.addr = ⊥
• DescriptiveComplexity.WideTile.leT DescriptiveComplexity.AddrExp.WTag.ctrl DescriptiveComplexity.AddrExp.WTag.ctrl = DescriptiveComplexity.AddrExp.binS FirstOrder.Language.wtLe

noncomputable def DescriptiveComplexity.WideTile.firstT : AddrExp.WTag → AddrExp.WTag → wtile2.Sentence

The bottom row, at a pair of tags: the cell of an element may carry a tile.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.WideTile.firstT x✝¹ x✝ = ⊥

noncomputable def DescriptiveComplexity.WideTile.wtileExp : ExpExpansion FirstOrder.Language.wtile

The expansion of a wide tile-system instance: the address expansion at the vocabulary of ordinary tile systems.

Equations

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

@[instance_reducible]

noncomputable def DescriptiveComplexity.WideTile.wtileStructure (A : Type) [FirstOrder.Language.wtile.Structure A] [LinearOrder A] : FirstOrder.Language.tiling.Structure (wtileExp.Map A)

The expanded structure, at the vocabulary of tile systems – equal to the expansion's own by definition, but not syntactically, so instance search has to be handed it.

Equations

• DescriptiveComplexity.WideTile.wtileStructure A = DescriptiveComplexity.AddrExp.addrStructure A

noncomputable def DescriptiveComplexity.WideTile.wtileEmbed {A : Type} [FirstOrder.Language.wtile.Structure A] [LinearOrder A] : WPoint A → wtileExp.Map A

The universe of the wide tiling sits inside the expansion.

Equations

• DescriptiveComplexity.WideTile.wtileEmbed = DescriptiveComplexity.AddrExp.addrEmbed

noncomputable def DescriptiveComplexity.WideTile.wtileEquiv {A : Type} [FirstOrder.Language.wtile.Structure A] [LinearOrder A] : WPoint A ≃ wtileExp.Map A

The points of the expansion are the universe of the wide tiling.

Equations

• DescriptiveComplexity.WideTile.wtileEquiv = DescriptiveComplexity.AddrExp.addrEquiv

@[simp]

theorem DescriptiveComplexity.WideTile.wtileEquiv_apply {A : Type} [FirstOrder.Language.wtile.Structure A] [LinearOrder A] (p : WPoint A) : wtileEquiv p = wtileEmbed p

The seven symbols

The two tile systems agree

The membership

theorem DescriptiveComplexity.wideTiling_mem_NEXPTIME : NEXPTIME.Mem WideTiling

The wide tiling is in NEXPTIME, which is NP.exp: the expansion turns it into DescriptiveComplexity.TILING, and that problem is in NP. This is the second natural member the class has, beside the wide machine.