The cell of an encoded tuple: what one leaf read reads

Every atom subroutine of the EXPSPACE program bottoms out in the same operation: ask one membership question of the block value held in an argument block of a register. The machine asks it by scanning to a cell – the register cell of the element whose tag is that block and whose coordinates spell the tuple – and reading the register's track there. This file is the joint between the two descriptions:

• DescriptiveComplexity.Draw.Data.blkElt – the element an encoded tuple is, in a given argument block, and encCoord – its coordinates, computed from the control's slots (the cf of DescriptiveComplexity.Draw.Data.nameGF);
• DescriptiveComplexity.Draw.Data.encG_iff – the leaf read's guard holds at exactly that cell, which is what a navigation-by-name scan needs of its stopping condition, and what makes the trip's arrival known;
• DescriptiveComplexity.Draw.Data.blk_encAsgTup_iff and blk_encTagTup_iff – the digit found there: at a block holding the encoding of a point, a member tuple's question is one bit of the point's assignment – with no tag to match, the member codes carrying none – and a tag witness's question is the point's tag test (DescriptiveComplexity.Draw.mem_encPt_asg, mem_encPt_tag).

What makes the scans stop at the encodings' cells at all is that an encoded tuple is canonically padded (encTup_isPad): the layout inhabits the first dd₀ coordinates only, which is the budget DescriptiveComplexity.Draw.Data.lyLt fixes.

The same padding is what carries all of this to a coarse file, where a register is not an element: DescriptiveComplexity.Draw.Data.ixEncG_iff says the read stops at the register the layout names by the encoded tuple's coordinates, and elt_reg_encCoord says that register's address is the cell the elementwise read would have gone to.

The element an encoded tuple is

def DescriptiveComplexity.Draw.Data.blkElt {L : FirstOrder.Language} (dt : Data L) {A R' P' : Type} (b : Fin dt.ko ⊕ Fin dt.ki) (v : Fin dt.dd → A) : Univ A R' P' dt.KIx dt.dd

The cell of a tuple in an argument block: the block's tag with the tuple as its coordinates. Reading a register's track at this cell is asking whether the tuple belongs to the block value the register holds.

Equations

• dt.blkElt b v = (DescriptiveComplexity.Draw.Tag.arg (toLex b), v)

@[simp]

theorem DescriptiveComplexity.Draw.Data.tagBlk_blkElt {L : FirstOrder.Language} (dt : Data L) {A R' P' : Type} (b : Fin dt.ko ⊕ Fin dt.ki) (v : Fin dt.dd → A) : tagBlk (dt.blkElt b v).1 = some b

@[simp]

theorem DescriptiveComplexity.Draw.Data.blkElt_coord {L : FirstOrder.Language} (dt : Data L) {A R' P' : Type} (b : Fin dt.ko ⊕ Fin dt.ki) (v : Fin dt.dd → A) (j : Fin dt.dd) : (dt.blkElt b v).2 j = v j

The coordinates of an encoded tuple

noncomputable def DescriptiveComplexity.Draw.Data.encCoord {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero one : A) {Q : Type} (c : PtCode dt.X) (pay : (Q → A) → Fin (blockArityBound dt.X.B) → A) (fc : Q → A) (j : Fin dt.dd0) : A

The coordinates a leaf read compares against: the encoded tuple of a fixed discrete datum over a payload the control supplies, cut down to the name slots' width.

Equations

• dt.encCoord zero one c pay fc j = DescriptiveComplexity.Draw.encTup dt.ly zero one c (pay fc) (Fin.castLE ⋯ j)

theorem DescriptiveComplexity.Draw.Data.encTup_isPad {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} (c : PtCode dt.X) (pay : Fin (blockArityBound dt.X.B) → A) (j : Fin dt.dd) (hj : dt.dd0 ≤ ↑j) : encTup dt.ly zero one c pay j = zero

An encoded tuple is canonically padded. The layout puts its code and payload coordinates among the first dd₀, so beyond them the tuple carries the designated zero: encoded tuples live in the cells the marks name, which is what lets the machine scan to them.

