The fold on a final segment of the blocks

DescriptiveComplexity.Problems.Wide.Bridge joins the fold to the address increment when the block index type is the whole of Fin n. The inner loop of the EXPSPACE program is not like that: its register enumerates the valuations of the step formula's quantifier prefix, which live in the last q blocks of the address – the Kin half of the argument tags – while every other block of the register stays empty. So the join is restated here for an arbitrary family of block indices ι : Fin q → T, assumed to be an order embedding onto a final segment of the tag order:

• the embedding hypotheses are DescriptiveComplexity.Draw.IxSeg;
• DescriptiveComplexity.Draw.exists_carry_ix – an increment of the address whose image blocks are not all full has its carry inside the image (every tag after an image tag is an image tag, so the last non-full block cannot escape), and decomposes there;
• DescriptiveComplexity.Draw.foldFrom_carry_of_ix / foldFrom_above_of_ix / foldFrom_below_of_ix – the three fold rules, at the family DescriptiveComplexity.Draw.ixBlk of image blocks;
• DescriptiveComplexity.Draw.foldFrom_bot_of_ix / foldFrom_top_of_ix – the two ends: empty image blocks start the sweep at the matrix, full ones finish it at the whole prefix.

Everything is about the product order DescriptiveComplexity.lexRel on T × V; joining it to the machine's own order is the instance's le field, as everywhere in the layer.

structure DescriptiveComplexity.Draw.IxSeg {T : Type} {q : ℕ} (LeT : T → T → Prop) (ι : Fin q → T) : Prop

A final segment of the blocks: an order embedding of Fin q into the tags whose image is upward closed – every tag strictly above an image tag is an image tag. The Kin half of the argument tags is one.

• mono (j j' : Fin q) : WMLt LeT (ι j) (ι j') ↔ j < j'

  The embedding is strictly monotone, in both directions.

