What a rule owes the interpretation, and the algebra that discharges it

A hardness reduction into DescriptiveComplexity.DWideAcceptSpace emits a machine, and an interpretation has to write that machine down: one formula per relation symbol and tag tuple, read at the coordinates a transition's payload occupies. So each rule owes, of its guard and of the two things it computes, that a formula defines them – the same formula at every instance, since an interpretation carries one.

The obligation is quantified over the structure

The quantifier therefore sits outside the existential, and what it ranges over is DescriptiveComplexity.Draw.Env: a finite nonempty linearly ordered structure of the source vocabulary together with the two designated elements the reduction may name – the order's least and greatest. Bundling them into one record is what keeps the algebra readable: every statement below has a single extra binder e, and instance resolution finds the order, the finiteness and the structure inside it.

Guards are formulas; writes are sources

A guard may ask anything first-order of its data, and it has to: the program evaluates a logic, so a guard eventually compares two control slots in the order, or asks a relation of the source vocabulary of them – neither of which is a function of the equality pattern of the data. So DescriptiveComplexity.Draw.UGDefinable carries a formula over the payload coordinates, with DescriptiveComplexity.patSetF still available as one way of building it.

A write, by contrast, never asks anything: every value the program stores is a copy of one of its slots, one of the two designated elements, or the next element after a slot (which is what advancing a loop variable needs). So DescriptiveComplexity.Draw.USlotDefinable is a formula for the graph of the value, and DescriptiveComplexity.SlotVal builds all three cases.

The three obligations

A rule is written with its pointer and its tracks apart, so the obligations are carried in that shape: UGDefinable for the guard, UStDefinable for the pointer it leaves, UTrDefinable for the tracks it writes – with DescriptiveComplexity.Draw.URuleDefinable bundling the three together with the staticness of its two phases and its direction. That is what travels through the program's tower, one statement per rule, composed site by site, with a kit's abstract parameters (Match, setFlag …) contributing hypotheses of the same shape.

Which coordinate a slot occupies

@[reducible, inline]

abbrev DescriptiveComplexity.Draw.baseSym {L : FirstOrder.Language} {m : ℕ} (r : L.Relations m) : (L.sum FirstOrder.Language.order).Relations m

A relation of the source vocabulary, in the ordered expansion: named, because a raw Sum.inl is not recognized at the transparency rw matches at.

Equations

• DescriptiveComplexity.Draw.baseSym r = Sum.inl r

@[reducible]

noncomputable def DescriptiveComplexity.Draw.slotIx {Q W : Type} [Fintype Q] [Fintype W] (d : Q ⊕ W) : Fin (Fintype.card (Q ⊕ W))

The coordinate of a slot in a rule's payload.

Equations

• DescriptiveComplexity.Draw.slotIx d = (Fintype.equivFin (Q ⊕ W)) d

The structures a reduction's rules are read at

structure DescriptiveComplexity.Draw.Env (L : FirstOrder.Language) : Type 1

An environment: a finite nonempty linearly ordered structure of the source vocabulary, with the two elements a reduction may designate – the order's least and greatest, the only ones an interpretation can name. The program's rules are functions of one of these, and their definability is a statement about all of them, which is what an interpretation needs.

• α : Type

  The universe.

• ord : LinearOrder self.α

  Its order.

• fin : Finite self.α

  Which is finite.

• ne : Nonempty self.α

  And nonempty.

• str : L.Structure self.α

  And carries the source structure.

• zero : self.α

  The element a clear track holds.

• one : self.α

  The element a set track holds.

• hbot : IsBot self.zero

  The clear element is the order's least.

• htop : IsTop self.one

  The set element is its greatest.

• hzo : self.zero ≠ self.one

  The two differ.

theorem DescriptiveComplexity.Draw.Env.isBot_iff {L : FirstOrder.Language} (e : Env L) (a : e.α) : IsBot a ↔ a = e.zero

In a linear order, being a minimum is being the designated minimum.

theorem DescriptiveComplexity.Draw.Env.isTop_iff {L : FirstOrder.Language} (e : Env L) (a : e.α) : IsTop a ↔ a = e.one

And dually.

The three obligations, uniformly

def DescriptiveComplexity.Draw.UGDefinable {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] (N : (e : Env L) → (Q → e.α) → (W → e.α) → Prop) : Prop

