The fold, in the control's slots

DescriptiveComplexity.Problems.Wide.DrawAcc says what the machine must carry across the inner loop – one contribution per level plus the last leaf – and how a round rewrites it. This file puts that in the program's own slots, which is what the dstSt parameters of DescriptiveComplexity.Draw.Data.varRule are:

• initSt is DescriptiveComplexity.Draw.Data.initAcc – every accumulator the polarity's unit, which is what an empty register's fold is (accCVal_bot);
• postFold is DescriptiveComplexity.Draw.Data.setLeaf at postLeaf – the matrix's Boolean value at the atoms' verdicts, in the leaf flag;
• storeCarry b is DescriptiveComplexity.Draw.Data.carryAcc – untouched below the carry, absorbing the chain at it, reset above (accCVal_step);
• accBit is DescriptiveComplexity.Draw.Data.accVerdict – the chain from level 0, which is the whole prefix once the register is exhausted.

Every one of them is a function of the pointer alone, and each comes with the equation the run needs: what the next pointer's slots read back. The fold's own correctness is DrawAcc's; nothing here repeats it.

The accumulator vector

def DescriptiveComplexity.Draw.Data.readVec {L : FirstOrder.Language} (dt : Data L) {A : Type} (one : A) {m : ℕ} (accs : Fin m → dt.CtlIx) (f : dt.CtlIx → A) (j : ℕ) : Prop

A vector of control slots, read: one bit per index. Past the family it is False; a fold never looks there.

Equations

• dt.readVec one accs f j = ∃ (h : j < m), f (accs ⟨j, h⟩) = one

noncomputable def DescriptiveComplexity.Draw.Data.putVec {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero one : A) {m : ℕ} (accs : Fin m → dt.CtlIx) (f : dt.CtlIx → A) (b : Fin m → Prop) : dt.CtlIx → A

A vector of control slots, written.

Equations

• dt.putVec zero one accs f b q = if h : ∃ (j : Fin m), q = accs j then DescriptiveComplexity.Draw.bitVal zero one (b h.choose) else f q

theorem DescriptiveComplexity.Draw.Data.putVec_of_not_mem {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} {m : ℕ} {accs : Fin m → dt.CtlIx} {f : dt.CtlIx → A} {b : Fin m → Prop} {q : dt.CtlIx} (h : ∀ (j : Fin m), q ≠ accs j) : dt.putVec zero one accs f b q = f q

theorem DescriptiveComplexity.Draw.Data.readVec_putVec {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} (hzo : zero ≠ one) {m : ℕ} {accs : Fin m → dt.CtlIx} (hinj : Function.Injective accs) (f : dt.CtlIx → A) (b : Fin m → Prop) {j : ℕ} (hj : j < m) : dt.readVec one accs (dt.putVec zero one accs f b) j ↔ b ⟨j, hj⟩

A vector reads back, index by index.

def DescriptiveComplexity.Draw.Data.readAcc {L : FirstOrder.Language} (dt : Data L) {A : Type} (one : A) (f : dt.CtlIx → A) (j : ℕ) : Prop

The inner fold's accumulator vector, one bit per level.

Equations

• dt.readAcc one f j = dt.readVec one dt.accC f j

noncomputable def DescriptiveComplexity.Draw.Data.putAcc {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero one : A) (f : dt.CtlIx → A) (b : Fin dt.naDim → Prop) : dt.CtlIx → A

The inner fold's accumulator vector, written.

Equations

• dt.putAcc zero one f b = dt.putVec zero one dt.accC f b

def DescriptiveComplexity.Draw.Data.readSac {L : FirstOrder.Language} (dt : Data L) {A : Type} (one : A) (f : dt.CtlIx → A) (j : ℕ) : Prop

A sub-fold's accumulator vector: the element loops of the atom subroutines keep theirs in the sac slots, one per level of the defining sentence's own prefix.

Equations

• dt.readSac one f j = dt.readVec one dt.sacC f j

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

A sub-fold's accumulator vector, written.

Equations

