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

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.

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