Tiling a wide square is NEXPTIME-complete

The reduction WideRegAccept ≤ᶠᵒ[≤] WideTiling, and with it the completeness of the wide tiling: the drawing of DescriptiveComplexity.Problems.Wide.TilingHard.Tiles written down as a three-dimensional ordered interpretation, whose two halves are already proved –

• an accepting run draws a tiling (DescriptiveComplexity.TilingHard.tileable_of_accepts);
• a tiling is an accepting run (DescriptiveComplexity.TilingHard.wideRegAccept_of_tileable).

What this file adds is the bridge: the interpreted structure is the emitted one, symbol by symbol, so the identity is an isomorphism between them and the two halves apply to the interpretation itself.

The interpretation

noncomputable def DescriptiveComplexity.TilingHard.tileInterpOf (fF : TileTag → TileTag → wideOrd.Formula (Fin 2 × Fin 3)) : FOInterpretation wideOrd FirstOrder.Language.wtile TileTag 3

The drawing, as an interpretation: three dimensions – a tag, a symbol, a state and a transition – and one formula per symbol of the tile vocabulary. The bottom row is a parameter, as it is in the drawing itself (DescriptiveComplexity.TilingHard.tileStrOf).

Equations

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

noncomputable def DescriptiveComplexity.TilingHard.tileInterp : FOInterpretation wideOrd FirstOrder.Language.wtile TileTag 3

The clocked machine's drawing, as an interpretation: the bottom row is the register file.

Equations

• DescriptiveComplexity.TilingHard.tileInterp = DescriptiveComplexity.TilingHard.tileInterpOf DescriptiveComplexity.TilingHard.firstF

noncomputable def DescriptiveComplexity.TilingHard.tileInterpR : FOInterpretation wideOrd FirstOrder.Language.wtile TileTag 3

And the space-bounded machine's: the bottom row is the ruler.

Equations

• DescriptiveComplexity.TilingHard.tileInterpR = DescriptiveComplexity.TilingHard.tileInterpOf DescriptiveComplexity.TilingHard.firstRF

The reduction and the completeness

theorem DescriptiveComplexity.wideTiling_NEXPTIME_hard : NEXPTIME.Hard WideTiling

Tiling a wide square is NEXPTIME-hard: the wide machine on a clock is, and it is drawn as one.

theorem DescriptiveComplexity.wideTiling_NEXPTIME_complete : NEXPTIME.Complete WideTiling

Tiling a wide square is NEXPTIME-complete. The membership half is DescriptiveComplexity.wideTiling_mem_NEXPTIME: a wide tiling is an ordinary tiling of an exponential expansion, and DescriptiveComplexity.TILING is in NP. Registered in the Lax archive as Lax822549.TilingsComplete.wideTiling_NEXPTIME_complete.