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

@[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_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)