The evaluation's width is polynomial

The clock of the wide machines compares a product: the evaluation is charged a * b with a a width and b a number of rounds, and DescriptiveComplexity.Draw.Data.nexTotal_lt_two_pow' asks for each factor below 2 ^ (k * m). The rounds are bounded elsewhere: the VAL loop is an increment chain, injective into the subsets of the registers it is supported on. This file bounds the other factor, the width DescriptiveComplexity.Draw.Data.ixLegWidth times the number of spine positions.

Every layer's cost – an atom's, a matrix's, a gate block's, a round's, a variable's machinery's, a leg's – is built from the widths the legs are charged against and from the file's own numbers by addition and multiplication alone. So each is polynomial in a single bound q on all of them, and the bound proved here is q ^ 25: crude, and deliberately so, since what an instantiation has to show is q ^ 25 ≤ 2 ^ (k * m) with q polynomial in the drawn universe and m its size – room the exponent does not eat into.

The three combinators (add_le_pow, mul_le_pow, le_pow_of_le) are the whole method: a sum of two things below q ^ i is below q ^ (i + 1) because q is at least two, and a product adds the exponents. Written that way, each layer's bound is one line per node of its defining expression. The target exponent of a raised or constant bound is written explicitly, since neither the goal nor the argument determines it.

Bounding a polynomial by a power

theorem DescriptiveComplexity.Draw.add_le_pow {a b q i j k : ℕ} (hq : 2 ≤ q) (ha : a ≤ q ^ i) (hb : b ≤ q ^ j) (hi : i < k) (hj : j < k) : a + b ≤ q ^ k

A sum costs one exponent, both summands being below a power of a q that is at least two.

theorem DescriptiveComplexity.Draw.mul_le_pow {a b q i j k : ℕ} (hq : 1 ≤ q) (ha : a ≤ q ^ i) (hb : b ≤ q ^ j) (hk : i + j ≤ k) : a * b ≤ q ^ k

A product adds the exponents.

theorem DescriptiveComplexity.Draw.le_pow_one {a q : ℕ} (ha : a ≤ q) : a ≤ q ^ 1

A bound is a first power.

theorem DescriptiveComplexity.Draw.le_pow_of_le {a q i : ℕ} (k : ℕ) (hq : 1 ≤ q) (ha : a ≤ q ^ i) (hk : i ≤ k) : a ≤ q ^ k

Raising the exponent of a bound.

theorem DescriptiveComplexity.Draw.cst_le_pow {a q : ℕ} (k : ℕ) (hq : 16 ≤ q) (ha : a ≤ 16) (hk : 1 ≤ k) : a ≤ q ^ k

A constant of the program is below every positive power, the bound being at least sixteen and every constant written in these costs at most that.

The three shapes a layer of the tower is assembled in, stated over fresh naturals: the arithmetic is proved away from the machine's terms, as everything else in this budget pass is.

theorem DescriptiveComplexity.Draw.round_shape {q : ℕ} (hq16 : 16 ≤ q) {g m : ℕ} (hg : g ≤ q ^ 13) (hm : m ≤ q ^ 13) : 1 + g + 1 + 1 + 1 + m + 1 ≤ q ^ 19

The shape of a round of the VAL loop: two loops and five dispatches.

theorem DescriptiveComplexity.Draw.gates_shape {q : ℕ} (hq16 : 16 ≤ q) {g : ℕ} (hg : g ≤ q ^ 13) : 1 + g + 1 ≤ q ^ 15

The shape of a gates' leg: one loop between two dispatches.

theorem DescriptiveComplexity.Draw.varCD_shape {q : ℕ} (hq16 : 16 ≤ q) {vg rc p : ℕ} (hvg : vg ≤ q ^ 15) (hrc : rc ≤ q ^ 19) (hp : p ≤ q) : vg + rc + 3 * p + 6 + (2 * p + rc + 3) ≤ q ^ 23

The shape of a variable's machinery as one width: what it pays once, and what it pays per round of the VAL loop.

One bound for every number a leg's cost is built from

structure DescriptiveComplexity.Draw.Data.IxWidthBd {L : FirstOrder.Language} (dt : Data L) (A : Type) (w wP wR wK q : ℕ) : Prop

Every number the tower's costs are built from, below one bound. The four widths the legs are charged against (w for a walk to a named register, wP for a sweep of the file, wR for a reset, wK for a seek), the two enumerations an atom loops over, and the dimensions and arities of the data. The bound is asked to be at least sixteen so that the constants written into the costs – the thirteen dispatches of a stage atom, the largest of them – are below it too.

• cst : 16 ≤ q

  The bound dominates the constants the costs are written with.

• wLe : w ≤ q

  A walk to a named register.

• wPLe : wP ≤ q

  A sweep of the file.

• wRLe : wR ≤ q

  A reset.

• wKLe : wK ≤ q

  A seek.

• dd0Le : Nat.card (Lex (Fin dt.dd0 → A)) + 1 ≤ q

  The tuples an atom's comparison loops over.

• eDimLe : Nat.card (Lex (Fin dt.eDim → A)) + 1 ≤ q

  The tuples an expansion's leaf loops over.

• ntgLe : dt.ntgDim ≤ q

  The width of an expansion's tag walk.

• nfLe : dt.nfDim ≤ q

  The width of an expansion's leaf walk.