• dt.putSac zero one f b = dt.putVec zero one dt.sacC f b

theorem DescriptiveComplexity.Draw.Data.sacC_injective {L : FirstOrder.Language} (dt : Data L) : Function.Injective dt.sacC

theorem DescriptiveComplexity.Draw.Data.putAcc_of_not_acc {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} {f : dt.CtlIx → A} {b : Fin dt.naDim → Prop} {q : dt.CtlIx} (h : ∀ (j : Fin dt.naDim), q ≠ dt.accC j) : dt.putAcc zero one f b q = f q

theorem DescriptiveComplexity.Draw.Data.putSac_of_not_sac {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} {f : dt.CtlIx → A} {b : Fin dt.eDim → Prop} {q : dt.CtlIx} (h : ∀ (j : Fin dt.eDim), q ≠ dt.sacC j) : dt.putSac zero one f b q = f q

theorem DescriptiveComplexity.Draw.Data.readAcc_putAcc {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} (hzo : zero ≠ one) (f : dt.CtlIx → A) (b : Fin dt.naDim → Prop) {j : ℕ} (hj : j < dt.naDim) : dt.readAcc one (dt.putAcc zero one f b) j ↔ b ⟨j, hj⟩

The inner fold's vector reads back, level by level.

theorem DescriptiveComplexity.Draw.Data.readSac_putSac {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} (hzo : zero ≠ one) (f : dt.CtlIx → A) (b : Fin dt.eDim → Prop) {j : ℕ} (hj : j < dt.eDim) : dt.readSac one (dt.putSac zero one f b) j ↔ b ⟨j, hj⟩

A sub-fold's vector reads back, level by level.

The leaf flag

noncomputable def DescriptiveComplexity.Draw.Data.leafC {L : FirstOrder.Language} (dt : Data L) : dt.CtlIx

The leaf flag: the value of the matrix at the valuation the loop has just evaluated – the bit every carry absorbs.

Equations

• dt.leafC = dt.scratchC 0

noncomputable def DescriptiveComplexity.Draw.Data.postLeaf {L : FirstOrder.Language} (dt : Data L) {A : Type} (one : A) (v : dt.VarIx) (f : dt.CtlIx → A) : Prop

The matrix's Boolean value at the atoms' verdicts: what the machine knows once every atom subroutine has filed its bit.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.Draw.Data.setLeaf {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero one : A) (b : Prop) (f : dt.CtlIx → A) : dt.CtlIx → A

Storing the leaf.

Equations

• dt.setLeaf zero one b f = dt.setCtl zero one dt.leafC b f

theorem DescriptiveComplexity.Draw.Data.accC_ne_leafC {L : FirstOrder.Language} {dt : Data L} (j : Fin dt.naDim) : dt.accC j ≠ dt.leafC

theorem DescriptiveComplexity.Draw.Data.leafC_ne_accC {L : FirstOrder.Language} {dt : Data L} (j : Fin dt.naDim) : dt.leafC ≠ dt.accC j

@[simp]

theorem DescriptiveComplexity.Draw.Data.ctlBit_setLeaf {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} (hzo : zero ≠ one) (b : Prop) (f : dt.CtlIx → A) : dt.ctlBit one (dt.setLeaf zero one b f) dt.leafC ↔ b

theorem DescriptiveComplexity.Draw.Data.setLeaf_of_ne {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} {q : dt.CtlIx} (hne : q ≠ dt.leafC) (b : Prop) (f : dt.CtlIx → A) : dt.setLeaf zero one b f q = f q

theorem DescriptiveComplexity.Draw.Data.readAcc_setLeaf {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} (b : Prop) (f : dt.CtlIx → A) (j : ℕ) : dt.readAcc one (dt.setLeaf zero one b f) j ↔ dt.readAcc one f j

The accumulators ride along a write of the leaf flag.

The three updates

noncomputable def DescriptiveComplexity.Draw.Data.initAcc {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero one : A) (pol : ℕ → Bool) (f : dt.CtlIx → A) : dt.CtlIx → A

