The control's dictionary: which slot plays which role

The program's states carry a pointer f : dt.CtlIx → A, and every semantic parameter of the machinery – the coordinates a name guard compares against, the accumulators the folds update, the flags a verdict is stored in – is a designation of some of its slots. This file fixes them, once, with the casts through the budgets that DescriptiveComplexity.Draw.Data.eDim and friends were computed for:

role	slots
the coordinates of the current loop element	lvC (the first dd₀ of the lv family)
the inner fold's accumulators	accC
an element loop's sub-fold accumulators	sacC
the verdicts of the matrix's atoms	avC
the leaf reads of the current round	rdfC
the tag witnesses	tgfC
the gates' verdict, a copied bit, two scratch	gateFlagC, bitFlagC, scratchC

and the two operations every parameter is built from: reading a slot as a bit, and writing one (DescriptiveComplexity.Draw.Data.ctlBit and setCtl), with their read-back equations. Nothing here is about the tape; the machinery's dstSt parameters are functions of the pointer alone, and this is their vocabulary.

The designations

noncomputable def DescriptiveComplexity.Draw.Data.lvC {L : FirstOrder.Language} (dt : Data L) (j : Fin dt.dd0) : dt.CtlIx

The coordinates of the loop element: the first dd₀ loop-variable slots. A name guard compares a cell's name slots against these, so they are the coord of every read and write trip.

Equations

• dt.lvC j = DescriptiveComplexity.Draw.Ctl.lv (Fin.castLE ⋯ j)

noncomputable def DescriptiveComplexity.Draw.Data.accC {L : FirstOrder.Language} (dt : Data L) (j : Fin dt.naDim) : dt.CtlIx

The inner fold's accumulators: one per level of the quantifier prefix, and one over.

Equations

• dt.accC j = DescriptiveComplexity.Draw.Ctl.acc j

noncomputable def DescriptiveComplexity.Draw.Data.sacC {L : FirstOrder.Language} (dt : Data L) (j : Fin dt.eDim) : dt.CtlIx

A sub-fold's accumulators: one per level of an element loop's own prefix.

Equations

• dt.sacC j = DescriptiveComplexity.Draw.Ctl.sac j

noncomputable def DescriptiveComplexity.Draw.Data.avC {L : FirstOrder.Language} (dt : Data L) (a : Fin dt.natMax) : dt.CtlIx

The verdict of an atom of the matrix.

Equations

• dt.avC a = DescriptiveComplexity.Draw.Ctl.av a

noncomputable def DescriptiveComplexity.Draw.Data.rdfC {L : FirstOrder.Language} (dt : Data L) (a : Fin dt.nfDim) : dt.CtlIx

The verdict of a leaf read of the current element-loop round.

Equations

• dt.rdfC a = DescriptiveComplexity.Draw.Ctl.rdf a

noncomputable def DescriptiveComplexity.Draw.Data.tgfC {L : FirstOrder.Language} (dt : Data L) (a : Fin dt.ntgDim) : dt.CtlIx

A tag-witness flag.

Equations

• dt.tgfC a = DescriptiveComplexity.Draw.Ctl.tgf a

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

The gates' verdict flag: cleared by a failing block, read by the verdict checkpoint.

Equations

• dt.gateFlagC = DescriptiveComplexity.Draw.Ctl.flag 0

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

The copied bit of a tuple loop: written by the read trip's verdict exit, read back by the write trip.

Equations

• dt.bitFlagC = DescriptiveComplexity.Draw.Ctl.flag 1

noncomputable def DescriptiveComplexity.Draw.Data.scratchC {L : FirstOrder.Language} (dt : Data L) (k : Fin 6) : dt.CtlIx

The remaining scratch flags: the last leaf's value, the comparison loops' accumulator and their two verdict bits, and two spare.

Equations

• dt.scratchC k = DescriptiveComplexity.Draw.Ctl.flag (k.addNat 2)

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

The ∃-levels' gate flag of a VAL round: the conjunction, over the existentially quantified levels of the variable's pack, of “this level's inner block is an encoding”. The last free scratch flag.

Equations

• dt.existGateC = DescriptiveComplexity.Draw.Ctl.flag 7

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

The ∀-levels' gate flag of a VAL round: the same conjunction over the universally quantified levels. Reuses the outer gates' flag, which is dead once the verdict checkpoint has dispatched on it – nothing inside the VAL loop reads it again.

Equations

• dt.allGateC = DescriptiveComplexity.Draw.Ctl.flag 0

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