• natOfLe (vi : dt.VarIx) : dt.natOf vi ≤ q

  The number of atoms of a variable's matrix.

• nInLe (vi : dt.VarIx) : dt.nIn vi ≤ q

  The number of inner gates of a variable.

• arOfLe (vi : dt.VarIx) : dt.arOf vi ≤ q

  The number of outer gates of a variable.

• arityLe (iv : dt.d.B.ι) : dt.d.B.arity iv ≤ q

  The arity of a stage relation.

• nvLe : dt.nv ≤ q

  The number of positions of the spine.

The layers, bottom-up

theorem DescriptiveComplexity.Draw.Data.ixExpBody_le {L : FirstOrder.Language} {dt : Data L} {A : Type} {w wP wR wK q : ℕ} (h : dt.IxWidthBd A w wP wR wK q) : (w + 2) * dt.ntgDim + 2 + ((2 + (w + 2) * dt.nfDim) * (Nat.card (Lex (Fin dt.eDim → A)) + 1) + 1) ≤ q ^ 7

The read of an expansion is polynomial: the walk down the tags, then the loop over the leaf's tuples. It is the body of an exp atom and of a gate block alike.

theorem DescriptiveComplexity.Draw.Data.ixKindCost_le {L : FirstOrder.Language} {dt : Data L} {A : Type} {w wP wR wK q : ℕ} (h : dt.IxWidthBd A w wP wR wK q) (vi : dt.VarIx) (κ : MatAtom dt.X dt.d.B (dt.nOf vi)) : dt.ixKindCost A vi w wP wR wK κ ≤ q ^ 10

An atom's cost is polynomial, whatever its kind: a comparison, an expansion's read, or a stage atom's random access.

theorem DescriptiveComplexity.Draw.Data.ixMatCost_le {L : FirstOrder.Language} {dt : Data L} {A : Type} {w wP wR wK q : ℕ} (h : dt.IxWidthBd A w wP wR wK q) (vi : dt.VarIx) : dt.ixMatCost A vi w wP wR wK ≤ q ^ 10

A matrix's cost is polynomial: it is the largest of its atoms'.

theorem DescriptiveComplexity.Draw.Data.ixGateCost_le {L : FirstOrder.Language} {dt : Data L} {A : Type} {w wP wR wK q : ℕ} (h : dt.IxWidthBd A w wP wR wK q) : dt.ixGateCost A w wP ≤ q ^ 10

A gate block's cost is polynomial: a sweep of the file and an expansion's read.

theorem DescriptiveComplexity.Draw.Data.ixGateLoop_le {L : FirstOrder.Language} {dt : Data L} {A : Type} {w wP wR wK q : ℕ} (h : dt.IxWidthBd A w wP wR wK q) (n : ℕ) (hn : n ≤ q) : (dt.ixGateCost A w wP + 2) * n + 1 ≤ q ^ 13

A loop over a gate block is polynomial: what a variable's gates leg and a round of the VAL loop both pay, at their own number of gates.

theorem DescriptiveComplexity.Draw.Data.ixRoundCost_le {L : FirstOrder.Language} {dt : Data L} {A : Type} {w wP wR wK q : ℕ} (h : dt.IxWidthBd A w wP wR wK q) (vi : dt.VarIx) : dt.ixRoundCost A vi w wP wR wK ≤ q ^ 19

A round of the VAL loop is polynomial: the inner gates and the matrix, each looped over once.

theorem DescriptiveComplexity.Draw.Data.ixVarGatesCost_le {L : FirstOrder.Language} {dt : Data L} {A : Type} {w wP wR wK q : ℕ} (h : dt.IxWidthBd A w wP wR wK q) (vi : dt.VarIx) : dt.ixVarGatesCost A vi w wP ≤ q ^ 15

The gates' leg of a variable is polynomial.

theorem DescriptiveComplexity.Draw.Data.ixVarCD_le {L : FirstOrder.Language} {dt : Data L} {A : Type} {w wP wR wK q : ℕ} (h : dt.IxWidthBd A w wP wR wK q) (vi : dt.VarIx) : dt.ixVarCD A vi w wP wR wK ≤ q ^ 23

A variable's machinery, as one width, is polynomial.

theorem DescriptiveComplexity.Draw.Data.ixLegWidth_le {L : FirstOrder.Language} {dt : Data L} {A : Type} {w wP wR wK q : ℕ} (h : dt.IxWidthBd A w wP wR wK q) : dt.ixLegWidth A w wP wR wK * dt.nv ≤ q ^ 25

The width the clock is handed is polynomial in the file's own numbers: the spine's width, times its number of positions, is below q ^ 25 whenever q bounds the four walk widths, the two enumerations, and the data's dimensions and arities.

This is the first of the two factors the clocked evaluation is charged (DescriptiveComplexity.Draw.Data.ixSpineCost_le_mul); the second is the number of VAL rounds.

theorem DescriptiveComplexity.Draw.Data.ixEvalWidth_le {L : FirstOrder.Language} {dt : Data L} {A : Type} {w wP wR wK q : ℕ} (h : dt.IxWidthBd A w wP wR wK q) : dt.ixEvalWidth A w wP wR wK ≤ q ^ 26

The clocked evaluation's whole width is polynomial too: the spine's, the output machinery's and the four joining steps, all below q ^ 26. What an instantiation owes of the clock's first factor is therefore q ^ 26 ≤ 2 ^ (k · m), and of the second the number of VAL rounds.