The file of the register channel, laid out

DescriptiveComplexity.Draw.Data.diagLaid reads the segment channel's ruler as a DescriptiveComplexity.Draw.LaidFile: one register per element of the universe, in the universe's own order, each naming its own tag's block and its own tuple. This file does the same for the register channel, whose file has one register per element the channel writes for.

Everything the evaluation asks of a layout is the elementwise one's, restricted:

• a register is an element, so the block and the named coordinates spell it (nameSep_regLaid);
• every block and named tuple has a register, provided the reduction writes for the argument elements – which is what it does, and what makes its file lie in the working region (hasName_regLaid);
• the registers grow with the elements (wmSetLt_wmRegSeg), which is the one property the singleton channel could not give.

@[reducible, inline]

abbrev DescriptiveComplexity.Draw.Data.RegIx {L : FirstOrder.Language} (dt : Data L) {A R' P' : Type} [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] : Type

The index of the register channel's file: the elements it writes for.

Equations

• dt.RegIx = { x : DescriptiveComplexity.Draw.Univ A R' P' dt.KIx dt.dd // DescriptiveComplexity.WMHasInp x }

noncomputable def DescriptiveComplexity.Draw.Data.regLaid {L : FirstOrder.Language} {dt : Data L} {A R' P' : Type} [LinearOrder A] [LinearOrder R'] [LinearOrder P'] [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] [Finite A] [Finite R'] [Finite P'] [Finite dt.KIx] (h : IsLinOrd WMLe) (hord : ∀ (x y : Univ A R' P' dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) : LaidFile dt A R' P' dt.RegIx

The register channel's file, laid out: one register per element the channel writes for, in the universe's own order, each naming its own tag's block and its own tuple.

Equations

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

theorem DescriptiveComplexity.Draw.Data.hasName_regLaid {L : FirstOrder.Language} {dt : Data L} {A R' P' : Type} [LinearOrder A] [LinearOrder R'] [LinearOrder P'] [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] [Finite A] [Finite R'] [Finite P'] [Finite dt.KIx] {h : IsLinOrd WMLe} {hord : ∀ (x y : Univ A R' P' dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y} (zero : A) (harg : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), WMHasInp (Tag.arg (toLex b), padTup zero c)) : (regLaid h hord).toLayout.HasName zero

The file has a register for every name, provided the channel writes for the argument elements: a register is an element, and a name is one of them. This is the one thing the reduction has to arrange about its channel, and arranging it is what puts the file in the working region – the argument tags are the greatest (DescriptiveComplexity.Draw.lt_arg).

The coherences the evaluation asks of a file

theorem DescriptiveComplexity.Draw.Data.elt_reg_regLaid {L : FirstOrder.Language} {dt : Data L} {A R' P' : Type} [LinearOrder A] [LinearOrder R'] [LinearOrder P'] [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] [Finite A] [Finite R'] [Finite P'] [Finite dt.KIx] {h : IsLinOrd WMLe} {hord : ∀ (x y : Univ A R' P' dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y} (zero : A) (harg : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), WMHasInp (Tag.arg (toLex b), padTup zero c)) (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A) : ↑((regLaid h hord).toLayout.reg ⋯ b c) = dt.blkElt b (pad zero c)

A named register stands for the element it names: the heltP coherence.

What the file costs to walk

noncomputable def DescriptiveComplexity.Draw.Data.regBound {L : FirstOrder.Language} (dt : Data L) {A R' P' : Type} [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] : ℕ

The number the register channel's walks are charged against: 2 ^ the number of registers, which is the size of the working region and the bound every address of the file is under.

Equations

• dt.regBound = 2 ^ Nat.card dt.RegIx

noncomputable def DescriptiveComplexity.Draw.Data.regW {L : FirstOrder.Language} (dt : Data L) {A R' P' : Type} [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] : ℕ

The width a walk to a register is charged: twice the bound, plus two.

Equations

• dt.regW = 2 * dt.regBound + 2

noncomputable def DescriptiveComplexity.Draw.Data.regWP {L : FirstOrder.Language} (dt : Data L) {A R' P' : Type} [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] : ℕ

The width of the pass over the whole file: the file's two ends, the walk between them at one bound a step, and the marker's own address.

Equations

• dt.regWP = 2 * dt.regBound + Nat.card dt.RegIx * dt.regBound + 3

noncomputable def DescriptiveComplexity.Draw.Data.regWR {L : FirstOrder.Language} (dt : Data L) {A R' P' : Type} [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] : ℕ

The width of a read below the file: an address under the first register is under the bound.

Equations

• dt.regWR = dt.regBound + 4

noncomputable def DescriptiveComplexity.Draw.Data.regWK {L : FirstOrder.Language} (dt : Data L) {A R' P' : Type} [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] : ℕ

The width of a stage's inner loop: a pass per bit of the address it carries, each pass priced as regWP.

Equations

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

The file's two ends