Where the states, the symbols and the transitions sit

The instance the reduction emits has universe Draw.Tag R P K × (Fin dd → A), and its states, symbols and transitions are elements of it. This file says which elements they are.

The layout is the simplest one that works. A state, a symbol and a transition each carry a payload of c coordinates – c is the program's choice, and dd is at least c – and the coordinates beyond the payload hold a designated element. That padding is not decoration: without it an element would have n^(dd-c) spellings, and the machine's promises are that there is one start state, one blank, and at most one transition per state and symbol (DescriptiveComplexity.TMData.Deterministic). A canonical spelling is what makes those provable.

What distinguishes the three is the tag, which is also what carries everything about a transition except its data: its rule index. So

• a state is (phase p, pad w) – the call site in the tag, the pointer in w;
• a symbol is (sym, pad w) – the tracks in w (DrawTracks);
• a transition is (ctrl r, pad w) – the rule in the tag, its data in w.

Two elements with different tags are different, and two with the same tag differ exactly when their payloads do (DescriptiveComplexity.Draw.pad_injective). Those are the distinctness facts the well-formedness and determinism obligations are discharged from.

Canonical payloads

noncomputable def DescriptiveComplexity.Draw.pad {A : Type} {c dd : ℕ} (zero : A) (w : Fin c → A) : Fin dd → A

The canonical tuple carrying a payload: the payload in the first c coordinates, the designated element in the rest.

Equations

• DescriptiveComplexity.Draw.pad zero w j = if h : ↑j < c then w ⟨↑j, h⟩ else zero

def DescriptiveComplexity.Draw.unpad {A : Type} {c dd : ℕ} (hc : c ≤ dd) (v : Fin dd → A) : Fin c → A

Reading a payload back.

Equations

• DescriptiveComplexity.Draw.unpad hc v i = v ⟨↑i, ⋯⟩

def DescriptiveComplexity.Draw.IsPad {A : Type} {dd : ℕ} (c : ℕ) (zero : A) (v : Fin dd → A) : Prop

Being canonically padded: nothing but the designated element beyond the payload. This is the condition that gives an element one spelling, and so the machine's promises their uniqueness.

Equations

• DescriptiveComplexity.Draw.IsPad c zero v = ∀ (j : Fin dd), c ≤ ↑j → v j = zero

@[simp]

theorem DescriptiveComplexity.Draw.pad_of_lt {A : Type} {c dd : ℕ} {zero : A} {w : Fin c → A} (j : Fin dd) (h : ↑j < c) : pad zero w j = w ⟨↑j, h⟩

@[simp]

theorem DescriptiveComplexity.Draw.pad_of_ge {A : Type} {c dd : ℕ} {zero : A} {w : Fin c → A} (j : Fin dd) (h : c ≤ ↑j) : pad zero w j = zero

theorem DescriptiveComplexity.Draw.isPad_pad {A : Type} {c dd : ℕ} {zero : A} {w : Fin c → A} : IsPad c zero (pad zero w)

@[simp]

theorem DescriptiveComplexity.Draw.unpad_pad {A : Type} {c dd : ℕ} {zero : A} {w : Fin c → A} (hc : c ≤ dd) : unpad hc (pad zero w) = w

A payload reads back.

theorem DescriptiveComplexity.Draw.pad_unpad {A : Type} {c dd : ℕ} {zero : A} {v : Fin dd → A} (hc : c ≤ dd) (hv : IsPad c zero v) : pad zero (unpad hc v) = v

A canonically padded tuple is the padding of what it carries, so the two descriptions of an element – “it is pad of something” and “it is padded” – are the same.

theorem DescriptiveComplexity.Draw.pad_injective {A : Type} {c dd : ℕ} {zero : A} (hc : c ≤ dd) : Function.Injective (pad zero)

Distinct payloads give distinct tuples, which is where every uniqueness promise of the emitted machine comes from.

The three kinds of element

noncomputable def DescriptiveComplexity.Draw.stateElt {A : Type} {c dd : ℕ} {R P K : Type} (zero : A) (p : P) (w : Fin c → A) : Tag R P K × (Fin dd → A)

A state: the call site in the tag, the pointer in the payload.

Equations

• DescriptiveComplexity.Draw.stateElt zero p w = (DescriptiveComplexity.Draw.Tag.phase p, DescriptiveComplexity.Draw.pad zero w)

noncomputable def DescriptiveComplexity.Draw.symElt {A : Type} {c dd : ℕ} {R P K : Type} (zero : A) (w : Fin c → A) : Tag R P K × (Fin dd → A)

A symbol: the tracks in the payload.

Equations

• DescriptiveComplexity.Draw.symElt zero w = (DescriptiveComplexity.Draw.Tag.sym, DescriptiveComplexity.Draw.pad zero w)

noncomputable def DescriptiveComplexity.Draw.trElt {A : Type} {c dd : ℕ} {R P K : Type} (zero : A) (r : R) (w : Fin c → A) : Tag R P K × (Fin dd → A)

A transition: the rule in the tag, the rule's data in the payload.

Equations

• DescriptiveComplexity.Draw.trElt zero r w = (DescriptiveComplexity.Draw.Tag.ctrl r, DescriptiveComplexity.Draw.pad zero w)

theorem DescriptiveComplexity.Draw.stateElt_inj {A : Type} {c dd : ℕ} {zero : A} {R P K : Type} (hc : c ≤ dd) {p p' : P} {w w' : Fin c → A} (h : stateElt zero p w = stateElt zero p' w') : p = p' ∧ w = w'

A state is determined by its call site and its pointer.

theorem DescriptiveComplexity.Draw.symElt_inj {A : Type} {c dd : ℕ} {zero : A} {R P K : Type} (hc : c ≤ dd) {w w' : Fin c → A} (h : symElt zero w = symElt zero w') : w = w'

A symbol is determined by its tracks.