theorem DescriptiveComplexity.Draw.Data.isPad_of_encMap {L : FirstOrder.Language} {dt : Data L} {A : Type} [LinearOrder A] {zero one : A} [L.Structure A] {p : dt.X.Map A} {v : Fin dt.dd → A} (h : encMap dt.ly zero one p v) (j : Fin dt.dd) (hj : dt.dd0 ≤ ↑j) : v j = zero

An encoding's members are canonically padded, so a block value that encodes a point is decided by the questions the machine can ask: the cells it can scan to are exactly the padded ones.

The cell the guard identifies

theorem DescriptiveComplexity.Draw.Data.encG_iff {L : FirstOrder.Language} {dt : Data L} {A R' P' : Type} [LinearOrder A] [LinearOrder R'] [LinearOrder P'] {zero one : A} {st : TapeStD dt A R' P'} (hzo : zero ≠ one) {cell : Univ A R' P' dt.KIx dt.dd → Univ A R' P' dt.KIx dt.dd → Prop} (hinj : Function.Injective cell) {Q : Type} (b : Fin dt.ko ⊕ Fin dt.ki) (c : PtCode dt.X) (pay : (Q → A) → Fin (blockArityBound dt.X.B) → A) (fc : Q → A) (u : Univ A R' P' dt.KIx dt.dd) : dt.nameGF one b (dt.encCoord zero one c pay) fc (dt.back cell zero one ⋯ st (cell u)) ↔ u = dt.blkElt b (encTup dt.ly zero one c (pay fc))

A leaf read stops at exactly the encoded tuple's cell. The guard of the trip – the block one-hot, the padding mark and the name slots against the coordinates the control computes – holds at a register cell precisely when that cell is the cell of the encoded tuple.

theorem DescriptiveComplexity.Draw.Data.nameG_iff {L : FirstOrder.Language} {dt : Data L} {A R' P' : Type} [LinearOrder A] [LinearOrder R'] [LinearOrder P'] {zero one : A} {st : TapeStD dt A R' P'} (hzo : zero ≠ one) {cell : Univ A R' P' dt.KIx dt.dd → Univ A R' P' dt.KIx dt.dd → Prop} (hinj : Function.Injective cell) {Q : Type} (b : Fin dt.ko ⊕ Fin dt.ki) (coord : Fin dt.dd0 → Q) (fc : Q → A) (u : Univ A R' P' dt.KIx dt.dd) : dt.nameG one b coord fc (dt.back cell zero one ⋯ st (cell u)) ↔ u = dt.blkElt b (pad zero fun (j : Fin dt.dd0) => fc (coord j))

A coordinate-loop trip stops at exactly the padded cell of the tuple the control holds. The comparison and copy loops enumerate tuples of dd₀ coordinates and visit the canonically padded cell of each, in whichever block they are reading.

The register an encoded tuple is, at an arbitrary file

theorem DescriptiveComplexity.Draw.Data.ixEncG_iff {L : FirstOrder.Language} {dt : Data L} {A R' P' : Type} {zero one : A} {I : Type} {lay : Layout dt A R' P' I} {stI : TapeSt dt A R' P' I} (hzo : zero ≠ one) (hinj : Function.Injective lay.cell) (hsep : lay.NameSep zero ⋯) (hhas : lay.HasName zero) {Q : Type} (b : Fin dt.ko ⊕ Fin dt.ki) (c : PtCode dt.X) (pay : (Q → A) → Fin (blockArityBound dt.X.B) → A) (fc : Q → A) (u : I) : dt.nameGF one b (dt.encCoord zero one c pay) fc (dt.ixBack lay zero one ⋯ stI (lay.cell u)) ↔ u = lay.reg hhas b (dt.encCoord zero one c pay fc)

A leaf read at a coarse file stops at exactly one register: the one the layout names by the encoded tuple's coordinates. The elementwise DescriptiveComplexity.Draw.Data.encG_iff read at a file whose registers are not elements – the trips of an expansion atom ask which register they stopped at, and the answer is a name the layout knows.

