Documentation

DescriptiveComplexity.Problems.Wide.TilingHard.Grid

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).

source
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
Instances For
    Dependency graph
    source
    @[simp]
    theorem DescriptiveComplexity.TilingHard.tpCol_dig {A : Type} (s : A → Prop) (x : A) :
    tpCol s (tpDig x) ↔ s x
    Dependency graph
    source
    theorem DescriptiveComplexity.TilingHard.tpCol_dig_of_mem {A : Type} {s : A → Prop} {p : TilePt A} (h : tpCol s p) :
    TPDig p

    A coordinate holds digits alone, which is what makes it a position.

    Dependency graph
    source
    theorem DescriptiveComplexity.TilingHard.tpDig_eq_self {A : Type} {p : TilePt A} (h : TPDig p) :
    tpDig (p.2 0) = p

    A digit is the digit of its own first coordinate.

    Dependency graph
    source
    theorem DescriptiveComplexity.TilingHard.tpCol_injective {A : Type} :
    Function.Injective tpCol

    Two addresses with the same coordinate are the same address.

    Dependency graph
    source
    theorem DescriptiveComplexity.TilingHard.exists_tpCol {A : Type} {u : TilePt A → Prop} (h : ∀ (p : TilePt A), u p → TPDig p) :
    ∃ (s : A → Prop), u = tpCol s

    Every position is a coordinate: an address holding digits alone is the coordinate of the elements those digits belong to.

    Dependency graph
    source
    theorem DescriptiveComplexity.TilingHard.tpCol_setLe {A : Type} [LinearOrder A] [FirstOrder.Language.wide.Structure A] (s t : A → Prop) :
    WMSetLe tpLe (tpCol s) (tpCol t) ↔ WMSetLe WMLe s t

    The order on coordinates is the machine's order on addresses: they differ at a digit, and there the emitted order is the machine's.

    Dependency graph

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

    source
    theorem DescriptiveComplexity.TilingHard.not_tpCol_bot {A : Type} (p : TilePt A) :
    ¬tpCol (fun (x : A) => False) p

    The empty coordinate holds nothing.

    Dependency graph
    source
    theorem DescriptiveComplexity.TilingHard.exists_tpCol_of_posn {A : Type} [LinearOrder A] [FirstOrder.Language.wide.Structure A] {p : WPoint (TilePt A)} (hp : (wideTileData (TilePt A)).Posn p) :
    ∃ (s : A → Prop), p = Sum.inl (tpCol s)

    Every position of the emitted tiling is the coordinate of an address of the machine.

    Dependency graph
    source
    theorem DescriptiveComplexity.TilingHard.minPos_tpCol_bot {A : Type} [LinearOrder A] [Finite A] [FirstOrder.Language.wide.Structure A] (hlin : IsLinOrd WMLe) :
    MinPos (wideTileData (TilePt A)).Le (wideTileData (TilePt A)).Posn (Sum.inl (tpCol fun (x : A) => False))

    The empty coordinate is the least position, which is where the machine's head starts and where the bottom row is.

    Dependency graph
    source
    theorem DescriptiveComplexity.TilingHard.eq_bot_of_minPos {A : Type} [LinearOrder A] [Finite A] [FirstOrder.Language.wide.Structure A] (hlin : IsLinOrd WMLe) {p : WPoint (TilePt A)} (h : MinPos (wideTileData (TilePt A)).Le (wideTileData (TilePt A)).Posn p) :
    p = Sum.inl (tpCol fun (x : A) => False)

    And it is the only one: a least position is the empty coordinate.

    Dependency graph
    source
    theorem DescriptiveComplexity.TilingHard.maxPos_tpCol_top {A : Type} [LinearOrder A] [Finite A] [FirstOrder.Language.wide.Structure A] (hlin : IsLinOrd WMLe) :
    MaxPos (wideTileData (TilePt A)).Le (wideTileData (TilePt A)).Posn (Sum.inl (tpCol fun (x : A) => True))

    The full coordinate is the last position, which is the other column with a neighbor missing.

    Dependency graph
    source
    theorem DescriptiveComplexity.TilingHard.eq_top_of_maxPos {A : Type} [LinearOrder A] [Finite A] [FirstOrder.Language.wide.Structure A] (hlin : IsLinOrd WMLe) {p : WPoint (TilePt A)} (h : MaxPos (wideTileData (TilePt A)).Le (wideTileData (TilePt A)).Posn p) :
    p = Sum.inl (tpCol fun (x : A) => True)

    And it is the only one: a last position is the full coordinate.

    Dependency graph
    source
    theorem DescriptiveComplexity.TilingHard.succPos_tpCol {A : Type} [LinearOrder A] [Finite A] [FirstOrder.Language.wide.Structure A] (hlin : IsLinOrd WMLe) (s t : A → Prop) :
    SuccPos (wideTileData (TilePt A)).Le (wideTileData (TilePt A)).Posn (Sum.inl (tpCol s)) (Sum.inl (tpCol t)) ↔ WMIncr WMLe s t

    The successor of a coordinate is the increment of the address: nothing lies strictly between an address and its increment, and every position is a coordinate.

    Dependency graph