The layout's geometry is the padding layer's, so its formulas are written

The bridge the defining formulas of the EXPSPACE reduction are read through. DescriptiveComplexity.Padding already carries the shape formulas every tagged-tuple interpretation in this library needs – a coordinate is the least element (DescriptiveComplexity.botF), a tuple is canonically padded (DescriptiveComplexity.canonF), two tuples are equal (DescriptiveComplexity.eqTupF), they agree below a length (DescriptiveComplexity.agreeF), one is the padded reading of the other through an index map (DescriptiveComplexity.padTupF) – each with its realization lemma. The EXPSPACE layout speaks of the same objects under its own names (DescriptiveComplexity.Draw.pad, DescriptiveComplexity.Draw.unpad, DescriptiveComplexity.Draw.IsPad), and this file says they are the same:

• DescriptiveComplexity.Draw.pad_eq_pad and DescriptiveComplexity.Draw.unpad_eq_pref – the two paddings and the two readings are one definition;
• DescriptiveComplexity.Draw.isPad_iff_canon – being canonically padded is being canonical, once the designated zero is the order's least element, which is the choice a reduction into DescriptiveComplexity.DWideAcceptSpace makes anyway (an interpretation cannot name an arbitrary element, and the two designated ones have to be ⊥ and ⊤);
• DescriptiveComplexity.Draw.realize_canonF_isPad and DescriptiveComplexity.Draw.realize_padTupF_pad – the two realizations in the layout's own vocabulary, which is the form the eleven defining formulas will cite.

So the shape half of the interpretation is already written. What is not, and what the remaining work is, is the rule half: a transition's guard and what it writes are arbitrary functions in DescriptiveComplexity.Draw.Rule, and each kit owes a syntactic counterpart – a quantifier-free formula over the payload slots for the guard, and per-slot “copy this slot or write this constant” for the destination and the written symbol.

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

The layout's padding is the padding layer's: one definition under two names.

theorem DescriptiveComplexity.Draw.unpad_eq_pref {A : Type} {c dd : ℕ} (hc : c ≤ dd) (v : Fin dd → A) : unpad hc v = pref hc v

And its reading back is the prefix.

theorem DescriptiveComplexity.Draw.isPad_iff_canon {A : Type} {c dd : ℕ} [PartialOrder A] {zero : A} (h₀ : IsBot zero) (v : Fin dd → A) : IsPad c zero v ↔ Canon c v

Being canonically padded is being canonical, once the designated element is a least one: IsBot and “equal to zero” are the same condition on a coordinate, by antisymmetry.

The two realizations, in the layout's own terms

theorem DescriptiveComplexity.Draw.realize_canonF_isPad {L : FirstOrder.Language} {A : Type} [L.Structure A] [LinearOrder A] {γ : Type} {dd : ℕ} {v : γ → A} {zero : A} (h₀ : IsBot zero) {c : ℕ} {x : Fin dd → γ} : (canonF c x).Realize v ↔ IsPad c zero fun (j : Fin dd) => v (x j)

A tuple of the interpreted universe is canonically padded, as a formula: DescriptiveComplexity.canonF read at the layout's IsPad, with the least element for zero. This is what the defining formula of a transition, of an accepting state and of the blank all begin with – the condition that gives an element one spelling, and so the emitted machine its determinism.

theorem DescriptiveComplexity.Draw.realize_padTupF_pad {L : FirstOrder.Language} {A : Type} [L.Structure A] [LinearOrder A] {γ : Type} {dd : ℕ} {v : γ → A} {zero : A} (h₀ : IsBot zero) {c : ℕ} (hc : c ≤ dd) {u x : Fin dd → γ} : (padTupF (fun (j : Fin c) => Fin.castLE hc j) u x).Realize v ↔ (fun (j : Fin dd) => v (x j)) = pad zero (unpad hc fun (j : Fin dd) => v (u j))

A tuple of the interpreted universe is a padded payload read off another one, as a formula: DescriptiveComplexity.padTupF at the layout's pad and unpad. This is the shape of Src, Dst, Read and Write – the tag of the target is decided when the formula is built, and what is left of each is that its coordinates are the padded reading of the transition's.