The folds at the empty valuation: every accumulator the polarity's unit.

Equations

• dt.initAcc zero one pol f = dt.putAcc zero one f fun (j : Fin dt.naDim) => pol ↑j = false

noncomputable def DescriptiveComplexity.Draw.Data.accVerdict {L : FirstOrder.Language} (dt : Data L) {A : Type} (one : A) (pol : ℕ → Bool) (f : dt.CtlIx → A) : Prop

The verdict the accumulators spell: the chain from level 0, closed by the leaf flag – the value of the whole prefix once the register is exhausted.

Equations

• dt.accVerdict one pol f = DescriptiveComplexity.Draw.chainFrom pol (dt.readAcc one f) (dt.ctlBit one f dt.leafC) dt.ki 0

noncomputable def DescriptiveComplexity.Draw.Data.carryAcc {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero one : A) (pol : ℕ → Bool) (c : ℕ) (f : dt.CtlIx → A) : dt.CtlIx → A

The folds at an increment's carry block: the levels before the carry keep their bit, the carry level absorbs the chain below it, the levels after it reset.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.Draw.Data.readAcc_initAcc {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} (hzo : zero ≠ one) (pol : ℕ → Bool) (f : dt.CtlIx → A) {j : ℕ} (hj : j < dt.naDim) : dt.readAcc one (dt.initAcc zero one pol f) j ↔ pol j = false

What the initialized vector reads: the polarity's unit at every level, which is DescriptiveComplexity.Draw.accCVal_bot's value.

theorem DescriptiveComplexity.Draw.Data.readAcc_carryAcc {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} (hzo : zero ≠ one) (pol : ℕ → Bool) (c : ℕ) (f : dt.CtlIx → A) {j : ℕ} (hj : j < dt.naDim) : dt.readAcc one (dt.carryAcc zero one pol c f) j ↔ if j < c then dt.readAcc one f j else if j = c then if pol c = true then dt.readAcc one f c ∨ chainFrom pol (dt.readAcc one f) (dt.ctlBit one f dt.leafC) dt.ki (c + 1) else dt.readAcc one f c ∧ chainFrom pol (dt.readAcc one f) (dt.ctlBit one f dt.leafC) dt.ki (c + 1) else pol j = false

What the vector reads after a carry: exactly the shape DescriptiveComplexity.Draw.accCVal_step asks for.

The same for a sub-fold

An element loop of an atom subroutine folds its own prefix – the defining sentence's – over the sac slots, with its own leaf flag. The three updates are the same three; only the family and the width change.

noncomputable def DescriptiveComplexity.Draw.Data.subLeafC {L : FirstOrder.Language} (dt : Data L) : dt.CtlIx

The sub-fold's leaf flag: the value of a defining sentence's matrix at the tuple the element loop has just read.

Equations

• dt.subLeafC = dt.scratchC 4

noncomputable def DescriptiveComplexity.Draw.Data.setSubLeaf {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero one : A) (b : Prop) (f : dt.CtlIx → A) : dt.CtlIx → A

Storing a sub-fold's leaf.

Equations

• dt.setSubLeaf zero one b f = dt.setCtl zero one dt.subLeafC b f

noncomputable def DescriptiveComplexity.Draw.Data.initSac {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero one : A) (pol : ℕ → Bool) (f : dt.CtlIx → A) : dt.CtlIx → A

A sub-fold at its first tuple.

Equations

• dt.initSac zero one pol f = dt.putSac zero one f fun (j : Fin dt.eDim) => pol ↑j = false

noncomputable def DescriptiveComplexity.Draw.Data.sacVerdict {L : FirstOrder.Language} (dt : Data L) {A : Type} (one : A) (pol : ℕ → Bool) (f : dt.CtlIx → A) : Prop

What a sub-fold concludes: the chain from level 0, closed by its leaf flag.

Equations

• dt.sacVerdict one pol f = DescriptiveComplexity.Draw.chainFrom pol (dt.readSac one f) (dt.ctlBit one f dt.subLeafC) dt.eDim 0

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

