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

theorem DescriptiveComplexity.WideTile.realize_one {A : Type} [FirstOrder.Language.wtile.Structure A] [LinearOrder A] (rt : FirstOrder.Language.tiling.Relations 1) (φ : AddrExp.WTag → wtile1.Sentence) (h : ∀ (τ : Fin 1 → wtileExp.Tag), wtileExp.relSentence rt τ = AddrExp.onS1 (φ (τ 0))) (x : wtileExp.Map A) : FirstOrder.Language.Structure.RelMap rt ![x] ↔ A ⊨ φ (↑x).1

Reading a unary symbol of the expanded vocabulary at one point.

theorem DescriptiveComplexity.WideTile.realize_two {A : Type} [FirstOrder.Language.wtile.Structure A] [LinearOrder A] (rt : FirstOrder.Language.tiling.Relations 2) (φ : AddrExp.WTag → AddrExp.WTag → wtile2.Sentence) (h : ∀ (τ : Fin 2 → wtileExp.Tag), wtileExp.relSentence rt τ = AddrExp.onS2 (φ (τ 0) (τ 1))) (x y : wtileExp.Map A) : FirstOrder.Language.Structure.RelMap rt ![x, y] ↔ A ⊨ φ (↑x).1 (↑y).1

Reading a binary symbol of the expanded vocabulary at two points.

The seven symbols

theorem DescriptiveComplexity.WideTile.relMap_posn {A : Type} [FirstOrder.Language.wtile.Structure A] [LinearOrder A] (p : WPoint A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.tlPosn ![wtileEmbed p] ↔ (wideTileData A).Posn p

The positions of the expanded tiling are the addresses.

theorem DescriptiveComplexity.WideTile.relMap_mark {A : Type} [FirstOrder.Language.wtile.Structure A] [LinearOrder A] (rt : FirstOrder.Language.tiling.Relations 1) (r : FirstOrder.Language.wtile.Relations 1) (h : ∀ (τ : Fin 1 → wtileExp.Tag), wtileExp.relSentence rt τ = AddrExp.onS1 (markT r (τ 0))) (p : WPoint A) : FirstOrder.Language.Structure.RelMap rt ![wtileEmbed p] ↔ wpMark (fun (x : A) => FirstOrder.Language.Structure.RelMap r ![x]) p

A mark of the expanded tiling is the corresponding mark of the instance, carried by the tiles alone.

theorem DescriptiveComplexity.WideTile.relMap_attr {A : Type} [FirstOrder.Language.wtile.Structure A] [LinearOrder A] (rt : FirstOrder.Language.tiling.Relations 2) (r : FirstOrder.Language.wtile.Relations 2) (h : ∀ (τ : Fin 2 → wtileExp.Tag), wtileExp.relSentence rt τ = AddrExp.onS2 (binT r (τ 0) (τ 1))) (p q : WPoint A) : FirstOrder.Language.Structure.RelMap rt ![wtileEmbed p, wtileEmbed q] ↔ wpAttr (fun (x y : A) => FirstOrder.Language.Structure.RelMap r ![x, y]) p q

A compatibility of the expanded tiling is the corresponding relation of the instance, holding of tiles alone.

theorem DescriptiveComplexity.WideTile.relMap_le {A : Type} [FirstOrder.Language.wtile.Structure A] [LinearOrder A] (p q : WPoint A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.tlLe ![wtileEmbed p, wtileEmbed q] ↔ (wideTileData A).Le p q

The order of the expanded tiling: addresses in the binary-number order the instance's own order induces, then the tiles in that order.

theorem DescriptiveComplexity.WideTile.relMap_first {A : Type} [FirstOrder.Language.wtile.Structure A] [LinearOrder A] (p q : WPoint A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.tlFirst ![wtileEmbed p, wtileEmbed q] ↔ (wideTileData A).First p q

The bottom row of the expanded tiling: the address cutting the initial segment of an element may carry that element's tiles.

The two tile systems agree

theorem DescriptiveComplexity.WideTile.wtileAgree {A : Type} [FirstOrder.Language.wtile.Structure A] [LinearOrder A] : (∀ (p : WPoint A), (wideTileData A).Posn p ↔ (tileData (wtileExp.Map A)).Posn (wtileEquiv p)) ∧ (∀ (p q : WPoint A), (wideTileData A).Le p q ↔ (tileData (wtileExp.Map A)).Le (wtileEquiv p) (wtileEquiv q)) ∧ (∀ (p : WPoint A), (wideTileData A).Tile p ↔ (tileData (wtileExp.Map A)).Tile (wtileEquiv p)) ∧ (∀ (p : WPoint A), (wideTileData A).Acc p ↔ (tileData (wtileExp.Map A)).Acc (wtileEquiv p)) ∧ (∀ (p q : WPoint A), (wideTileData A).Horiz p q ↔ (tileData (wtileExp.Map A)).Horiz (wtileEquiv p) (wtileEquiv q)) ∧ (∀ (p q : WPoint A), (wideTileData A).Vert p q ↔ (tileData (wtileExp.Map A)).Vert (wtileEquiv p) (wtileEquiv q)) ∧ (∀ (p q : WPoint A), (wideTileData A).First p q ↔ (tileData (wtileExp.Map A)).First (wtileEquiv p) (wtileEquiv q)) ∧ (∀ (p : WPoint A), (wideTileData A).Base p ↔ (tileData (wtileExp.Map A)).Base (wtileEquiv p)) ∧ (∀ (p : WPoint A), (wideTileData A).Start p ↔ (tileData (wtileExp.Map A)).Start (wtileEquiv p)) ∧ (∀ (p : WPoint A), (wideTileData A).EdgeL p ↔ (tileData (wtileExp.Map A)).EdgeL (wtileEquiv p)) ∧ ∀ (p : WPoint A), (wideTileData A).EdgeR p ↔ (tileData (wtileExp.Map A)).EdgeR (wtileEquiv p)

The expanded tile system is the wide one, field by field, along the bijection between the universes.

theorem DescriptiveComplexity.WideTile.wideTiling_iff_expansion (A : Type) [FirstOrder.Language.wtile.Structure A] [LinearOrder A] : WideTiling.Holds A ↔ TILING.Holds (wtileExp.Map A)

A wide tiling is an ordinary tiling of the expansion.

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.