The control's reads and writes are definable

Everything the program keeps in its control is a bit – a flag, an accumulator, a verdict – and every write of one is DescriptiveComplexity.Draw.Data.putVec or its one-slot special case setCtl: the named slots take the bits of a family, and every other slot rides along. So one lemma per shape settles the whole control layer, given that the questions behind the bits are definable.

Reading is the same statement one step simpler: DescriptiveComplexity.Draw.Data.readVec is an existential over the levels of a slot family, and ctlBit is a single atom.

Reading

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

A control slot, read as a bit.

theorem DescriptiveComplexity.Draw.Data.uGDefinable_readVec {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {m : ℕ} (accs : Fin m → dt.CtlIx) (j : ℕ) : UGDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => dt.readVec e.one accs f j

A vector of control slots, read at a level: one atom below the length, and nothing above it – a decision the formula is built with.

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

The inner fold's accumulator, read at a level.

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

A sub-fold's accumulator, read at a level.

Writing

theorem DescriptiveComplexity.Draw.Data.uStDefinable_putVec {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {m : ℕ} {accs : Fin m → dt.CtlIx} (hinj : Function.Injective accs) {b : (e : Env L) → Fin m → (dt.CtlIx → e.α) → (dt.SlotIx → e.α) → Prop} (hb : ∀ (j : Fin m), UGDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (g : dt.SlotIx → e.α) => b e j f g) : UStDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (g : dt.SlotIx → e.α) => dt.putVec e.zero e.one accs f fun (j : Fin m) => b e j f g

A vector of control slots, written: the named slots take the bits of the family, and every other slot rides along – so the whole write is definable as soon as each of the family's questions is.

theorem DescriptiveComplexity.Draw.Data.uStDefinable_setCtl {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] (q : dt.CtlIx) {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.setCtl e.zero e.one q (b e f g) f

One control slot, written.

theorem DescriptiveComplexity.Draw.Data.uStDefinable_putAcc {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {b : (e : Env L) → Fin dt.naDim → (dt.CtlIx → e.α) → (dt.SlotIx → e.α) → Prop} (hb : ∀ (j : Fin dt.naDim), UGDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (g : dt.SlotIx → e.α) => b e j f g) : UStDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (g : dt.SlotIx → e.α) => dt.putAcc e.zero e.one f fun (j : Fin dt.naDim) => b e j f g

The inner fold's accumulator vector, written.

theorem DescriptiveComplexity.Draw.Data.uStDefinable_setLeaf {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.setLeaf e.zero e.one (b e f g) f

The leaf flag, stored.

theorem DescriptiveComplexity.Draw.Data.uStDefinable_initAcc {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.initAcc e.zero e.one pol f

The folds at the empty valuation: every accumulator the polarity's unit, which is a question the formula is built from.