A sub-fold at a tuple successor, the carry coordinate given.

Equations

• One or more equations did not get rendered due to their size.

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

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

@[simp]

theorem DescriptiveComplexity.Draw.Data.ctlBit_setSubLeaf {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} (hzo : zero ≠ one) (b : Prop) (f : dt.CtlIx → A) : dt.ctlBit one (dt.setSubLeaf zero one b f) dt.subLeafC ↔ b

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

A sub-fold's accumulators ride along a write of its leaf flag.

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

The loop's wide tuple rides along a write of a sub-fold's accumulators.

theorem DescriptiveComplexity.Draw.Data.readSac_carrySac {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} (hzo : zero ≠ one) (pol : ℕ → Bool) (c : ℕ) (f : dt.CtlIx → A) {j : ℕ} (hj : j < dt.eDim) : dt.readSac one (dt.carrySac zero one pol c f) j ↔ if j < c then dt.readSac one f j else if j = c then if pol c = true then dt.readSac one f c ∨ chainFrom pol (dt.readSac one f) (dt.ctlBit one f dt.subLeafC) dt.eDim (c + 1) else dt.readSac one f c ∧ chainFrom pol (dt.readSac one f) (dt.ctlBit one f dt.subLeafC) dt.eDim (c + 1) else pol j = false

theorem DescriptiveComplexity.Draw.Data.sacVerdict_iff_foldFrom {L : FirstOrder.Language} {dt : Data L} {A : Type} {one : A} {α : Type} {le : α → α → Prop} {P : (Fin dt.eDim → α) → Prop} {pol : ℕ → Bool} {v : Fin dt.eDim → α} {f : dt.CtlIx → A} (hacc : ∀ j < dt.eDim, dt.readSac one f j ↔ accCVal pol P le j v) (hleaf : dt.ctlBit one f dt.subLeafC ↔ P v) : dt.sacVerdict one pol f ↔ foldFrom pol P le 0 v

A sub-fold's verdict is its fold, by the same chain.

What the two readings are worth

theorem DescriptiveComplexity.Draw.Data.accVerdict_iff_foldFrom {L : FirstOrder.Language} {dt : Data L} {A : Type} {one : A} {α : Type} {le : α → α → Prop} {P : (Fin dt.ki → α) → Prop} {pol : ℕ → Bool} {v : Fin dt.ki → α} {f : dt.CtlIx → A} (hacc : ∀ j < dt.ki, dt.readAcc one f j ↔ accCVal pol P le j v) (hleaf : dt.ctlBit one f dt.leafC ↔ P v) : dt.accVerdict one pol f ↔ foldFrom pol P le 0 v

The verdict is the fold: if the accumulators hold the contributions and the leaf flag the matrix at the current valuation, the chain from level 0 is the fold's value there – so the exit checkpoint's guard reads the sweep's answer off the control.

theorem DescriptiveComplexity.Draw.Data.postLeaf_iff_qfValue {L : FirstOrder.Language} {dt : Data L} {A : Type} {one : A} [L.Structure A] [LinearOrder A] [LinearOrder (dt.X.Map A)] {v : dt.VarIx} {f : dt.CtlIx → A} {σ : dt.d.B.Assignment (dt.X.Map A)} {w : Fin (dt.nOf v) → dt.X.Map A} (hav : ∀ (k : Fin (dt.natOf v)), dt.ctlBit one f (dt.avC (Fin.castLE ⋯ k)) ↔ MatAtom.holds σ w (dt.kindOf v k)) : dt.postLeaf one v f ↔ qfValue (dt.matOf v) fun (a : ((dt.X.E.sum FirstOrder.Language.order).sum dt.d.B.lang).BoundedFormula Empty (dt.nOf v)) => (matAtom? a).elim False (MatAtom.holds σ w)

The leaf flag's value is the matrix: once every atom subroutine has filed its verdict, the Boolean function the control computes is the matrix at the atoms' readings – DescriptiveComplexity.Draw.realize_iff_qfValue_holds's right-hand side, which is what the machine's leaf must be.