The order key a reduction writes is the block-major one

The address layer of a wide machine reads an address over a universe T × V ordered by DescriptiveComplexity.lexRel – block index first, coordinate second (DescriptiveComplexity.Problems.Wide.Blocks). A reduction's universe is a tagged tuple Tag × (Fin d → A), and the only order on it that a first-order interpretation can define is the one the library already has, DescriptiveComplexity.tagTupleLe, whose defining formula is DescriptiveComplexity.lexLeF.

They are the same order:

DescriptiveComplexity.Wide.tagTupleLe_iff_lexRel – the definable order on a tagged tuple universe is lexRel of the tag order and the lexicographic order on coordinates.

So a reduction writes DescriptiveComplexity.lexLeF for wmLe, takes its tag type to be Fin n – one index per variable of its kernel, plus the scratch – and the whole of Blocks, Bridge and the fold applies to the instance it has drawn. This is the last thing that has to be checked before a program is written: it is what makes the layout definable rather than merely convenient.

The two linearity facts come with it, since every lemma of the address layer asks for them: DescriptiveComplexity.Wide.isLinOrd_tagTupleLe, transported from the LinearOrder the library builds by DescriptiveComplexity.tagTupleOrder, and DescriptiveComplexity.Wide.isLinOrd_tupLeLex, which is the same statement with no tag at all.

theorem DescriptiveComplexity.Wide.isLinOrd_tagTupleLe {Tag : Type} [LinearOrder Tag] {d : ℕ} {A : Type} [LinearOrder A] : IsLinOrd tagTupleLe

The lexicographic order on tagged tuples is a linear order, as a plain relation: transported from DescriptiveComplexity.tagTupleOrder, which is the same comparison read as a LinearOrder.

theorem DescriptiveComplexity.Wide.isLinOrd_tupLeLex {d : ℕ} {A : Type} [LinearOrder A] : IsLinOrd tupLeLex

The lexicographic order on tuples is a linear order: the previous statement with a single tag.

theorem DescriptiveComplexity.Wide.tagTupleLe_iff_lexRel {Tag : Type} [LinearOrder Tag] {d : ℕ} {A : Type} [LinearOrder A] (p q : Tag × (Fin d → A)) : tagTupleLe p q ↔ lexRel (fun (x1 x2 : Tag) => x1 ≤ x2) tupLeLex p q

The definable order on a tagged tuple universe is the block-major order. A reduction's wmLe is DescriptiveComplexity.lexLeF, whose meaning is DescriptiveComplexity.tagTupleLe; the address layer of a wide machine reads DescriptiveComplexity.lexRel; and this says the two agree, so an address over the universe the reduction draws decomposes into one block per tag.

The index a clocked program lays its file out by

A program with no clock gives every element of the universe a register; a clocked one cannot, since the only stretches it can walk are a fixed number of tuple roll-overs long and the universe is |Tag| of those. What it can afford is one register per block and tuple, which is also all that a register's contents ever depend on. Its order is the lexicographic product of the block order and the tuples' (DescriptiveComplexity.lexRel), and the block order is written down rather than borrowed: it has to be the one under which a block's tag is monotone, so that a mark on the file counts in the same order as the address it stands for (DescriptiveComplexity.ixAddr).

@[reducible, inline]

abbrev DescriptiveComplexity.Wide.BlkIx (K A : Type) (dd : ℕ) : Type

The index of the file a clocked program lays out: a block of the argument inventory – or none, for the registers that belong to no block – and a tuple of the instance.

Equations

• DescriptiveComplexity.Wide.BlkIx K A dd = (Option K × (Fin dd → A))

def DescriptiveComplexity.Wide.blkTagLe (K : Type) [LinearOrder K] : Option K → Option K → Prop

The order of the blocks: the blockless registers first, then the blocks in their own order. Which order this is matters: it is the one under which the tag of a block (DescriptiveComplexity.blkTag) is monotone, so that the marks a program keeps on its file count in the same order as the addresses they stand for (DescriptiveComplexity.ixAddr). It is a relation and not an instance, because Option carries an order of its own and two paths to one notation are worse than none.

Equations

• DescriptiveComplexity.Wide.blkTagLe K none x✝ = True
• DescriptiveComplexity.Wide.blkTagLe K (some val) none = False
• DescriptiveComplexity.Wide.blkTagLe K (some k) (some k') = (k ≤ k')

theorem DescriptiveComplexity.Wide.isLinOrd_blkTagLe (K : Type) [LinearOrder K] : IsLinOrd (blkTagLe K)

The block order is linear.

noncomputable def DescriptiveComplexity.Wide.blkLe (K A : Type) [LinearOrder K] [LinearOrder A] (dd : ℕ) : BlkIx K A dd → BlkIx K A dd → Prop

The order the registers are laid out in: block-major, then the tuple's own lexicographic order.

Equations

• DescriptiveComplexity.Wide.blkLe K A dd = DescriptiveComplexity.lexRel (DescriptiveComplexity.Wide.blkTagLe K) DescriptiveComplexity.tupLeLex

theorem DescriptiveComplexity.Wide.isLinOrd_blkLe (K A : Type) [LinearOrder K] [LinearOrder A] (dd : ℕ) : IsLinOrd (blkLe K A dd)

The layout order is linear, by the same lemma the universe's own order is proved from.

theorem DescriptiveComplexity.Wide.card_blkIx (K A : Type) [Finite K] (dd : ℕ) : Nat.card (BlkIx K A dd) = (Nat.card K + 1) * Nat.card (Fin dd → A)

How many registers the file has: one per block, one more for the blockless ones, times the tuples.