The blocks of an address are the valuation the fold runs on

The join between the two halves of the sweep. DescriptiveComplexity.Problems.Wide.Blocks reads an address over a block-major universe as a family of blocks and says how that family changes along one increment; DescriptiveComplexity.Problems.Wide.Fold says how a quantifier prefix folds along one step of the lexicographic enumeration of its valuations. They are the same step, and this file says so:

with the block index type taken to be Fin n – which a reduction may simply choose, one index per variable of its kernel – the family of blocks DescriptiveComplexity.wmBlk s is a valuation, the value order is DescriptiveComplexity.WMSetLe, and every hypothesis the fold's three step rules ask for is read off DescriptiveComplexity.wmIncr_lexRel_iff.

So DescriptiveComplexity.foldFrom_carry_of_wmIncr is the fold rule at the carry index, stated about an address increment and nothing else – the form a program's step obligation will be discharged in. The blocks after the carry are full before the step and empty after it, which is exactly the fold's “maximal” and “minimal” hypotheses (DescriptiveComplexity.wmSetLe_of_full, DescriptiveComplexity.wmSetLe_of_empty), and the successor hypothesis is DescriptiveComplexity.wmSetLt_iff_of_wmIncr read through DescriptiveComplexity.wmLt_wmSetLe_iff.

theorem DescriptiveComplexity.wmLt_fin_iff {n : ℕ} (σ τ : Fin n) : WMLt (fun (x1 x2 : Fin n) => x1 ≤ x2) σ τ ↔ σ < τ

On an initial segment of ℕ the order the address layer writes is the order.

def DescriptiveComplexity.mkAddr {n : ℕ} {V : Type} (p : Fin n → V → Prop) : Fin n × V → Prop

The address a family of blocks is. A program's configurations sit at addresses it has to build from the blocks it means them to have, which is the inverse of DescriptiveComplexity.wmBlk.

Equations

• DescriptiveComplexity.mkAddr p q = p q.1 q.2

@[simp]

theorem DescriptiveComplexity.wmBlk_mkAddr {n : ℕ} {V : Type} (p : Fin n → V → Prop) : wmBlk (mkAddr p) = p

@[simp]

theorem DescriptiveComplexity.mkAddr_wmBlk {n : ℕ} {V : Type} (s : Fin n × V → Prop) : mkAddr (wmBlk s) = s

theorem DescriptiveComplexity.blocks_agree_lt {n : ℕ} {V : Type} {s s' : Fin n × V → Prop} {τ : Fin n} (hbefore : ∀ (σ : Fin n), WMLt (fun (x1 x2 : Fin n) => x1 ≤ x2) σ τ → ∀ (v : V), wmBlk s' σ v ↔ wmBlk s σ v) (i : Fin n) : ↑i < ↑τ → wmBlk s i = wmBlk s' i

The same, at the carry index itself: every strictly earlier block agrees.

theorem DescriptiveComplexity.blocks_top_after {n : ℕ} {V : Type} [Finite V] {LeV : V → V → Prop} {s : Fin n × V → Prop} {τ : Fin n} (hV : IsLinOrd LeV) (hfull : ∀ (σ : Fin n), WMLt (fun (x1 x2 : Fin n) => x1 ≤ x2) τ σ → ∀ (v : V), wmBlk s σ v) (i : Fin n) : ↑τ < ↑i → ∀ (a : V → Prop), WMSetLe LeV a (wmBlk s i)

The blocks after the carry index are maximal before the step: they are full, and a full block is above every block.

theorem DescriptiveComplexity.blocks_succ_at {n : ℕ} {V : Type} [Finite V] {LeV : V → V → Prop} {s s' : Fin n × V → Prop} {τ : Fin n} (hV : IsLinOrd LeV) (hincr : WMIncr LeV (wmBlk s τ) (wmBlk s' τ)) (a : V → Prop) : WMLt (WMSetLe LeV) a (wmBlk s' τ) ↔ WMSetLe LeV a (wmBlk s τ)

At the carry index the new block is the successor of the old one, which is the successor hypothesis the fold asks for.

The fold rule of an address increment

theorem DescriptiveComplexity.foldFrom_carry_of_wmIncr {n : ℕ} {V : Type} [Finite V] {LeV : V → V → Prop} {s s' : Fin n × V → Prop} {τ : Fin n} {pol : ℕ → Bool} {P : (Fin n → V → Prop) → Prop} (hV : IsLinOrd LeV) (hfull : ∀ (σ : Fin n), WMLt (fun (x1 x2 : Fin n) => x1 ≤ x2) τ σ → ∀ (v : V), wmBlk s σ v) (hincr : WMIncr LeV (wmBlk s τ) (wmBlk s' τ)) (hbefore : ∀ (σ : Fin n), WMLt (fun (x1 x2 : Fin n) => x1 ≤ x2) σ τ → ∀ (v : V), wmBlk s' σ v ↔ wmBlk s σ v) : foldFrom pol P (WMSetLe LeV) (↑τ) (wmBlk s') ↔ if pol ↑τ = true then foldFrom pol P (WMSetLe LeV) (↑τ) (wmBlk s) ∨ foldFrom pol P (WMSetLe LeV) (↑τ + 1) (wmBlk s') else foldFrom pol P (WMSetLe LeV) (↑τ) (wmBlk s) ∧ foldFrom pol P (WMSetLe LeV) (↑τ + 1) (wmBlk s')

The fold rule at the carry index of an address increment. The accumulator at the carry index absorbs the subtree the sweep has just finished – every deeper block having been full – and takes in the accumulator one level down, which is the new leaf. This is the step obligation of a one-pass program, with the address layer and the fold joined.