An address, read block by block

A reduction into a wide machine chooses the order wmLe of the instance it draws, and the whole design of the sweep depends on choosing it block-major: the universe of the instance is a product T × V – a block index and a coordinate – ordered by DescriptiveComplexity.lexRel, so that an address is a family of blocks, one per index (DescriptiveComplexity.wmBlk). One block per variable of the kernel, one for the scratch, and the sweep's two structural facts become theorems about this decomposition:

• the address order is lexicographic on blocks (DescriptiveComplexity.wmSetLt_lexRel_iff): two addresses compare at the least index where their blocks differ. So the addresses agreeing on a prefix of the blocks form a contiguous stretch of the tape, which is what lets a guessed relation of arity smaller than the number of variables be kept consistent by one state bit rather than by comparing distant cells;
• the increment carries block by block (DescriptiveComplexity.wmIncr_lexRel_iff): there is a last index whose block is not full, that block increments, every later block is emptied and every earlier one is untouched. That is the roll-over information the sweep folds its accumulators by – “which variables have just been requantified” – and it is what a machine computes when it increments the mirror of its own head position.

A third fact comes from the same reading and is what a program on a clock lives on:

• the addresses avoiding a set of blocks are an initial stretch (DescriptiveComplexity.wmAvoids_of_wmSetLe), provided the set is closed downwards in the index order – the smallest index being the most significant digit. So a program that keeps its data in the least significant blocks and leaves the others empty never leaves a segment of the tape at the bottom, and the surplus blocks multiply its clock while costing it nothing.

All of them are stated at arbitrary linear order relations on T and on V, so they apply to whatever key a reduction chooses; DescriptiveComplexity.isLinOrd_lexRel supplies the linearity of the product.

The blocks of an address

def DescriptiveComplexity.wmBlk {T V : Type} (s : T × V → Prop) (τ : T) : V → Prop

The block of an address at an index: the coordinates the address holds there.

Equations

• DescriptiveComplexity.wmBlk s τ v = s (τ, v)

@[simp]

theorem DescriptiveComplexity.wmBlk_apply {T V : Type} (s : T × V → Prop) (τ : T) (v : V) : wmBlk s τ v ↔ s (τ, v)

theorem DescriptiveComplexity.wmLt_lexRel_iff {T V : Type} {LeT : T → T → Prop} {LeV : V → V → Prop} (hT : IsLinOrd LeT) (p q : T × V) : WMLt (lexRel LeT LeV) p q ↔ WMLt LeT p.1 q.1 ∨ p.1 = q.1 ∧ WMLt LeV p.2 q.2

The strict order of a block-major product: strictly earlier index, or the same index and a strictly earlier coordinate.

theorem DescriptiveComplexity.wmLt_same_iff {T V : Type} {LeT : T → T → Prop} {LeV : V → V → Prop} (hT : IsLinOrd LeT) (τ : T) (u w : V) : WMLt (lexRel LeT LeV) (τ, u) (τ, w) ↔ WMLt LeV u w

Inside one block, the order of the product is the order of the block.

theorem DescriptiveComplexity.pair_eq_iff {T V : Type} (τ : T) (u w : V) : (τ, w) = (τ, u) ↔ w = u

Two coordinates of the same block name the same element exactly when they are equal.

theorem DescriptiveComplexity.wmSetLt_lexRel_iff {T V : Type} {LeT : T → T → Prop} {LeV : V → V → Prop} (hT : IsLinOrd LeT) (s t : T × V → Prop) : WMSetLt (lexRel LeT LeV) s t ↔ ∃ (τ : T), (∀ (σ : T), WMLt LeT σ τ → ∀ (v : V), wmBlk s σ v ↔ wmBlk t σ v) ∧ WMSetLt LeV (wmBlk s τ) (wmBlk t τ)

The address order is lexicographic on blocks: two addresses compare at the least index where their blocks differ, and there by the order of that block. So the addresses agreeing on a prefix of the blocks are consecutive.

The working region

A program that keeps its data in the least significant blocks and leaves the others empty never leaves an initial stretch of the tape: the smallest block index is the most significant digit, so putting anything in a block a program avoids makes an address bigger than every address that avoids it. That is what buys a clocked program its budget – the surplus blocks multiply the clock and cost the program nothing – and what makes “the region” a segment rather than a scattered set.

