The loop variables are definable: the one write that is not a copy

Everything the EXPSPACE program writes is a copy of one of its slots or one of the two designated elements – except the loop advance. A loop element is a tuple over the instance, and advancing it is DescriptiveComplexity.Draw.tupNext, the lexicographic successor: the coordinates below the one that rolls over keep their value, the one that rolls over takes the next element of the order, and the ones above it reset.

Two things make that definable all the same.

• Which coordinate rolls over is decided by which coordinates are maximal, and that is in the equality pattern – so the case split is read off the pattern (DescriptiveComplexity.Draw.uSlotDefinable_cases).
• The value at the carry is DescriptiveComplexity.ordSucc of a single coordinate, which is exactly the source DescriptiveComplexity.SlotVal.succ names.

DescriptiveComplexity.Draw.tupNext_apply_of_carry is the coordinatewise reading of tupNext, and the three statements after it are what a variable's pack owes for its loop: the loop started, the loop advanced, and the loop exhausted – at both widths.

tupNext, coordinate by coordinate

theorem DescriptiveComplexity.Draw.isMaxTup_iff_eq_top {A : Type} [LinearOrder A] {D : ℕ} {one : A} (ht : IsTop one) (t : Fin D → A) : IsMaxTup t ↔ ∀ (p : Fin D), t p = one

Being exhausted is holding the greatest element everywhere.

theorem DescriptiveComplexity.Draw.tupNext_of_isMaxTup {A : Type} [LinearOrder A] {D : ℕ} {t : Fin D → A} (h : IsMaxTup t) : tupNext t = t

An exhausted tuple stands still.

theorem DescriptiveComplexity.Draw.tupSuccAt_of_carry {A : Type} [LinearOrder A] [Finite A] {D : ℕ} {t : Fin D → A} {p : Fin D} (hp : ¬IsTop (t p)) (hab : ∀ (j : Fin D), p < j → IsTop (t j)) : TupSuccAt p t (tupNext t)

A tuple below the top steps at its carry coordinate.

theorem DescriptiveComplexity.Draw.tupCarry_of_carry {A : Type} [LinearOrder A] [Finite A] {D : ℕ} {t : Fin D → A} {p : Fin D} (hp : ¬IsTop (t p)) (hab : ∀ (j : Fin D), p < j → IsTop (t j)) : tupCarry t = ↑p

And the coordinate it carries is that one.

theorem DescriptiveComplexity.Draw.tupCarry_of_isMaxTup {A : Type} [LinearOrder A] {D : ℕ} {t : Fin D → A} (h : IsMaxTup t) : tupCarry t = D

An exhausted tuple carries past its last coordinate.

theorem DescriptiveComplexity.Draw.tupCarry_le {A : Type} [LinearOrder A] {D : ℕ} {t : Fin D → A} : tupCarry t ≤ D

The carry never passes the last coordinate.

theorem DescriptiveComplexity.Draw.tupNext_apply_of_carry {A : Type} [LinearOrder A] [Finite A] {D : ℕ} {zero : A} (hb : IsBot zero) {t : Fin D → A} {p : Fin D} (hp : ¬IsTop (t p)) (hab : ∀ (j : Fin D), p < j → IsTop (t j)) (j : Fin D) : tupNext t j = if j < p then t j else if j = p then ordSucc (t j) else zero

The next tuple, coordinate by coordinate: below the carry a copy, at the carry the next element, above it the least one. This is the reading the interpretation writes down.

theorem DescriptiveComplexity.Draw.exists_carry {A : Type} [LinearOrder A] {D : ℕ} {one : A} (ht : IsTop one) {t : Fin D → A} (h : ¬IsMaxTup t) : ∃ (p : Fin D), t p ≠ one ∧ ∀ (j : Fin D), p < j → t j = one

A tuple that is not exhausted has a carry coordinate.

theorem DescriptiveComplexity.Draw.tupCarry_eq_iff {A : Type} [LinearOrder A] [Finite A] {D : ℕ} {one : A} (ht : IsTop one) {t : Fin D → A} (p : Fin D) : tupCarry t = ↑p ↔ t p ≠ one ∧ ∀ (j : Fin D), p < j → t j = one

What the carry coordinate is: the greatest coordinate below the top.

theorem DescriptiveComplexity.Draw.tupCarry_eq_card_iff {A : Type} [LinearOrder A] [Finite A] {D : ℕ} {one : A} (ht : IsTop one) {t : Fin D → A} : tupCarry t = D ↔ ∀ (p : Fin D), t p = one

And when there is none: the tuple is exhausted.

theorem DescriptiveComplexity.Draw.botTup_eq {A : Type} [LinearOrder A] [Finite A] {D : ℕ} {zero : A} [Nonempty A] (hb : IsBot zero) (p : Fin D) : botTup p = zero

The least tuple is the constant designated element.

The three obligations of a loop element

theorem DescriptiveComplexity.Draw.Data.uSlotDefinable_tupNext_lvE {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] (j : Fin dt.eDim) : USlotDefinable fun (x : Env L) (f : dt.CtlIx → x.α) (x_1 : dt.SlotIx → x.α) => tupNext (dt.readLvE f) j

A loop element's coordinate is definable after the advance: the carry is a question about the pattern, and the value at it is the next element.

theorem DescriptiveComplexity.Draw.Data.uStDefinable_advLvE {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] : UStDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => dt.advLvE f

The wide loop, advanced, is definable.

theorem DescriptiveComplexity.Draw.Data.uStDefinable_initLvE {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] : UStDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => dt.initLvE f

The wide loop, started, is definable.

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

The wide loop's exhaustion test is definable.

theorem DescriptiveComplexity.Draw.Data.uGDefinable_tupCarry_eq {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] (c₀ : ℕ) : UGDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => tupCarry (dt.readLvE f) = c₀

Which coordinate carries is a definable question: it is decided by which coordinates are maximal, and that is what a slot atom says.

The narrow width

theorem DescriptiveComplexity.Draw.Data.uSlotDefinable_tupNext_lvC {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] (j : Fin dt.dd0) : USlotDefinable fun (x : Env L) (f : dt.CtlIx → x.α) (x_1 : dt.SlotIx → x.α) => tupNext (dt.readLv f) j

A narrow loop element's coordinate is definable after the advance.

theorem DescriptiveComplexity.Draw.Data.uStDefinable_advLvN {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] : UStDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => dt.advLvN f

The narrow loop, advanced, is definable.

theorem DescriptiveComplexity.Draw.Data.uStDefinable_initLvN {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] : UStDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => dt.initLvN f

The narrow loop, started, is definable.

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

The narrow loop's exhaustion test is definable.