A guard is definable: one formula over the payload coordinates decides it at every environment.

Equations

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

def DescriptiveComplexity.Draw.USlotDefinable {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] (V : (e : Env L) → (Q → e.α) → (W → e.α) → e.α) : Prop

A written value is definable: one formula over the payload coordinates and one more variable defines its graph.

Equations

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

def DescriptiveComplexity.Draw.UStDefinable {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] (F : (e : Env L) → (Q → e.α) → (W → e.α) → Q → e.α) : Prop

A pointer a rule leaves is definable: one value per control slot.

Equations

• DescriptiveComplexity.Draw.UStDefinable F = ∀ (q : Q), DescriptiveComplexity.Draw.USlotDefinable fun (e : DescriptiveComplexity.Draw.Env L) (f : Q → e.α) (g : W → e.α) => F e f g q

def DescriptiveComplexity.Draw.UTrDefinable {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] (F : (e : Env L) → (Q → e.α) → (W → e.α) → W → e.α) : Prop

And so are the tracks it writes: one value per track slot.

Equations

• DescriptiveComplexity.Draw.UTrDefinable F = ∀ (s : W), DescriptiveComplexity.Draw.USlotDefinable fun (e : DescriptiveComplexity.Draw.Env L) (f : Q → e.α) (g : W → e.α) => F e f g s

structure DescriptiveComplexity.Draw.URuleDefinable {L : FirstOrder.Language} {Q W P : Type} [Fintype Q] [Fintype W] (rl : (e : Env L) → Rule e.α Q W P) : Prop

A rule is definable: its two phases and its direction do not depend on the instance at all – they are decided when the formula is built – its guard is defined by a formula, and the pointer it leaves and the tracks it writes are named slot by slot. This is what travels through the program's tower.

• srcPh : ∃ (p : P), ∀ (e : Env L), (rl e).srcPh = p

  The phase it fires from is the same at every instance.

• dstPh : ∃ (p : P), ∀ (e : Env L), (rl e).dstPh = p

  And so is the phase it moves to.

• right : ∃ (b : Bool), ∀ (e : Env L), (rl e).moveRight ↔ b = true

  And so is its direction.

• guard : UGDefinable fun (e : Env L) => (rl e).guard

  The guard is defined by a formula.

• dst : UStDefinable fun (e : Env L) => (rl e).dstSt

  The pointer it leaves is definable slot by slot.

• wr : UTrDefinable fun (e : Env L) => (rl e).wr

  And so are the tracks it writes.

def DescriptiveComplexity.Draw.URulesDefinable {L : FirstOrder.Language} {Q W P : Type} [Fintype Q] [Fintype W] {S : Type} {Sh : S → Type} (rules : (e : Env L) → (i : S) → Sh i → Rule e.α Q W P) : Prop

A whole site's rules are definable.

Equations

• DescriptiveComplexity.Draw.URulesDefinable rules = ∀ (i : S) (ρ : Sh i), DescriptiveComplexity.Draw.URuleDefinable fun (e : DescriptiveComplexity.Draw.Env L) => rules e i ρ

The atoms of a guard

A slot holds one of the two designated elements; two slots hold the same element; one slot is at most another; and a relation of the source vocabulary holds of a tuple of slots. The last two are what an equality pattern cannot say, and what a program that evaluates a logic needs.

And their connectives

theorem DescriptiveComplexity.Draw.UGDefinable.congr {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] {N N' : (e : Env L) → (Q → e.α) → (W → e.α) → Prop} (h : UGDefinable N) (he : ∀ (e : Env L) (f : Q → e.α) (g : W → e.α), N' e f g ↔ N e f g) : UGDefinable N'

A guard stated one way is a guard stated any equivalent way.

