The folds are definable

What the program's control holds between rounds is a fold: one accumulator per level of a quantifier prefix, closed by a leaf flag. Reading it back is DescriptiveComplexity.Draw.chainFrom, a recursion down the levels, and writing it at a carry is DescriptiveComplexity.Draw.Data.putVec of a family whose entries branch on the carry.

Both are definable, and for the same reason: the recursion is over a fixed number of levels, so recursing the same way builds the pattern function. The atoms are DescriptiveComplexity.Draw.Data.uGDefinable_readVec and uGDefinable_ctlBit; everything else is the connectives.

The matrix's own value at the atoms' verdicts (DescriptiveComplexity.Draw.qfValue) is the same shape one level down – a recursion over the syntax rather than over the levels – so it is here too.

The chain

theorem DescriptiveComplexity.Draw.Data.uGDefinable_chainFrom {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {m : ℕ} (accs : Fin m → dt.CtlIx) {leaf : (e : Env L) → (dt.CtlIx → e.α) → (dt.SlotIx → e.α) → Prop} (hleaf : UGDefinable leaf) (pol : ℕ → Bool) (n j : ℕ) : UGDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (g : dt.SlotIx → e.α) => chainFrom pol (dt.readVec e.one accs f) (leaf e f g) n j

A fold, read back, is definable: the recursion down the levels is finite, so recursing the same way builds the formula. The leaf it closes with is the caller's – a flag of the control, or a bit it is about to store.

theorem DescriptiveComplexity.Draw.Data.uGDefinable_accVerdict {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] (pol : ℕ → Bool) : UGDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => dt.accVerdict e.one pol f

The inner fold's verdict is definable.

theorem DescriptiveComplexity.Draw.Data.uGDefinable_sacVerdict {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] (pol : ℕ → Bool) : UGDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => dt.sacVerdict e.one pol f

A sub-fold's verdict is definable.

The write at a carry

theorem DescriptiveComplexity.Draw.Data.uStDefinable_carryVec {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {m : ℕ} {accs : Fin m → dt.CtlIx} (hinj : Function.Injective accs) (leafSlot : dt.CtlIx) (pol : ℕ → Bool) (n c : ℕ) : UStDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => dt.putVec e.zero e.one accs f fun (j : Fin m) => if ↑j < c then dt.readVec e.one accs f ↑j else if ↑j = c then if pol c = true then dt.readVec e.one accs f c ∨ chainFrom pol (dt.readVec e.one accs f) (dt.ctlBit e.one f leafSlot) n (c + 1) else dt.readVec e.one accs f c ∧ chainFrom pol (dt.readVec e.one accs f) (dt.ctlBit e.one f leafSlot) n (c + 1) else pol ↑j = false

A fold at a tuple successor is definable: below the carry each level keeps its bit, the carry absorbs the chain below it, and the levels above it reset – three branches decided when the formula is built.

theorem DescriptiveComplexity.Draw.Data.uStDefinable_carryAcc {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] (pol : ℕ → Bool) (c : ℕ) : UStDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => dt.carryAcc e.zero e.one pol c f

The inner fold at a carry.

theorem DescriptiveComplexity.Draw.Data.uStDefinable_carrySac {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] (pol : ℕ → Bool) (c : ℕ) : UStDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => dt.carrySac e.zero e.one pol c f

A sub-fold at a carry.

theorem DescriptiveComplexity.Draw.Data.uStDefinable_initSac {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] (pol : ℕ → Bool) : UStDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => dt.initSac e.zero e.one pol f

A sub-fold at its first tuple.

theorem DescriptiveComplexity.Draw.Data.uStDefinable_setSubLeaf {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {b : (e : Env L) → (dt.CtlIx → e.α) → (dt.SlotIx → e.α) → Prop} (hb : UGDefinable b) : UStDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (g : dt.SlotIx → e.α) => dt.setSubLeaf e.zero e.one (b e f g) f

Storing a sub-fold's leaf.

The atoms a leaf is evaluated from

theorem DescriptiveComplexity.Draw.Data.uGDefinable_blkAtomHolds {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {B : SOBlock} {n : ℕ} (v : Fin n → dt.CtlIx) (κ : BlkAtom L B n) : UGDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => BlkAtom.holds (fun (x : B.ι) (x_1 : Fin (B.arity x) → e.α) => False) (fun (j : Fin n) => f (v j)) κ

A block atom's value at the control is definable. Three of its four shapes are what a guard may now ask: two control slots are equal, one is at most another, and a relation of the source vocabulary holds of a tuple of them – the last two being exactly what an equality pattern cannot say. The fourth, a relation variable of the block, is a read leaf and never evaluated here.

The matrix at its atoms' verdicts

theorem DescriptiveComplexity.Draw.Data.uGDefinable_qfValue {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {L' : FirstOrder.Language} {α : Type} {n : ℕ} (φ : L'.BoundedFormula α n) (val : (e : Env L) → (dt.CtlIx → e.α) → (dt.SlotIx → e.α) → L'.BoundedFormula α n → Prop) : (∀ (a : L'.BoundedFormula α n), UGDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (g : dt.SlotIx → e.α) => val e f g a) → UGDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (g : dt.SlotIx → e.α) => qfValue φ (val e f g)

A quantifier-free formula's value at a definable reading of its atoms is definable: a recursion over the syntax, the atoms being the caller's.

theorem DescriptiveComplexity.Draw.Data.uGDefinable_postLeaf {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] (v : dt.VarIx) : UGDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => dt.postLeaf e.one v f

The matrix's value at the atoms' verdicts is definable: each atom's verdict is one of finitely many control flags.