theorem DescriptiveComplexity.Draw.Data.pad_encCoord {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} {Q : Type} (c : PtCode dt.X) (pay : (Q → A) → Fin (blockArityBound dt.X.B) → A) (fc : Q → A) : pad zero (dt.encCoord zero one c pay fc) = encTup dt.ly zero one c (pay fc)

The coordinates of an encoded tuple are the tuple, cut down: what the control computes for a leaf read is the payload the layout stores, so padding it back gives the encoded tuple itself.

theorem DescriptiveComplexity.Draw.Data.elt_reg_encCoord {L : FirstOrder.Language} {dt : Data L} {A R' P' : Type} {zero one : A} {I : Type} {lay : Layout dt A R' P' I} {elt : I → Univ A R' P' dt.KIx dt.dd} (hhas : lay.HasName zero) (helt : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (w : Fin dt.dd0 → A), elt (lay.reg hhas b w) = dt.blkElt b (pad zero w)) {Q : Type} (b : Fin dt.ko ⊕ Fin dt.ki) (c : PtCode dt.X) (pay : (Q → A) → Fin (blockArityBound dt.X.B) → A) (fc : Q → A) : elt (lay.reg hhas b (dt.encCoord zero one c pay fc)) = dt.blkElt b (encTup dt.ly zero one c (pay fc))

The register a leaf read names holds the encoded tuple: with the file's names coherent with the encoding, the address of that register is the elementwise cell the same read would have gone to. This is the one place the coarse file and the encoding have to agree, and DescriptiveComplexity.Draw.Data.pad_encCoord is why they do.

What the trip finds there

theorem DescriptiveComplexity.Draw.Data.regBit_blkElt {L : FirstOrder.Language} {dt : Data L} {A R' P' : Type} [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] [Finite A] [Finite R'] [Finite P'] [Finite dt.KIx] (hlin : IsLinOrd WMLe) (m : Univ A R' P' dt.KIx dt.dd → Prop) (b : Fin dt.ko ⊕ Fin dt.ki) (v : Fin dt.dd → A) : regBit m (wmSeg (dt.blkElt b v)) ↔ wmBlk m (Tag.arg (toLex b)) v

A register's digit at the cell of a tuple is the block value's membership question: the track holds a bit per element, and the elements of one argument block are that block's tuples.

theorem DescriptiveComplexity.Draw.Data.blk_encAsgTup_iff {L : FirstOrder.Language} {dt : Data L} {A R' P' : Type} [LinearOrder A] {zero one : A} [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] [Finite A] [Finite R'] [Finite P'] [Finite dt.KIx] [L.Structure A] (hzo : zero ≠ one) (hlin : IsLinOrd WMLe) {m : Univ A R' P' dt.KIx dt.dd → Prop} {b : Fin dt.ko ⊕ Fin dt.ki} {p : dt.X.Map A} (hp : wmBlk m (Tag.arg (toLex b)) = encMap dt.ly zero one p) (i : dt.X.B.ι) (w : Fin (dt.X.B.arity i) → A) : regBit m (wmSeg (dt.blkElt b (encAsgTup dt.ly zero one i w))) ↔ (↑p).2 i w

One leaf read is one bit of the assignment: at a block holding the encoding of a point, the register's digit at a member tuple's cell says that the point carries the tuple's tag and its assignment holds of the payload. This is DescriptiveComplexity.Draw.mem_encPt_asg with the machine's cell in place of the membership question.

theorem DescriptiveComplexity.Draw.Data.blk_encTagTup_iff {L : FirstOrder.Language} {dt : Data L} {A R' P' : Type} [LinearOrder A] {zero one : A} [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] [Finite A] [Finite R'] [Finite P'] [Finite dt.KIx] [L.Structure A] (hzo : zero ≠ one) (hlin : IsLinOrd WMLe) {m : Univ A R' P' dt.KIx dt.dd → Prop} {b : Fin dt.ko ⊕ Fin dt.ki} {p : dt.X.Map A} (hp : wmBlk m (Tag.arg (toLex b)) = encMap dt.ly zero one p) (t : dt.X.Tag) : regBit m (wmSeg (dt.blkElt b (encTagTup dt.ly zero one t))) ↔ (↑p).1 = t

A tag witness's question is the point's tag test.