theorem DescriptiveComplexity.Draw.Data.gateFlagC_ne_scratchC {L : FirstOrder.Language} (dt : Data L) (k : Fin 6) : dt.gateFlagC ≠ dt.scratchC k

Distinctness

The roles are disjoint families of the same inductive, so telling them apart is a matter of constructors – except inside a family, where it is the index. These are the facts an update needs: writing one slot leaves the others alone.

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

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

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

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

theorem DescriptiveComplexity.Draw.Data.lvC_ne_bitFlagC {L : FirstOrder.Language} (dt : Data L) (j : Fin dt.dd0) : dt.lvC j ≠ dt.bitFlagC

Reading and writing one slot

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

A control slot, read as a bit.

Equations

• dt.ctlBit one f q = (f q = one)

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

A control slot, written: the pointer with one slot set to a bit.

Equations

• dt.setCtl zero one q b f = Function.update f q (DescriptiveComplexity.Draw.bitVal zero one b)

@[simp]

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

@[simp]

theorem DescriptiveComplexity.Draw.Data.ctlBit_setCtl_of_ne {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} {q q' : dt.CtlIx} (hne : q' ≠ q) (b : Prop) (f : dt.CtlIx → A) : dt.ctlBit one (dt.setCtl zero one q b f) q' ↔ dt.ctlBit one f q'

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

A write leaves the other slots' values alone, not only their bits.

The tuple enumeration

An element loop runs over the tuples of source elements in the lexicographic order, one coordinatewise successor per round (DescriptiveComplexity.TupSucc, which DescriptiveComplexity.Draw.reflTransGen_of_tupLoop indexes its rounds by). The loop's three semantic parameters are the functions behind that relation: where it starts, what it advances to, and when it is done.

def DescriptiveComplexity.Draw.IsMaxTup {D : ℕ} {A : Type} [LinearOrder A] (t : Fin D → A) : Prop

The tuple is exhausted: every coordinate is maximal, i.e., it is the lexicographic top.

Equations

• DescriptiveComplexity.Draw.IsMaxTup t = ∀ (p : Fin D) (a : A), a ≤ t p

theorem DescriptiveComplexity.Draw.exists_tupSucc_of_not_isMaxTup {D : ℕ} {A : Type} [LinearOrder A] [Finite A] {t : Fin D → A} (h : ¬IsMaxTup t) : ∃ (w : Fin D → A), TupSucc t w

A non-exhausted tuple has a successor.

noncomputable def DescriptiveComplexity.Draw.tupNext {D : ℕ} {A : Type} [LinearOrder A] (t : Fin D → A) : Fin D → A

The next tuple, the lexicographic successor – itself at the top, where no round follows.

Equations

• DescriptiveComplexity.Draw.tupNext t = if h : ∃ (w : Fin D → A), DescriptiveComplexity.TupSucc t w then h.choose else t

theorem DescriptiveComplexity.Draw.tupSucc_tupNext {D : ℕ} {A : Type} [LinearOrder A] [Finite A] {t : Fin D → A} (h : ¬IsMaxTup t) : TupSucc t (tupNext t)

Below the top, the next tuple is a successor.

The coordinate a round carries

A fold's update rule needs to know which coordinate rolled over, and the loop's control does: it is the greatest non-maximal coordinate of the tuple, which is the witness of DescriptiveComplexity.TupSucc – unique, so the machine's dstSt may name it.

def DescriptiveComplexity.Draw.TupSuccAt {D : ℕ} {A : Type} [LinearOrder A] (p : Fin D) (t t' : Fin D → A) : Prop

The body of DescriptiveComplexity.TupSucc at a named coordinate.

Equations

• DescriptiveComplexity.Draw.TupSuccAt p t t' = ((∀ j < p, t j = t' j) ∧ (t p < t' p ∧ ∀ (a : A), ¬(t p < a ∧ a < t' p)) ∧ ∀ (j : Fin D), p < j → (∀ (a : A), a ≤ t j) ∧ ∀ (a : A), t' j ≤ a)

theorem DescriptiveComplexity.Draw.tupSuccAt_unique {D : ℕ} {A : Type} [LinearOrder A] {p p' : Fin D} {t t' : Fin D → A} (h : TupSuccAt p t t') (h' : TupSuccAt p' t t') : p = p'

The carried coordinate is unique: above it every coordinate is already maximal, and it is not.

noncomputable def DescriptiveComplexity.Draw.tupCarry {D : ℕ} {A : Type} [LinearOrder A] (t : Fin D → A) : ℕ

The coordinate a round carries, read off the tuple – as a level index, so that a fold's rules may use it directly; at the top, where no round follows, it is past the last coordinate.

Equations

