A gate's four folds

What a gate block's element loop carries between rounds is a composite write: started, it clears the loop element and sets the sub-fold to its polarity's unit; advanced, it stores the leaf, folds at the carry coordinate and steps the loop element; and its exit conjoins the sub-fold's verdict into the block's flag.

Each is two or three writes nested, and what makes them definable is not new machinery but the commutations: the three registers a gate writes – the loop element, the sub-fold's accumulators, and the sub-leaf flag – are disjoint, so each write reads what it was given. With those, the pieces are the ones already discharged.

The three registers are disjoint

theorem DescriptiveComplexity.Draw.Data.lvE_ne_sacC {L : FirstOrder.Language} {dt : Data L} (j j' : Fin dt.eDim) : dt.lvE j ≠ dt.sacC j'

theorem DescriptiveComplexity.Draw.Data.lvE_ne_subLeafC {L : FirstOrder.Language} {dt : Data L} (j : Fin dt.eDim) : dt.lvE j ≠ dt.subLeafC

theorem DescriptiveComplexity.Draw.Data.readLvE_putSac {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} (f : dt.CtlIx → A) (b : Fin dt.eDim → Prop) : dt.readLvE (dt.putSac zero one f b) = dt.readLvE f

The loop element rides along a write of the sub-fold.

theorem DescriptiveComplexity.Draw.Data.readLvE_setSubLeaf {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} (f : dt.CtlIx → A) (b : Prop) : dt.readLvE (dt.setSubLeaf zero one b f) = dt.readLvE f

And along a write of the sub-leaf flag.

theorem DescriptiveComplexity.Draw.Data.readLvE_carrySac {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} (pol : ℕ → Bool) (c : ℕ) (f : dt.CtlIx → A) : dt.readLvE (dt.carrySac zero one pol c f) = dt.readLvE f

The loop element rides along a fold at a carry.

theorem DescriptiveComplexity.Draw.Data.readSac_setSubLeaf' {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} (f : dt.CtlIx → A) (b : Prop) : dt.readSac one (dt.setSubLeaf zero one b f) = dt.readSac one f

The sub-fold's accumulators ride along a write of the sub-leaf flag.

Composing a write with a write

theorem DescriptiveComplexity.Draw.Data.uStDefinable_putVec_comp {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) {F : (e : Env L) → (dt.CtlIx → e.α) → (dt.SlotIx → e.α) → dt.CtlIx → e.α} (hF : UStDefinable F) : UStDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (g : dt.SlotIx → e.α) => dt.putVec e.zero e.one accs (F e f g) fun (j : Fin m) => b e j f g

A vector write over a definable base: the named slots take the bits of the family, and every other slot is whatever the base left there.

theorem DescriptiveComplexity.Draw.Data.uStDefinable_putLvE_comp {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {w : (e : Env L) → (dt.CtlIx → e.α) → (dt.SlotIx → e.α) → Fin dt.eDim → e.α} (hw : ∀ (j : Fin dt.eDim), USlotDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (g : dt.SlotIx → e.α) => w e f g j) {F : (e : Env L) → (dt.CtlIx → e.α) → (dt.SlotIx → e.α) → dt.CtlIx → e.α} (hF : UStDefinable F) : UStDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (g : dt.SlotIx → e.α) => dt.putLvE (F e f g) (w e f g)

A loop-element write over a definable base.

The three shapes a fold has

A gate block and an expansion atom fold the same way – only the prefix and the leaf differ – so the three shapes are stated at an arbitrary polarity and an arbitrary definable leaf, and each machinery instantiates them.

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

A sub-fold's verdict at a stored leaf is definable: the accumulators ride along the store, and the leaf it closes with is what was stored.

theorem DescriptiveComplexity.Draw.Data.uStDefinable_initSac_initLvE {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 (dt.initLvE f)

A loop started is definable: the loop element cleared and the sub-fold at its polarity's unit.

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

A conjoining exit is definable: the leaf stored, and a flag written from a question the caller supplies.

theorem DescriptiveComplexity.Draw.Data.uStDefinable_advSac {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] (pol : ℕ → Bool) {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.advLvE (dt.carrySac e.zero e.one pol (tupCarry (dt.readLvE f)) (dt.setSubLeaf e.zero e.one (b e f g) f))

A round, folded and advanced, is definable. Three writes nested – the leaf stored, the sub-fold folded at its carry, the loop element stepped – and three commutations: the fold does not touch the loop element, the store touches neither the accumulators nor it, so each write reads what it was given, and the carry itself is a question about which coordinates are maximal.

A gate's four folds

theorem DescriptiveComplexity.Draw.Data.uStDefinable_gateInit {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] (t : dt.X.Tag) : UStDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => dt.gateInit e.zero e.one t f

A gate's domain loop, started.

theorem DescriptiveComplexity.Draw.Data.uStDefinable_gateAdv {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] [L.IsRelational] (t : dt.X.Tag) (hn : (dt.domPk t).n ≤ dt.eDim) (hrd : dt.domNr t ≤ dt.nfDim) : UStDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => dt.gateAdv e.zero e.one t hn hrd f

A gate's domain round, folded and advanced.

theorem DescriptiveComplexity.Draw.Data.uStDefinable_gateExit {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] [L.IsRelational] (t : dt.X.Tag) (hc : Fintype.card dt.X.Tag ≤ dt.ntgDim) (hn : (dt.domPk t).n ≤ dt.eDim) (hrd : dt.domNr t ≤ dt.nfDim) : UStDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => dt.gateExit e.zero e.one t hc hn hrd f

A gate's conjoining exit: the leaf stored, and the block's flag conjoined with the decoding and the sub-fold's verdict.

theorem DescriptiveComplexity.Draw.Data.uStDefinable_igateExit {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] [L.IsRelational] (flag : dt.CtlIx) (t : dt.X.Tag) (hc : Fintype.card dt.X.Tag ≤ dt.ntgDim) (hn : (dt.domPk t).n ≤ dt.eDim) (hrd : dt.domNr t ≤ dt.nfDim) : UStDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => dt.igateExit e.zero e.one flag t hc hn hrd f

An inner gate's conjoining exit, the same into the level's flag.