The grid of the emitted tiling is the machine's tape

The bridge the hardness reduction is built on: the coordinates of DescriptiveComplexity.WideTiling at the emitted instance are exactly the addresses of the machine's own instance, in the machine's own order.

A coordinate is an address of the emitted universe holding digits alone (DescriptiveComplexity.wtpPosn), a digit is the diagonal triple of an element (DescriptiveComplexity.tpDig), and the emitted order puts every point that is not a digit below every digit. So a coordinate is a set of digits, the two coordinates being compared differ at a digit, and there the emitted order is the machine's: the binary-number order on coordinates is the binary-number order on the machine's addresses (tpCol_setLe).

def DescriptiveComplexity.TilingHard.tpCol {A : Type} (s : A → Prop) : TilePt A → Prop

The coordinate an address of the machine is: the digits of its elements.

Equations

• DescriptiveComplexity.TilingHard.tpCol s p = ∃ (a : A), s a ∧ p = DescriptiveComplexity.tpDig a

@[simp]

theorem DescriptiveComplexity.TilingHard.tpCol_dig {A : Type} (s : A → Prop) (x : A) : tpCol s (tpDig x) ↔ s x

The bottom row and the step from one row to the next