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

theorem DescriptiveComplexity.Draw.elim_unslot {Q W : Type} [Fintype Q] [Fintype W] {A : Type} (w : Fin (Fintype.card (Q ⊕ W)) → A) (d : Q ⊕ W) : Sum.elim (fun (q : Q) => unslot w (Sum.inl q)) (fun (s : W) => unslot w (Sum.inr s)) d = w (slotIx d)

The two halves of a rule's data, put back together, is the data.

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.

theorem DescriptiveComplexity.Draw.uGDefinable_slotOne {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] (d : Q ⊕ W) : UGDefinable fun (e : Env L) (f : Q → e.α) (g : W → e.α) => Sum.elim f g d = e.one

theorem DescriptiveComplexity.Draw.uGDefinable_slotZero {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] (d : Q ⊕ W) : UGDefinable fun (e : Env L) (f : Q → e.α) (g : W → e.α) => Sum.elim f g d = e.zero

theorem DescriptiveComplexity.Draw.uGDefinable_slotEq {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] (d d' : Q ⊕ W) : UGDefinable fun (x : Env L) (f : Q → x.α) (g : W → x.α) => Sum.elim f g d = Sum.elim f g d'

theorem DescriptiveComplexity.Draw.uGDefinable_slotLe {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] (d d' : Q ⊕ W) : UGDefinable fun (x : Env L) (f : Q → x.α) (g : W → x.α) => Sum.elim f g d ≤ Sum.elim f g d'

One slot is at most another.

theorem DescriptiveComplexity.Draw.uGDefinable_slotRel {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] {m : ℕ} (r : L.Relations m) (ts : Fin m → Q ⊕ W) : UGDefinable fun (e : Env L) (f : Q → e.α) (g : W → e.α) => FirstOrder.Language.Structure.RelMap r fun (j : Fin m) => Sum.elim f g (ts j)

A relation of the source vocabulary, of a tuple of slots: the one thing a guard asks of the instance itself, and the reason a guard is a formula rather than a reading of the equality pattern.

theorem DescriptiveComplexity.Draw.uGDefinable_ctlOne {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] (q : Q) : UGDefinable fun (e : Env L) (f : Q → e.α) (x : W → e.α) => f q = e.one

theorem DescriptiveComplexity.Draw.uGDefinable_ctlZero {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] (q : Q) : UGDefinable fun (e : Env L) (f : Q → e.α) (x : W → e.α) => f q = e.zero

theorem DescriptiveComplexity.Draw.uGDefinable_trkOne {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] (s : W) : UGDefinable fun (e : Env L) (x : Q → e.α) (g : W → e.α) => g s = e.one

theorem DescriptiveComplexity.Draw.uGDefinable_trkZero {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] (s : W) : UGDefinable fun (e : Env L) (x : Q → e.α) (g : W → e.α) => g s = e.zero

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

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

theorem DescriptiveComplexity.Draw.uGDefinable_mixEq {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] (q : Q) (s : W) : UGDefinable fun (x : Env L) (f : Q → x.α) (g : W → x.α) => f q = g s

theorem DescriptiveComplexity.Draw.uGDefinable_ctlLe {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] (q q' : Q) : UGDefinable fun (x : Env L) (f : Q → x.α) (x_1 : W → x.α) => f q ≤ f q'

theorem DescriptiveComplexity.Draw.uGDefinable_ctlRel {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] {m : ℕ} (r : L.Relations m) (ts : Fin m → Q) : UGDefinable fun (e : Env L) (f : Q → e.α) (x : W → e.α) => FirstOrder.Language.Structure.RelMap r fun (j : Fin m) => f (ts j)

theorem DescriptiveComplexity.Draw.uGDefinable_const {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] (p : Prop) : UGDefinable fun (x : Env L) (x_1 : Q → x.α) (x_2 : W → x.α) => p

A condition of the kit, not of the data: decided when the formula is built, so any Prop will do – the two ends among them.

theorem DescriptiveComplexity.Draw.uGDefinable_true {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] : UGDefinable fun (x : Env L) (x_1 : Q → x.α) (x_2 : W → x.α) => True

theorem DescriptiveComplexity.Draw.uGDefinable_false {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] : UGDefinable fun (x : Env L) (x_1 : Q → x.α) (x_2 : W → x.α) => False

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.not {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] {N : (e : Env L) → (Q → e.α) → (W → e.α) → Prop} (h : UGDefinable N) : UGDefinable fun (e : Env L) (f : Q → e.α) (g : W → e.α) => ¬N e f g

theorem DescriptiveComplexity.Draw.UGDefinable.imp {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.iff {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_forall {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] {ι : Type u_1} [Finite ι] {R : ι → (e : Env L) → (Q → e.α) → (W → e.α) → Prop} (h : ∀ (i : ι), UGDefinable (R i)) : UGDefinable fun (e : Env L) (f : Q → e.α) (g : W → e.α) => ∀ (i : ι), R i e f g

A conjunction over any finite index type – the shape a one-hot clause or a Match over a block of slots has.

theorem DescriptiveComplexity.Draw.uGDefinable_exists {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] {ι : Type u_1} [Finite ι] {R : ι → (e : Env L) → (Q → e.α) → (W → e.α) → Prop} (h : ∀ (i : ι), UGDefinable (R i)) : UGDefinable fun (e : Env L) (f : Q → e.α) (g : W → e.α) => ∃ (i : ι), R i e f g

And a disjunction over any finite index type.

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

theorem DescriptiveComplexity.Draw.uSlotDefinable_of_slotVal {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] (sv : SlotVal (Fintype.card (Q ⊕ W))) {V : (e : Env L) → (Q → e.α) → (W → e.α) → e.α} (hV : ∀ (e : Env L) (w : Fin (Fintype.card (Q ⊕ W)) → e.α), (V e (fun (q : Q) => unslot w (Sum.inl q)) fun (s : W) => unslot w (Sum.inr s)) = SlotVal.eval e.zero e.one w sv) : USlotDefinable V

A source names a written value: the three cases of DescriptiveComplexity.SlotVal, read at the payload coordinates.

theorem DescriptiveComplexity.Draw.uSlotDefinable_zero {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] : USlotDefinable fun (e : Env L) (x : Q → e.α) (x_1 : W → e.α) => e.zero

theorem DescriptiveComplexity.Draw.uSlotDefinable_one {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] : USlotDefinable fun (e : Env L) (x : Q → e.α) (x_1 : W → e.α) => e.one

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

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

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

The next element after a control slot – what advancing a loop variable writes, and the only source that reads the order.

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

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_bitVal {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] {N : (e : Env L) → (Q → e.α) → (W → e.α) → Prop} (h : UGDefinable N) : USlotDefinable fun (e : Env L) (f : Q → e.α) (g : W → e.α) => bitVal e.zero e.one (N e f g)

A bit is a written value: the two designated elements, chosen by a guard – so every DescriptiveComplexity.Draw.bitVal a rule writes is definable as soon as the question behind it is.

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_zero {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] : UReadable fun (e : Env L) (x : Q → e.α) (x_1 : W → e.α) => e.zero

theorem DescriptiveComplexity.Draw.uReadable_one {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] : UReadable fun (e : Env L) (x : Q → e.α) (x_1 : W → e.α) => e.one

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

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'

theorem DescriptiveComplexity.Draw.UReadable.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 : UReadable V) (h' : UReadable V') : UReadable 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.

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_of_slots {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.α} {V : Fin (Fintype.card (Q ⊕ W)) → (e : Env L) → (Q → e.α) → (W → e.α) → e.α} (hV : ∀ (k : Fin (Fintype.card (Q ⊕ W))), USlotDefinable (V k)) (hF : ∀ (e : Env L) (w : Fin (Fintype.card (Q ⊕ W)) → e.α) (k : Fin (Fintype.card (Q ⊕ W))), F e w k = V k e (fun (q : Q) => unslot w (Sum.inl q)) fun (s : W) => unslot w (Sum.inr s)) : UPayloadDefinable F

A payload is definable when each of its coordinates is, the coordinate formulas being conjoined at the output variables they name.

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

theorem DescriptiveComplexity.Draw.uRight_of_true {L : FirstOrder.Language} {Q W P : Type} {rl : (e : Env L) → Rule e.α Q W P} (h : ∀ (e : Env L), (rl e).moveRight) : ∃ (b : Bool), ∀ (e : Env L), (rl e).moveRight ↔ b = true

A rule that always moves right.

theorem DescriptiveComplexity.Draw.uRight_of_false {L : FirstOrder.Language} {Q W P : Type} {rl : (e : Env L) → Rule e.α Q W P} (h : ∀ (e : Env L), ¬(rl e).moveRight) : ∃ (b : Bool), ∀ (e : Env L), (rl e).moveRight ↔ b = true

And one that always moves left.

The shape of most of the program's rules

theorem DescriptiveComplexity.Draw.uRuleDefinable_of_keep {L : FirstOrder.Language} {Q W P : Type} [Fintype Q] [Fintype W] {rl : (e : Env L) → Rule e.α Q W P} (hst : (∃ (p : P), ∀ (e : Env L), (rl e).srcPh = p) ∧ (∃ (p : P), ∀ (e : Env L), (rl e).dstPh = p) ∧ ∃ (b : Bool), ∀ (e : Env L), (rl e).moveRight ↔ b = true) (hg : UGDefinable fun (e : Env L) => (rl e).guard) (hd : ∀ (e : Env L) (f : Q → e.α) (g : W → e.α), (rl e).dstSt f g = f) (hw : ∀ (e : Env L) (f : Q → e.α) (g : W → e.α), (rl e).wr f g = g) : URuleDefinable rl

A guard, with the pointer and the tracks riding along unchanged.

theorem DescriptiveComplexity.Draw.uRuleDefinable_of_keepSt {L : FirstOrder.Language} {Q W P : Type} [Fintype Q] [Fintype W] {rl : (e : Env L) → Rule e.α Q W P} (hst : (∃ (p : P), ∀ (e : Env L), (rl e).srcPh = p) ∧ (∃ (p : P), ∀ (e : Env L), (rl e).dstPh = p) ∧ ∃ (b : Bool), ∀ (e : Env L), (rl e).moveRight ↔ b = true) (hg : UGDefinable fun (e : Env L) => (rl e).guard) (hd : ∀ (e : Env L) (f : Q → e.α) (g : W → e.α), (rl e).dstSt f g = f) (hw : UTrDefinable fun (e : Env L) => (rl e).wr) : URuleDefinable rl

A rule that keeps its pointer, writing only its tracks.

theorem DescriptiveComplexity.Draw.uRuleDefinable_of_keepWr {L : FirstOrder.Language} {Q W P : Type} [Fintype Q] [Fintype W] {rl : (e : Env L) → Rule e.α Q W P} (hst : (∃ (p : P), ∀ (e : Env L), (rl e).srcPh = p) ∧ (∃ (p : P), ∀ (e : Env L), (rl e).dstPh = p) ∧ ∃ (b : Bool), ∀ (e : Env L), (rl e).moveRight ↔ b = true) (hg : UGDefinable fun (e : Env L) => (rl e).guard) (hd : UStDefinable fun (e : Env L) => (rl e).dstSt) (hw : ∀ (e : Env L) (f : Q → e.α) (g : W → e.α), (rl e).wr f g = g) : URuleDefinable rl

A rule that keeps its tracks, writing only its pointer – every checkpoint's dispatch.