• DescriptiveComplexity.Draw.tupCarry t = if h : ∃ (p : Fin D), DescriptiveComplexity.Draw.TupSuccAt p t (DescriptiveComplexity.Draw.tupNext t) then ↑h.choose else D

theorem DescriptiveComplexity.Draw.tupCarry_eq {D : ℕ} {A : Type} [LinearOrder A] {t : Fin D → A} {p : Fin D} (hp : TupSuccAt p t (tupNext t)) : tupCarry t = ↑p

What the carried coordinate is: the witness of the tuple's step, which is unique.

theorem DescriptiveComplexity.Draw.tupSuccAt_tupCarry {D : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {t : Fin D → A} (h : ¬IsMaxTup t) : ∃ (p : Fin D), ↑p = tupCarry t ∧ TupSuccAt p t (tupNext t)

Below the top the carried coordinate is a level, and the round steps there.

noncomputable def DescriptiveComplexity.Draw.botTup {D : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : Fin D → A

The first tuple: every coordinate the least element.

Equations

• DescriptiveComplexity.Draw.botTup x✝ = Finset.univ.min' ⋯

theorem DescriptiveComplexity.Draw.botTup_le {D : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (p : Fin D) (a : A) : botTup p ≤ a

The loop element, read and written

Two widths, one family of slots: an element loop of an expansion atom or a domain gate enumerates the whole prefix of its defining sentence – up to eDim coordinates – while a coordinate loop (a block copy, a comparison) enumerates the dd₀ coordinates a cell's name carries. The first dd₀ slots of the wide tuple are the narrow one (lvC_eq_lvE), so a leaf read of a wide loop names its cell from the coordinates it computes and a leaf read of a narrow one from the slots directly.

noncomputable def DescriptiveComplexity.Draw.Data.readLv {L : FirstOrder.Language} (dt : Data L) {A : Type} (f : dt.CtlIx → A) : Fin dt.dd0 → A

The loop element's coordinates, read out of the control.

Equations

• dt.readLv f j = f (dt.lvC j)

noncomputable def DescriptiveComplexity.Draw.Data.putLv {L : FirstOrder.Language} (dt : Data L) {A : Type} (f : dt.CtlIx → A) (w : Fin dt.dd0 → A) : dt.CtlIx → A

The loop element's coordinates, written: the pointer with the loop-variable slots set to a tuple.

Equations

• dt.putLv f w q = if h : ∃ (j : Fin dt.dd0), q = dt.lvC j then w h.choose else f q

theorem DescriptiveComplexity.Draw.Data.putLv_of_not_lv {L : FirstOrder.Language} {dt : Data L} {A : Type} {f : dt.CtlIx → A} {w : Fin dt.dd0 → A} {q : dt.CtlIx} (h : ∀ (j : Fin dt.dd0), q ≠ dt.lvC j) : dt.putLv f w q = f q

@[simp]

theorem DescriptiveComplexity.Draw.Data.readLv_putLv {L : FirstOrder.Language} {dt : Data L} {A : Type} (f : dt.CtlIx → A) (w : Fin dt.dd0 → A) : dt.readLv (dt.putLv f w) = w

theorem DescriptiveComplexity.Draw.Data.putLv_acc {L : FirstOrder.Language} {dt : Data L} {A : Type} (f : dt.CtlIx → A) (w : Fin dt.dd0 → A) (k : Fin dt.naDim) : dt.putLv f w (dt.accC k) = f (dt.accC k)

theorem DescriptiveComplexity.Draw.Data.putLv_av {L : FirstOrder.Language} {dt : Data L} {A : Type} (f : dt.CtlIx → A) (w : Fin dt.dd0 → A) (a : Fin dt.natMax) : dt.putLv f w (dt.avC a) = f (dt.avC a)

noncomputable def DescriptiveComplexity.Draw.Data.lvE {L : FirstOrder.Language} (dt : Data L) (j : Fin dt.eDim) : dt.CtlIx

A loop variable of an element loop, at the full width.

Equations

• dt.lvE j = DescriptiveComplexity.Draw.Ctl.lv j

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

theorem DescriptiveComplexity.Draw.Data.lvC_eq_lvE {L : FirstOrder.Language} (dt : Data L) (j : Fin dt.dd0) : dt.lvC j = dt.lvE (Fin.castLE ⋯ j)

noncomputable def DescriptiveComplexity.Draw.Data.readLvE {L : FirstOrder.Language} (dt : Data L) {A : Type} (f : dt.CtlIx → A) : Fin dt.eDim → A

The wide loop element, read out of the control.

Equations

• dt.readLvE f j = f (dt.lvE j)

noncomputable def DescriptiveComplexity.Draw.Data.putLvE {L : FirstOrder.Language} (dt : Data L) {A : Type} (f : dt.CtlIx → A) (w : Fin dt.eDim → A) : dt.CtlIx → A

The wide loop element, written.

Equations

• dt.putLvE f w q = if h : ∃ (j : Fin dt.eDim), q = dt.lvE j then w h.choose else f q

theorem DescriptiveComplexity.Draw.Data.putLvE_of_not_lv {L : FirstOrder.Language} {dt : Data L} {A : Type} {f : dt.CtlIx → A} {w : Fin dt.eDim → A} {q : dt.CtlIx} (h : ∀ (j : Fin dt.eDim), q ≠ dt.lvE j) : dt.putLvE f w q = f q

@[simp]

theorem DescriptiveComplexity.Draw.Data.readLvE_putLvE {L : FirstOrder.Language} {dt : Data L} {A : Type} (f : dt.CtlIx → A) (w : Fin dt.eDim → A) : dt.readLvE (dt.putLvE f w) = w

theorem DescriptiveComplexity.Draw.Data.putLvE_acc {L : FirstOrder.Language} {dt : Data L} {A : Type} (f : dt.CtlIx → A) (w : Fin dt.eDim → A) (k : Fin dt.naDim) : dt.putLvE f w (dt.accC k) = f (dt.accC k)

The accumulators, the verdicts and the flags ride along a write of the wide loop element.

theorem DescriptiveComplexity.Draw.Data.putLvE_av {L : FirstOrder.Language} {dt : Data L} {A : Type} (f : dt.CtlIx → A) (w : Fin dt.eDim → A) (a : Fin dt.natMax) : dt.putLvE f w (dt.avC a) = f (dt.avC a)

The loop's three operations

DescriptiveComplexity.Draw.tupNext and friends, in the slots: where a loop starts, what it advances to, and when it is done – the initEl/advEl/ IsMaxEl of every element loop, at either width.

noncomputable def DescriptiveComplexity.Draw.Data.initLvE {L : FirstOrder.Language} (dt : Data L) {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (f : dt.CtlIx → A) : dt.CtlIx → A

The wide loop, started.

Equations

• dt.initLvE f = dt.putLvE f DescriptiveComplexity.Draw.botTup

noncomputable def DescriptiveComplexity.Draw.Data.advLvE {L : FirstOrder.Language} (dt : Data L) {A : Type} [LinearOrder A] (f : dt.CtlIx → A) : dt.CtlIx → A

The wide loop, advanced.

Equations

• dt.advLvE f = dt.putLvE f (DescriptiveComplexity.Draw.tupNext (dt.readLvE f))

def DescriptiveComplexity.Draw.Data.IsMaxLvE {L : FirstOrder.Language} (dt : Data L) {A : Type} [LinearOrder A] (f : dt.CtlIx → A) : Prop

The wide loop, exhausted.

Equations

• dt.IsMaxLvE f = DescriptiveComplexity.Draw.IsMaxTup (dt.readLvE f)

noncomputable def DescriptiveComplexity.Draw.Data.initLvN {L : FirstOrder.Language} (dt : Data L) {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (f : dt.CtlIx → A) : dt.CtlIx → A

The narrow loop, started.

Equations

• dt.initLvN f = dt.putLv f DescriptiveComplexity.Draw.botTup

noncomputable def DescriptiveComplexity.Draw.Data.advLvN {L : FirstOrder.Language} (dt : Data L) {A : Type} [LinearOrder A] (f : dt.CtlIx → A) : dt.CtlIx → A

The narrow loop, advanced.

Equations

• dt.advLvN f = dt.putLv f (DescriptiveComplexity.Draw.tupNext (dt.readLv f))

def DescriptiveComplexity.Draw.Data.IsMaxLvN {L : FirstOrder.Language} (dt : Data L) {A : Type} [LinearOrder A] (f : dt.CtlIx → A) : Prop

The narrow loop, exhausted.

Equations

• dt.IsMaxLvN f = DescriptiveComplexity.Draw.IsMaxTup (dt.readLv f)

@[simp]

theorem DescriptiveComplexity.Draw.Data.readLvE_initLvE {L : FirstOrder.Language} {dt : Data L} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (f : dt.CtlIx → A) : dt.readLvE (dt.initLvE f) = botTup

@[simp]

theorem DescriptiveComplexity.Draw.Data.readLv_initLvN {L : FirstOrder.Language} {dt : Data L} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (f : dt.CtlIx → A) : dt.readLv (dt.initLvN f) = botTup