Documentation

DescriptiveComplexity.Problems.Wide.TilingHard.Emit

The tile system a machine is drawn as, and its grid #

The instance the hardness reduction emits, read semantically: a FirstOrder.Language.wtile-structure on the tagged triples DescriptiveComplexity.TilePt, with the tiles of DescriptiveComplexity.Problems.Wide.TilingHard.Tiles and an order whose digits come last.

That last point is what makes the grid the right size. A coordinate of DescriptiveComplexity.WideTiling is an address holding digits alone, so the square is indexed by the subsets of the diagonal – one per subset of the machine's own instance, which is exactly one per tape address and one per time step. The other points of the emitted universe are tiles, and they are ordered below every digit, so they never enter a coordinate and never disturb the binary-number order the coordinates are compared by: two coordinates differ at a digit, and there the emitted order is the machine's own.

The order on the emitted universe #

source
@[instance_reducible]
noncomputable instance DescriptiveComplexity.TilingHard.instLinearOrderTileTag :
LinearOrder TileTag

A linear order on the tags, to order the points that are not digits.

Equations
Dependency graph
source
def DescriptiveComplexity.TilingHard.tpLe {A : Type} [LinearOrder A] [FirstOrder.Language.wide.Structure A] (p q : TilePt A) :
Prop

The order the emitted instance carries: the points that are not digits first, in the lexicographic order of their tag and their triple, then the digits in the machine's own order.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Dependency graph
    source
    theorem DescriptiveComplexity.TilingHard.isLinOrd_tagTuple {A : Type} [LinearOrder A] :
    IsLinOrd tagTupleLe

    The lexicographic order on the emitted universe is linear – Mathlib's, read through DescriptiveComplexity.tagTupleLe_iff_le.

    Dependency graph
    source
    theorem DescriptiveComplexity.TilingHard.eq_of_tpDig {A : Type} {p q : TilePt A} (hp : TPDig p) (hq : TPDig q) (h : p.2 0 = q.2 0) :
    p = q

    A digit is determined by the element it is the digit of.

    Dependency graph
    source
    theorem DescriptiveComplexity.TilingHard.isLinOrd_tpLe {A : Type} [LinearOrder A] [FirstOrder.Language.wide.Structure A] (h : IsLinOrd WMLe) :
    IsLinOrd tpLe

    The emitted order is linear, given that the machine's is: the digits carry the machine's order, and everything else the lexicographic one.

    Dependency graph
    source
    theorem DescriptiveComplexity.TilingHard.tpLe_dig {A : Type} [LinearOrder A] [FirstOrder.Language.wide.Structure A] (x y : A) :
    tpLe (tpDig x) (tpDig y) ↔ WMLe x y

    Between two digits the emitted order is the machine's.

    Dependency graph

    The structure the reduction emits #

    source
    @[instance_reducible]
    noncomputable def DescriptiveComplexity.TilingHard.tileStrOf {A : Type} [LinearOrder A] [FirstOrder.Language.wide.Structure A] (F : TilePt A → TilePt A → Prop) :
    FirstOrder.Language.wtile.Structure (TilePt A)

    The tile system a wide machine is drawn as: the tiles of DescriptiveComplexity.Problems.Wide.TilingHard.Tiles on the tagged triples, with the digits last in the order. This is the instance the hardness reductions emit, read semantically – the formulas that write it down come later, and are checked against exactly this.

    The bottom row is a parameter, because it is the one thing the two machines this drawing serves describe differently: the clocked machine's tape is a register file and the space-bounded machine's the ruler of all the segments. Everything else – the tiles, the two compatibilities, the edges and the corner – is the same drawing.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Dependency graph
      source
      @[instance_reducible]
      noncomputable def DescriptiveComplexity.TilingHard.tileStr (A : Type) [LinearOrder A] [FirstOrder.Language.wide.Structure A] :
      FirstOrder.Language.wtile.Structure (TilePt A)

      The drawing of the clocked machine: the tile system above with the register file for its bottom row.

      Equations
      Instances For
        Dependency graph
        source
        @[instance_reducible]
        noncomputable def DescriptiveComplexity.TilingHard.tileStrR (A : Type) [LinearOrder A] [FirstOrder.Language.wide.Structure A] :
        FirstOrder.Language.wtile.Structure (TilePt A)

        The drawing of the space-bounded machine: the same tile system with the ruler of all the segments for its bottom row.

        Equations
        Instances For
          Dependency graph
          source
          @[simp]
          theorem DescriptiveComplexity.TilingHard.wtLe_tileStrOf {A : Type} [LinearOrder A] [FirstOrder.Language.wide.Structure A] (F : TilePt A → TilePt A → Prop) (p q : TilePt A) :
          WTLe p q ↔ tpLe p q
          Dependency graph
          source
          @[simp]
          theorem DescriptiveComplexity.TilingHard.wtLe_tileStr {A : Type} [LinearOrder A] [FirstOrder.Language.wide.Structure A] (p q : TilePt A) :
          WTLe p q ↔ tpLe p q
          Dependency graph
          source
          @[simp]
          theorem DescriptiveComplexity.TilingHard.wtDig_tileStr {A : Type} [LinearOrder A] [FirstOrder.Language.wide.Structure A] (p : TilePt A) :
          WTDig p ↔ TPDig p
          Dependency graph
          source
          @[simp]
          theorem DescriptiveComplexity.TilingHard.wtTile_tileStr {A : Type} [LinearOrder A] [FirstOrder.Language.wide.Structure A] (p : TilePt A) :
          WTTile p ↔ TPTile p
          Dependency graph
          source
          @[simp]
          theorem DescriptiveComplexity.TilingHard.wtAcc_tileStr {A : Type} [LinearOrder A] [FirstOrder.Language.wide.Structure A] (p : TilePt A) :
          WTAcc p ↔ TPAcc p
          Dependency graph
          source
          @[simp]
          theorem DescriptiveComplexity.TilingHard.wtHoriz_tileStr {A : Type} [LinearOrder A] [FirstOrder.Language.wide.Structure A] (p q : TilePt A) :
          WTHoriz p q ↔ TPHoriz p q
          Dependency graph
          source
          @[simp]
          theorem DescriptiveComplexity.TilingHard.wtVert_tileStr {A : Type} [LinearOrder A] [FirstOrder.Language.wide.Structure A] (p q : TilePt A) :
          WTVert p q ↔ TPVert p q
          Dependency graph
          source
          @[simp]
          theorem DescriptiveComplexity.TilingHard.wtFirst_tileStr {A : Type} [LinearOrder A] [FirstOrder.Language.wide.Structure A] (p q : TilePt A) :
          WTFirst p q ↔ TPFirst p q
          Dependency graph
          source
          @[simp]
          theorem DescriptiveComplexity.TilingHard.wtFirst_tileStrR {A : Type} [LinearOrder A] [FirstOrder.Language.wide.Structure A] (p q : TilePt A) :
          WTFirst p q ↔ TPFirstR p q
          Dependency graph
          source
          @[simp]
          theorem DescriptiveComplexity.TilingHard.wtBase_tileStr {A : Type} [LinearOrder A] [FirstOrder.Language.wide.Structure A] (p : TilePt A) :
          WTBase p ↔ TPBase p
          Dependency graph
          source
          @[simp]
          theorem DescriptiveComplexity.TilingHard.wtStart_tileStr {A : Type} [LinearOrder A] [FirstOrder.Language.wide.Structure A] (p : TilePt A) :
          WTStart p ↔ TPStart p
          Dependency graph
          source
          @[simp]
          theorem DescriptiveComplexity.TilingHard.wtEdgeL_tileStr {A : Type} [LinearOrder A] [FirstOrder.Language.wide.Structure A] (p : TilePt A) :
          WTEdgeL p ↔ TPEdgeL p
          Dependency graph
          source
          @[simp]
          theorem DescriptiveComplexity.TilingHard.wtEdgeR_tileStr {A : Type} [LinearOrder A] [FirstOrder.Language.wide.Structure A] (p : TilePt A) :
          WTEdgeR p ↔ TPEdgeR p
          Dependency graph