The names a trip walks to are definable

Every trip of the program is aimed by a naming guard: this cell is the canonically padded cell of the element whose block is b and whose first dd₀ coordinates spell a given tuple. The coordinate loops spell it from the control directly (DescriptiveComplexity.Draw.Data.nameG); the leaf reads of the element loops spell an encoded tuple (DescriptiveComplexity.Draw.Data.encCoord), and this file says that is a naming guard the interpretation can write down too.

The reason is the layout, not the data: at each coordinate an encoded tuple holds a component of the one-hot code – one of the two designated elements – or a payload position, or the clear element, and which it holds is decided by DescriptiveComplexity.Draw.EncLayout when the formula is built. So an encoded coordinate is DescriptiveComplexity.Draw.UReadable as soon as the payload is, and every payload the program spells is a control slot or the clear element.

An encoded coordinate

theorem DescriptiveComplexity.Draw.Data.uReadable_encTup {L : FirstOrder.Language} {dt : Data L} {Q : Type} [Fintype Q] [Fintype dt.SlotIx] {c : PtCode dt.X} {pay : (e : Env L) → (Q → e.α) → Fin (blockArityBound dt.X.B) → e.α} (hpay : ∀ (p : Fin (blockArityBound dt.X.B)), UReadable fun (e : Env L) (f : Q → e.α) (x : dt.SlotIx → e.α) => pay e f p) (k : Fin dt.dd) : UReadable fun (e : Env L) (f : Q → e.α) (x : dt.SlotIx → e.α) => encTup dt.ly e.zero e.one c (pay e f) k

A coordinate of an encoded tuple is readable: the code coordinates hold a designated element, the payload coordinates the payload, the rest the clear element – three cases the layout decides, not the data.

theorem DescriptiveComplexity.Draw.Data.uReadable_encCoord {L : FirstOrder.Language} {dt : Data L} {Q : Type} [Fintype Q] [Fintype dt.SlotIx] (c : PtCode dt.X) {pay : (e : Env L) → (Q → e.α) → Fin (blockArityBound dt.X.B) → e.α} (hpay : ∀ (p : Fin (blockArityBound dt.X.B)), UReadable fun (e : Env L) (f : Q → e.α) (x : dt.SlotIx → e.α) => pay e f p) (j : Fin dt.dd0) : UReadable fun (e : Env L) (f : Q → e.α) (x : dt.SlotIx → e.α) => dt.encCoord e.zero e.one c (pay e) f j

A name coordinate the control computes is readable.

The naming guard, from readable coordinates

theorem DescriptiveComplexity.Draw.Data.uGDefinable_nameGF_of_readable {L : FirstOrder.Language} {dt : Data L} {Q : Type} [Fintype Q] [Fintype dt.SlotIx] {b : Fin dt.ko ⊕ Fin dt.ki} {cf : (e : Env L) → (Q → e.α) → Fin dt.dd0 → e.α} (hcf : ∀ (j : Fin dt.dd0), UReadable fun (e : Env L) (f : Q → e.α) (x : dt.SlotIx → e.α) => cf e f j) : UGDefinable fun (e : Env L) (f : Q → e.α) (g : dt.SlotIx → e.α) => dt.nameGF e.one b (cf e) f g

A naming guard whose coordinates are readable is definable. This is DescriptiveComplexity.Draw.Data.uGDefinable_nameGF with its hypothesis in the form the encoded names supply it.

theorem DescriptiveComplexity.Draw.Data.uGDefinable_tagWitnessMatch {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] (b : Fin dt.ko ⊕ Fin dt.ki) (t : dt.X.Tag) : UGDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (g : dt.SlotIx → e.α) => dt.tagWitnessMatch e.zero e.one b t f g

A witness read's name is definable: the tag's encoded tuple, whose payload is the clear element throughout.

The payload a read leaf spells