theorem DescriptiveComplexity.Draw.UGDefinable.and {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] {N N' : (e : Env L) → (Q → e.α) → (W → e.α) → Prop} (h : UGDefinable N) (h' : UGDefinable N') : UGDefinable fun (e : Env L) (f : Q → e.α) (g : W → e.α) => N e f g ∧ N' e f g

theorem DescriptiveComplexity.Draw.UGDefinable.or {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] {N N' : (e : Env L) → (Q → e.α) → (W → e.α) → Prop} (h : UGDefinable N) (h' : UGDefinable N') : UGDefinable fun (e : Env L) (f : Q → e.α) (g : W → e.α) => N e f g ∨ N' e f g

theorem DescriptiveComplexity.Draw.UGDefinable.ite {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] {N N' : (e : Env L) → (Q → e.α) → (W → e.α) → Prop} {p : Prop} [Decidable p] (h : UGDefinable N) (h' : UGDefinable N') : UGDefinable fun (e : Env L) (f : Q → e.α) (g : W → e.α) => if p then N e f g else N' e f g

A condition decided when the formula is built – by the kit, not by the data.

The atoms of a written value

@[reducible, inline]

abbrev DescriptiveComplexity.Draw.outVar {Q W : Type} [Fintype Q] [Fintype W] : Fin (Fintype.card (Q ⊕ W)) ⊕ Unit

The variable a written value is named at.

Equations

• DescriptiveComplexity.Draw.outVar = Sum.inr ()

def DescriptiveComplexity.Draw.liftG {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] (φ : (L.sum FirstOrder.Language.order).Formula (Fin (Fintype.card (Q ⊕ W)))) : (L.sum FirstOrder.Language.order).Formula (Fin (Fintype.card (Q ⊕ W)) ⊕ Unit)

A guard's formula, read in the context a written value is named in.

Equations

• DescriptiveComplexity.Draw.liftG φ = FirstOrder.Language.Formula.relabel Sum.inl φ

theorem DescriptiveComplexity.Draw.USlotDefinable.congr {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] {V V' : (e : Env L) → (Q → e.α) → (W → e.α) → e.α} (h : USlotDefinable V) (he : ∀ (e : Env L) (f : Q → e.α) (g : W → e.α), V' e f g = V e f g) : USlotDefinable V'

theorem DescriptiveComplexity.Draw.USlotDefinable.ite {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] {V V' : (e : Env L) → (Q → e.α) → (W → e.α) → e.α} {p : Prop} [Decidable p] (h : USlotDefinable V) (h' : USlotDefinable V') : USlotDefinable fun (e : Env L) (f : Q → e.α) (g : W → e.α) => if p then V e f g else V' e f g

A value chosen by a condition of the kit – not of the data – is definable when both branches are.

theorem DescriptiveComplexity.Draw.uSlotDefinable_cases {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] {V V' : (e : Env L) → (Q → e.α) → (W → e.α) → e.α} {ι : Type u_1} [Finite ι] {R : ι → (e : Env L) → (Q → e.α) → (W → e.α) → Prop} {U : ι → (e : Env L) → (Q → e.α) → (W → e.α) → e.α} (hR : ∀ (i : ι), UGDefinable (R i)) (hU : ∀ (i : ι), USlotDefinable (U i)) (h₀ : USlotDefinable V') (hpos : ∀ (e : Env L) (f : Q → e.α) (g : W → e.α) (i : ι), R i e f g → V e f g = U i e f g) (hneg : ∀ (e : Env L) (f : Q → e.α) (g : W → e.α), (∀ (i : ι), ¬R i e f g) → V e f g = V' e f g) : USlotDefinable V

A value chosen by definable cases: finitely many conditions, each definable, at most one of which is asked to hold, with a default. This is what a write depending on which coordinate of a tuple rolled over needs.

Values a slot may be compared with

def DescriptiveComplexity.Draw.UReadable {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] (V : (e : Env L) → (Q → e.α) → (W → e.α) → e.α) : Prop

A readable value: one a slot may be compared with. Every written value is one, the comparison being the graph formula read at that slot.

Equations

• DescriptiveComplexity.Draw.UReadable V = ∀ (s : W), DescriptiveComplexity.Draw.UGDefinable fun (e : DescriptiveComplexity.Draw.Env L) (f : Q → e.α) (g : W → e.α) => g s = V e f g

theorem DescriptiveComplexity.Draw.USlotDefinable.readable {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] {V : (e : Env L) → (Q → e.α) → (W → e.α) → e.α} (h : USlotDefinable V) : UReadable V

Every written value is readable.

theorem DescriptiveComplexity.Draw.UReadable.congr {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] {V V' : (e : Env L) → (Q → e.α) → (W → e.α) → e.α} (h : UReadable V) (he : ∀ (e : Env L) (f : Q → e.α) (g : W → e.α), V' e f g = V e f g) : UReadable V'

From slots to payloads

theorem DescriptiveComplexity.Draw.uStDefinable_id {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] : UStDefinable fun (x : Env L) (f : Q → x.α) (x_1 : W → x.α) => f

theorem DescriptiveComplexity.Draw.uTrDefinable_id {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] : UTrDefinable fun (x : Env L) (x_1 : Q → x.α) (g : W → x.α) => g

theorem DescriptiveComplexity.Draw.UStDefinable.congr {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] {F F' : (e : Env L) → (Q → e.α) → (W → e.α) → Q → e.α} (h : UStDefinable F) (he : ∀ (e : Env L) (f : Q → e.α) (g : W → e.α) (q : Q), F' e f g q = F e f g q) : UStDefinable F'

theorem DescriptiveComplexity.Draw.UTrDefinable.congr {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] {G G' : (e : Env L) → (Q → e.α) → (W → e.α) → W → e.α} (h : UTrDefinable G) (he : ∀ (e : Env L) (f : Q → e.α) (g : W → e.α) (s : W), G' e f g s = G e f g s) : UTrDefinable G'

theorem DescriptiveComplexity.Draw.UStDefinable.update {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] {V : (e : Env L) → (Q → e.α) → (W → e.α) → e.α} {F : (e : Env L) → (Q → e.α) → (W → e.α) → Q → e.α} [DecidableEq Q] (h : UStDefinable F) (q₀ : Q) (hV : USlotDefinable V) : UStDefinable fun (e : Env L) (f : Q → e.α) (g : W → e.α) => Function.update (F e f g) q₀ (V e f g)

Updating one control slot: every other slot is what it was, and the choice between the two cases is made per slot, when the formula is built.

theorem DescriptiveComplexity.Draw.UTrDefinable.update {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] {V : (e : Env L) → (Q → e.α) → (W → e.α) → e.α} {G : (e : Env L) → (Q → e.α) → (W → e.α) → W → e.α} [DecidableEq W] (h : UTrDefinable G) (s₀ : W) (hV : USlotDefinable V) : UTrDefinable fun (e : Env L) (f : Q → e.α) (g : W → e.α) => Function.update (G e f g) s₀ (V e f g)

Updating one track slot.

theorem DescriptiveComplexity.Draw.UStDefinable.ite {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] {F F' : (e : Env L) → (Q → e.α) → (W → e.α) → Q → e.α} {p : Prop} [Decidable p] (h : UStDefinable F) (h' : UStDefinable F') : UStDefinable fun (e : Env L) (f : Q → e.α) (g : W → e.α) => if p then F e f g else F' e f g

A pointer written by cases, the cases being decided by the kit.

The payload statements the interpretation reads

def DescriptiveComplexity.Draw.UPayloadDefinable {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] (F : (e : Env L) → (Fin (Fintype.card (Q ⊕ W)) → e.α) → Fin (Fintype.card (Q ⊕ W)) → e.α) : Prop

A payload transformation is definable: one formula over the input and the output coordinates defines its graph.

Equations

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

theorem DescriptiveComplexity.Draw.uPayloadDefinable_stPl {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] {F : (e : Env L) → (Q → e.α) → (W → e.α) → Q → e.α} (h : UStDefinable F) : UPayloadDefinable fun (e : Env L) (w : Fin (Fintype.card (Q ⊕ W)) → e.α) => stPl e.zero (F e (fun (q : Q) => unslot w (Sum.inl q)) fun (s : W) => unslot w (Sum.inr s))

A definable pointer is a definable destination payload. The control slots are what the rule computes and the track slots are cleared.

theorem DescriptiveComplexity.Draw.uPayloadDefinable_syPl {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] {G : (e : Env L) → (Q → e.α) → (W → e.α) → W → e.α} (h : UTrDefinable G) : UPayloadDefinable fun (e : Env L) (w : Fin (Fintype.card (Q ⊕ W)) → e.α) => syPl e.zero (G e (fun (q : Q) => unslot w (Sum.inl q)) fun (s : W) => unslot w (Sum.inr s))

A definable track family is a definable written payload.

The direction, written as a literal

The shape of most of the program's rules