The call sites' kits, at the concrete slots

The kit instantiations of the EXPSPACE program: each call site of the program is one of the kit shapes of the layer, at the slot inventory of DescriptiveComplexity.Problems.Wide.DrawSlots. This file fixes the slots and guards; the phase embeddings stay parameters (each call site gets its own copy of the shape's phases in the program's phase sum), and so does the control location a name guard compares against (the Ctl sizing is fixed with the site enumeration, not here).

The register-file service slots are the same for every kit – reg the register mark, regLast the file-top mark (the greatest element's cell is the file's top), wk the working-cell marker – and the guards are exactly the slot conditions the kits' separation lemmas were built around.

Slot distinctness

The facts every discharge asks about the service slots, provable once: the walked registers, the register mark, the file-top mark and the marker are pairwise distinct constructors.

theorem DescriptiveComplexity.Draw.Data.mir_ne_reg {L : FirstOrder.Language} (dt : Data L) : Slot.mir ≠ Slot.reg

theorem DescriptiveComplexity.Draw.Data.tgt_ne_reg {L : FirstOrder.Language} (dt : Data L) : Slot.tgt ≠ Slot.reg

theorem DescriptiveComplexity.Draw.Data.regLast_ne_mir {L : FirstOrder.Language} (dt : Data L) : Slot.regLast ≠ Slot.mir

theorem DescriptiveComplexity.Draw.Data.regLast_ne_tgt {L : FirstOrder.Language} (dt : Data L) : Slot.regLast ≠ Slot.tgt

theorem DescriptiveComplexity.Draw.Data.wk_ne_mir {L : FirstOrder.Language} (dt : Data L) : Slot.wk ≠ Slot.mir

theorem DescriptiveComplexity.Draw.Data.wk_ne_tgt {L : FirstOrder.Language} (dt : Data L) : Slot.wk ≠ Slot.tgt

theorem DescriptiveComplexity.Draw.Data.tgt_ne_mir {L : FirstOrder.Language} (dt : Data L) : Slot.tgt ≠ Slot.mir

theorem DescriptiveComplexity.Draw.Data.ltp_ne_mir {L : FirstOrder.Language} (dt : Data L) : Slot.ltp ≠ Slot.mir

theorem DescriptiveComplexity.Draw.Data.bot_ne_mir {L : FirstOrder.Language} (dt : Data L) : Slot.bot ≠ Slot.mir

The plain sweeps: COMPARE and COPY

def DescriptiveComplexity.Draw.Data.compareKit {L : FirstOrder.Language} (dt : Data L) {A Q P : Type} (one : A) (emb : SweepPh → P) : FlagSweepKit A Q dt.SlotIx P

COMPARE's kit: one question per cell of the logical interval – every stage track agrees with its next.

Equations

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

def DescriptiveComplexity.Draw.Data.copyKit {L : FirstOrder.Language} (dt : Data L) {A Q P : Type} (ph : P) : WriteSweepKit A Q dt.SlotIx P

COPY's kit: every stage track takes its next's digit, the next stage riding along for the following round.

Equations

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

The register-file trips

def DescriptiveComplexity.Draw.Data.seekKit {L : FirstOrder.Language} (dt : Data L) {A Q P : Type} (emb : SeekPh → P) : SeekKit A Q dt.SlotIx P

The random access: MIRROR sought to TARGET, marker in tow.

Equations

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

def DescriptiveComplexity.Draw.Data.advKit {L : FirstOrder.Language} (dt : Data L) {A Q P : Type} (emb : AdvPh → P) : AdvKit A Q dt.SlotIx P

One round of the outer sweep: the working cell advances one address, MIRROR incremented in tow.

Equations

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

def DescriptiveComplexity.Draw.Data.clearMirKit {L : FirstOrder.Language} (dt : Data L) {A Q P : Type} (emb : TrackPh → P) : ClearKit A Q dt.SlotIx P

Clearing the MIRROR register, at a random access's reset.

Equations

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

def DescriptiveComplexity.Draw.Data.tgtTopKit {L : FirstOrder.Language} (dt : Data L) {A Q P : Type} (one : A) (emb : TrackPh → P) : MapKit A Q dt.SlotIx P

TARGET := the logical top: the pattern write of startup – the digit set exactly at the argument-tagged cells, read off the one-hot marks.

Equations

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

The navigation-by-name trips

def DescriptiveComplexity.Draw.Data.nameGF {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (one : A) (b : Fin dt.ko ⊕ Fin dt.ki) (cf : (Q → A) → Fin dt.dd0 → A) : (Q → A) → (dt.SlotIx → A) → Prop

The name guard, at computed coordinates: this cell is the canonically padded cell of the element whose block is b and whose first dd0 coordinates are the ones the control computes through cf. The trips of the coordinate loops read the control's slots directly (DescriptiveComplexity.Draw.Data.nameG); the leaf reads of the element loops compute an encoded tuple from them (DescriptiveComplexity.Problems.Wide.DrawName), and both are this guard.

Equations

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

def DescriptiveComplexity.Draw.Data.nameG {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (one : A) (b : Fin dt.ko ⊕ Fin dt.ki) (coord : Fin dt.dd0 → Q) : (Q → A) → (dt.SlotIx → A) → Prop

The name guard: this cell is the canonically padded cell of the element whose block is b and whose first dd0 coordinates the control holds at coord.

Equations

• dt.nameG one b coord = dt.nameGF one b fun (fc : Q → A) (j : Fin dt.dd0) => fc (coord j)