• final (j : Fin q) (t : T) : WMLt LeT (ι j) t → ∃ (j' : Fin q), t = ι j'

  The image is a final segment of the tag order.

def DescriptiveComplexity.Draw.ixBlk {T V : Type} {q : ℕ} (ι : Fin q → T) (s : T × V → Prop) : Fin q → V → Prop

The image blocks of an address, as a valuation of the fold.

Equations

• DescriptiveComplexity.Draw.ixBlk ι s j = DescriptiveComplexity.wmBlk s (ι j)

theorem DescriptiveComplexity.Draw.exists_carry_ix {T V : Type} {LeT : T → T → Prop} {LeV : V → V → Prop} {q : ℕ} {ι : Fin q → T} {s s' : T × V → Prop} (hT : IsLinOrd LeT) (hseg : IxSeg LeT ι) (hincr : WMIncr (lexRel LeT LeV) s s') (hne : ∃ (j : Fin q) (v : V), ¬wmBlk s (ι j) v) : ∃ (c : Fin q), (∀ (σ : T), WMLt LeT σ (ι c) → ∀ (v : V), wmBlk s' σ v ↔ wmBlk s σ v) ∧ WMIncr LeV (wmBlk s (ι c)) (wmBlk s' (ι c)) ∧ (∀ (σ : T), WMLt LeT (ι c) σ → ∀ (v : V), wmBlk s σ v) ∧ ∀ (σ : T), WMLt LeT (ι c) σ → ∀ (v : V), ¬wmBlk s' σ v

The carry of an increment stays in a final segment whose blocks are not all full: the carry tag is the last tag with a non-full block, every tag above an image tag is an image tag, and some image block is non-full – so the carry decomposition of DescriptiveComplexity.wmIncr_lexRel_iff happens at an image tag.

The fold rules at the image blocks

theorem DescriptiveComplexity.Draw.foldFrom_carry_of_ix {T V : Type} {LeT : T → T → Prop} {LeV : V → V → Prop} {q : ℕ} {ι : Fin q → T} {s s' : T × V → Prop} {pol : ℕ → Bool} {P : (Fin q → V → Prop) → Prop} [Finite V] (hV : IsLinOrd LeV) (hseg : IxSeg LeT ι) {c : Fin q} (hbefore : ∀ (σ : T), WMLt LeT σ (ι c) → ∀ (v : V), wmBlk s' σ v ↔ wmBlk s σ v) (hstep : WMIncr LeV (wmBlk s (ι c)) (wmBlk s' (ι c))) (hfull : ∀ (σ : T), WMLt LeT (ι c) σ → ∀ (v : V), wmBlk s σ v) : foldFrom pol P (WMSetLe LeV) (↑c) (ixBlk ι s') ↔ if pol ↑c = true then foldFrom pol P (WMSetLe LeV) (↑c) (ixBlk ι s) ∨ foldFrom pol P (WMSetLe LeV) (↑c + 1) (ixBlk ι s') else foldFrom pol P (WMSetLe LeV) (↑c) (ixBlk ι s) ∧ foldFrom pol P (WMSetLe LeV) (↑c + 1) (ixBlk ι s')

The fold rule at the carry index, when the carry tag is the c-th image tag: the accumulator there absorbs the finished subtree and takes in the deeper accumulator, exactly as over a full block index type.

theorem DescriptiveComplexity.Draw.foldFrom_below_of_ix {T V : Type} {LeT : T → T → Prop} {LeV : V → V → Prop} {q : ℕ} {ι : Fin q → T} {s' : T × V → Prop} {pol : ℕ → Bool} {P : (Fin q → V → Prop) → Prop} [Finite V] (hV : IsLinOrd LeV) (hseg : IxSeg LeT ι) {c : Fin q} (hafter : ∀ (σ : T), WMLt LeT (ι c) σ → ∀ (v : V), ¬wmBlk s' σ v) {j : ℕ} (hj : ↑c < j) : foldFrom pol P (WMSetLe LeV) j (ixBlk ι s') ↔ P (ixBlk ι s')

Below the carry index the accumulators reset to the new leaf: the image blocks there have been emptied.

theorem DescriptiveComplexity.Draw.foldFrom_above_of_ix {T V : Type} {LeT : T → T → Prop} {LeV : V → V → Prop} {q : ℕ} {ι : Fin q → T} {s s' : T × V → Prop} {pol : ℕ → Bool} {P : (Fin q → V → Prop) → Prop} (hseg : IxSeg LeT ι) {c : Fin q} (hbefore : ∀ (σ : T), WMLt LeT σ (ι c) → ∀ (v : V), wmBlk s' σ v ↔ wmBlk s σ v) {j : ℕ} (hjq : j < q) (hj : j < ↑c) : foldFrom pol P (WMSetLe LeV) j (ixBlk ι s') ↔ if pol j = true then (∃ (a : V → Prop), WMLt (WMSetLe LeV) a (ixBlk ι s ⟨j, hjq⟩) ∧ altQuantFrom pol P (j + 1) (Function.update (ixBlk ι s) ⟨j, hjq⟩ a)) ∨ foldFrom pol P (WMSetLe LeV) (j + 1) (ixBlk ι s') else (∀ (a : V → Prop), WMLt (WMSetLe LeV) a (ixBlk ι s ⟨j, hjq⟩) → altQuantFrom pol P (j + 1) (Function.update (ixBlk ι s) ⟨j, hjq⟩ a)) ∧ foldFrom pol P (WMSetLe LeV) (j + 1) (ixBlk ι s')

Above the carry index only the deeper accumulator changes: the image blocks up to the level are untouched by the increment.

The two ends of the enumeration

theorem DescriptiveComplexity.Draw.foldFrom_bot_of_ix {T V : Type} {LeV : V → V → Prop} {q : ℕ} {ι : Fin q → T} {s : T × V → Prop} {pol : ℕ → Bool} {P : (Fin q → V → Prop) → Prop} [Finite V] (hV : IsLinOrd LeV) (hempty : ∀ (j : Fin q) (v : V), ¬wmBlk s (ι j) v) {j : ℕ} : foldFrom pol P (WMSetLe LeV) j (ixBlk ι s) ↔ P (ixBlk ι s)

Empty image blocks start the sweep at the matrix: nothing has been accumulated yet.

theorem DescriptiveComplexity.Draw.foldFrom_top_of_ix {T V : Type} {LeV : V → V → Prop} {q : ℕ} {ι : Fin q → T} {s : T × V → Prop} {pol : ℕ → Bool} {P : (Fin q → V → Prop) → Prop} [Finite V] (hV : IsLinOrd LeV) (hfull : ∀ (j : Fin q) (v : V), wmBlk s (ι j) v) {j : ℕ} : foldFrom pol P (WMSetLe LeV) j (ixBlk ι s) ↔ altQuantFrom pol P j (ixBlk ι s)

Full image blocks finish the sweep at the whole prefix: every leaf has been seen.

The fold along a tuple loop

The element loops of the atom subroutines enumerate tuples of source elements in the control, stepping by the lexicographic successor DescriptiveComplexity.TupSucc – whose components are exactly the hypotheses of the fold's three step rules, at value type the source structure itself. These are the control-scale twins of the rules above; the two ends need no twin, DescriptiveComplexity.foldFrom_bot / foldFrom_top apply as they stand at an all-minimal / all-maximal tuple.

theorem DescriptiveComplexity.Draw.wmLt_le_iff {A : Type} [LinearOrder A] {a b : A} : WMLt (fun (x1 x2 : A) => x1 ≤ x2) a b ↔ a < b

The strict form of the order relation the fold reads is the strict order.