theorem DescriptiveComplexity.Draw.Data.uReadable_pad_ctl {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {c : ℕ} {q : Fin c → dt.CtlIx} (p : Fin (blockArityBound dt.X.B)) : UReadable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => pad e.zero (fun (i : Fin c) => f (q i)) p

A padded payload of control slots is readable, position by position: below the arity a slot of the control, beyond it the clear element – and which is which the arity decides.

theorem DescriptiveComplexity.Draw.Data.uGDefinable_domMatch {L : FirstOrder.Language} [L.IsRelational] {dt : Data L} [Fintype dt.SlotIx] (b : Fin dt.ko ⊕ Fin dt.ki) (t : dt.X.Tag) (r : Fin (dt.domNr t)) (hn : (dt.domPk t).n ≤ dt.eDim) : UGDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (g : dt.SlotIx → e.α) => dt.domMatch e.zero e.one b t r hn f g

A domain read leaf's name is definable: its payload is the loop element at the levels the leaf's atom reads, padded.

The well-shapedness questions

The gates' file test asks of a cell that its name slots spell an encoded tuple: the witness of some tag, or a member of some relation variable. The first is a disjunction over a finite type of tags; the second quantifies a tuple of the instance, which no combinator covers – so the existential has to go, and the layout is what removes it. At a coordinate the encoding does not read from the payload the value is pinned; at one it does, the tuple is free, and a witness can be read straight off the cell.

def DescriptiveComplexity.Draw.Data.PayCoord {L : FirstOrder.Language} (dt : Data L) (i : dt.X.B.ι) (j : Fin dt.dd0) : Prop

A name coordinate the payload reaches: the encoded tuple is free there, so a well-shapedness test must not ask anything of it.

Equations

• dt.PayCoord i j = ∃ (p : Fin (DescriptiveComplexity.blockArityBound dt.X.B)), ↑p < dt.X.B.arity i ∧ dt.ly.pIx p = Fin.castLE ⋯ j

theorem DescriptiveComplexity.Draw.Data.encAsgTup_congr_of_not_payCoord {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} {i : dt.X.B.ι} {j : Fin dt.dd0} (h : ¬dt.PayCoord i j) (w w' : Fin (dt.X.B.arity i) → A) : encAsgTup dt.ly zero one i w (Fin.castLE ⋯ j) = encAsgTup dt.ly zero one i w' (Fin.castLE ⋯ j)

Away from the payload the encoded tuple does not depend on it.

theorem DescriptiveComplexity.Draw.Data.uGDefinable_exists_encAsgTup {L : FirstOrder.Language} {dt : Data L} {Q : Type} [Fintype Q] [Fintype dt.SlotIx] (i : dt.X.B.ι) : UGDefinable fun (e : Env L) (x : Q → e.α) (g : dt.SlotIx → e.α) => ∃ (w : Fin (dt.X.B.arity i) → e.α), ∀ (j : Fin dt.dd0), g (Slot.name j) = encAsgTup dt.ly e.zero e.one i w (Fin.castLE ⋯ j)

A member of a relation variable is a definable question of the cell: the payload coordinates carry no condition – a witness is read off the cell there – and every other coordinate is pinned by the code and the padding.

theorem DescriptiveComplexity.Draw.Data.uGDefinable_eq_encTagTup {L : FirstOrder.Language} {dt : Data L} {Q : Type} [Fintype Q] [Fintype dt.SlotIx] (t : dt.X.Tag) (j : Fin dt.dd0) : UGDefinable fun (e : Env L) (x : Q → e.α) (g : dt.SlotIx → e.α) => g (Slot.name j) = encTagTup dt.ly e.zero e.one t (Fin.castLE ⋯ j)

The tag witness is a definable question of the cell.

theorem DescriptiveComplexity.Draw.Data.uGDefinable_wellShapedG {L : FirstOrder.Language} {dt : Data L} {Q : Type} [Fintype Q] [Fintype dt.SlotIx] (b : Fin dt.ko ⊕ Fin dt.ki) : UGDefinable fun (e : Env L) (x : Q → e.α) (g : dt.SlotIx → e.α) => dt.wellShapedG e.zero e.one b g

A gate's well-shapedness question is definable.

theorem DescriptiveComplexity.Draw.Data.uGDefinable_wellShapedIG {L : FirstOrder.Language} {dt : Data L} {Q : Type} [Fintype Q] [Fintype dt.SlotIx] (b : Fin dt.ko ⊕ Fin dt.ki) : UGDefinable fun (e : Env L) (x : Q → e.α) (g : dt.SlotIx → e.α) => dt.wellShapedIG e.zero e.one b g

And so is an inner gate's, the digit read off the VAL register.

The leaf of a domain sentence

theorem DescriptiveComplexity.Draw.Data.uGDefinable_domLeafVal {L : FirstOrder.Language} [L.IsRelational] {dt : Data L} [Fintype dt.SlotIx] (t : dt.X.Tag) (hn : (dt.domPk t).n ≤ dt.eDim) (hrd : dt.domNr t ≤ dt.nfDim) : UGDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => dt.domLeafVal e.one t hn hrd f

The value of a domain sentence's matrix from the control is definable: its block atoms are read flags, and its other atoms are the questions a guard may ask of the instance – an equality, an order comparison, a relation of the source vocabulary – at the loop element.