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

noncomputable def DescriptiveComplexity.TilingHard.tileEquivOf (A : Type) [FirstOrder.Language.wide.Structure A] [LinearOrder A] (F : TilePt A → TilePt A → Prop) (fF : TileTag → TileTag → wideOrd.Formula (Fin 2 × Fin 3)) (hF : ∀ (v : Fin 2 × Fin 3 → A) (t₁ t₂ : TileTag), (fF t₁ t₂).Realize v ↔ F (argPt v t₁ 0) (argPt v t₂ 1)) : FirstOrder.Language.wtile.Equiv ((tileInterpOf fF).Map A) (TilePt A)

The interpreted structure is the emitted one: the identity map is an isomorphism, since every symbol's formula was checked against the predicate it draws.

Equations

• DescriptiveComplexity.TilingHard.tileEquivOf A F fF hF = { toEquiv := Equiv.refl ((DescriptiveComplexity.TilingHard.tileInterpOf fF).Map A), map_fun' := ⋯, map_rel' := ⋯ }

noncomputable def DescriptiveComplexity.TilingHard.tileEquiv (A : Type) [FirstOrder.Language.wide.Structure A] [LinearOrder A] : FirstOrder.Language.wtile.Equiv (tileInterp.Map A) (TilePt A)

The clocked machine's drawing, as an isomorphism.

Equations

• DescriptiveComplexity.TilingHard.tileEquiv A = DescriptiveComplexity.TilingHard.tileEquivOf A DescriptiveComplexity.TPFirst DescriptiveComplexity.TilingHard.firstF ⋯

noncomputable def DescriptiveComplexity.TilingHard.tileEquivR (A : Type) [FirstOrder.Language.wide.Structure A] [LinearOrder A] : FirstOrder.Language.wtile.Equiv (tileInterpR.Map A) (TilePt A)

And the space-bounded machine's.

Equations

• DescriptiveComplexity.TilingHard.tileEquivR A = DescriptiveComplexity.TilingHard.tileEquivOf A DescriptiveComplexity.TPFirstR DescriptiveComplexity.TilingHard.firstRF ⋯

theorem DescriptiveComplexity.TilingHard.wideTiling_map_iff (A : Type) [FirstOrder.Language.wide.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : WideTiling.Holds (tileInterp.Map A) ↔ WideTiling.Holds (TilePt A)

The interpreted structure is a yes-instance exactly when the emitted one is.

The reduction and the completeness

noncomputable def DescriptiveComplexity.wideRegAccept_ordered_fo_reduction_wideTiling : OrderedFOReduction WideRegAccept WideTiling

A wide machine on a clock is drawn as a tiling of the emitted square. The universe is three-dimensional – a tag with a symbol, a state and a transition – and the machine's promises ride on the start tile, so a no-instance's drawing has no corner and hence no tiling.

Equations

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

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.