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

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

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

@[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

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.

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.

@[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

What the two readings are worth