def DescriptiveComplexity.wmAvoids {T V : Type} (H : T → Prop) (s : T × V → Prop) : Prop

An address avoids a set of block indices when its blocks there are empty.

Equations

• DescriptiveComplexity.wmAvoids H s = ∀ (τ : T), H τ → ∀ (v : V), ¬s (τ, v)

def DescriptiveComplexity.wmAvoidTop {T V : Type} (H : T → Prop) : T × V → Prop

The greatest address avoiding a set of blocks: full everywhere else.

Equations

• DescriptiveComplexity.wmAvoidTop H p = ¬H p.1

theorem DescriptiveComplexity.wmSetLe_wmAvoidTop {T V : Type} {LeT : T → T → Prop} {LeV : V → V → Prop} [Finite T] [Finite V] (hT : IsLinOrd LeT) (hV : IsLinOrd LeV) {H : T → Prop} {s : T × V → Prop} (hs : wmAvoids H s) : WMSetLe (lexRel LeT LeV) s (wmAvoidTop H)

Every address avoiding a set of blocks is at or below its top.

theorem DescriptiveComplexity.wmAvoids_of_wmSetLe {T V : Type} {LeT : T → T → Prop} {LeV : V → V → Prop} [Finite T] [Finite V] (hT : IsLinOrd LeT) (hV : IsLinOrd LeV) {H : T → Prop} (hdown : ∀ (τ σ : T), LeT τ σ → H σ → H τ) {s t : T × V → Prop} (hle : WMSetLe (lexRel LeT LeV) s t) (ht : wmAvoids H t) : wmAvoids H s

The region is an initial stretch of the tape: an address below one that avoids a downward-closed set of blocks avoids it too. So a sweep upwards stays in the region until it leaves it once and for all, and the program never has to say where it is.

theorem DescriptiveComplexity.mul_add_lt_two_pow {k j m a b s : ℕ} (hkj : k + 1 < j) (hm : 0 < m) (ha : a ≤ 2 ^ (k * m)) (hb : b ≤ 2 ^ (k * m)) (hs : s ≤ 2 ^ (k * m)) : a * b + s < 2 ^ ((k + j) * m)

A product plus an opening fits the clock: a counted program's cost is not «rounds × width» alone – there is the opening before the evaluation and the odd step between phases – and an additive term of the region's own size still fits, at the price of one more surplus block than the product alone needs.

The arithmetic: a · b + s ≤ 2 ^ (2km) + 2 ^ (km) ≤ 2 ^ (2km + 1), and 2km + 1 < (k + j)m as soon as k + 1 < j.

theorem DescriptiveComplexity.mul_add_lt_two_pow' {k j m a b s : ℕ} (hk : 1 ≤ k) (hkj : k + 1 < j) (hm : 0 < m) (ha : a ≤ 2 ^ (k * m)) (hb : b ≤ 2 ^ (k * m)) (hs : s ≤ 2 ^ ((k + 1) * m)) : a * b + s < 2 ^ ((k + j) * m)

A product and an opening twice the region fit the clock: the same sum as mul_add_lt_two_pow with the additive term allowed a whole extra factor of 2 ^ m – which is what an opening that sweeps the file and the region costs, where the region is 2 ^ (k · m) and the sweep goes out and back. One working block is enough for it (1 ≤ k), since the opening is then below the product itself.

theorem DescriptiveComplexity.wmIncr_lexRel_iff {T V : Type} {LeT : T → T → Prop} {LeV : V → V → Prop} (hT : IsLinOrd LeT) (s t : T × V → Prop) : WMIncr (lexRel LeT LeV) s t ↔ ∃ (τ : T), (∀ (σ : T), WMLt LeT τ σ → ∀ (v : V), wmBlk s σ v) ∧ WMIncr LeV (wmBlk s τ) (wmBlk t τ) ∧ (∀ (σ : T), WMLt LeT σ τ → ∀ (v : V), wmBlk t σ v ↔ wmBlk s σ v) ∧ ∀ (σ : T), WMLt LeT τ σ → ∀ (v : V), ¬wmBlk t σ v

The increment of an address carries block by block: at the last index whose block is not full, that block increments; every later block is emptied and every earlier one is left alone. The index is the carry index, and which blocks it empties is exactly the roll-over information the sweep folds by.